Make (p.baby.20241204.doc.baby.Baby.H.Map.Make)

Parameters

module E : OrderedType

Signature

Sourcetype key = E.t

The type of keys.

Sourcetype 'a binding = key * 'a

A binding (x, v) is a pair of a key x and a value v.

Sourcetype 'a map

The abstract type of maps. A map is an immutable data structure.

A map, also known as a dictionary, represents a finite mapping of keys to values. It can also be thought of as a set of bindings, with the property that each key appears in at most one binding.

The parameter 'a is the type of the values.

Sourcetype 'a t = 'a map

A synonym for the type map.

In the following, we document the behavior of each operation only in the case where the relation $\leq$ is a total order. (To find out what this means, see OrderedType.compare.)

Some operations are higher-order functions: they expect a function f as an argument. Examples of higher-order functions include iter, fold, and map. When we document the time complexity of a higher-order function, we discount the cost of the calls to f.

Constructing maps

Sourceval empty : 'a map

empty is the empty map.

Sourceval singleton : key -> 'a -> 'a map

singleton x v returns a map whose sole binding is (x, v).

Sourceval add : key -> 'a -> 'a map -> 'a map

add x v m returns a map that contains all of the bindings of the map m plus the binding (x, v). If for some value v' a binding (x, v') was already present in the map m then it is replaced with the binding (x, v). If furthermore v' and v are physically equal then the map m is returned.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval remove : key -> 'a map -> 'a map

remove x m returns a map that contains all of the bindings of the map m, except any binding for the key x.

If the result is logically equal to m, then the result is physically equal to m.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval update : key -> ('a option -> 'a option) -> 'a t -> 'a t

update x f m returns a map m' that agrees with the map m at every key except at the key x, whose presence and value in the map are transformed by the function f. The map m' is characterized by the following two equations:

find_opt x m' = f (find_opt x m)
at every key y other than x, find_opt y m' = find_opt y m.

update x f m invokes the function f exactly once. If the result of this invocation of f is physically equal to its argument, then m' is physically equal to m.

Sourceval add_to_list : key -> 'a -> 'a list map -> 'a list map

add_to_list x v m returns a map m' that agrees with the map m at every key except at the key x, where the value x is pushed in front of the list that was previously associated with x. The map m' is characterized by the following three equations:

find_opt x m' = Some [v] if find_opt x m is None,
find_opt x m' = Some (v :: vs) if find_opt x m is Some vs,
at every key y other than x, find_opt y m' = find_opt y m.

Sourceval remove_min_binding : 'a map -> 'a map

If the map m is nonempty, then remove_min_binding m returns the map m, deprived of its minimum binding. Otherwise, it raises Not_found.

It is equivalent to remove (fst (min_binding m)) m.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval remove_max_binding : 'a map -> 'a map

If the map m is nonempty, then remove_max_binding m returns the map m, deprived of its maximum binding. Otherwise, it raises Not_found.

