From 6cfcba76baa8f30c42624e911bd34a702f785766 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 2 Mar 2004 18:56:53 +0000 Subject: [PATCH] Big bug fixed: batchParser applied the varsprefix prefix also to constants and inductive types!!! It is now possible to specify independently the prefix for variables and the prefix for all the other objects. --- helm/gTopLevel/batchParser.ml | 28 +++++++++++++++++++++------- helm/gTopLevel/batchParser.mli | 7 ++++--- helm/gTopLevel/regtest.ml | 18 ++++++++++++------ helm/gTopLevel/testlibrary.ml | 13 +++++++++---- 4 files changed, 46 insertions(+), 20 deletions(-) diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml index f7370422f..0d959ac65 100644 --- a/helm/gTopLevel/batchParser.ml +++ b/helm/gTopLevel/batchParser.ml @@ -28,15 +28,29 @@ 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 constants_only ~prefix = + let test_prefix = + if prefix = "" then + (fun _ -> true) + else + (fun uri -> Pcre.pmatch ~rex:(Pcre.regexp ("^" ^ prefix)) uri) + in + fun uri -> + test_prefix uri && (not (String.sub uri (String.length uri - 4) 4 = ".var")) + +let uri_predicate = ref (constants_only ~prefix:"") -let uri_pred_of_conf tryvars varsprefix = +let uri_pred_of_conf tryvars ~prefix ~varsprefix = if not tryvars then - constants_only + constants_only ~prefix else - let rex = Pcre.regexp ("^" ^ varsprefix) in - (fun uri -> Pcre.pmatch ~rex uri) + let test_prefix = Pcre.pmatch ~rex:(Pcre.regexp ("^" ^ prefix)) in + let test_varsprefix = Pcre.pmatch ~rex:(Pcre.regexp ("^" ^ varsprefix)) in + fun uri -> + if String.sub uri (String.length uri - 4) 4 = ".var" then + test_varsprefix uri + else + test_prefix uri module DisambiguateCallbacks = struct @@ -57,7 +71,7 @@ module DisambiguateCallbacks = module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks) -let parse mqi_handle ?(uri_pred = constants_only) = +let parse mqi_handle ?(uri_pred = constants_only ~prefix:"") = uri_predicate := uri_pred; let empty_environment = DisambiguatingParser.EnvironmentP3.of_string diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli index 9ba49ef52..b6410fe3b 100644 --- a/helm/gTopLevel/batchParser.mli +++ b/helm/gTopLevel/batchParser.mli @@ -26,12 +26,13 @@ exception Failure of string (** uri_pred which rejects ll .var URIs *) -val constants_only: (string -> bool) +val constants_only: prefix:string -> (string -> bool) (** @param variables enabled - * @param variables prefix + * @param variables prefix varsprefix * @return uri predicate suitable for functions below *) -val uri_pred_of_conf: bool -> string -> (string -> bool) +val uri_pred_of_conf: + bool -> prefix:string -> varsprefix:string -> (string -> bool) (** Parse a cic term from the given string using disambiguating parser in * batch mode if possible, otherwise raises Failure above. diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 4e72bdd54..d90371759 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -275,8 +275,8 @@ let restore_environment filename = else CicEnvironment.empty () -let main mqi_handle generate dump fnames tryvars varsprefix = - let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in +let main mqi_handle generate dump fnames tryvars prefix varsprefix = + let uri_pred = BatchParser.uri_pred_of_conf tryvars ~prefix ~varsprefix in if generate then begin (* gen mode *) @@ -347,7 +347,8 @@ let _ = let tryvars = ref false in let dump = ref false in let nodump = ref false in - let varsprefix = ref "" in + let prefix = ref "" in + let varsprefix = ref "###" in let usage = "regtest [OPTION] ... test1 ..." in let spec = ["-gen", Arg.Set gen, @@ -360,14 +361,19 @@ let _ = "--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)" ; + "-prefix", Arg.Set_string prefix, + "limit object choices to URIs beginning with prefix" ; + "--prefix", Arg.Set_string prefix, + "limit object choices to URIs beginning with prefix" ; "-varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix" ; + "limit variable choices to URIs beginning with prefix; overrides -prefix" ; "--varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix" ; + "limit variable choices to URIs beginning with prefix; overrides -prefix" ] in 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 mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix; + if !varsprefix = "###" then varsprefix := !prefix ; + main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix; MQIConn.close mqi_handle diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index ea6e4c6c0..af459000a 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -12,7 +12,7 @@ let verbose = false exception Failure of string let fail msg = raise (Failure msg) -let uri_predicate = ref BatchParser.constants_only +let uri_predicate = ref (BatchParser.constants_only ~prefix:"") module DisambiguateCallbacks = struct @@ -147,18 +147,23 @@ let _ = (HelmLogger.string_of_html_msg msg)); let names = ref [] in let tryvars = ref false in - let varsprefix = ref "" in + let prefix = ref "" 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)" ; + "-prefix", Arg.Set_string prefix, + "limit object choices to URIs beginning with prefix" ; "-varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix" ; + "limit variable choices to URIs beginning with prefix; overrides -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; + if !varsprefix = "####" then varsprefix := !prefix ; + uri_predicate := + BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix; let status = (ref [], ref [], ref []) in (* URIs *) List.iter (fun name -> -- 2.39.2