4 let mqi_debug_fun = ignore
6 let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
10 exception Failure of string
11 let fail msg = raise (Failure msg)
13 module DisambiguateCallbacks =
15 let output_html ?(append_NL = true) msg =
17 (if append_NL then print_string else print_endline)
18 (Ui_logger.string_of_html_msg msg)
20 let interactive_user_uri_choice
21 ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id =
23 (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
25 let interactive_interpretation_choice _ = fail "Multiple interpretations"
26 let input_or_locate_uri ~title = fail "Unknown identifier"
29 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
31 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
34 let obj = CicCache.get_obj uri in
35 let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
36 Cic2acic.acic_object_of_cic_object obj
38 let ids_to_uris = Hashtbl.create 1023 in
39 let round_trip annterm =
40 debug_print "(1) acic -> ast";
42 Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
44 debug_print ("ast: " ^ CicAstPp.pp_term ast);
46 Disambiguate'.disambiguate_term mqi_handle [] [] ast
47 DisambiguateTypes.Environment.empty
49 debug_print ("term: " ^ CicPp.ppterm term)
52 | Cic.AConstant (_, _, _, None, ty, _) ->
53 debug_print "Cic.AConstant (ty)";
55 | Cic.AConstant (_, _, _, Some bo, ty, _) ->
57 debug_print "Cic.AConstant (bo)";
60 debug_print "Cic.AConstant (ty)";
62 | Cic.AVariable (_, _, None, ty, _) ->
63 debug_print "Cic.AVariable (ty)";
65 | Cic.AVariable (_, _, Some bo, ty, _) ->
66 debug_print "Cic.AVariable (bo)";
68 debug_print "Cic.AVariable (ty)";
70 | Cic.ACurrentProof (_, _, _, _, proof, ty, _) ->
71 debug_print "Cic.ACurrentProof (proof)";
73 debug_print "Cic.ACurrentProof (ty)";
75 | Cic.AInductiveDefinition _ ->
76 debug_print "AInductiveDefinition: boh ..."
78 let test_uri uri = try test_uri uri; true with _ -> false
85 let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in
90 | `Stdin -> input_line stdin
91 | `Cmdline -> Sys.argv.(!idx)
93 printf "Testing URI: %-55s " (uri_str ^ " ..."); flush stdout;
94 let uri = UriManager.uri_of_string uri_str in
95 if test_uri uri then begin
96 print_endline "
\e[01;32m[ OK ]
\e[00m";
99 print_endline "
\e[01;31m[ FAILED ]
\e[00m";
100 nok := uri_str :: !nok
103 with Invalid_argument _ | End_of_file ->
105 print_endline "TestLibrary report";
106 print_endline "Succeeded URIs:";
107 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
108 print_endline "Failed URIs:";
109 List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);