prima implementazione di demodulate, superposition_left e superposition_right

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

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index 9a0566ec2e6048d3801b60a1f33dffda65b8db11..f9f14df106b971a457c2f10fbed7841bf6ab2c46 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 =
@@ -612,6 +611,8 @@ let end_element ctxt tag =
             mk_obj_attributes (`Class `Projection :: acc) tl
         | ("class", "elimProp") :: tl ->
             mk_obj_attributes (`Class (`Elim Cic.Prop) :: acc) tl
+        | ("class", "elimCProp") :: tl ->
+            mk_obj_attributes (`Class (`Elim Cic.CProp) :: acc) tl
         | ("class", "elimSet") :: tl ->
             mk_obj_attributes (`Class (`Elim Cic.Set) :: acc) tl
         | ("class", "elimType") :: tl ->
@@ -639,8 +640,19 @@ let parse uri filename =
   let xml_parser = P.create_parser callbacks in
   ctxt.xml_parser <- Some xml_parser;
   try
-    P.parse xml_parser (`Gzip_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"