X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=6c76a6b2d79e09f88c2e991ec4c6adc7cc9ab7cb;hb=d48c8c8358c9dc4083254d847d7c4ee13d47e6ab;hp=90563a6186ec078dc9d34252c8372ad6aa59b9be;hpb=edb6ab182b915ebc8b2810574b0a87bdab39d051;p=helm.git

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 90563a618..6c76a6b2d 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -1,9 +1,11 @@
 
 open Printf
 
+Helm_registry.load_from "gTopLevel.conf.xml";;
+
 let mqi_debug_fun = ignore
 let mqi_flags = []
-let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
+let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
 
 let verbose = false
 
@@ -15,17 +17,12 @@ let uri_predicate = ref BatchParser.constants_only
 
 module DisambiguateCallbacks =
  struct
-  let output_html ?(append_NL = true) msg =
-    if verbose then
-      (if append_NL then print_string else print_endline)
-        (Ui_logger.string_of_html_msg msg)
-
   let interactive_user_uri_choice
    ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
      List.filter !uri_predicate choices
 
   let interactive_interpretation_choice _ = raise Multiple_interpretations
-  let input_or_locate_uri ~title = fail "Unknown identifier"
+  let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
  end
 
 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
@@ -33,9 +30,9 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 
 let test_uri uri =
-  let obj = CicCache.get_obj uri in
+  let obj = CicEnvironment.get_obj uri in
   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
-    Cic2acic.acic_object_of_cic_object obj
+    Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
   in
   let ids_to_uris = Hashtbl.create 1023 in
   let round_trip annterm =
@@ -43,9 +40,12 @@ let test_uri uri =
     let (ast, _) =
       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
     in
-    debug_print ("ast: " ^ CicAstPp.pp_term ast);
+    let new_pp = BoxPp.pp_term ast in
+    debug_print ("ast:\n" ^ new_pp);
+    let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
+    debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
     let (_, _, term) =
-      Disambiguate'.disambiguate_term mqi_handle [] [] ast
+      Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
         DisambiguateTypes.Environment.empty
     in
     debug_print ("term: " ^ CicPp.ppterm term)
@@ -88,15 +88,15 @@ let test_uri uri =
         (Printexc.to_string exn));
       `Nok
 
-let report ok nok maybe =
+let report (ok,nok,maybe) =
   print_newline ();
   print_endline "TestLibrary report";
   print_endline "Succeeded URIs:";
-  List.iter (fun s -> print_endline ("\t" ^ s)) ok;
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
   print_endline "Failed URIs:";
-  List.iter (fun s -> print_endline ("\t" ^ s)) nok;
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
   print_endline "Multiple answers URIs:";
-  List.iter (fun s -> print_endline ("\t" ^ s)) maybe;
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
   print_newline ()
 
 let do_uri (ok, nok, maybe) uri =
@@ -116,19 +116,26 @@ let do_uri (ok, nok, maybe) uri =
 let do_file status fname =
   try
     let ic = open_in fname in
-    while true do
-      let line = input_line ic in
-      try
-        let uri = UriManager.uri_of_string line in
-        do_uri status uri
-      with UriManager.IllFormedUri _ ->
-        printf "Error parsing URI '%s', ignoring it" line
-    done
+    (try
+      while true do
+        let line = input_line ic in
+        try
+          let uri = UriManager.uri_of_string line in
+          do_uri status uri
+        with UriManager.IllFormedUri _ ->
+          printf "Error parsing URI '%s', ignoring it" line
+      done
+    with End_of_file ->
+     close_in ic)
   with exn ->
     printf "Error trying to access '%s' (%s), skipping the file\n%!"
       fname (Printexc.to_string exn)
 
 let _ =
+  HelmLogger.register_log_callback
+   (fun ?(append_NL = true) msg ->
+     (if append_NL then prerr_endline else prerr_string)
+       (HelmLogger.string_of_html_msg msg));
   let names = ref [] in
   let tryvars = ref false in
   let varsprefix = ref "" in
@@ -154,5 +161,5 @@ let _ =
           do_file status name
         else
           printf "Don't know what to do with '%s', ignoring it\n%!" name)
-    names
-
+    names ;
+  report status