6 Helm_registry.load_from "gTopLevel.conf.xml";;
9 HelmLogger.log ~append_NL:true (`Msg (`T s))
11 let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
15 exception Failure of string
16 let fail msg = raise (Failure msg)
18 let uri_predicate = ref (BatchParser.constants_only ~prefix:"")
20 module DisambiguateCallbacks =
22 let interactive_user_uri_choice
23 ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
24 List.filter !uri_predicate choices
26 let interactive_interpretation_choice =
30 | _::tl -> n::(aux (n+1) tl)
34 let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
37 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
39 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
42 let obj = CicEnvironment.get_obj uri in
43 let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
44 Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
46 let ids_to_uris = Hashtbl.create 1023 in
47 let round_trip annterm =
48 debug_print "(1) acic -> ast";
50 Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
52 let new_pp = BoxPp.pp_term ast in
53 debug_print ("ast:\n" ^ new_pp);
54 let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
55 debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
57 Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
58 DisambiguateTypes.Environment.empty in
60 (fun (domain, _, term) ->
62 ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
63 debug_print ("term: " ^ CicPp.ppterm term)
68 | Cic.AConstant (_, _, _, None, ty, _) ->
69 debug_print "Cic.AConstant (ty)";
71 | Cic.AConstant (_, _, _, Some bo, ty, _) ->
73 debug_print "Cic.AConstant (bo)";
74 let n = round_trip bo in
76 debug_print "Cic.AConstant (ty)";
77 round_trip ty (* + n *)
78 | Cic.AVariable (_, _, None, ty, _) ->
79 debug_print "Cic.AVariable (ty)";
81 | Cic.AVariable (_, _, Some bo, ty, _) ->
83 debug_print "Cic.AVariable (bo)";
84 let n = round_trip bo in
86 debug_print "Cic.AVariable (ty)";
87 round_trip ty (* + n *)
88 | Cic.ACurrentProof (_, _, _, _, _, _, _) ->
90 | Cic.AInductiveDefinition _ ->
91 debug_print "AInductiveDefinition: boh ..." ;
97 (Sys.signal Sys.sigalrm
100 (* We do this in case that some "with _" intercepts the first exception *)
101 ignore (Unix.alarm 1) ;
108 ignore (Unix.alarm !time_out) ;
109 if test_uri uri = 1 then `Ok else `Maybe
112 (* We do this to clear the alarm set by the signal handler *)
113 ignore (Unix.alarm 0) ;
116 prerr_endline (sprintf "Top Level Uncaught Exception: %s"
117 (Printexc.to_string exn));
120 let report (ok,nok,maybe,timeout) =
122 print_endline "TestLibrary report";
123 print_endline "Succeeded URIs:";
124 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
125 print_endline "Failed URIs:";
126 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
127 print_endline "Multiple answers URIs:";
128 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
130 print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):");
131 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
134 let do_uri (ok, nok, maybe, timeout) uri =
135 let uri_str = UriManager.string_of_uri uri in
136 printf "Testing URI: %-55s %!" (uri_str ^ " ...");
137 match test_uri uri with
139 print_endline "
\e[01;32m[ OK ]
\e[00m";
142 print_endline "
\e[01;31m[ FAILED ]
\e[00m";
143 nok := uri_str :: !nok
145 print_endline "
\e[01;33m[ MANY ]
\e[00m";
146 maybe := uri_str :: !maybe
148 print_endline "
\e[01;34m[TIMEOUT!]
\e[00m";
149 timeout := uri_str :: !timeout
151 let do_file status fname =
153 let ic = open_in fname in
156 let line = input_line ic in
158 let uri = UriManager.uri_of_string line in
160 with UriManager.IllFormedUri _ ->
161 printf "Error parsing URI '%s', ignoring it" line
166 printf "Error trying to access '%s' (%s), skipping the file\n%!"
167 fname (Printexc.to_string exn)
170 HelmLogger.register_log_callback
171 (fun ?(append_NL = true) msg ->
172 (if append_NL then prerr_endline else prerr_string)
173 (HelmLogger.string_of_html_msg msg));
174 let names = ref [] in
175 let tryvars = ref false in
176 let prefix = ref "" in
177 let varsprefix = ref "####" in
178 let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
180 [ "-vars", Arg.Set tryvars, "try also variables" ;
181 "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
182 "-prefix", Arg.Set_string prefix,
183 "limit object choices to URIs beginning with prefix" ;
184 "-varsprefix", Arg.Set_string varsprefix,
185 "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
186 "-timeout", Arg.Set_int time_out,
187 "number of seconds before a timeout; 0 means no timeout"
190 Arg.parse spec (fun name -> names := name :: !names) usage;
191 let names = List.rev !names in
192 if !varsprefix = "####" then varsprefix := !prefix ;
194 BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
195 let status = (ref [], ref [], ref [], ref []) in (* <ok, nok, maybe, timeout> URIs *)
199 let uri = UriManager.uri_of_string name in
201 with UriManager.IllFormedUri _ ->
202 if Sys.file_exists name then
205 printf "Don't know what to do with '%s', ignoring it\n%!" name)