aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cMap.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-01-25 19:25:34 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-01-25 19:25:34 +0100
commit92fda8598da9221bc24deb8b5636233b77d9c45b (patch)
tree4e89eab6dbe1dbb53e12d89dd498d96e157a1168 /lib/cMap.mli
parent8434840413d7cef32ed83539a0c7ef4de13ec528 (diff)
Equipping extended maps with fold operator defined for any monad.
Diffstat (limited to 'lib/cMap.mli')
-rw-r--r--lib/cMap.mli15
1 files changed, 15 insertions, 0 deletions
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 23d3801e0..cd3d2f5b1 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -14,6 +14,13 @@ sig
val compare : t -> t -> int
end
+module type MonadS =
+sig
+ type +'a t
+ val return : 'a -> 'a t
+ val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
module type S = Map.S
module type ExtS =
@@ -59,6 +66,14 @@ sig
i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *)
end
+ module Monad(M : MonadS) :
+ sig
+ val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ end
+ (** Fold operators parameterized by any monad. *)
+
end
module Make(M : Map.OrderedType) : ExtS with