]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/regtest.ml
- regtest now handles more than one interpretation: the tests committed
[helm.git] / helm / gTopLevel / regtest.ml
index e31b1da05645605bef43461df06f5368d9772171..4e72bdd544616a50078e82e26910c2b2d84755e4 100644 (file)
@@ -191,17 +191,33 @@ 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 s = print_endline_to_channel (Lazy.force och) s in
+  let print_interpretation test =
+    print_endline "## Interpretation dump ##";
+    print_endline "# Disambiguation environment:";
+    print_endline test.eenv;
+    print_endline "# Metasenv:";
+    print_endline test.emetasenv;
+    print_endline "# Term:";
+    print_endline test.eterm;
+    print_endline "# Type:";
+    print_endline test.etype;
+    print_endline "# Reduced term:";
+    print_endline test.ereduced;
+  in
   let rec aux =
    function
       [],[] -> true
     | ex::extl, fo::fotl ->
-       as_expected_one och ex fo &&
-       aux (extl,fotl)
+        let outcome1 = as_expected_one och ex fo in
+        let outcome2 = aux (extl,fotl) in
+        outcome1 && outcome2
     | [],found ->
-       print_endline "### Too many interpretations found" ;
+       print_endline "### Too many interpretations found:" ;
+       List.iter print_interpretation found;
        false
     | expected,[] ->
-       print_endline "### Too few interpretations found" ;
+       print_endline "### Too few interpretations found:" ;
+       List.iter print_interpretation expected;
        false
   in
    let outcome = aux (expected,found) in