Initial revision

[helm.git] / helm / interface / theoryTypeChecker.ml

diff --git a/helm/interface/theoryTypeChecker.ml b/helm/interface/theoryTypeChecker.ml
new file mode 100644 (file)
index 0000000..2d24536
--- /dev/null
+++ b/helm/interface/theoryTypeChecker.ml
@@ -0,0 +1,29 @@
+exception NotWellTyped of string;;
+
+let typecheck uri =
+  let rec typecheck_term curi t =
+  let module T = Theory in
+  let module P = CicTypeChecker in
+  let module C = CicCache in
+  let module U = UriManager in
+  let obj_typecheck uri =
+   try
+    P.typecheck (U.uri_of_string uri)
+   with
+    P.NotWellTyped s ->
+     raise (NotWellTyped
+      ("Type Checking was NOT successfull due to an error during " ^
+       "type-checking of term " ^ uri ^ ":\n\n" ^ s))
+  in
+    match t with
+       T.Theorem uri -> obj_typecheck (curi ^ "/" ^ uri)
+     | T.Definition uri -> obj_typecheck (curi ^ "/" ^ uri)
+     | T.Axiom uri -> obj_typecheck (curi ^ "/" ^ uri)
+     | T.Variable uri -> obj_typecheck (curi ^ "/" ^ uri)
+     | T.Section (uri,l) -> typecheck_theory l (curi ^ "/" ^ uri)
+ and typecheck_theory l curi =
+  List.iter (typecheck_term curi) l
+ in
+  let (uri, l) = TheoryCache.get_theory uri in
+   typecheck_theory l uri
+;;