aboutsummaryrefslogtreecommitdiff
path: root/clib
diff options
context:
space:
mode:
Diffstat (limited to 'clib')
-rw-r--r--clib/cSig.mli2
-rw-r--r--clib/hMap.ml8
2 files changed, 10 insertions, 0 deletions
diff --git a/clib/cSig.mli b/clib/cSig.mli
index 859018ca4b..0012bcef17 100644
--- a/clib/cSig.mli
+++ b/clib/cSig.mli
@@ -68,6 +68,8 @@ sig
val remove: key -> 'a t -> 'a t
val merge:
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+ val union:
+ (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter: (key -> 'a -> unit) -> 'a t -> unit
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 09ffb39c21..db59ef47b0 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -290,6 +290,14 @@ struct
in
Int.Map.merge fm s1 s2
+ let union f s1 s2 =
+ let fm h m1 m2 =
+ let m = Map.union f m1 m2 in
+ if Map.is_empty m then None
+ else Some m
+ in
+ Int.Map.union fm s1 s2
+
let compare f s1 s2 =
let fc m1 m2 = Map.compare f m1 m2 in
Int.Map.compare fc s1 s2