diff options
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 } |