From e801a25712df6bf28e7dd7dac947d068f4453e5b Mon Sep 17 00:00:00 2001 From: fbesson Date: Fri, 31 Jul 2009 09:23:29 +0000 Subject: 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 --- plugins/micromega/persistent_cache.ml | 27 ++++++++++++++++++++------- 1 file changed, 20 insertions(+), 7 deletions(-) (limited to 'plugins/micromega/persistent_cache.ml') 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 -- cgit v1.2.3