make use of gzipped type and body

diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend
index 78af7a0f1b37c18215a9f15df61aeed9d31c3561..1d596495f03ef0d118ba558b2ddd72e225f8c5b1 100644 (file)
--- a/helm/ocaml/cic/.depend
+++ b/helm/ocaml/cic/.depend
@@ -2,14 +2,12 @@ deannotate.cmi: cic.cmo
 cicParser3.cmi: cic.cmo 
 cicParser2.cmi: cicParser3.cmi cic.cmo 
 cicPxpParser.cmi: cic.cmo 
-cicPushParser.cmi: cicParser.cmi 
+cicPushParser.cmi: cic.cmo 
 cicParser.cmi: cic.cmo 
 cicUtil.cmi: cic.cmo 
 helmLibraryObjects.cmi: cic.cmo 
 cic.cmo: cicUniv.cmi 
 cic.cmx: cicUniv.cmx 
-xmlPushParser.cmo: xmlPushParser.cmi 
-xmlPushParser.cmx: xmlPushParser.cmi 
 cicUniv.cmo: cicUniv.cmi 
 cicUniv.cmx: cicUniv.cmi 
 deannotate.cmo: cic.cmo deannotate.cmi 
@@ -22,12 +20,10 @@ cicPxpParser.cmo: deannotate.cmi cicParser3.cmi cicParser2.cmi \
     cicPxpParser.cmi 
 cicPxpParser.cmx: deannotate.cmx cicParser3.cmx cicParser2.cmx \
     cicPxpParser.cmi 
-cicPushParser.cmo: xmlPushParser.cmi deannotate.cmi cicUniv.cmi cic.cmo \
-    cicPushParser.cmi 
-cicPushParser.cmx: xmlPushParser.cmx deannotate.cmx cicUniv.cmx cic.cmx \
-    cicPushParser.cmi 
-cicParser.cmo: deannotate.cmi cicParser3.cmi cicParser2.cmi cicParser.cmi 
-cicParser.cmx: deannotate.cmx cicParser3.cmx cicParser2.cmx cicParser.cmi 
+cicPushParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicPushParser.cmi 
+cicPushParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicPushParser.cmi 
+cicParser.cmo: cicPushParser.cmi cicParser.cmi 
+cicParser.cmx: cicPushParser.cmx cicParser.cmi 
 cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi 
 cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi 
 helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi 

diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile
index a7f4b568b3cc51ac9e3700e2c09383e41bd53f15..3cf15ac561fa1ddf5ba83cf28eca737a5509ddeb 100644 (file)
--- a/helm/ocaml/cic/Makefile
+++ b/helm/ocaml/cic/Makefile
@@ -1,9 +1,8 @@
 PACKAGE = cic
-REQUIRES = helm-urimanager helm-pxp helm-xml expat
+REQUIRES = helm-urimanager helm-xml expat pxp-engine helm-pxp
 PREDICATES =
 
 INTERFACE_FILES = \
-       xmlPushParser.mli       \
        cicUniv.mli             \
        deannotate.mli          \
        cicParser3.mli          \