It is equivalent to remove (fst (max_binding m)) m.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval union : (key -> 'a -> 'a -> 'a option) -> 'a map -> 'a map -> 'a map

union f m1 m2 returns a map m that is a form of union of the maps m1 and m2. This map is defined as follows:

if a key x is present in the map m1 with value v1 and present in the map m2 with value v2, then its absence or presence (and value) in the map m are determined by the result of the function call f x v1 v2, whose type is 'a option.
if a key x is absent in one map then its absence or presence (and value) in the map m are determined by the other map.

union is a special case of merge. Indeed, union f m1 m2 is logically equal to merge f' m1 m2, where f' is defined as follows:

f' _ None None = None
f' _ (Some v) None = Some v
f' _ None (Some v) = Some v
f' x (Some v1) (Some v2) = f x v1 v2

Time complexity: $O(m.\log (\frac{n}{m}))$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Sourceval inter : (key -> 'a -> 'b -> 'c option) -> 'a map -> 'b map -> 'c map

inter f m1 m2 returns a map m that is a form of intersection of the maps m1 and m2. This map is defined as follows:

if a key x is present in the map m1 with value v1 and present in the map m2 with value v2, then its absence or presence (and value) in the map m are determined by the result of the function call f x v1 v2, whose type is 'a option.
if a key x is absent in m1 or in m2 then it is absent in the map m.

inter is a special case of merge. Indeed, inter f m1 m2 is logically equal to merge f' m1 m2, where f' is defined as follows:

f' x (Some v1) (Some v2) = f x v1 v2
f' _ _ _ = None

Time complexity: $O(m.\log (\frac{n}{m}))$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Sourceval diff : 'a map -> 'b map -> 'a map

diff m1 m2 returns the difference of the maps m1 and m2, that is, the restriction of the map m1 to the complement of the domain of the map m2.

If the result is logically equal to m1, then the result is physically equal to m1.

diff is a special case of merge. Indeed, diff m1 m2 is logically equal to merge f m1 m2, where f is defined as follows:

f _ od1 None = od1
f _ od1 (Some _) = None

Time complexity: $O(m.\log (\frac{n}{m}))$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Sourceval xor : 'a map -> 'a map -> 'a map

xor m1 m2 returns the symmetric difference of the maps m1 and m2, that is, a map that contains the bindings of the map m1 whose keys do not appear in the map m2 and the bindings of the set m2 whose keys do not appear in the map m1.

xor is a special case of merge. Indeed, xor m1 m2 is logically equal to merge f m1 m2, where f is defined as follows:

f _ (Some v1) None = Some v1
f _ None (Some v2) = Some v2
f _ (Some _) (Some _) = None
f None None = None

Time complexity: $O(m.\log (\frac{n}{m}))$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Source

val merge : 
  (key -> 'a option -> 'b option -> 'c option) ->
  'a map ->
  'b map ->
  'c map

merge f m1 m2 returns a map m that is computed based on the maps m1 and m2. Assuming that the equation f None None = None holds, the map m is characterized by the following equation: for every key x, find_opt x m = f x (find_opt x m1) (find_opt x m2) holds.

In other words, the presence and value of each key x in the map m are determined by the result of applying f to the key x and to the presence and value of the key x in the maps m1 and m2.

Time complexity: $O(n.\log (n))$ , where $n$ is the size of the larger map.

Sourceval split : key -> 'a map -> 'a map * 'a option * 'a map

split x m returns a triple (l, data, r), where the map l contains the bindings of m whose key is less than x, the map r contains the bindings of m whose key is greater than x, data is Some v if m contains the binding (x, v), and data is None if m contains no binding for the key x.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Querying maps

Sourceval is_empty : 'a map -> bool

is_empty m determines whether the map m is empty.

Time complexity: $O(1)$ .

Sourceval min_binding : 'a map -> 'a binding

If the map m is nonempty, min_binding m returns the minimum binding of this map, that is, the binding whose key is minimal. Otherwise, it raises Not_found.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval min_binding_opt : 'a map -> 'a binding option

If the map m is nonempty, min_binding_opt s returns Some b, where b is the minimum binding of this map, that is, the binding whose key is minimal. Otherwise, it returns None.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval max_binding : 'a map -> 'a binding

If the map m is nonempty, max_binding m returns the maximum binding of this map, that is, the binding whose key is maximal. Otherwise, it raises Not_found.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval max_binding_opt : 'a map -> 'a binding option

If the map m is nonempty, max_binding_opt s returns Some b, where b is the maximum binding of this map, that is, the binding whose key is maximal. Otherwise, it returns None.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval choose : 'a map -> 'a binding

If the map m is nonempty, choose m returns an arbitrary binding of this map. Otherwise, it raises Not_found.

choose respects equality: if the maps m1 and m2 are equal then choose m1 and choose m2 are equal.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval choose_opt : 'a map -> 'a binding option

If the map m is nonempty, choose_opt s returns Some b, where b is an arbitrary binding of this map. Otherwise, it returns None.

choose_opt respects equality: if the maps m1 and m2 are equal then choose_opt m1 and choose_opt m2 are equal.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval mem : key -> 'a map -> bool

mem x m determines whether the map m contains a binding for the key x.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval find : key -> 'a map -> 'a

If the map m contains a binding (x, v) then find x m returns v. Otherwise, it raises Not_found.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval find_opt : key -> 'a map -> 'a option

If the map m contains a binding (x, v) then find_opt x m returns Some v. Otherwise, it returns None.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval disjoint : 'a map -> 'b map -> bool

disjoint m1 m2 determines whether the maps m1 and m2 are disjoint, that is, whether the intersection of their domains is empty.

Time complexity: $O(m.\log (\frac{n}{m}))$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Sourceval sub : ('a -> 'b -> bool) -> 'a map -> 'b map -> bool

If leq is a preorder on values, then sub leq is a preorder on maps.

sub leq m1 m2 is true if, for every binding (x, v1) in the map m1, there exists a binding (x, v2) in the map m2 and leq v1 v2 is true.

Time complexity: $O(m)$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Sourceval equal : ('a -> 'b -> bool) -> 'a map -> 'b map -> bool

If eq is an equality test over values, then equal eq is an equality test over maps.

Time complexity: $O(m)$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Sourceval compare : ('a -> 'b -> int) -> 'a map -> 'b map -> int

If cmp is a total ordering function over values of type 'a, then compare cmp is a total ordering function over maps. (Which specific ordering is used is unspecified.)

Time complexity: $O(m)$ , where $m$ is the size of the smaller map and $n$ is the size of the larger map.

Sourceval cardinal : 'a map -> int

cardinal m returns the cardinal of the map m, that is, the number of its bindings.

Time complexity: in the weight-balanced-tree implementation (Baby.W), $O(1)$ ; in the height-balanced-tree implementation (Baby.H), $O(n)$ , where $n$ is the size of the map m.

Conversions to and from maps

Sourceval of_list : 'a binding list -> 'a map

of_list bs constructs a map whose bindings are the elements of the list bs.

The list is read from left to right. If two bindings have the same key, then the rightmost binding (the one that is read last) takes precedence.

This function has adaptive time complexity. In the worst case, its complexity is $O(n.\log n)$ , where $n$ is the length of the list bs. However, if the list bs is sorted, then its complexity is only $O(n)$ . In between these extremes, its complexity degrades gracefully.

Sourceval to_list : 'a map -> 'a binding list

to_list m constructs a list whose elements are the bindings of the map m, in increasing order.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval bindings : 'a map -> 'a binding list

bindings is a synonym for to_list.

Sourceval of_array : 'a binding array -> 'a map

of_array bs constructs a map whose bindings are the elements of the array bs.

The array is read from left to right. If two bindings have the same key, then the rightmost binding (the one that is read last) takes precedence.

This function has adaptive time complexity. In the worst case, its complexity is $O(n.\log n)$ , where $n$ is the length of the array bs. However, if the array bs is sorted, then its complexity is only $O(n)$ . In between these extremes, its complexity degrades gracefully.

Sourceval to_array : 'a map -> 'a binding array

to_array m constructs an array whose elements are the bindings of the map m, in increasing order.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval of_seq : 'a binding Seq.t -> 'a map

of_seq bs constructs a map whose elements are the bindings of the sequence bs. (The whole sequence is immediately consumed.)

The sequence is read from left to right. If two bindings have the same key, then the rightmost binding (the one that is read last) takes precedence.

This function has adaptive time complexity. In the worst case, its complexity is $O(n.\log n)$ , where $n$ is the length of the sequence bs. However, if the sequence bs is sorted, then its complexity is only $O(n)$ . In between these extremes, its complexity degrades gracefully.

Sourceval add_seq : 'a binding Seq.t -> 'a map -> 'a map

add_seq bs m extends the map m with the elements of the sequence bs.

It is equivalent to union (fun _ _ v -> v) m (of_seq bs).

Its time complexity is the combined time complexity of of_seq and union.

Sourceval to_seq : 'a map -> 'a binding Seq.t

to_seq m constructs a (persistent) increasing sequence whose elements are the bindings of the map m.

The time complexity of consuming the entire sequence is $O(n)$ , where $n$ is the size of the map m. The worst-case time complexity of demanding one element is $O(\log n)$ .

Sourceval to_seq_from : key -> 'a map -> 'a binding Seq.t

to_seq_from x m constructs a (persistent) increasing sequence whose elements are the bindings of the map m whose key is greater than or equal to x.

The time complexity of consuming the entire sequence is $O(n)$ , where $n$ is the size of the map m. The time complexity of demanding one element is $O(\log n)$ .

Sourceval to_rev_seq : 'a map -> 'a binding Seq.t

to_rev_seq m constructs a (persistent) decreasing sequence whose elements are the bindings of the map m.

The time complexity of consuming the entire sequence is $O(n)$ , where $n$ is the size of the map m. The time complexity of demanding one element is $O(\log n)$ .

Iterating, searching, transforming maps

Sourceval iter : (key -> 'a -> unit) -> 'a map -> unit

iter consume m produces an increasing sequence whose elements are the bindings of the map m. The function consume is applied in turn to each binding in the sequence. For each binding (x, v), the key x and the value v form two separate arguments to consume.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval fold : (key -> 'a -> 's -> 's) -> 'a map -> 's -> 's

fold consume m init produces an increasing sequence whose elements are the bindings of the map m. The function consume is applied in turn to each binding in the sequence. For each binding (x, v), the key x and the value v form two separate arguments to consume.

A current state is threaded through this sequence of function invocations; each call to consume receives a current state s and produces an updated state s'. The initial value of the state is init. The final value of the state is returned by fold.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval for_all : (key -> 'a -> bool) -> 'a map -> bool

for_all p m tests whether all bindings (x, v) in the map m satisfy p x v = true.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval exists : (key -> 'a -> bool) -> 'a map -> bool

exists p m tests whether at least one binding (x, v) in the map m satisfies p x v = true.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval find_first : (key -> bool) -> 'a map -> 'a binding

find_first f m requires the function f to be a monotonically increasing function of keys to Boolean values. It returns the least binding (x, v) of the map m such that f x is true, if there is such a binding. If there is none, it raises Not_found.

In other words, when the bindings of the map are enumerated as an increasing sequence, find_first f m returns the first binding that follows the threshold of the function f.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval find_first_opt : (key -> bool) -> 'a map -> 'a binding option

find_first_opt f m requires the function f to be a monotonically increasing function of keys to Boolean values. It returns Some (x, v), where (x, v) is the least binding of the map m such that f x is true, if there is such a binding. If there is none, it returns None.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval find_last : (key -> bool) -> 'a map -> 'a binding

find_last f m requires the function f to be a monotonically decreasing function of keys to Boolean values. It returns the greatest binding (x, v) of the map m such that f x is true, if there is such a binding. If there is none, it raises Not_found.

In other words, when the bindings of the map are enumerated as an increasing sequence, find_last f m returns the last binding that precedes the threshold of the function f.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval find_last_opt : (key -> bool) -> 'a map -> 'a binding option

find_last_opt f m requires the function f to be a monotonically decreasing function of keys to Boolean values. It returns Some (x, v), where (x, v) is the greatest binding of the map m such that f x is true, if there is such a binding. If there is none, it raises Not_found.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval map : ('a -> 'b) -> 'a map -> 'b map

map f m computes the image m' of the map m through the function f.

For every binding (x, v) in the map m, there is a binding (x, f v) in the map m'.

The bindings are passed to the function f in increasing order.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval mapi : (key -> 'a -> 'b) -> 'a map -> 'b map

mapi f m computes the image m' of the map m through the function f.

For every binding (x, v) in the map m, there is a binding (x, f x v) in the map m'.

The bindings are passed to the function f in increasing order of keys.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval filter : (key -> 'a -> bool) -> 'a map -> 'a map

filter p m returns a map m' that contains the bindings of x to v in the map m such that p x v is true.

If, for every binding (x, v) in the map m, p x v is true, then the result of filter p m is physically equal to m.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval filter_map : (key -> 'a -> 'b option) -> 'a map -> 'b map

filter_map f m computes the image m' of the map m through the function f.

For every binding (x, v) in the map m, if f x v is Some v', then the binding (x, v') is in the map m'.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Sourceval partition : (key -> 'a -> bool) -> 'a map -> 'a map * 'a map

partition p m returns a pair (m1, m2), where the map m1 contains the bindings of x to v in the map m such that p x v is true, and the map m2 contains the bindings of x to v in the map m such that p x v is false.

Time complexity: $O(n)$ , where $n$ is the size of the map m.

Random access

Caution: the following functions exist only in the weight-balanced-tree implementation (Baby.W). In the height-balanced tree implementation (Baby.H), they raise an exception of the form Failure _.

In the following descriptions, a map is viewed as an increasing sequence of bindings. Thus, the index of a binding is its index in the sequence. The valid indices in a map m are the integers in the semi-open interval of 0 to cardinal m.

Sourceval get : 'a map -> int -> 'a binding

get m i requires 0 <= i && i < cardinal m. It returns the binding that lies at index i in the map m.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval index : key -> 'a map -> int

If the key x exists in the map m, then index x m returns the index i where a binding for this key lies in the map m. (Thus, get m i is (x, v), where v is find x m.) Otherwise, it raises Not_found.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval cut : 'a map -> int -> 'a map * 'a map

cut m i requires 0 <= i && i <= cardinal m. It returns a pair (m1, m2), where the map m1 contains the bindings of m whose index is less than i and the map m2 contains the bindings of m whose index is greater than or equal to i.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Sourceval cut_and_get : 'a map -> int -> 'a map * 'a binding * 'a map

cut_and_get m i requires 0 <= i && i < cardinal m. It returns a triple (m1, b, m2), where the map m1 contains the bindings of m whose index is less than i, the binding b is get m i, and the map m2 contains the bindings of m whose index is greater than i.

Time complexity: $O(\log n)$ , where $n$ is the size of the map m.

Enumerations

Sourcemodule Enum : sig ... end

The submodule Enum offers an abstract data type of enumerations, which allow efficient iteration over a map.