- added testlibrary .opts

[helm.git] / helm / gTopLevel / testlibrary.ml

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index bdc07e97798c43afd1f3304aa5e142e8328cb09f..a4675a75100ed18f92493712e9862c740414c489 100644 (file)
--- 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
@@ -28,8 +30,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 +53,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 +75,37 @@ let main () =
   | Cic.AInductiveDefinition _ ->
       debug_print "AInductiveDefinition: boh ..."
 
-let _ = main ()
+let test_uri uri = try test_uri uri; true with _ -> false
+
+let _ =
+  let idx = ref 0 in
+  let ok = ref [] in
+  let nok = ref [] in
+  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: %s ...\t";
+      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 ()