diff --git a/helm/ocaml/cic/cicParser.mli b/helm/ocaml/cic/cicParser.mli
index 33c5b4b198835413dc1e21ff53b1ca00206af983..9472b4c54606bd35a67c71c0b9766d73e8dd1fa1 100644 (file)
--- a/helm/ocaml/cic/cicParser.mli
+++ b/helm/ocaml/cic/cicParser.mli
@@ -34,11 +34,13 @@ exception Parser_failure of string
   (* given the filename of an xml file of a cic object, it returns
    * its internal annotated representation. In the case of constants (whose
    * type is splitted from the body), a second xml file (for the body) must be
-   * provided. *)
+   * provided.
+   * Both files are assumed to be gzipped. *)
 val annobj_of_xml: UriManager.uri -> string -> string option -> Cic.annobj
 
   (* given the filename of an xml file of a cic object, it returns its internal
    * logical representation. In the case of constants (whose type is splitted
-   * from the body), a second xml file (for the body) must be provided. *)
+   * from the body), a second xml file (for the body) must be provided.
+   * Both files are assumed to be gzipped. *)
 val obj_of_xml : UriManager.uri -> string -> string option -> Cic.obj
 

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index 31ded7ef22d74efab484affc82cd92f7dde82daf..4365184bb9858b90133f89df40e696ae14f29942 100644 (file)
--- a/helm/ocaml/cic/cicPushParser.ml
+++ b/helm/ocaml/cic/cicPushParser.ml
@@ -639,7 +639,7 @@ 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);
+    P.parse xml_parser (`Gzip_file filename);
 (*    debug_print (string_of_stack stack);*)
     List.hd ctxt.stack
   with

diff --git a/helm/ocaml/cic/test.ml b/helm/ocaml/cic/test.ml
index c92e1d498980f1de89137b328dc9dc582c279c1d..d7b6c25759b54f8197660524315dddc48445f82e 100644 (file)
--- a/helm/ocaml/cic/test.ml
+++ b/helm/ocaml/cic/test.ml
@@ -37,7 +37,7 @@ let unlink f =
     Unix.unlink f
 
 let rec parse uri tmpfile1 tmpfile2 =
-(*  prerr_endline (sprintf "%s %s" tmpfile1 (match tmpfile2 with None -> "None" | Some f -> "Some " ^ f));*)
+(*prerr_endline (sprintf "%s %s" tmpfile1 (match tmpfile2 with None -> "None" | Some f -> "Some " ^ f));*)
   (try
     let uri' = UriManager.uri_of_string uri in
     let time_new0 = Unix.gettimeofday () in
@@ -46,6 +46,13 @@ let rec parse uri tmpfile1 tmpfile2 =
     let time_new1 = Unix.gettimeofday () in
 
     let time_old0 = Unix.gettimeofday () in
+    ignore (Unix.system (sprintf "gunzip -c %s > test.tmp && mv test.tmp %s"
+      tmpfile1 tmpfile1));
+    (match tmpfile2 with
+    | Some tmpfile2 ->
+        ignore (Unix.system (sprintf "gunzip -c %s > test.tmp && mv test.tmp %s"
+          tmpfile2 tmpfile2));
+    | None -> ());
     let obj_old = CicPxpParser.CicParser.annobj_of_xml uri' tmpfile1 tmpfile2 in
     let time_old1 = Unix.gettimeofday () in
 
@@ -79,48 +86,3 @@ let _ =
     done
   with End_of_file -> ()
 
-(* Parsing test:
- * - XmlPushParser version *)
-(*open Printf*)
-(*open XmlPushParser*)
-
-(*let print s = print_endline s; flush stdout*)
-
-(*let callbacks =*)
-(*  { default_callbacks with*)
-(*      start_element =*)
-(*        Some (fun tag attrs ->*)
-(*          let length = List.length attrs in*)
-(*          print (sprintf "opening %s [%s]"*)
-(*            tag (String.concat ";" (List.map fst attrs))));*)
-(*      end_element = Some (fun tag -> print ("closing " ^ tag));*)
-(*      character_data = Some (fun data -> print "character data ...");*)
-(*  }*)
-
-(*let xml_parser = create_parser callbacks*)
-
-(*let _ = parse xml_parser (`File Sys.argv.(1))*)
-
-(* Parsing test:
- * - Pure expat version (without XmlPushParser mediation).
- * Originally written only to test if XmlPushParser mediation caused overhead.
- * That was not the case. *)
-
-(*let _ =*)
-(*  let ic = open_in Sys.argv.(1) in*)
-(*  let expat_parser = Expat.parser_create ~encoding:None in*)
-(*  Expat.set_start_element_handler expat_parser*)
-(*    (fun tag attrs ->*)
-(*      let length = List.length attrs in*)
-(*      print (sprintf "opening %s [%d attribute%s]"*)
-(*      tag length (if length = 1 then "" else "s")));*)
-(*  Expat.set_end_element_handler expat_parser*)
-(*    (fun tag -> print ("closing " ^ tag));*)
-(*  Expat.set_character_data_handler expat_parser*)
-(*    (fun data -> print "character data ...");*)
-(*  try*)
-(*    while true do*)
-(*      Expat.parse expat_parser (input_line ic ^ "\n")*)
-(*    done*)
-(*  with End_of_file -> Expat.final expat_parser*)
-