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 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 interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = List.filter !uri_predicate choices 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 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 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 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 ~dbd [] [] new_ast ~aliases:DisambiguateTypes.Environment.empty ~initial_ugraph:CicUniv.empty_ugraph in 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)"; let n = round_trip bo in *) debug_print "Cic.AConstant (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)"; let n = round_trip bo in *) debug_print "Cic.AVariable (ty)"; round_trip ty (* + n *) | Cic.ACurrentProof (_, _, _, _, _, _, _) -> assert false | Cic.AInductiveDefinition _ -> 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 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