Allowing different types of, not to be mixed, generic Stores through

functor application. Rewritten the interface btw.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16267 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 67 insertions, 34 deletions

diff --git a/lib/store.ml b/lib/store.ml
index 536e5f280e..4d6a74ec12 100644
--- a/lib/store.ml
+++ b/lib/store.ml
@@ -15,6 +15,25 @@
 (* We use a dynamic "name" allocator. But if we needed to serialise stores, we
 might want something static to avoid troubles with plugins order. *)
 
+module type T =
+sig
+end
+
+module type S =
+sig
+  type t
+  type 'a field
+  val empty : t
+  val set : t -> 'a field -> 'a -> t
+  val get : t -> 'a field -> 'a option
+  val remove : t -> 'a field -> t
+  val merge : t -> t -> t
+  val field : unit -> 'a field
+end
+
+module Make (M : T) : S =
+struct
+
 let next =
   let count = ref 0 in fun () ->
   let n = !count in
@@ -23,29 +42,22 @@ let next =
 
 type t = Obj.t Int.Map.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
+type 'a field = int
 
 let empty = Int.Map.empty
 
-let field () =
-  let fid = next () in
-  let set a s =
-    Int.Map.add fid (Obj.repr a) s
-  in
-  let get s =
-    try Some (Obj.obj (Int.Map.find fid s))
-    with _ -> None
-  in
-  let remove s =
-    Int.Map.remove fid s
-  in
-  { set = set ; get = get ; remove = remove }
+let set s (id : 'a field) (x : 'a) = Int.Map.add id (Obj.repr x) s
+
+let get s (id : 'a field) : 'a option =
+  try Some (Obj.obj (Int.Map.find id s))
+  with _ -> None
+
+let remove s (id : 'a field) =
+  Int.Map.remove id s
+
+let merge s1 s2 =
+  Int.Map.fold Int.Map.add s1 s2
+
+let field () = next ()
+
+end
diff --git a/lib/store.mli b/lib/store.mli
index 5df0c99a76..8eab314ed7 100644
--- a/lib/store.mli
+++ b/lib/store.mli
@@ -9,17 +9,38 @@
 (*** This module implements an "untyped store", in this particular case we
         see it as an extensible record whose fields are left unspecified. ***)
 
-type t
-
-module Field : sig
-  type 'a field = {
-    set : 'a -> t -> t ;
-    get : t -> 'a option ;
-    remove : t -> t 
-  }
-  type 'a t = 'a field
+module type T =
+sig
+(** FIXME: Waiting for first-class modules... *)
 end
 
-val empty : t
+module type S =
+sig
+  type t
+  (** Type of stores *)
 
-val field : unit -> 'a Field.field
+  type 'a field
+  (** Type of field of such stores *)
+
+  val empty : t
+  (** Empty store *)
+
+  val set : t -> 'a field -> 'a -> t
+  (** Set a field *)
+
+  val get : t -> 'a field -> 'a option
+  (** Get the value of a field, if any *)
+
+  val remove : t -> 'a field -> t
+  (** Unset the value of the field *)
+
+  val merge : t -> t -> t
+  (** [merge s1 s2] adds all the fields of [s1] into [s2]. *)
+
+  val field : unit -> 'a field
+  (** Create a new field *)
+
+end
+
+module Make (M : T) : S
+(** Create a new store type. *)