New functions UriManager.uri_is_var, UriManager.uri_is_con.

[helm.git] / helm / ocaml / cic / cicPushParser.ml

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index 31ded7ef22d74efab484affc82cd92f7dde82daf..2c4ded3961dfc71ae2d82fb365a9becafc0a72a0 100644 (file)
--- a/helm/ocaml/cic/cicPushParser.ml
+++ b/helm/ocaml/cic/cicPushParser.ml
@@ -35,7 +35,6 @@ open Printf
    <!ELEMENT Def %term;>
    <!ELEMENT Hidden EMPTY>
    <!ELEMENT Goal %term;>
-   <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern* )>
 *)
 
 module CicParser =
@@ -67,6 +66,9 @@ type stack_entry =
   | Inductive_type of string * string * bool * Cic.annterm *
       (string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
   | Meta_subst of Cic.annterm option
+  | Obj_class of Cic.object_class
+  | Obj_field of string (* field name *)
+  | Obj_generated
   | Tag of string * (string * string) list  (* tag name, attributes *)
       (* ZACK TODO add file position to tag stack entry so that when attribute
        * errors occur, the position of their _start_tag_ could be printed
@@ -99,6 +101,9 @@ let string_of_stack ctxt =
       | Inductive_type (id, name, _, _, _) ->
           sprintf "Inductive_type %s (id=%s)" name id
       | Meta_subst _ -> "Meta_subst"
+      | Obj_class _ -> "Obj_class"
+      | Obj_field name -> "Obj_field " ^ name
+      | Obj_generated -> "Obj_generated"
       | Tag (tag, _) -> "Tag " ^ tag)
       ctxt.stack)) ^ "]"
 
@@ -169,6 +174,18 @@ let pop_cics ctxt =
   ctxt.stack <- new_stack;
   values
 
+let pop_class_modifiers ctxt =
+  let rec aux acc stack =
+    match stack with
+    | (Cic_term (Cic.ASort _) as m) :: tl
+    | (Obj_field _ as m) :: tl ->
+        aux (m :: acc) tl
+    | tl -> acc, tl
+  in
+  let values, new_stack = aux [] ctxt.stack in
+  ctxt.stack <- new_stack;
+  values
+
 let pop_meta_substs ctxt =
   let rec aux acc stack =
     match stack with
@@ -280,9 +297,9 @@ let uri_list_of_string =
 let sort_of_string ctxt = function
   | "Prop" -> Cic.Prop
   | "Set"  -> Cic.Set
-  | "Type" ->
-(*      CicUniv.restart_numbering (); |+ useful only to test parser +| *)
-      Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
+  | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
+(*   | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *)
+  | "CProp" -> Cic.CProp
   | _ -> parse_error ctxt "sort expected"
 
 let patch_subst ctxt subst = function
@@ -599,27 +616,44 @@ let end_element ctxt tag =
         (* replace <instantiate> *)
       set_top ctxt (Cic_term (patch_subst ctxt subst term))
   | "attributes" ->
-      let (_, attrs) = pop_tag ctxt in
-      let rec mk_obj_attributes acc = function
-        | [] -> acc
-        | ("generated", "true") :: tl ->
-            mk_obj_attributes (`Generated :: acc) tl
-        | ("class", "coercion") :: tl ->
-            mk_obj_attributes (`Class `Coercion :: acc) tl
-        | ("class", "record") :: tl ->
-            mk_obj_attributes (`Class `Record :: acc) tl
-        | ("class", "projection") :: tl ->
-            mk_obj_attributes (`Class `Projection :: acc) tl
-        | ("class", "elimProp") :: tl ->
-            mk_obj_attributes (`Class (`Elim Cic.Prop) :: acc) tl
-        | ("class", "elimSet") :: tl ->
-            mk_obj_attributes (`Class (`Elim Cic.Set) :: acc) tl
-        | ("class", "elimType") :: tl ->
-            let univ = CicUniv.fresh ~uri:ctxt.uri () in
-            mk_obj_attributes (`Class (`Elim (Cic.Type univ)) :: acc) tl
-        | _ -> attribute_error ()
+      let rec aux acc = function  (* retrieve object attributes *)
+        | Obj_class c :: tl -> aux (`Class c :: acc) tl
+        | Obj_generated :: tl -> aux (`Generated :: acc) tl
+        | tl -> acc, tl
       in
-      push ctxt (Cic_attributes (mk_obj_attributes [] attrs))
+      let obj_attrs, new_stack = aux [] ctxt.stack in
+      ctxt.stack <- new_stack;
+      set_top ctxt (Cic_attributes obj_attrs)
+  | "generated" -> set_top ctxt Obj_generated
+  | "field" ->
+      push ctxt
+        (match pop_tag_attrs ctxt with
+        | ["name", name] -> Obj_field name
+        | _ -> attribute_error ())
+  | "class" ->
+      let class_modifiers = pop_class_modifiers ctxt in
+      push ctxt
+        (match pop_tag_attrs ctxt with
+        | ["value", "coercion"] -> Obj_class `Coercion
+        | ["value", "elim"] ->
+            (match class_modifiers with
+            | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
+            | _ ->
+                parse_error
+                  "unexpected extra content for \"elim\" object class")
+        | ["value", "record"] ->
+            let fields =
+              List.map
+                (function
+                  | Obj_field name -> name
+                  | _ ->
+                      parse_error
+                        "unexpected extra content for \"record\" object class")
+                class_modifiers
+            in
+            Obj_class (`Record fields)
+        | ["value", "projection"] -> Obj_class `Projection
+        | _ -> attribute_error ())
   | tag ->
       match find_helm_exception ctxt with
       | Some (exn, arg) -> raise (Getter_failure (exn, arg))
@@ -639,12 +673,24 @@ let parse uri filename =
   let xml_parser = P.create_parser callbacks in
   ctxt.xml_parser <- Some xml_parser;
   try
-    P.parse xml_parser (`File filename);
+    (try
+      P.parse xml_parser (`Gzip_file filename);
+    with exn ->
+      ctxt.xml_parser <- None;
+      (* ZACK: the above "<- None" is vital for garbage collection. Without it
+       * we keep in memory a circular structure parser -> callbacks -> ctxt ->
+       * parser. I don't know if the ocaml garbage collector is supposed to
+       * collect such structures, but for sure the expat bindings will (orribly)
+       * leak when used in conjunction with such structures *)
+      raise exn);
+    ctxt.xml_parser <- None; (* ZACK: same comment as above *)
 (*    debug_print (string_of_stack stack);*)
+    (* assert (List.length ctxt.stack = 1) *)
     List.hd ctxt.stack
   with
   | Failure "int_of_string" -> parse_error ctxt "integer number expected"
   | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
+  | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
   | Parser_failure _
   | Getter_failure _ as exn ->
       raise exn