diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /lib/store.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'lib/store.ml')
-rw-r--r-- | lib/store.ml | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/lib/store.ml b/lib/store.ml new file mode 100644 index 00000000..bc1b335f --- /dev/null +++ b/lib/store.ml @@ -0,0 +1,61 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*** This module implements an "untyped store", in this particular case we + see it as an extensible record whose fields are left unspecified. ***) + +(* We give a short implementation of a universal type. This is mostly equivalent + to what is proposed by module Dyn.ml, except that it requires no explicit tag. *) +module type Universal = sig + type t + + type 'a etype = { + put : 'a -> t ; + get : t -> 'a option + } + + val embed : unit -> 'a etype +end + +(* We use a dynamic "name" allocator. But if we needed to serialise stores, we +might want something static to avoid troubles with plugins order. *) + +let next = + let count = ref 0 in fun () -> + let n = !count in + incr count; + n + +type t = Obj.t Util.Intmap.t + +module Field = struct + type 'a field = { + set : 'a -> t -> t ; + get : t -> 'a option ; + remove : t -> t + } + type 'a t = 'a field +end + +open Field + +let empty = Util.Intmap.empty + +let field () = + let fid = next () in + let set a s = + Util.Intmap.add fid (Obj.repr a) s + in + let get s = + try Some (Obj.obj (Util.Intmap.find fid s)) + with _ -> None + in + let remove s = + Util.Intmap.remove fid s + in + { set = set ; get = get ; remove = remove } |