- comment inside .test file that explain what follows

- use a list to clear buffers
- better comment for .test file format

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index 8f42a29fcfbcaa23343fb78f0c9b55f044d5c376..b79ca5bf13770eea507d7a1887933ef50d4977d5 100644 (file)
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -33,7 +33,7 @@ let usage () =
   exit 2
 
 let rawsep = "###"
-let sep = Pcre.regexp rawsep
+let sep = Pcre.regexp (sprintf "^%s" rawsep)
 let msg_prefix = "*** REGTEST *** "
 let print_msg s = prerr_endline (msg_prefix ^ s)
 
@@ -42,11 +42,13 @@ type state = Term | EMetasenv | ETerm | EType | EReduced
 (* regtest file format
  *    < cic term in concrete syntax >
  *    separator (* see sep above *)
- *    < expected cic term after disambiguation as PPed by CicPp.ppterm >
+ *    < expected metasenv after disambiguation (CicMetaSubst.ppmetasenv)  >
  *    separator (* see sep above *)
- *    < expected cic type as per type_of as PPed by CicPp.ppterm >
+ *    < expected cic term after disambiguation (CicPp.ppterm) >
  *    separator (* see sep above *)
- *    < expected reduced cic term as PPed by CicPp.ppterm >
+ *    < expected cic type as per type_of (CicPp.ppterm) >
+ *    separator (* see sep above *)
+ *    < expected reduced cic term as (CicPp.ppterm) >
  *)
 
 type regtest = {
@@ -57,15 +59,18 @@ type regtest = {
   ereduced: string; (* expected reduced term *)
 }
 
-  (* this should be the only function here printing on stdout *)
 let print_test test fname =
   let oc = open_out fname in
   output_string oc
     (String.concat ""
-      [ test.term; rawsep ^ "\n";
-        test.emetasenv; rawsep ^ "\n";
-        test.eterm; rawsep ^ "\n";
-        test.etype; rawsep ^ "\n";
+      [ test.term;
+        sprintf "%s (* METASENV after disambiguation  *)\n" rawsep;
+        test.emetasenv;
+        sprintf "%s (* TERM after disambiguation      *)\n" rawsep;
+        test.eterm;
+        sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep;
+        test.etype;
+        sprintf "%s (* REDUCED disambiguated term     *)\n" rawsep;
         test.ereduced ]);
   close_out oc
 
@@ -85,12 +90,15 @@ let parse_regtest =
     | EReduced -> assert false
   in
   let buffer_of_state = function
-    | Term ->  term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype | EReduced -> ereduced
+    | Term ->  term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype
+    | EReduced -> ereduced
+  in
+  let clear_buffers () =
+    List.iter Buffer.clear [ term; emetasenv; eterm; etype; ereduced ]
   in
   fun fname ->
     state := Term;
-    Buffer.clear term; Buffer.clear emetasenv; Buffer.clear eterm;
-    Buffer.clear etype; Buffer.clear ereduced;
+    clear_buffers ();
     let ic = open_in fname in
     (try
       while true do
@@ -108,14 +116,6 @@ let parse_regtest =
 
 let as_expected expected found = (* ignores "term" field *)
   let outcome = ref true in
-  if expected.emetasenv <> found.emetasenv then begin
-    print_msg "Metasenv mismatch";
-    print_msg "  expected:";
-    print_msg ("  " ^ expected.emetasenv);
-    print_msg "  found:";
-    print_msg ("  " ^ found.emetasenv);
-    outcome := false;
-  end;
   if expected.eterm <> found.eterm then begin
     print_msg "Term mismatch";
     print_msg "  expected:";
@@ -124,6 +124,14 @@ let as_expected expected found = (* ignores "term" field *)
     print_msg ("  " ^ found.eterm);
     outcome := false;
   end;
+  if expected.emetasenv <> found.emetasenv then begin
+    print_msg "Metasenv mismatch";
+    print_msg "  expected:";
+    print_msg ("  " ^ expected.emetasenv);
+    print_msg "  found:";
+    print_msg ("  " ^ found.emetasenv);
+    outcome := false;
+  end;
   if expected.etype <> found.etype then begin
     print_msg "Type mismatch";
     print_msg "  expected:";