addition of lia.cache - csdp.cache is now handled by micromega not csdpcert

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 7 deletions

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 272cc8931..cbacc48e4 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -40,6 +40,10 @@ module type PHashtable =
 	Once closed, a table cannot be used.
 	i.e, copy, find,add will raise UnboundTable *)
 
+    val memo : string -> (key -> 'a) -> (key -> 'a)
+      (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
+	  Note that the cache is just loaded when needed *)
+
   end
 
 open Hashtbl
@@ -86,15 +90,12 @@ let finally f rst =
 
 
 (** [from_file f] returns a hashtable by parsing records from file [f].
-    The structure of the file is
-    (KEY NL ELEM NL)* 
-    where 
-    NL is the character '\n'
-    KEY and ELEM are strings (without NL) parsed 
-    by the functions Key.parse and Elem.parse
+    Elements of the file are marshelled pairs of Caml structures.
+    (To ensure portability across platforms, closures are not allowed.)
 
     Raises Sys_error if the file cannot be open
-    Raises InvalidTableFormat if the file does not conform to the format,
+    Raises InvalidTableFormat if the file does not conform to the format
+    i.e, Marshal.from_channel fails
 *)
 
 
@@ -167,6 +168,18 @@ let find t k =
       let res = Table.find tbl k in
 	res 
 
+let memo cache f = 
+  let tbl = lazy (open_in cache) in
+    fun x -> 
+      let tbl = Lazy.force tbl in
+	try 
+	  find tbl x
+	with
+	    Not_found -> 
+	      let res = f x in
+		add tbl x res ;
+		res
+
 end