jon.recoil.org

Module Pair.Map

type !+'a t

union_sharing f m1 m2 is a version of union f m1 m2 that maximizes sharing of the result with m1.

union_shared f m1 m2 is a version of union_sharing f m1 m2 that also exploits sharing of m1 and m2 to avoid calling f when possible, assuming that f x x = Some x for all xs.

diff f m1 m2 computes a map whose keys are a subset of the keys of m1. When a binding is defined in both m1 and m2, the function f is used to combine them. Bindings that are only present in m1 are preserved. This is a special case of merge: diff f m1 m2 is equivalent to merge f' m1 m2, where

  • f' _key None _ = None
  • f' _key (Some v) None = Some v
  • f' key (Some v1) (Some v2) = f key v1 v2

diff_shared f m1 m2 is a version of diff_sharing f m1 m2 that further exploits sharing of m1 and m2 to avoid calling f when possible, assuming that f x x always returns None.