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

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index bdc07e977..90563a618 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -1,4 +1,6 @@
 
+open Printf
+
 let mqi_debug_fun = ignore
 let mqi_flags = []
 let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
@@ -6,8 +8,11 @@ let mqi_handle = MQIConn.init mqi_flags 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 =
@@ -16,11 +21,10 @@ module DisambiguateCallbacks =
         (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 interactive_interpretation_choice _ = raise Multiple_interpretations
   let input_or_locate_uri ~title = fail "Unknown identifier"
  end
 
@@ -28,8 +32,7 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
 
 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 
-let main () =
-  let uri = UriManager.uri_of_string (Sys.argv.(1)) in
+let test_uri uri =
   let obj = CicCache.get_obj uri in
   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
     Cic2acic.acic_object_of_cic_object obj
@@ -52,8 +55,10 @@ let main () =
       debug_print "Cic.AConstant (ty)";
       round_trip ty
   | Cic.AConstant (_, _, _, Some bo, ty, _) ->
+(*
       debug_print "Cic.AConstant (bo)";
       round_trip bo;
+*)
       debug_print "Cic.AConstant (ty)";
       round_trip ty
   | Cic.AVariable (_, _, None, ty, _) ->
@@ -72,5 +77,82 @@ let main () =
   | Cic.AInductiveDefinition _ ->
       debug_print "AInductiveDefinition: boh ..."
 
-let _ = main ()
+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 report ok nok maybe =
+  print_newline ();
+  print_endline "TestLibrary report";
+  print_endline "Succeeded URIs:";
+  List.iter (fun s -> print_endline ("\t" ^ s)) ok;
+  print_endline "Failed URIs:";
+  List.iter (fun s -> print_endline ("\t" ^ s)) nok;
+  print_endline "Multiple answers URIs:";
+  List.iter (fun s -> print_endline ("\t" ^ s)) 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 "[   OK   ]";
+      ok := uri_str :: !ok
+  | `Nok ->
+      print_endline "[ FAILED ]";
+      nok := uri_str :: !nok
+  | `Maybe ->
+      print_endline "[  MANY  ]";
+      maybe := uri_str :: !maybe
+
+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
+  with exn ->
+    printf "Error trying to access '%s' (%s), skipping the file\n%!"
+      fname (Printexc.to_string exn)
+
+let _ =
+  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