X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=34f71d41201601264975689ad6dd4249b6923aaa;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ea6e4c6c037db42b62fb335e94a6776bc9d7546a;hpb=5e1c4e50b88cd1b75a14a34b93297a3aba6af890;p=helm.git diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index ea6e4c6c0..34f71d412 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -1,18 +1,29 @@ 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 dbd = Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () +(* let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun () +*) let verbose = false exception Failure of string let fail msg = raise (Failure msg) -let uri_predicate = ref BatchParser.constants_only +let uri_predicate = ref (BatchParser.constants_only ~prefix:"") module DisambiguateCallbacks = struct @@ -35,8 +46,13 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) let debug_print s = prerr_endline ("^^^^^^ " ^ s) -let test_uri uri = - let obj = CicEnvironment.get_obj uri in +let test_uri typecheck uri = + if typecheck then + try ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);1 + with CicTypeChecker.TypeCheckerFailure s | + CicTypeChecker.AssertFailure s -> 0 + else + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let (annobj, _, _, ids_to_inner_sorts, _, _, _) = Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in @@ -44,17 +60,19 @@ let test_uri uri = let round_trip annterm = debug_print "(1) acic -> ast"; let (ast, _) = - Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm + Acic2Ast.ast_of_acic ids_to_inner_sorts (*ids_to_uris*) annterm in 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 res = - Disambiguate'.disambiguate_term mqi_handle [] [] new_ast - DisambiguateTypes.Environment.empty in + Disambiguate'.disambiguate_term ~dbd [] [] new_ast + ~aliases:DisambiguateTypes.Environment.empty + ~initial_ugraph:CicUniv.empty_ugraph + in List.iter - (fun (domain, _, term) -> + (fun (domain, _, term, _) -> debug_print ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ; debug_print ("term: " ^ CicPp.ppterm term) @@ -88,16 +106,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 +143,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 +161,11 @@ let do_uri (ok, nok, maybe) uri = | `Maybe -> print_endline "[ MANY ]"; maybe := uri_str :: !maybe + | `TimeOut -> + print_endline "[TIMEOUT!]"; + timeout := uri_str :: !timeout) -let do_file status fname = +let do_file typecheck status fname = try let ic = open_in fname in (try @@ -130,7 +173,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,27 +190,36 @@ let _ = (HelmLogger.string_of_html_msg msg)); let names = ref [] in let tryvars = ref false in - let varsprefix = ref "" in + let typecheck = ref false in + let prefix = ref "" 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)" ; + "-prefix", Arg.Set_string prefix, + "limit object choices to URIs beginning with prefix" ; "-varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix" ; + "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; let names = List.rev !names in - uri_predicate := BatchParser.uri_pred_of_conf !tryvars !varsprefix; - let status = (ref [], ref [], ref []) in (* URIs *) + if !varsprefix = "####" then varsprefix := !prefix ; + uri_predicate := + BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix; + let status = (ref [], ref [], ref [], ref []) in (* 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 ;