X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=34f71d41201601264975689ad6dd4249b6923aaa;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=bdc07e97798c43afd1f3304aa5e142e8328cb09f;hpb=f71c28c100c2e7d2f5a279c79be893f74264897e;p=helm.git diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index bdc07e977..34f71d412 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -1,76 +1,226 @@ -let mqi_debug_fun = ignore +open Printf + +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 mqi_handle = MQIConn.init mqi_flags mqi_debug_fun + +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 ~prefix:"") + module DisambiguateCallbacks = struct - let output_html ?(append_NL = true) msg = - if verbose then - (if append_NL then print_string else print_endline) - (Ui_logger.string_of_html_msg msg) - let interactive_user_uri_choice - ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id = - List.filter - (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = + List.filter !uri_predicate choices - let interactive_interpretation_choice _ = fail "Multiple interpretations" - let input_or_locate_uri ~title = fail "Unknown identifier" + 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 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 obj = CicCache.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 obj + Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in let ids_to_uris = Hashtbl.create 1023 in 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 - debug_print ("ast: " ^ CicAstPp.pp_term ast); - let (_, _, term) = - Disambiguate'.disambiguate_term mqi_handle [] [] ast - DisambiguateTypes.Environment.empty + 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 ~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, _) -> debug_print "Cic.AConstant (ty)"; round_trip ty | 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 + +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 _ = main () +let test_uri typecheck uri = + try + 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*) + | exn -> raise exn +let report (ok,nok,maybe,timeout) = + 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_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 typecheck (ok, nok, maybe, timeout) uri = + let uri_str = UriManager.string_of_uri uri in + printf "Testing URI: %-55s %!" (uri_str ^ " ..."); + (match test_uri typecheck uri with + | `Ok -> + print_endline "[ OK ]"; + ok := uri_str :: !ok + | `Nok -> + print_endline "[ FAILED ]"; + nok := uri_str :: !nok + | `Maybe -> + print_endline "[ MANY ]"; + maybe := uri_str :: !maybe + | `TimeOut -> + print_endline "[TIMEOUT!]"; + timeout := uri_str :: !timeout) + +let do_file typecheck status fname = + try + let ic = open_in fname in + (try + while true do + let line = input_line ic in + try + let uri = UriManager.uri_of_string line in + do_uri typecheck status uri + with UriManager.IllFormedUri _ -> + printf "Error parsing URI '%s', ignoring it" line + done + with End_of_file -> + close_in ic) + with exn -> + printf "Error trying to access '%s' (%s), skipping the file\n%!" + fname (Printexc.to_string exn) + +let _ = + 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 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; 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 + 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 !typecheck status uri + with UriManager.IllFormedUri _ -> + if Sys.file_exists name then + do_file !typecheck status name + else + printf "Don't know what to do with '%s', ignoring it\n%!" name) + names ; + report status