Initial revision

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

diff --git a/helm/interface/theoryCache.ml b/helm/interface/theoryCache.ml
new file mode 100644 (file)
index 0000000..47a8646
--- /dev/null
+++ b/helm/interface/theoryCache.ml
@@ -0,0 +1,32 @@
+type check_status = Checked | Unchecked;;
+
+let hashtable = Hashtbl.create 17;;
+
+let get_term_and_type_checking_info uri =
+ try
+  Hashtbl.find hashtable uri
+ with
+  Not_found -> 
+   let filename = Getter.get uri in
+    let term = TheoryParser.theory_of_xml filename in
+     Hashtbl.add hashtable uri (term, Unchecked) ;
+     (term, Unchecked)
+;;
+
+
+let get_theory uri =
+ fst (get_term_and_type_checking_info uri)
+;;
+
+let is_type_checked uri =
+ match snd (get_term_and_type_checking_info uri) with
+    Checked   -> true
+  | Unchecked -> false
+;;
+
+let set_type_checking_info uri =
+ match Hashtbl.find hashtable uri with
+  (term, _) ->
+   Hashtbl.remove hashtable uri ;
+   Hashtbl.add hashtable uri (term, Checked)
+;;