A binding (x, v) is a pair of a key x and a value v.
type'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.
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.
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.
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.
val update : key->('a option->'a option)->'at->'at
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.
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.
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.
val union : (key->'a->'a->'a option)->'amap->'amap->'amap
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.
val inter : (key->'a->'b->'c option)->'amap->'bmap->'cmap
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.
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.
val merge :
(key->'a option->'b option->'c option)->'amap->'bmap->'cmap
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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).
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).
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.
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.
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.
val find_first_opt : (key-> bool)->'amap->'abinding 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.
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.
val find_last_opt : (key-> bool)->'amap->'abinding 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.
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.
val filter_map : (key->'a->'b option)->'amap->'bmap
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.
val partition : (key->'a-> bool)->'amap->'amap * 'amap
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.
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.
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.
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.