Module type Prime_enummap.S

The type of the keys of the map.

The type of the map.

The empty map.

singleton k e is the one-element map binding k to e.

Holds for the empty map only.

cardinal m is the cardinality of m.

mem k m is true iff m has a binding for k.

app m is the partial function corresponding to m. This is the same as find except for the argument ordering and that it does not raise any exception.

find k m returns the binding for k in m or raises Not_found if it is unbound.

locate k m is a pair (present, pos) where present is true iff k is bound in m and pos is the number of keys of m preceding k.

get i m is the ith value of m.

raises Invalid_argument

if the index is out of bounds.

get_binding m i is the ith binding of m according to the key order.

min_binding m is the binding of m with the smallest key.

max_binding m is the binding of m with the largest key.

pred_binding m k is the last binding strictly before k in m.

succ_binding m k is the first binding strictly after k in m.

add k e m is the map which agrees with m on all keys except that k is mapped to e.

pop k m is Some (k, remove k m) if m binds k to e, otherwise None.

pop_min m is the tuple (k, e, m') where (k, e) is the binding of m with the minimal key and m' is the remainder of m.

pop_max m is the tuple (k, e, m') where (k, e) is the binding of m with the maximum key and m' is the remainder of m.

remove k m is the map which agrees with m on all keys except that k is unbound. If k is unbound in m, then remove k m is m.

update k f m is the map m with k rebound to f v where v is the current binding of k in m and None means no binding for both argument and result.

cut_binding k m is (e_opt, sL, sR) where e_opt is the element bound to k, if any, and sL and sR are the submaps of m with keys smaller or langer than k, respectively.

A (key, element) pair for each binding of the map in key order.

Assuming bindings is a key-ordered list of bindings, as returned from bindings, of_ordered_bindings bindings is a map containing precisely those bindings, computed in linear time. This is an optimisation of List.fold (uncurry add) bindings empty.

raises Invalid_argument

of bindings is not sorted.

asc_bindings ?where m is the sequence of bindings of e in order of increasing keys, optionally restricted to keys in a subrange given by where.

parameter where

must be monotonically increasing, in which case the returned bindings will be the continuous range with keys at which this function evaluates to zero.

dsc_bindings ?where m is the sequence of bindings of m in order of decreasing keys, optionally restricted to keys in a subrange given by where.

parameter where

must be monotonically increasing, in which case the returned bindings will be the continuous range with keys at which this function evaluates to zero.

search f m is the first f k e for k ↦ e in m which is different from None, or None if no such mapping exists in m.

fold f m is the composition of f k e for each (k, e) in m, applied in order of increasing keys.

fold_rev f m is the composition of f k e for each (k, e) in m applied in order of decreasing keys.

iter f m calls f k e for each (k, e) in m in order of increasing keys.

for_all f m is true iff f k e is true for all bindings (k, e) of m.

exists f m is true iff f k e for some binding (k, e) of m.

map f m is the minimal map which for each (k, e) of m contains (k, f e).

mapi f m is the minimal map which for each (k, e) of m contains (k, f k e).

fmapi f m is the minimal map which contains (k, e) iff f k e' = Some e for some (k, e') in m.

filter f m is the maximal submap of m such that f k e holds for each binding (k, e).

compare f is a total order over maps using f to compare elements.

equal f m0 m1 is true iff m0 and m1 have the same keys and f is true on the respective mappings for each key.

merge f m1 m2 is the map containing a binding (k, e) for each k bound in at least one of the maps, such that f (find k m1) (find k m2) = Some e.

finter f m1 m2 is the minimal map which for each shared key k of m1 and m2 contains (k, e) if f k m1 m2 = Some e for some e.

funion f m1 m2 is the minimal map which contains all bindings of finter f m1 m2 and all bindings of m1 and m2 whose key does not occur in the other map.

fcompl f m1 m2 is the minimal map which contains the bindings of finter f m1 m2 and the bindings of m2 with the key not in m1.

fpatch f m1 m2 is the minimal map which contains the bindings of m2 having keys disjoint from m1, and which contains (k, e) iff (k, e') is in m1 and f k e' (find k m2) = Some e.

split_union mA mB is a triple (mA', mB', mC') where mA' and mB' are the respective bindings of mA and mB which have disjoint keys, and mC' has a binding (k, f k a b) for each pair of bindings (k, a) of mA and (k, b) of mB sharing k.