From 52f95aaf56e9f915b2e049db92a706bdc15c8867 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 29 Oct 2004 12:21:39 +0000
Subject: [PATCH] added test script for typechecking URIs given on STDIN

---
 helm/gTopLevel/Makefile.in      |  4 ++++
 helm/gTopLevel/typecheck_uri.ml | 23 +++++++++++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 helm/gTopLevel/typecheck_uri.ml

diff --git a/helm/gTopLevel/Makefile.in b/helm/gTopLevel/Makefile.in
index 42dd44be1..4b44c3418 100644
--- a/helm/gTopLevel/Makefile.in
+++ b/helm/gTopLevel/Makefile.in
@@ -134,6 +134,10 @@ librarytest: testlibrary
 	./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
 librarytest.opt: testlibrary.opt
 	./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
+typecheck_uri: typecheck_uri.ml
+	$(OCAMLFIND) ocamlc -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
+typecheck_uri.opt: typecheck_uri.ml
+	$(OCAMLFIND) opt -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
 
 MAIN = ./gTopLevel
 ARGS =
diff --git a/helm/gTopLevel/typecheck_uri.ml b/helm/gTopLevel/typecheck_uri.ml
new file mode 100644
index 000000000..e6df5cd61
--- /dev/null
+++ b/helm/gTopLevel/typecheck_uri.ml
@@ -0,0 +1,23 @@
+
+
+open Printf
+
+let _ = Helm_registry.load_from "gTopLevel.conf.xml"
+
+let test_uri uri =
+  (try
+    Printf.printf "%s ... " uri;
+    let uri = UriManager.uri_of_string uri in
+    flush stdout;
+    ignore (CicTypeChecker.typecheck uri);
+    print_endline "ok";
+  with _ -> print_endline "failure");
+  flush stdout
+
+let _ =
+  try
+    while true do
+      test_uri (input_line stdin)
+    done
+  with End_of_file -> ()
+
-- 
2.39.2