Added universes handling. Tag PRE_UNIVERSES may help ;)

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

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index fccdc19c619530b67093437c77a00254b2534869..f35ee096a23f5fa63b0abf1efc06ff33ba1d7d60 100644 (file)
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -38,7 +38,12 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
 
 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 
-let test_uri uri =
+let test_uri typecheck uri =
+  if typecheck then
+    try ignore(CicTypeChecker.typecheck uri);1
+    with CicTypeChecker.TypeCheckerFailure s | 
+         CicTypeChecker.AssertFailure s -> 0
+  else
   let obj = CicEnvironment.get_obj uri in
   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
     Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
@@ -103,10 +108,10 @@ ignore
 ;;
 
 
-let test_uri uri =
+let test_uri typecheck uri =
   try
    ignore (Unix.alarm !time_out) ;
-   if test_uri uri = 1 then `Ok else `Maybe
+   if test_uri typecheck uri = 1 then `Ok else `Maybe
   with
   | TimeOut ->
      (* We do this to clear the alarm set by the signal handler *)
@@ -133,10 +138,10 @@ let report (ok,nok,maybe,timeout) =
   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
   print_newline ()
 
-let do_uri (ok, nok, maybe, timeout) uri =
+let do_uri typecheck (ok, nok, maybe, timeout) uri =
   let uri_str = UriManager.string_of_uri uri in
   printf "Testing URI: %-55s %!" (uri_str ^ " ...");
-  match test_uri uri with
+  (match test_uri typecheck uri with
   | `Ok ->
       print_endline "\e[01;32m[   OK   ]\e[00m";
       ok := uri_str :: !ok
@@ -148,9 +153,12 @@ let do_uri (ok, nok, maybe, timeout) uri =
       maybe := uri_str :: !maybe
   | `TimeOut ->
       print_endline "\e[01;34m[TIMEOUT!]\e[00m";
-      timeout := uri_str :: !timeout
+      timeout := uri_str :: !timeout);
+  print_endline "--";
+  print_endline (CicUniv.print_stats ());
+  print_endline "--"
 
-let do_file status fname =
+let do_file typecheck status fname =
   try
     let ic = open_in fname in
     (try
@@ -158,7 +166,7 @@ let do_file status fname =
         let line = input_line ic in
         try
           let uri = UriManager.uri_of_string line in
-          do_uri status uri
+          do_uri typecheck status uri
         with UriManager.IllFormedUri _ ->
           printf "Error parsing URI '%s', ignoring it" line
       done
@@ -175,6 +183,7 @@ let _ =
        (HelmLogger.string_of_html_msg msg));
   let names = ref [] in
   let tryvars = ref false in
+  let typecheck = ref false in
   let prefix = ref "" in
   let varsprefix = ref "####" in
   let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
@@ -186,7 +195,8 @@ let _ =
       "-varsprefix", Arg.Set_string varsprefix,
         "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
       "-timeout", Arg.Set_int time_out,
-       "number of seconds before a timeout; 0 means no timeout"
+       "number of seconds before a timeout; 0 means no timeout";
+       "-typecheck", Arg.Set typecheck, "simply typechek the uri"
     ]
   in
   Arg.parse spec (fun name -> names := name :: !names) usage;
@@ -199,10 +209,10 @@ let _ =
     (fun name ->
       try
         let uri = UriManager.uri_of_string name in
-        do_uri status uri
+        do_uri !typecheck status uri
       with UriManager.IllFormedUri _ ->
         if Sys.file_exists name then
-          do_file status name
+          do_file !typecheck status name
         else
           printf "Don't know what to do with '%s', ignoring it\n%!" name)
     names ;