]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/test.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic / test.ml
index c92e1d498980f1de89137b328dc9dc582c279c1d..134ff789de2ff3087ebbfa0601759372be0d06ad 100644 (file)
@@ -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
 
@@ -60,9 +67,7 @@ let rec parse uri tmpfile1 tmpfile2 =
     when Str.string_match body_RE uri 0 ->
       parse uri tmpfile1 None
   | CicParser.Parser_failure msg ->
-      printf "%s FAILED (%s)\n" uri msg; flush stdout);
-  unlink tmpfile1;
-  (match tmpfile2 with None -> () | Some f -> unlink f)
+      printf "%s FAILED (%s)\n" uri msg; flush stdout)
 
 let _ =
   try
@@ -79,48 +84,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*)
-