From: Stefano Zacchiroli Date: Tue, 10 May 2005 10:58:05 +0000 (+0000) Subject: make use of gzipped type and body X-Git-Tag: single_binding~91 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=005aba457de4e6d77f664b17fb0f4846a16e2361;p=helm.git make use of gzipped type and body --- diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 78af7a0f1..1d596495f 100644 --- 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 a7f4b568b..3cf15ac56 100644 --- 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 33c5b4b19..9472b4c54 100644 --- 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 31ded7ef2..4365184bb 100644 --- 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 c92e1d498..d7b6c2575 100644 --- 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*) -