]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/testlibrary.ml
Added () to MQInit.init.
[helm.git] / helm / gTopLevel / testlibrary.ml
index 0d09eb0e3704de85f942b8fd5f0ecde7b47a6f5b..a60aada5d3380d26222767970cc78c1efe3d6ac5 100644 (file)
@@ -3,27 +3,24 @@ open Printf
 
 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
 
 exception Failure of string
+exception Multiple_interpretations
 let fail msg = raise (Failure msg)
 
+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 =
-     List.filter
-      (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+   ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
+     List.filter !uri_predicate choices
 
-  let interactive_interpretation_choice _ = fail "Multiple interpretations"
-  let input_or_locate_uri ~title = fail "Unknown identifier"
+  let interactive_interpretation_choice _ = raise Multiple_interpretations
+  let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
  end
 
 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
@@ -31,9 +28,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 =
@@ -41,9 +38,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)
@@ -75,37 +75,90 @@ let test_uri uri =
   | Cic.AInductiveDefinition _ ->
       debug_print "AInductiveDefinition: boh ..."
 
-let test_uri uri = try test_uri uri; true with _ -> false
+let test_uri uri =
+  try
+    test_uri uri;
+    `Ok
+  with
+  | Multiple_interpretations -> `Maybe
+  | exn ->
+      prerr_endline (sprintf "Top Level Uncaught Exception: %s"
+        (Printexc.to_string exn));
+      `Nok
 
-let _ =
-  let idx = ref 0 in
-  let ok = ref [] in
-  let nok = ref [] in
+let report (ok,nok,maybe) =
+  print_newline ();
+  print_endline "TestLibrary report";
+  print_endline "Succeeded URIs:";
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
+  print_endline "Failed URIs:";
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
+  print_endline "Multiple answers URIs:";
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
+  print_newline ()
+
+let do_uri (ok, nok, maybe) uri =
+  let uri_str = UriManager.string_of_uri uri in
+  printf "Testing URI: %-55s %!" (uri_str ^ " ...");
+  match test_uri uri with
+  | `Ok ->
+      print_endline "\e[01;32m[   OK   ]\e[00m";
+      ok := uri_str :: !ok
+  | `Nok ->
+      print_endline "\e[01;31m[ FAILED ]\e[00m";
+      nok := uri_str :: !nok
+  | `Maybe ->
+      print_endline "\e[01;33m[  MANY  ]\e[00m";
+      maybe := uri_str :: !maybe
+
+let do_file status fname =
   try
-    let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in
-    while true do
-      incr idx;
-      let uri_str =
-        match mode with
-        | `Stdin -> input_line stdin
-        | `Cmdline -> Sys.argv.(!idx)
-      in
-      printf "Testing URI: %-55s " (uri_str ^ " ..."); flush stdout;
-      let uri = UriManager.uri_of_string uri_str in
-      if test_uri uri then begin
-        print_endline "\e[01;32m[   OK   ]\e[00m";
-        ok := uri_str :: !ok
-      end else begin
-        print_endline "\e[01;31m[ FAILED ]\e[00m";
-        nok := uri_str :: !nok
-      end
-    done
-  with Invalid_argument _ | End_of_file ->
-    print_newline ();
-    print_endline "TestLibrary report";
-    print_endline "Succeeded URIs:";
-    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
-    print_endline "Failed URIs:";
-    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
-    print_newline ()
+    let ic = open_in fname in
+    (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 _ =
+  Helm_registry.load_from "triciclo.conf.xml";
+  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
+  let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
+  let spec =
+    [ "-vars", Arg.Set tryvars, "try also variables" ;
+      "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
+      "-varsprefix", Arg.Set_string varsprefix,
+        "limit variable choices to URIs beginning with prefix" ;
+    ]
+  in
+  Arg.parse spec (fun name -> names := name :: !names) usage;
+  let names = List.rev !names in
+  uri_predicate := BatchParser.uri_pred_of_conf !tryvars !varsprefix;
+  let status = (ref [], ref [], ref []) in  (* <ok, nok, maybe> URIs *)
+  List.iter
+    (fun name ->
+      try
+        let uri = UriManager.uri_of_string name in
+        do_uri status uri
+      with UriManager.IllFormedUri _ ->
+        if Sys.file_exists name then
+          do_file status name
+        else
+          printf "Don't know what to do with '%s', ignoring it\n%!" name)
+    names ;
+  report status