X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=f35ee096a23f5fa63b0abf1efc06ff33ba1d7d60;hb=cf8abaf99bf9065c82d8f668d441bc4c0a2a13df;hp=af459000a0c18e44de8f41e20b1f14e16e4dc5e6;hpb=6cfcba76baa8f30c42624e911bd34a702f785766;p=helm.git

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index af459000a..f35ee096a 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -1,9 +1,12 @@
 
 open Printf
 
+let time_out = ref 5;;
+
 Helm_registry.load_from "gTopLevel.conf.xml";;
 
-let mqi_debug_fun = ignore
+let mqi_debug_fun s =
+ HelmLogger.log ~append_NL:true (`Msg (`T s))
 let mqi_flags = []
 let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
 
@@ -35,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
@@ -88,16 +96,35 @@ let test_uri uri =
       debug_print "AInductiveDefinition: boh ..." ;
       assert false
 
-let test_uri uri =
+exception TimeOut;;
+                                                                                
+ignore
+ (Sys.signal Sys.sigalrm
+   (Sys.Signal_handle
+     (fun _ ->
+       (* We do this in case that some "with _" intercepts the first exception *)
+       ignore (Unix.alarm 1) ;
+       raise TimeOut)))
+;;
+
+
+let test_uri typecheck uri =
   try
-   if test_uri uri = 1 then `Ok else `Maybe
+   ignore (Unix.alarm !time_out) ;
+   if test_uri typecheck uri = 1 then `Ok else `Maybe
   with
+  | TimeOut ->
+     (* We do this to clear the alarm set by the signal handler *)
+     ignore (Unix.alarm 0) ;
+     `TimeOut
+     (*
   | exn ->
       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
         (Printexc.to_string exn));
-      `Nok
+      `Nok*)
+  | exn -> raise exn
 
-let report (ok,nok,maybe) =
+let report (ok,nok,maybe,timeout) =
   print_newline ();
   print_endline "TestLibrary report";
   print_endline "Succeeded URIs:";
@@ -106,12 +133,15 @@ let report (ok,nok,maybe) =
   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 ();
+  print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):");
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
   print_newline ()
 
-let do_uri (ok, nok, maybe) 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 "[   OK   ]";
       ok := uri_str :: !ok
@@ -121,8 +151,14 @@ let do_uri (ok, nok, maybe) uri =
   | `Maybe ->
       print_endline "[  MANY  ]";
       maybe := uri_str :: !maybe
-
-let do_file status fname =
+  | `TimeOut ->
+      print_endline "[TIMEOUT!]";
+      timeout := uri_str :: !timeout);
+  print_endline "--";
+  print_endline (CicUniv.print_stats ());
+  print_endline "--"
+
+let do_file typecheck status fname =
   try
     let ic = open_in fname in
     (try
@@ -130,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
@@ -147,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
@@ -157,6 +194,9 @@ let _ =
         "limit object choices to URIs beginning with prefix" ; 
       "-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";
+       "-typecheck", Arg.Set typecheck, "simply typechek the uri"
     ]
   in
   Arg.parse spec (fun name -> names := name :: !names) usage;
@@ -164,15 +204,15 @@ let _ =
   if !varsprefix = "####" then varsprefix := !prefix ;
   uri_predicate :=
    BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
-  let status = (ref [], ref [], ref []) in  (* <ok, nok, maybe> URIs *)
+  let status = (ref [], ref [], ref [], ref []) in  (* <ok, nok, maybe, timeout> URIs *)
   List.iter
     (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 ;