+++ /dev/null
-
-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 ~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 uri =
- let obj = CicEnvironment.get_obj 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 mqi_handle [] [] new_ast
- DisambiguateTypes.Environment.empty 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 uri =
- try
- ignore (Unix.alarm !time_out) ;
- if test_uri 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
-
-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 (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
- | `Ok ->
- print_endline "\e[01;32m[ OK ]\e[00m";
- ok := uri_str :: !ok
- | `Nok ->
- print_endline "\e[01;31m[ FAILED ]\e[00m";
- nok := uri_str :: !nok
- | `Maybe ->
- print_endline "\e[01;33m[ MANY ]\e[00m";
- maybe := uri_str :: !maybe
- | `TimeOut ->
- print_endline "\e[01;34m[TIMEOUT!]\e[00m";
- timeout := uri_str :: !timeout
-
-let do_file 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 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 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"
- ]
- 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 (* <ok, nok, maybe, timeout> URIs *)
- List.iter
- (fun name ->
- try
- let uri = UriManager.uri_of_string name in
- do_uri status uri
- with UriManager.IllFormedUri _ ->
- if Sys.file_exists name then
- do_file status name
- else
- printf "Don't know what to do with '%s', ignoring it\n%!" name)
- names ;
- report status
projects / helm.git / blobdiff