The regression tests now check also the generated disambiguation environments.

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index 515c417cb4cc1e29d996e3b9ae9b450ba96d9ebc..f7370422f7fccf70b03ebe0bd9508c0b27eb2223 100644 (file)
--- a/helm/gTopLevel/batchParser.ml
+++ b/helm/gTopLevel/batchParser.ml
@@ -66,11 +66,10 @@ let parse mqi_handle ?(uri_pred = constants_only) =
   let empty_context = [] in
   let empty_metasenv = [] in
   fun input ->
-   List.map (fun (_,metasenv,term) -> metasenv,term)
-    (Disambiguate'.disambiguate_term
-      mqi_handle empty_context empty_metasenv input empty_environment)
+   (Disambiguate'.disambiguate_term
+     mqi_handle empty_context empty_metasenv input empty_environment)
 
 let parse_pp mqi_handle ?uri_pred input = 
- List.map (fun (_,t) -> CicPp.ppterm t)
+ List.map (fun (_,_,t) -> CicPp.ppterm t)
   (parse mqi_handle ?uri_pred input)
 

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index ff82e6fa057d9001dc43e4241d5e0a03df0640f1..9ba49ef52b9ff80b11b1c9dfce55727b3de67dd1 100644 (file)
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -37,7 +37,9 @@ val uri_pred_of_conf: bool -> string -> (string -> bool)
    * 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: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> (Cic.metasenv * Cic.term) list
+val parse:
+ MQIConn.handle -> ?uri_pred:(string -> bool) -> string ->
+  (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list
 
   (** as above, but instead of returning the parsed cic term, pretty prints it
    * (ignoring returned metasenv)

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index fb91bf2004f55f77adc6b1c8f68c4c4b265d3d9b..e31b1da05645605bef43461df06f5368d9772171 100644 (file)
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -34,10 +34,13 @@ let print s = print_string s; flush stdout
 let print_endline s = print_endline s
 let print_endline_to_channel ch s = output_string ch (s ^ "\n")
 
-type state = Term | EMetasenv | ETerm | EType | EReduced
+type state = Term | EEnv | EMetasenv | ETerm | EType | EReduced
 
 (* regtest file format
  *    < cic term in concrete syntax >
+ *    separatorseparator INTERPRETATION NUMBER <n> separatorseparator
+ *    separator (* see sep above *)
+ *    < expected disambiguating environment (EnvironmentP3.to_string)  >
  *    separator (* see sep above *)
  *    < expected metasenv after disambiguation (CicMetaSubst.ppmetasenv)  >
  *    separator (* see sep above *)
@@ -46,10 +49,12 @@ type state = Term | EMetasenv | ETerm | EType | EReduced
  *    < expected cic type as per type_of (CicPp.ppterm) >
  *    separator (* see sep above *)
  *    < expected reduced cic term as (CicPp.ppterm) >
+ *    ... (* repeat from ... INTERPRETATION NUMBER ... *)
  *)
 
 type regtest = {
   term: string; (* raw cic term *)
+  eenv : string; (* disambiguating parsing environment *)
   emetasenv : string; (* expected metasenv *)
   eterm: string;  (* expected term *)
   etype: string;  (* expected type *)
@@ -66,6 +71,8 @@ let print_test tests fname =
      output_string oc
        (String.concat ""
          [ sprintf "%s%s INTERPRETATION NUMBER %d %s%s\n" rawsep rawsep !i rawsep rawsep ;
+           sprintf "%s (* disambiguation environment  *)\n" rawsep;
+           test.eenv;
            sprintf "%s (* METASENV after disambiguation  *)\n" rawsep;
            test.emetasenv;
            sprintf "%s (* TERM after disambiguation      *)\n" rawsep;
@@ -79,6 +86,7 @@ let print_test tests fname =
 
 let parse_regtest =
   let term = Buffer.create 1024 in  (* raw term *)
+  let eenv = Buffer.create 1024 in  (* disambiguating parser environment *)
   let emetasenv = Buffer.create 1024 in  (* expected metasenv *)
   let eterm = Buffer.create 1024 in (* raw expected term *)
   let etype = Buffer.create 1024 in (* raw expected type *)
@@ -86,18 +94,19 @@ let parse_regtest =
   let state = ref Term in
   let bump_state () =
     match !state with
-    | Term -> state := EMetasenv
+    | Term -> state := EEnv
+    | EEnv -> state := EMetasenv
     | EMetasenv -> state := ETerm
     | ETerm -> state := EType
     | EType -> state := EReduced
     | EReduced -> assert false
   in
   let buffer_of_state = function
-    | Term ->  term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype
+    | Term ->  term | EEnv -> eenv | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype
     | EReduced -> ereduced
   in
   let clear_buffers () =
-    List.iter Buffer.clear [ emetasenv; eterm; etype; ereduced ]
+    List.iter Buffer.clear [ eenv; emetasenv; eterm; etype; ereduced ]
   in
   fun fname ->
     state := Term;
@@ -105,7 +114,8 @@ let parse_regtest =
     let res = ref [] in
     let push_res () =
      res :=
-      { term = Buffer.contents term;
+      {term = Buffer.contents term;
+       eenv = Buffer.contents eenv;
        emetasenv = Buffer.contents emetasenv;
        eterm = Buffer.contents eterm;
        etype = Buffer.contents etype;
@@ -130,10 +140,13 @@ let parse_regtest =
 
 let as_expected_one och expected found = (* ignores "term" field *)
   let eterm_ok = expected.eterm = found.eterm in
+  let eenv_ok = expected.eenv = found.eenv in
   let emetasenv_ok = expected.emetasenv = found.emetasenv in
   let etype_ok = expected.etype = found.etype in
   let ereduced_ok = expected.ereduced = found.ereduced in
-  let outcome = eterm_ok && emetasenv_ok && etype_ok && ereduced_ok in
+  let outcome =
+   eterm_ok && eenv_ok && emetasenv_ok && etype_ok && ereduced_ok
+  in
    begin
     let print_endline s = print_endline_to_channel (Lazy.force och) s in
     if not eterm_ok then begin
@@ -143,6 +156,13 @@ let as_expected_one och expected found = (* ignores "term" field *)
       print_endline "# found:";
       print_endline ("  " ^ found.eterm);
     end;
+    if not eenv_ok then begin
+      print_endline "### Disambiguation environment mismatch ###";
+      print_endline "# expected:";
+      print_endline ("  " ^ expected.eenv);
+      print_endline "# found:";
+      print_endline ("  " ^ found.eenv);
+    end;
     if not emetasenv_ok then begin
       print_endline "### Metasenv mismatch ###";
       print_endline "# expected:";
@@ -191,7 +211,7 @@ let as_expected report_fname expected found =
 let test_this mqi_handle uri_pred raw_term =
   let empty_context = [] in
   List.map
-   (function (metasenv, cic_term) ->
+   (function (env, metasenv, cic_term) ->
      let etype =
       try
        CicPp.ppterm
@@ -203,8 +223,8 @@ let test_this mqi_handle uri_pred raw_term =
        CicPp.ppterm (CicReduction.whd empty_context cic_term)
       with _ -> "MALFORMED"
      in
-     {
-       term = raw_term;  (* useless *)
+     { term = raw_term;  (* useless *)
+       eenv = DisambiguatingParser.EnvironmentP3.to_string env ^ "\n";
        emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
        eterm = CicPp.ppterm cic_term ^ "\n";
        etype = etype ^ "\n";