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.

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index f7370422f7fccf70b03ebe0bd9508c0b27eb2223..0d959ac6540861dbd31bdb9843079ca89a56673f 100644 (file)
--- 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 9ba49ef52b9ff80b11b1c9dfce55727b3de67dd1..b6410fe3bc1af096d6e6b8ae4c1c9847c9e9a989 100644 (file)
--- 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 4e72bdd544616a50078e82e26910c2b2d84755e4..d90371759b21e98e10f2bcab460aa6272f202c0d 100644 (file)
--- 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 ea6e4c6c037db42b62fb335e94a6776bc9d7546a..af459000a0c18e44de8f41e20b1f14e16e4dc5e6 100644 (file)
--- 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  (* <ok, nok, maybe> URIs *)
   List.iter
     (fun name ->