From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Feb 2004 11:52:51 +0000 (+0000)
Subject: - regtest: better argument handling (using Arg)
X-Git-Tag: V_0_2_3~74
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a78c9d9b4da1f7b4ec83141449c4e81c5c96cff;p=helm.git

- regtest: better argument handling (using Arg)
- regtest: -dump and -nodump to dump the environment (that is authomatically
  restored if found)
- Makefile: new target envtest that generates the environments without
  changing the .test files
---

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index d66843453..0f3318ab2 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -80,14 +80,17 @@ uninstall:
 
 .PHONY: install uninstall clean test
 
-TESTS := $(patsubst %, %.test, $(wildcard tests/*.cic))
-gentest: $(TESTS)
+INTESTS := $(wildcard tests/*.cic)
+OUTTESTS := $(patsubst %, %.test, $INTESTS)
+gentest: $(OUTTESTS)
 cleantest:
-	rm -f $(TESTS)
-tests/%.cic.test: tests/%.cic
+	rm -f $(OUTTESTS)
+tests/%.cic.test: tests/%.cic regtest
 	time ./regtest -gen $<
 test:
-	time ./regtest $(TESTS)
+	time ./regtest $(INTESTS)
+envtest:
+	time ./regtest -dump $(INTESTS)
 
 ifneq ($(MAKECMDGOALS), depend)
    include .depend   
diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index b79ca5bf1..3a601e0c3 100644
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -27,11 +27,6 @@ open Printf
 
 let argc = Array.length Sys.argv
 
-let usage () =
-  prerr_endline "Usage: regtest <file.test> ...";
-  prerr_endline "       regtest (-gen|--gen) <file.cic> ...";
-  exit 2
-
 let rawsep = "###"
 let sep = Pcre.regexp (sprintf "^%s" rawsep)
 let msg_prefix = "*** REGTEST *** "
@@ -173,39 +168,96 @@ let test_this raw_term =
     ereduced = ereduced ^ "\n";
   }
 
-let main () =
-  if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *)
-    print_msg "[ Gen mode ]";
-    for i = 2 to argc - 1 do
-      let fname = Sys.argv.(i) in
+let dump_environment filename =
+  try
+    let oc = open_out filename in
+    CicEnvironment.dump_to_channel oc;
+    close_out oc
+  with exc ->
+    prerr_endline
+     ("DUMP_ENVIRONMENT FAILURE, uncaught excecption " ^
+       Printexc.to_string exc) ;
+    raise exc
+;;
+
+let restore_environment filename =
+  if Sys.file_exists filename then
+   begin
+    try
+      let ic = open_in filename in
+      CicEnvironment.restore_from_channel ic;
+      close_in ic
+    with exc ->
+      prerr_endline
+       ("RESTORE_ENVIRONMENT FAILURE, uncaught excecption " ^
+         Printexc.to_string exc) ;
+      raise exc
+   end
+  else
+   CicEnvironment.empty ()
+;;
+
+let main generate dump fnames =
+ if generate then
+  begin
+   (* gen mode *)
+   print_msg "[ Gen mode ]";
+   List.iter
+    (function fname ->
       let test_fname = fname ^ ".test" in
+      let env_fname = fname ^ ".env" in
       print_msg (sprintf "Generating regtest %s -> %s\n ..."
         fname test_fname);
       let raw_term = (parse_regtest fname).term in
       let result = test_this raw_term in
-      print_test result test_fname
-    done
-  end else begin  (* regtest mode *)
-    prerr_endline "[ Regtest mode ]";
+      print_test result test_fname ;
+      if dump then dump_environment env_fname ;
+    ) fnames
+  end else
+   begin
+    (* regtest mode *)
+    print_msg "[ Regtest mode ]";
     let (ok, nok) = (ref 0, ref []) in
-    for i = 1 to argc - 1 do
-      let fname = Sys.argv.(i) in
-      prerr_endline ("# " ^ fname);
-      try
-        let expected = parse_regtest fname in
-        let actual = test_this expected.term in
-        if as_expected expected actual then
-          incr ok
-        else
-          nok := fname :: !nok;
-      with e -> nok := fname :: !nok
-    done;
+    List.iter
+     (function fname ->
+       let env_fname = fname ^ ".env" in
+       let test_fname = fname ^ ".test" in
+       restore_environment env_fname ;
+       prerr_endline ("# " ^ fname);
+       try
+         let expected = parse_regtest test_fname in
+         let actual = test_this expected.term in
+         if dump then dump_environment env_fname ;
+         if as_expected expected actual then
+           incr ok
+         else
+           nok := fname :: !nok;
+       with e -> nok := fname :: !nok
+     ) fnames ;
     print_msg "Regtest completed:";
     print_msg (sprintf "Succeeded: %d" !ok);
     print_msg (sprintf "Failed: %d" (List.length !nok));
     List.iter (fun fname -> print_msg (sprintf "  %s failed :-(" fname))
       (List.rev !nok)
   end
+;;
 
-let _ = try main () with Invalid_argument _ -> usage ()
-
+let _ =
+ let fnames = ref [] in
+ let gen = ref false in
+ let dump = ref false in
+ let nodump = ref false 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" ]
+ in
+  Arg.parse spec (function 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
+;;
diff --git a/helm/gTopLevel/tests/.cvsignore b/helm/gTopLevel/tests/.cvsignore
index e69de29bb..03bd4129b 100644
--- a/helm/gTopLevel/tests/.cvsignore
+++ b/helm/gTopLevel/tests/.cvsignore
@@ -0,0 +1 @@
+*.env