Merge branch 'experimental/upstream' into upstream

1 files changed, 61 insertions, 0 deletions

diff --git a/lib/store.ml b/lib/store.ml
new file mode 100644
index 00000000..28eb65c8
--- /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 Not_found -> None
+  in
+  let remove s =
+    Util.Intmap.remove fid s
+  in
+  { set = set ; get = get ; remove = remove }