The disambiguation now returns a list of interpretations.

[helm.git] / helm / gTopLevel / regtest.ml

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index 76621b5ecf8d611a9507db803e1e1f79e2cf5dfd..4142afa1afcd9b42ce6d16153eda029cc8583666 100644 (file)
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -55,19 +55,26 @@ type regtest = {
   ereduced: string; (* expected reduced term *)
 }
 
-let print_test test fname =
+let print_test tests fname =
   let oc = open_out fname in
-  output_string oc
-    (String.concat ""
-      [ 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 ]);
+  output_string oc (List.hd tests).term;
+  let i = ref 0 in
+  List.iter
+   (function test ->
+     incr i ;
+     output_string oc
+       (String.concat ""
+         [ sprintf "INTERPRETATION NUMBER %d\n" !i;
+           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;
+           "\n" ])
+   ) tests;
   close_out oc
 
 let parse_regtest =
@@ -104,24 +111,20 @@ let parse_regtest =
         | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
       done
     with End_of_file -> ());
-    { term = Buffer.contents term;
+    [{ term = Buffer.contents term;
       emetasenv = Buffer.contents emetasenv;
       eterm = Buffer.contents eterm;
       etype = Buffer.contents etype;
-      ereduced = Buffer.contents ereduced }
+      ereduced = Buffer.contents ereduced }]
 
-let as_expected report_fname expected found = (* ignores "term" field *)
+let as_expected_one och expected found = (* ignores "term" field *)
   let eterm_ok = expected.eterm = found.eterm 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
-  if outcome then
-   (if Sys.file_exists report_fname then Sys.remove report_fname)
-  else
    begin
-    let och = open_out report_fname in
-    let print_endline = print_endline_to_channel och in
+    let print_endline = print_endline_to_channel (Lazy.force och) in
     if not eterm_ok then begin
       print_endline "### Term mismatch ###";
       print_endline "# expected:";
@@ -150,30 +153,53 @@ let as_expected report_fname expected found = (* ignores "term" field *)
       print_endline "# found:";
       print_endline ("  " ^ found.ereduced);
     end;
-    close_out och ;
    end;
   outcome
 
+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 rec aux =
+   function
+      [],[] -> true
+    | ex::extl, fo::fotl ->
+       as_expected_one och ex fo &&
+       aux (extl,fotl)
+    | [],found ->
+       print_endline "### Too many interpretations found" ;
+       false
+    | expected,[] ->
+       print_endline "### Too few interpretations found" ;
+       false
+  in
+   let outcome = aux (expected,found) in
+    (if Lazy.lazy_is_val och then close_out (Lazy.force och)) ;
+    outcome
+
 let test_this mqi_handle uri_pred raw_term =
   let empty_context = [] in
-  let (metasenv, cic_term) = BatchParser.parse mqi_handle ~uri_pred raw_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 = etype ^ "\n";
-    ereduced = ereduced ^ "\n";
-  }
+  List.map
+   (function (metasenv, cic_term) ->
+     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 = etype ^ "\n";
+       ereduced = ereduced ^ "\n";
+     }
+   ) (BatchParser.parse mqi_handle ~uri_pred raw_term)
 
 let dump_environment filename =
   try
@@ -214,9 +240,9 @@ let main mqi_handle generate  dump fnames tryvars varsprefix =
       let env_fname = fname ^ ".env" in
       print_endline (sprintf "Generating regtest %s -> %s\n ..."
         fname test_fname);
-      let raw_term = (parse_regtest fname).term in
-      let result = test_this mqi_handle uri_pred raw_term in
-      print_test result test_fname ;
+      let raw_term = (List.hd (parse_regtest fname)).term in
+      let results = test_this mqi_handle uri_pred raw_term in
+      print_test results test_fname ;
       if dump then dump_environment env_fname ;
     ) fnames
   end else
@@ -235,7 +261,7 @@ let main mqi_handle generate  dump fnames tryvars varsprefix =
        let is_ok = 
         try
           let expected = parse_regtest test_fname in
-          let actual = test_this mqi_handle uri_pred expected.term in
+          let actual = test_this mqi_handle uri_pred (List.hd expected).term in
           if dump then dump_environment env_fname ;
           if as_expected report_fname expected actual then
            (incr ok ; true)