X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2Fregtest.ml;h=4142afa1afcd9b42ce6d16153eda029cc8583666;hb=29442b4d21cf07992ad4e5c981085dada1f90fe4;hp=a1ecd302f12525c8c96857d7dfdeb526d539a328;hpb=29c4c207d66c4643e642abc8f70efd40aadc499d;p=helm.git

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index a1ecd302f..4142afa1a 100644
--- 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 test_this uri_pred raw_term =
-  let empty_context = [] in
-  let (metasenv, cic_term) = BatchParser.parse ~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"
+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
-  {
-    term = raw_term;  (* useless *)
-    emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
-    eterm = CicPp.ppterm cic_term ^ "\n";
-    etype = etype ^ "\n";
-    ereduced = ereduced ^ "\n";
-  }
+   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
+  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
@@ -202,7 +228,7 @@ let restore_environment filename =
   else
    CicEnvironment.empty ()
 
-let main generate dump fnames tryvars varsprefix =
+let main mqi_handle generate  dump fnames tryvars varsprefix =
  let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in
  if generate then
   begin
@@ -214,9 +240,9 @@ let main 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 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 generate dump fnames tryvars varsprefix =
        let is_ok = 
         try
           let expected = parse_regtest test_fname in
-          let actual = test_this 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)
@@ -265,6 +291,10 @@ let _ =
   (fun ?(append_NL = true) msg ->
     (if append_NL then prerr_endline else prerr_string)
       (HelmLogger.string_of_html_msg msg));
+ 
+ let mqi_debug_fun = ignore in
+ let mqi_handle = MQIConn.init ~log:mqi_debug_fun () in
+ 
  let fnames = ref [] in
  let gen = ref false in
  let tryvars = ref false in
@@ -292,5 +322,5 @@ let _ =
   Arg.parse spec (fun filename -> fnames := filename::!fnames ) usage ;
   if !fnames = [] then
    Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ;
-  main !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix
-
+  main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix;
+  MQIConn.close mqi_handle