X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=34f71d41201601264975689ad6dd4249b6923aaa;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a60aada5d3380d26222767970cc78c1efe3d6ac5;hpb=694386f0213ea7c07afb173a378335e7030020f9;p=helm.git diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index a60aada5d..34f71d412 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -1,17 +1,29 @@ open Printf -let mqi_debug_fun = ignore +let time_out = ref 5;; + +Helm_registry.load_from "gTopLevel.conf.xml";; + +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 -exception Multiple_interpretations let fail msg = raise (Failure msg) -let uri_predicate = ref BatchParser.constants_only +let uri_predicate = ref (BatchParser.constants_only ~prefix:"") module DisambiguateCallbacks = struct @@ -19,7 +31,14 @@ module DisambiguateCallbacks = ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = List.filter !uri_predicate choices - let interactive_interpretation_choice _ = raise Multiple_interpretations + let interactive_interpretation_choice = + let rec aux n = + function + [] -> [] + | _::tl -> n::(aux (n+1) tl) + in + aux 0 + let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title) end @@ -27,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 @@ -36,17 +60,24 @@ 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 (_, _, term) = - Disambiguate'.disambiguate_term mqi_handle [] [] new_ast - DisambiguateTypes.Environment.empty + let res = + Disambiguate'.disambiguate_term ~dbd [] [] new_ast + ~aliases:DisambiguateTypes.Environment.empty + ~initial_ugraph:CicUniv.empty_ugraph in - debug_print ("term: " ^ CicPp.ppterm term) + List.iter + (fun (domain, _, term, _) -> + debug_print + ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ; + debug_print ("term: " ^ CicPp.ppterm term) + ) res ; + List.length res in match annobj with | Cic.AConstant (_, _, _, None, ty, _) -> @@ -55,38 +86,55 @@ let test_uri uri = | Cic.AConstant (_, _, _, Some bo, ty, _) -> (* debug_print "Cic.AConstant (bo)"; - round_trip bo; + let n = round_trip bo in *) debug_print "Cic.AConstant (ty)"; - round_trip ty + round_trip ty (* + n *) | Cic.AVariable (_, _, None, ty, _) -> debug_print "Cic.AVariable (ty)"; round_trip ty | Cic.AVariable (_, _, Some bo, ty, _) -> +(* debug_print "Cic.AVariable (bo)"; - round_trip bo; + let n = round_trip bo in +*) debug_print "Cic.AVariable (ty)"; - round_trip ty - | Cic.ACurrentProof (_, _, _, _, proof, ty, _) -> - debug_print "Cic.ACurrentProof (proof)"; - round_trip proof; - debug_print "Cic.ACurrentProof (ty)"; - round_trip ty + round_trip ty (* + n *) + | Cic.ACurrentProof (_, _, _, _, _, _, _) -> + assert false | Cic.AInductiveDefinition _ -> - debug_print "AInductiveDefinition: boh ..." + 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 - test_uri uri; - `Ok + ignore (Unix.alarm !time_out) ; + if test_uri typecheck uri = 1 then `Ok else `Maybe with - | Multiple_interpretations -> `Maybe + | 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:"; @@ -95,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 @@ -110,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 @@ -119,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 @@ -130,34 +184,42 @@ let do_file status fname = fname (Printexc.to_string exn) let _ = - Helm_registry.load_from "triciclo.conf.xml"; HelmLogger.register_log_callback (fun ?(append_NL = true) msg -> (if append_NL then prerr_endline else prerr_string) (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 ;