summaryrefslogtreecommitdiff
path: root/lib/store.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /lib/store.mli
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/store.mli')
-rw-r--r--lib/store.mli43
1 files changed, 32 insertions, 11 deletions
diff --git a/lib/store.mli b/lib/store.mli
index 5df0c99a..8eab314e 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. *)