From edb6ab182b915ebc8b2810574b0a87bdab39d051 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 7 Feb 2004 10:33:09 +0000 Subject: [PATCH] - added options "-vars" and "-varsprefix" - ported testlibrary to Arg module --- helm/gTopLevel/batchParser.ml | 20 +++++-- helm/gTopLevel/batchParser.mli | 16 ++++- helm/gTopLevel/regtest.ml | 55 ++++++++++------- helm/gTopLevel/testlibrary.ml | 105 +++++++++++++++++++++------------ 4 files changed, 129 insertions(+), 67 deletions(-) diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml index 05fd7a614..bd7165bec 100644 --- a/helm/gTopLevel/batchParser.ml +++ b/helm/gTopLevel/batchParser.ml @@ -28,6 +28,16 @@ let verbose = false exception Failure of string let fail msg = raise (Failure msg) +let constants_only uri = not (String.sub uri (String.length uri - 4) 4 = ".var") +let uri_predicate = ref constants_only + +let uri_pred_of_conf tryvars varsprefix = + if not tryvars then + constants_only + else + let rex = Pcre.regexp ("^" ^ varsprefix) in + (fun uri -> Pcre.pmatch ~rex uri) + module DisambiguateCallbacks = struct let output_html ?(append_NL = true) msg = @@ -36,9 +46,8 @@ module DisambiguateCallbacks = (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" @@ -50,7 +59,8 @@ let mqi_debug_fun = ignore let mqi_flags = [] let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun -let parse = +let parse ?(uri_pred = constants_only) = + uri_predicate := uri_pred; let empty_environment = DisambiguatingParser.EnvironmentP3.of_string DisambiguatingParser.EnvironmentP3.empty @@ -64,5 +74,5 @@ let parse = in (metasenv, term) -let parse_pp input = CicPp.ppterm (snd (parse input)) +let parse_pp ?uri_pred input = CicPp.ppterm (snd (parse ?uri_pred input)) diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli index 7d8f4bcd7..b63845aa8 100644 --- a/helm/gTopLevel/batchParser.mli +++ b/helm/gTopLevel/batchParser.mli @@ -25,12 +25,22 @@ exception Failure of string + (** uri_pred which rejects ll .var URIs *) +val constants_only: (string -> bool) + + (** @param variables enabled + * @param variables prefix + * @return uri predicate suitable for functions below *) +val uri_pred_of_conf: bool -> string -> (string -> bool) + (** Parse a cic term from the given string using disambiguating parser in - * batch mode if possible, otherwise raises Failure above *) -val parse: string -> Cic.metasenv * Cic.term + * batch mode if possible, otherwise raises Failure above. + * uri_pred is the predicate used to select which uris are tried. Per default + * only constant URIs are accepted *) +val parse: ?uri_pred:(string -> bool) -> string -> Cic.metasenv * Cic.term (** as above, but instead of returning the parsed cic term, pretty prints it * (ignoring returned metasenv) *) -val parse_pp: string -> string +val parse_pp: ?uri_pred:(string -> bool) -> string -> string diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index f3635f3d8..c146683ad 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -154,20 +154,18 @@ let as_expected report_fname expected found = (* ignores "term" field *) end; outcome -let test_this raw_term = +let test_this uri_pred raw_term = let empty_context = [] in - let (metasenv, cic_term) = BatchParser.parse raw_term in + let (metasenv, cic_term) = BatchParser.parse ~uri_pred raw_term in let etype = try CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term) - with - _ -> "MALFORMED" + with _ -> "MALFORMED" in let ereduced = try CicPp.ppterm (CicReduction.whd empty_context cic_term) - with - _ -> "MALFORMED" + with _ -> "MALFORMED" in { term = raw_term; (* useless *) @@ -187,7 +185,6 @@ let dump_environment filename = ("DUMP_ENVIRONMENT FAILURE, uncaught excecption " ^ Printexc.to_string exc) ; raise exc -;; let restore_environment filename = if Sys.file_exists filename then @@ -204,9 +201,9 @@ let restore_environment filename = end else CicEnvironment.empty () -;; -let main generate dump fnames = +let main generate dump fnames tryvars varsprefix = + let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in if generate then begin (* gen mode *) @@ -218,7 +215,7 @@ let main generate dump fnames = print_endline (sprintf "Generating regtest %s -> %s\n ..." fname test_fname); let raw_term = (parse_regtest fname).term in - let result = test_this raw_term in + let result = test_this uri_pred raw_term in print_test result test_fname ; if dump then dump_environment env_fname ; ) fnames @@ -238,7 +235,7 @@ let main generate dump fnames = let is_ok = try let expected = parse_regtest test_fname in - let actual = test_this expected.term in + let actual = test_this uri_pred expected.term in if dump then dump_environment env_fname ; if as_expected report_fname expected actual then (incr ok ; true) @@ -248,7 +245,11 @@ let main generate dump fnames = in let timediff = Unix.gettimeofday () -. time in print (sprintf "done in %f seconds\t" timediff) ; - print_endline (if is_ok then "[ OK ]" else "[ FAILED ]") + print_endline + (if is_ok then + "[ OK ]" + else + "[ FAILED ]") ) fnames ; print_endline "*** Summary ***"; print_endline (sprintf "Succeeded: %d" !ok); @@ -256,24 +257,34 @@ let main generate dump fnames = List.iter (fun fname -> print_endline (sprintf " %s failed :-(" fname)) (List.rev !nok) end -;; let _ = let fnames = ref [] in let gen = ref false in + let tryvars = ref false in let dump = ref false in let nodump = ref false in + let varsprefix = ref "" in let usage = "regtest [OPTION] ... test1 ..." in let spec = - ["-gen", Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ; - "--gen", Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ; - "-dump", Arg.Set dump, "dumps the final environment" ; - "--dump", Arg.Set dump, "dumps the final environment" ; - "-nodump", Arg.Set dump, "do not dump the final environment" ; - "--nodump", Arg.Set dump, "do not dump the final environment" ] + ["-gen", Arg.Set gen, + "generate the tests; implies -dump (unless -nodump is specified)" ; + "--gen", Arg.Set gen, + "generate the tests; implies -dump (unless -nodump is specified)" ; + "-dump", Arg.Set dump, "dump the final environment" ; + "--dump", Arg.Set dump, "dump the final environment" ; + "-nodump", Arg.Set nodump, "do not dump the final environment" ; + "--nodump", Arg.Set nodump, "do not dump the final environment" ; + "-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" ; + "--varsprefix", Arg.Set_string varsprefix, + "limit variable choices to URIs beginning with prefix" ; + ] in - Arg.parse spec (function filename -> fnames := filename::!fnames ) usage ; + Arg.parse spec (fun filename -> fnames := filename::!fnames ) usage ; if !fnames = [] then Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ; - main !gen ((!gen || !dump) && (not !nodump)) !fnames -;; + main !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix + diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index 681b9b362..90563a618 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -11,6 +11,8 @@ 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 = @@ -19,9 +21,8 @@ module DisambiguateCallbacks = (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" @@ -87,41 +88,71 @@ 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)) ok; + print_endline "Failed URIs:"; + List.iter (fun s -> print_endline ("\t" ^ s)) nok; + print_endline "Multiple answers URIs:"; + List.iter (fun s -> print_endline ("\t" ^ s)) 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 + let ic = open_in fname 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 + 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 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 () + with exn -> + printf "Error trying to access '%s' (%s), skipping the file\n%!" + fname (Printexc.to_string exn) + +let _ = + 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 -- 2.39.2