From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 2 Mar 2004 14:53:13 +0000 (+0000)
Subject: Regtest fixed. It can now work also with multiple answers.
X-Git-Tag: v0_0_4~59
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb5df9e3b544239848e779f3eaa542174b5c5806;p=helm.git

Regtest fixed. It can now work also with multiple answers.
---

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index 4142afa1a..fb91bf200 100644
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -29,6 +29,7 @@ let argc = Array.length Sys.argv
 
 let rawsep = "###"
 let sep = Pcre.regexp (sprintf "^%s" rawsep)
+let sep2 = Pcre.regexp (sprintf "^%s%s" rawsep rawsep)
 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")
@@ -64,7 +65,7 @@ let print_test tests fname =
      incr i ;
      output_string oc
        (String.concat ""
-         [ sprintf "INTERPRETATION NUMBER %d\n" !i;
+         [ sprintf "%s%s INTERPRETATION NUMBER %d %s%s\n" rawsep rawsep !i rawsep rawsep ;
            sprintf "%s (* METASENV after disambiguation  *)\n" rawsep;
            test.emetasenv;
            sprintf "%s (* TERM after disambiguation      *)\n" rawsep;
@@ -72,8 +73,7 @@ let print_test tests fname =
            sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep;
            test.etype;
            sprintf "%s (* REDUCED disambiguated term     *)\n" rawsep;
-           test.ereduced;
-           "\n" ])
+           test.ereduced ])
    ) tests;
   close_out oc
 
@@ -97,25 +97,36 @@ let parse_regtest =
     | EReduced -> ereduced
   in
   let clear_buffers () =
-    List.iter Buffer.clear [ term; emetasenv; eterm; etype; ereduced ]
+    List.iter Buffer.clear [ emetasenv; eterm; etype; ereduced ]
   in
   fun fname ->
     state := Term;
-    clear_buffers ();
+    let first = ref true in
+    let res = ref [] in
+    let push_res () =
+     res :=
+      { term = Buffer.contents term;
+       emetasenv = Buffer.contents emetasenv;
+       eterm = Buffer.contents eterm;
+       etype = Buffer.contents etype;
+       ereduced = Buffer.contents ereduced } :: !res ;
+    in
+    Buffer.clear term;
     let ic = open_in fname in
     (try
       while true do
         let line = input_line ic in
         match line with
+        | l when Pcre.pmatch ~rex:sep2 l ->
+            if !first then first := false else push_res () ;
+            clear_buffers ();
+            state := Term
         | l when Pcre.pmatch ~rex:sep l -> bump_state ()
         | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
       done
     with End_of_file -> ());
-    [{ term = Buffer.contents term;
-      emetasenv = Buffer.contents emetasenv;
-      eterm = Buffer.contents eterm;
-      etype = Buffer.contents etype;
-      ereduced = Buffer.contents ereduced }]
+    push_res () ;
+    List.rev !res
 
 let as_expected_one och expected found = (* ignores "term" field *)
   let eterm_ok = expected.eterm = found.eterm in
@@ -124,7 +135,7 @@ let as_expected_one och expected found = (* ignores "term" field *)
   let ereduced_ok = expected.ereduced = found.ereduced in
   let outcome = eterm_ok && emetasenv_ok && etype_ok && ereduced_ok in
    begin
-    let print_endline = print_endline_to_channel (Lazy.force och) in
+    let print_endline s = print_endline_to_channel (Lazy.force och) s in
     if not eterm_ok then begin
       print_endline "### Term mismatch ###";
       print_endline "# expected:";
@@ -159,7 +170,7 @@ let as_expected_one och expected found = (* ignores "term" field *)
 let as_expected report_fname expected found =
  (if Sys.file_exists report_fname then Sys.remove report_fname) ;
  let och = lazy (open_out report_fname) in
- let print_endline = print_endline_to_channel (Lazy.force och) in
+ let print_endline s = print_endline_to_channel (Lazy.force och) s in
   let rec aux =
    function
       [],[] -> true