]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/typecheck_uri.ml
added test script for typechecking URIs given on STDIN
[helm.git] / helm / gTopLevel / typecheck_uri.ml
diff --git a/helm/gTopLevel/typecheck_uri.ml b/helm/gTopLevel/typecheck_uri.ml
new file mode 100644 (file)
index 0000000..e6df5cd
--- /dev/null
@@ -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 -> ()
+