X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fregtest.ml;h=aebc746889cf98e18615271c3a9d58b45cd3b81b;hb=98295941bee765a0cb4070eb3f2df553228c11c8;hp=625ac6440fd615c4231055527b92b844652adbc5;hpb=3ee539bf94fa9c894bdb0e81262d080e1c895371;p=helm.git

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index 625ac6440..aebc74688 100644
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -29,7 +29,7 @@ let argc = Array.length Sys.argv
 
 let rawsep = "###"
 let sep = Pcre.regexp (sprintf "^%s" rawsep)
-let print s = print_string s
+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")
 
@@ -154,20 +154,18 @@ let as_expected report_fname expected found = (* ignores "term" field *)
    end;
   outcome
 
-let test_this raw_term =
+let test_this uri_pred raw_term =
   let empty_context = [] in
-  let (metasenv, cic_term) = BatchParser.parse raw_term 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"
+   with _ -> "MALFORMED"
   in
   let ereduced =
    try
     CicPp.ppterm (CicReduction.whd empty_context cic_term)
-   with
-    _ -> "MALFORMED"
+   with _ -> "MALFORMED"
   in
   {
     term = raw_term;  (* useless *)
@@ -187,7 +185,6 @@ let dump_environment filename =
      ("DUMP_ENVIRONMENT FAILURE, uncaught excecption " ^
        Printexc.to_string exc) ;
     raise exc
-;;
 
 let restore_environment filename =
   if Sys.file_exists filename then
@@ -204,9 +201,9 @@ let restore_environment filename =
    end
   else
    CicEnvironment.empty ()
-;;
 
-let main generate dump fnames =
+let main generate dump fnames tryvars varsprefix =
+ let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in
  if generate then
   begin
    (* gen mode *)
@@ -218,7 +215,7 @@ let main generate dump fnames =
       print_endline (sprintf "Generating regtest %s -> %s\n ..."
         fname test_fname);
       let raw_term = (parse_regtest fname).term in
-      let result = test_this raw_term in
+      let result = test_this uri_pred raw_term in
       print_test result test_fname ;
       if dump then dump_environment env_fname ;
     ) fnames
@@ -238,7 +235,7 @@ let main generate dump fnames =
        let is_ok = 
         try
           let expected = parse_regtest test_fname in
-          let actual = test_this expected.term in
+          let actual = test_this uri_pred expected.term in
           if dump then dump_environment env_fname ;
           if as_expected report_fname expected actual then
            (incr ok ; true)
@@ -248,7 +245,11 @@ let main generate dump fnames =
        in
         let timediff = Unix.gettimeofday () -. time in
          print (sprintf "done in %f seconds\t" timediff) ;
-         print_endline (if is_ok then "[   OK   ]" else "[ FAILED ]")
+         print_endline
+          (if is_ok then
+            "[   OK   ]"
+          else
+            "[ FAILED ]")
      ) fnames ;
     print_endline "*** Summary ***";
     print_endline (sprintf "Succeeded: %d" !ok);
@@ -256,24 +257,39 @@ let main generate dump fnames =
     List.iter (fun fname -> print_endline (sprintf "  %s failed :-(" fname))
       (List.rev !nok)
   end
-;;
 
 let _ =
+ Helm_registry.load_from "triciclo.conf.xml";
+ HelmLogger.register_log_callback
+  (fun ?(append_NL = true) msg ->
+    (if append_NL then prerr_endline else prerr_string)
+      (HelmLogger.string_of_html_msg msg));
  let fnames = ref [] in
  let gen = ref false in
+ let tryvars = ref false in
  let dump = ref false in
  let nodump = ref false in
+ let varsprefix = ref "" in
  let usage = "regtest [OPTION] ... test1 ..." in
  let spec =
-   ["-gen",    Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ;
-    "--gen",    Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ;
-    "-dump",   Arg.Set dump, "dumps the final environment" ;
-    "--dump",   Arg.Set dump, "dumps the final environment" ;
-    "-nodump", Arg.Set dump, "do not dump the final environment" ;
-    "--nodump", Arg.Set dump, "do not dump the final environment" ]
+   ["-gen", Arg.Set gen,
+      "generate the tests; implies -dump (unless -nodump is specified)" ;
+    "--gen", Arg.Set gen,
+      "generate the tests; implies -dump (unless -nodump is specified)" ;
+    "-dump", Arg.Set dump, "dump the final environment" ;
+    "--dump", Arg.Set dump, "dump the final environment" ;
+    "-nodump", Arg.Set nodump, "do not dump the final environment" ;
+    "--nodump", Arg.Set nodump, "do not dump the final environment" ;
+    "-vars", Arg.Set tryvars, "try also variables" ;
+    "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
+    "-varsprefix", Arg.Set_string varsprefix,
+      "limit variable choices to URIs beginning with prefix" ;
+    "--varsprefix", Arg.Set_string varsprefix,
+      "limit variable choices to URIs beginning with prefix" ;
+   ]
  in
-  Arg.parse spec (function filename -> fnames := filename::!fnames ) usage ;
+  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
-;;
+  main !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix
+