Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.Sign up
Original bug ID: 6449
There is a generic merge operation in the Map functor:
A more optimized implementation is possible when the merge function is such that:
merge k (Some x1) None == x1
for some function f.
val union: (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t (** [union f m1 m2] computes a map whose keys is the union of keys of [m1] and of [m2]. When the same binding is defined in both arguments, the function is used to combine them. *) ... let rec union f s1 s2 = match (s1, s2) with | (Empty, s) | (s, Empty) -> s | (Node (l1, v1, d1, r1, h1), Node (l2, v2, d2, r2, h2)) -> if h1 >= h2 then let (l2, d2, r2) = split v1 s2 in let l = union f l1 l2 and r = union f r1 r2 in let d = match d2 with | None -> d1 | Some d2 -> f v1 d1 d2 in join l v1 d r else let (l1, d1, r1) = split v2 s1 in let l = union f l1 l2 and r = union f r1 r2 in let d = match d1 with | None -> d2 | Some d1 -> f v2 d1 d2 in join l v2 d r
Contrary to [merge], this [union] function does not need to traverse an operand when the other one is empty.
Any opposition to including this function?