From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Feb 2004 14:29:34 +0000 (+0000)
Subject: - do not crash any longer if type-checking or reduction fails
X-Git-Tag: V_0_2_3~90
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5589e7ec798fc3e5c70b2ef23db6b402d5181af;p=helm.git

- do not crash any longer if type-checking or reduction fails
- prints also the metasenv
---

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index ed8988bb8..73eaf06ee 100644
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -37,7 +37,7 @@ let sep = Pcre.regexp rawsep
 let msg_prefix = "*** REGTEST *** "
 let print_msg s = prerr_endline (msg_prefix ^ s)
 
-type state = Term | ETerm | EType | EReduced
+type state = Term | EMetasenv | ETerm | EType | EReduced
 
 (* regtest file format
  *    < cic term in concrete syntax >
@@ -51,6 +51,7 @@ type state = Term | ETerm | EType | EReduced
 
 type regtest = {
   term: string; (* raw cic term *)
+  emetasenv : string; (* expected metasenv *)
   eterm: string;  (* expected term *)
   etype: string;  (* expected type *)
   ereduced: string; (* expected reduced term *)
@@ -62,6 +63,7 @@ let print_test test fname =
   output_string oc
     (String.concat ""
       [ test.term; rawsep ^ "\n";
+        test.emetasenv; rawsep ^ "\n";
         test.eterm; rawsep ^ "\n";
         test.etype; rawsep ^ "\n";
         test.ereduced ]);
@@ -69,24 +71,26 @@ let print_test test fname =
 
 let parse_regtest =
   let term = Buffer.create 1024 in  (* raw term *)
+  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 *)
   let ereduced = Buffer.create 1024 in (* raw expected reducted term *)
   let state = ref Term in
   let bump_state () =
     match !state with
-    | Term -> state := ETerm
+    | Term -> state := EMetasenv
+    | EMetasenv -> state := ETerm
     | ETerm -> state := EType
     | EType -> state := EReduced
     | EReduced -> assert false
   in
   let buffer_of_state = function
-    | Term ->  term | ETerm -> eterm | EType -> etype | EReduced -> ereduced
+    | Term ->  term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype | EReduced -> ereduced
   in
   fun fname ->
     state := Term;
-    Buffer.clear term; Buffer.clear eterm; Buffer.clear etype;
-    Buffer.clear ereduced;
+    Buffer.clear term; Buffer.clear emetasenv; Buffer.clear eterm;
+    Buffer.clear etype; Buffer.clear ereduced;
     let ic = open_in fname in
     (try
       while true do
@@ -96,7 +100,9 @@ let parse_regtest =
         | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
       done
     with End_of_file -> ());
+prerr_endline ("@@@ " ^ Buffer.contents emetasenv);
     { term = Buffer.contents term;
+      emetasenv = Buffer.contents emetasenv;
       eterm = Buffer.contents eterm;
       etype = Buffer.contents etype;
       ereduced = Buffer.contents ereduced }
@@ -132,13 +138,24 @@ let as_expected expected found = (* ignores "term" field *)
 let test_this raw_term =
   let empty_context = [] in
   let (metasenv, cic_term) = BatchParser.parse raw_term in
-  let cic_type = CicTypeChecker.type_of_aux' metasenv empty_context cic_term in
-  let cic_reduced = CicReduction.whd empty_context cic_term in
+  let etype =
+   try
+    CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
+   with
+    _ -> "MALFORMED"
+  in
+  let ereduced =
+   try
+    CicPp.ppterm (CicReduction.whd empty_context cic_term)
+   with
+    _ -> "MALFORMED"
+  in
   {
     term = raw_term;  (* useless *)
+    emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
     eterm = CicPp.ppterm cic_term ^ "\n";
-    etype = CicPp.ppterm cic_type ^ "\n";
-    ereduced = CicPp.ppterm cic_reduced ^ "\n";
+    etype = etype ^ "\n";
+    ereduced = ereduced ^ "\n";
   }
 
 let main () =