diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /lib/store.mli | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/store.mli')
-rw-r--r-- | lib/store.mli | 43 |
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. *) |