X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=a60aada5d3380d26222767970cc78c1efe3d6ac5;hb=694386f0213ea7c07afb173a378335e7030020f9;hp=0d09eb0e3704de85f942b8fd5f0ecde7b47a6f5b;hpb=6fedbf02acadaa79520d0418a6b737c745dda5bd;p=helm.git diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index 0d09eb0e3..a60aada5d 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -3,27 +3,24 @@ open Printf let mqi_debug_fun = ignore let mqi_flags = [] -let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun +let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun () let verbose = false exception Failure of string +exception Multiple_interpretations let fail msg = raise (Failure msg) +let uri_predicate = ref BatchParser.constants_only + module DisambiguateCallbacks = struct - let output_html ?(append_NL = true) msg = - if verbose then - (if append_NL then print_string else print_endline) - (Ui_logger.string_of_html_msg msg) - let interactive_user_uri_choice - ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id = - List.filter - (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = + List.filter !uri_predicate choices - let interactive_interpretation_choice _ = fail "Multiple interpretations" - let input_or_locate_uri ~title = fail "Unknown identifier" + let interactive_interpretation_choice _ = raise Multiple_interpretations + let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title) end module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) @@ -31,9 +28,9 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) let debug_print s = prerr_endline ("^^^^^^ " ^ s) let test_uri uri = - let obj = CicCache.get_obj uri in + let obj = CicEnvironment.get_obj uri in let (annobj, _, _, ids_to_inner_sorts, _, _, _) = - Cic2acic.acic_object_of_cic_object obj + Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in let ids_to_uris = Hashtbl.create 1023 in let round_trip annterm = @@ -41,9 +38,12 @@ let test_uri uri = let (ast, _) = Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm in - debug_print ("ast: " ^ CicAstPp.pp_term ast); + 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 (_, _, term) = - Disambiguate'.disambiguate_term mqi_handle [] [] ast + Disambiguate'.disambiguate_term mqi_handle [] [] new_ast DisambiguateTypes.Environment.empty in debug_print ("term: " ^ CicPp.ppterm term) @@ -75,37 +75,90 @@ let test_uri uri = | Cic.AInductiveDefinition _ -> debug_print "AInductiveDefinition: boh ..." -let test_uri uri = try test_uri uri; true with _ -> false +let test_uri uri = + try + test_uri uri; + `Ok + with + | Multiple_interpretations -> `Maybe + | exn -> + prerr_endline (sprintf "Top Level Uncaught Exception: %s" + (Printexc.to_string exn)); + `Nok -let _ = - let idx = ref 0 in - let ok = ref [] in - let nok = ref [] in +let report (ok,nok,maybe) = + 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 () + +let do_uri (ok, nok, maybe) uri = + let uri_str = UriManager.string_of_uri uri in + printf "Testing URI: %-55s %!" (uri_str ^ " ..."); + match test_uri 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 + +let do_file status fname = try - let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in - while true do - incr idx; - let uri_str = - match mode with - | `Stdin -> input_line stdin - | `Cmdline -> Sys.argv.(!idx) - in - printf "Testing URI: %-55s " (uri_str ^ " ..."); flush stdout; - let uri = UriManager.uri_of_string uri_str in - if test_uri uri then begin - print_endline "[ OK ]"; - ok := uri_str :: !ok - end else begin - print_endline "[ FAILED ]"; - nok := uri_str :: !nok - end - done - with Invalid_argument _ | End_of_file -> - 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_newline () + 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 _ = + Helm_registry.load_from "triciclo.conf.xml"; + 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 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)" ; + "-varsprefix", Arg.Set_string varsprefix, + "limit variable choices to URIs beginning with prefix" ; + ] + in + Arg.parse spec (fun name -> names := name :: !names) usage; + let names = List.rev !names in + uri_predicate := BatchParser.uri_pred_of_conf !tryvars !varsprefix; + let status = (ref [], ref [], ref []) in (* 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