diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/micromega/persistent_cache.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
-rw-r--r-- | plugins/micromega/persistent_cache.ml | 180 |
1 files changed, 180 insertions, 0 deletions
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml new file mode 100644 index 00000000..f17e1c35 --- /dev/null +++ b/plugins/micromega/persistent_cache.ml @@ -0,0 +1,180 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* A persistent hashtable *) +(* *) +(* Frédéric Besson (Inria Rennes) 2009 *) +(* *) +(************************************************************************) + + +module type PHashtable = + sig + type 'a t + type key + + val create : int -> string -> 'a t + (** [create i f] creates an empty persistent table + with initial size i + associated with file [f] *) + + + val open_in : string -> 'a t + (** [open_in f] rebuilds a table from the records stored in file [f]. + As marshaling is not type-safe, it migth segault. + *) + + val find : 'a t -> key -> 'a + (** find has the specification of Hashtable.find *) + + val add : 'a t -> key -> 'a -> unit + (** [add tbl key elem] adds the binding [key] [elem] to the table [tbl]. + (and writes the binding to the file associated with [tbl].) + If [key] is already bound, raises KeyAlreadyBound *) + + val close : 'a t -> unit + (** [close tbl] is closing the table. + 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 will only be loaded when the function is used for the first time *) + + end + +open Hashtbl + +module PHashtable(Key:HashedType) : PHashtable with type key = Key.t = +struct + + type key = Key.t + + module Table = Hashtbl.Make(Key) + + + + exception InvalidTableFormat + exception UnboundTable + + + type mode = Closed | Open + + + type 'a t = + { + outch : out_channel ; + mutable status : mode ; + htbl : 'a Table.t + } + + +let create i f = + { + outch = open_out_bin f ; + status = Open ; + htbl = Table.create i + } + +let finally f rst = + try + let res = f () in + rst () ; res + with x -> + (try rst () + with _ -> raise x + ); raise x + + +let read_key_elem inch = + try + Some (Marshal.from_channel inch) + with + | End_of_file -> None + | _ -> raise InvalidTableFormat + +let open_in f = + let flags = [Open_rdonly;Open_binary;Open_creat] in + let inch = open_in_gen flags 0o666 f in + let htbl = Table.create 10 in + + let rec xload () = + match read_key_elem inch with + | None -> () + | Some (key,elem) -> + Table.add htbl key elem ; + xload () in + + try + finally (fun () -> xload () ) (fun () -> close_in inch) ; + { + outch = begin + let flags = [Open_append;Open_binary;Open_creat] in + open_out_gen flags 0o666 f + end ; + status = Open ; + htbl = htbl + } + with InvalidTableFormat -> + (* Try to keep as many entries as possible *) + begin + let flags = [Open_wronly; Open_trunc;Open_binary;Open_creat] in + let outch = open_out_gen flags 0o666 f in + Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl; + { outch = outch ; + status = Open ; + htbl = htbl + } + end + + +let close t = + let {outch = outch ; status = status ; htbl = tbl} = t in + match t.status with + | Closed -> () (* don't do it twice *) + | Open -> + close_out outch ; + Table.clear tbl ; + t.status <- Closed + +let add t k e = + let {outch = outch ; status = status ; htbl = tbl} = t in + if status = Closed + then raise UnboundTable + else + begin + Table.add tbl k e ; + Marshal.to_channel outch (k,e) [Marshal.No_sharing] + end + +let find t k = + let {outch = outch ; status = status ; htbl = tbl} = t in + if status = Closed + then raise UnboundTable + else + 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 + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) |