4 let mqi_debug_fun = ignore
6 let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
10 exception Failure of string
11 exception Multiple_interpretations
12 let fail msg = raise (Failure msg)
14 let uri_predicate = ref BatchParser.constants_only
16 module DisambiguateCallbacks =
18 let interactive_user_uri_choice
19 ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
20 List.filter !uri_predicate choices
22 let interactive_interpretation_choice _ = raise Multiple_interpretations
23 let input_or_locate_uri ~title = fail "Unknown identifier"
26 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
28 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
31 let obj = CicEnvironment.get_obj uri in
32 let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
33 Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
35 let ids_to_uris = Hashtbl.create 1023 in
36 let round_trip annterm =
37 debug_print "(1) acic -> ast";
39 Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
41 debug_print ("ast: " ^ CicAstPp.pp_term ast);
43 Disambiguate'.disambiguate_term mqi_handle [] [] ast
44 DisambiguateTypes.Environment.empty
46 debug_print ("term: " ^ CicPp.ppterm term)
49 | Cic.AConstant (_, _, _, None, ty, _) ->
50 debug_print "Cic.AConstant (ty)";
52 | Cic.AConstant (_, _, _, Some bo, ty, _) ->
54 debug_print "Cic.AConstant (bo)";
57 debug_print "Cic.AConstant (ty)";
59 | Cic.AVariable (_, _, None, ty, _) ->
60 debug_print "Cic.AVariable (ty)";
62 | Cic.AVariable (_, _, Some bo, ty, _) ->
63 debug_print "Cic.AVariable (bo)";
65 debug_print "Cic.AVariable (ty)";
67 | Cic.ACurrentProof (_, _, _, _, proof, ty, _) ->
68 debug_print "Cic.ACurrentProof (proof)";
70 debug_print "Cic.ACurrentProof (ty)";
72 | Cic.AInductiveDefinition _ ->
73 debug_print "AInductiveDefinition: boh ..."
80 | Multiple_interpretations -> `Maybe
82 prerr_endline (sprintf "Top Level Uncaught Exception: %s"
83 (Printexc.to_string exn));
86 let report (ok,nok,maybe) =
88 print_endline "TestLibrary report";
89 print_endline "Succeeded URIs:";
90 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
91 print_endline "Failed URIs:";
92 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
93 print_endline "Multiple answers URIs:";
94 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
97 let do_uri (ok, nok, maybe) uri =
98 let uri_str = UriManager.string_of_uri uri in
99 printf "Testing URI: %-55s %!" (uri_str ^ " ...");
100 match test_uri uri with
102 print_endline "
\e[01;32m[ OK ]
\e[00m";
105 print_endline "
\e[01;31m[ FAILED ]
\e[00m";
106 nok := uri_str :: !nok
108 print_endline "
\e[01;33m[ MANY ]
\e[00m";
109 maybe := uri_str :: !maybe
111 let do_file status fname =
113 let ic = open_in fname in
116 let line = input_line ic in
118 let uri = UriManager.uri_of_string line in
120 with UriManager.IllFormedUri _ ->
121 printf "Error parsing URI '%s', ignoring it" line
126 printf "Error trying to access '%s' (%s), skipping the file\n%!"
127 fname (Printexc.to_string exn)
130 Helm_registry.load_from "triciclo.conf.xml";
131 HelmLogger.register_log_callback
132 (fun ?(append_NL = true) msg ->
133 (if append_NL then prerr_endline else prerr_string)
134 (HelmLogger.string_of_html_msg msg));
135 let names = ref [] in
136 let tryvars = ref false in
137 let varsprefix = ref "" in
138 let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
140 [ "-vars", Arg.Set tryvars, "try also variables" ;
141 "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
142 "-varsprefix", Arg.Set_string varsprefix,
143 "limit variable choices to URIs beginning with prefix" ;
146 Arg.parse spec (fun name -> names := name :: !names) usage;
147 let names = List.rev !names in
148 uri_predicate := BatchParser.uri_pred_of_conf !tryvars !varsprefix;
149 let status = (ref [], ref [], ref []) in (* <ok, nok, maybe> URIs *)
153 let uri = UriManager.uri_of_string name in
155 with UriManager.IllFormedUri _ ->
156 if Sys.file_exists name then
159 printf "Don't know what to do with '%s', ignoring it\n%!" name)