X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=1b05e3c17fda7ecb24b2208f78b64d5eab204006;hb=c9995e146dc70bed25b9fe2913f3d5d31a4f9086;hp=681b9b36275bccad0cdb67790f6abb2f75d17a98;hpb=ad4a4b9f76a987637943341ab8465ef9a8a202d6;p=helm.git diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index 681b9b362..1b05e3c17 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -11,20 +11,16 @@ 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 _ = raise Multiple_interpretations - let input_or_locate_uri ~title = fail "Unknown identifier" + let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title) end module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) @@ -32,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 = @@ -42,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) @@ -87,41 +86,79 @@ let test_uri uri = (Printexc.to_string exn)); `Nok -let _ = - let idx = ref 0 in - let ok = ref [] in - let nok = ref [] in - let maybe = 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 - 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 - 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_endline "Multiple answers URIs:"; - List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe); - 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