From 16f4538e0eb7deba0e145298aa8fef847d8a51f9 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 5 Feb 2004 17:22:54 +0000
Subject: [PATCH] - added testlibrary .opts - build just gTopLevel per default

---
 helm/gTopLevel/Makefile       | 10 +++++----
 helm/gTopLevel/testlibrary.ml | 41 ++++++++++++++++++++++++++++++++---
 2 files changed, 44 insertions(+), 7 deletions(-)

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 54a2f1d16..8a41c7dc2 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -13,8 +13,8 @@ OCAMLDEP = ocamldep -pp camlp4o
 LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
 LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
 
-all: styles gTopLevel regtest
-opt: styles gTopLevel.opt regtest.opt
+all: styles gTopLevel
+opt: styles gTopLevel.opt
 
 start:
 	$(MAKE) -C ../hbugs/ start
@@ -59,6 +59,8 @@ gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
 
 testlibrary: $(TESTLIBOBJS) $(LIBRARIES)
 	$(OCAMLC) -linkpkg -o $@ $(TESTLIBOBJS)
+testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(LIBRARIES)
+	$(OCAMLOPT) -linkpkg -o $@ $(TESTLIBOBJS:.cmo=.cmx)
 regtest: $(REGTESTOBJS) $(LIBRARIES)
 	$(OCAMLC) -linkpkg -o $@ $(REGTESTOBJS)
 regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(LIBRARIES)
@@ -91,9 +93,9 @@ cleantest:
 	rm -f $(OUTTESTS)
 tests/%.cic.test: tests/%.cic regtest
 	time ./regtest -gen $<
-test:
+test: regtest
 	./regtest $(INTESTS) 2> /dev/null
-envtest:
+envtest: regtest
 	./regtest -dump $(INTESTS) 2> /dev/null
 
 ifneq ($(MAKECMDGOALS), depend)
diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index bdc07e977..a4675a751 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -1,4 +1,6 @@
 
+open Printf
+
 let mqi_debug_fun = ignore
 let mqi_flags = []
 let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
@@ -28,8 +30,7 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
 
 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 
-let main () =
-  let uri = UriManager.uri_of_string (Sys.argv.(1)) in
+let test_uri uri =
   let obj = CicCache.get_obj uri in
   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
     Cic2acic.acic_object_of_cic_object obj
@@ -52,8 +53,10 @@ let main () =
       debug_print "Cic.AConstant (ty)";
       round_trip ty
   | Cic.AConstant (_, _, _, Some bo, ty, _) ->
+(*
       debug_print "Cic.AConstant (bo)";
       round_trip bo;
+*)
       debug_print "Cic.AConstant (ty)";
       round_trip ty
   | Cic.AVariable (_, _, None, ty, _) ->
@@ -72,5 +75,37 @@ let main () =
   | Cic.AInductiveDefinition _ ->
       debug_print "AInductiveDefinition: boh ..."
 
-let _ = main ()
+let test_uri uri = try test_uri uri; true with _ -> false
+
+let _ =
+  let idx = ref 0 in
+  let ok = ref [] in
+  let nok = ref [] in
+  try
+    let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in
+    while true do
+      incr idx;
+      let uri_str =
+        match mode with
+        | `Stdin -> input_line stdin
+        | `Cmdline -> Sys.argv.(!idx)
+      in
+      printf "Testing URI: %s ...\t";
+      let uri = UriManager.uri_of_string uri_str in
+      if test_uri uri then begin
+        print_endline "[   OK   ]";
+        ok := uri_str :: !ok
+      end else begin
+        print_endline "[ FAILED ]";
+        nok := uri_str :: !nok
+      end
+    done
+  with Invalid_argument _ | End_of_file ->
+    print_newline ();
+    print_endline "TestLibrary report";
+    print_endline "Succeeded URIs:";
+    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
+    print_endline "Failed URIs:";
+    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
+    print_newline ()
 
-- 
2.39.2