Library
Module
Module type
Parameter
Class
Class type
module E : OrderedType
type elt = E.t
The type of elements.
type t = set
A synonym for the type set
.
val empty : set
empty
is the empty set.
add x s
returns a set that contains all elements of the set s
, plus x
. Thus, it is logically equal to union (singleton x) s
.
If the result is logically equal to s
, then the result is physically equal to s
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
remove x s
returns a set that contains all elements of the set s
, except x
. It is equivalent to diff s (singleton x)
.
If the result is logically equal to s
, then the result is physically equal to s
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If the set s
is nonempty, then remove_min_elt s
returns the set s
, deprived of its minimum element. Otherwise, it raises Not_found
.
It is equivalent to remove (min_elt s) s
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If the set s
is nonempty, then remove_max_elt s
returns the set s
, deprived of its maximum element. Otherwise, it raises Not_found
.
It is equivalent to remove (max_elt s) s
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
union s1 s2
returns the union of the sets s1
and s2
, that is, a set that contains all elements of the set s1
and all elements of the set s2
.
The weight-balanced-tree implementation (Baby.W
) offers the following guarantee: if the result is logically equal to s1
or to s2
, then the result is physically equal to s1
or to s2
. The height-balanced tree implementation (Baby.H
) does not offer this guarantee.
Time complexity: O(m.\log (\frac{n}{m}))
, where m
is the size of the smaller set and n
is the size of the larger set.
inter s1 s2
returns the intersection of the sets s1
and s2
, that is, a set that contains the common elements of the sets s1
and s2
.
The weight-balanced-tree implementation (Baby.W
) offers the following guarantee: if the result is logically equal to s1
or to s2
, then the result is physically equal to s1
or to s2
. The height-balanced tree implementation (Baby.H
) does not offer this guarantee.
Time complexity: O(m.\log (\frac{n}{m}))
, where m
is the size of the smaller set and n
is the size of the larger set.
diff s1 s2
returns the difference of the sets s1
and s2
, that is, a set that contains the elements of the set s1
that do not appear in the set s2
.
if the result is logically equal to s1
, then the result is physically equal to s1
.
Time complexity: O(m.\log (\frac{n}{m}))
, where m
is the size of the smaller set and n
is the size of the larger set.
xor s1 s2
returns the symmetric difference of the sets s1
and s2
, that is, a set that contains the elements of the set s1
that do not appear in the set s2
and the elements of the set s2
that do not appear in the set s1
.
Time complexity: O(m.\log (\frac{n}{m}))
, where m
is the size of the smaller set and n
is the size of the larger set.
split x s
returns a triple (l, present, r)
, where l
is the set of the elements of s
that are strictly less than x
, r
is the set of the elements of s
that are strictly greater than x
, and present
is true
if and only if x
is a member of the set s
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
val is_empty : set -> bool
is_empty s
determines whether the set s
is the empty set.
Time complexity: O(1)
.
If the set s
is nonempty, min_elt s
returns the minimum element of this set. Otherwise, it raises Not_found
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If the set s
is nonempty, min_elt_opt s
returns Some x
, where x
is the minimum element of this set. Otherwise, it returns None
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If the set s
is nonempty, max_elt s
returns the maximum element of this set. Otherwise, it raises Not_found
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If the set s
is nonempty, max_elt_opt s
returns Some x
, where x
is the maximum element of this set. Otherwise, it returns None
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If the set s
is nonempty, choose s
returns an arbitrary element of this set. Otherwise, it raises Not_found
.
choose
respects equality: if the sets s1
and s2
are equal then choose s1
and choose s2
are equal.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If the set s
is nonempty, choose_opt s
returns Some x
, where x
is an arbitrary element of this set. Otherwise, it returns None
.
choose_opt
respects equality: if the sets s1
and s2
are equal then choose_opt s1
and choose_opt s2
are equal.
Time complexity: O(\log n)
, where n
is the size of the set s
.
mem x s
determines whether the element x
is a member of the set s
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If x
is a member of the set s
, then find x s
returns the unique element x'
of the set s
such that x
and x'
are equivalent. (We say that x
and x'
are equivalent if compare x x' = 0
holds.) Otherwise, it raises Not_found
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If x
is a member of the set s
, then find_opt x s
returns Some x'
, where x'
is the unique element of the set s
such that x
and x'
are equivalent. (We say that x
and x'
are equivalent if compare x x' = 0
holds.) Otherwise, it returns None
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
disjoint s1 s2
determines whether the sets s1
and s2
are disjoint, that is, whether their intersection is empty. It is equivalent to is_empty (inter s1 s2)
.
Time complexity: O(m.\log (\frac{n}{m}))
, where m
is the size of the smaller set and n
is the size of the larger set.
subset s1 s2
determines whether the set s1
is a subset of the set s2
, that is, whether their difference is empty. It is equivalent to is_empty (diff s1 s2)
.
Time complexity: O(m.\log (\frac{n}{m}))
, where m
is the size of the smaller set and n
is the size of the larger set.
equal s1 s2
determines whether the sets s1
and s2
are equal, that is, whether their symmetric difference is empty. It is equivalent to is_empty (xor s1 s2)
.
Time complexity: O(m)
, where m
is the size of the smaller set and n
is the size of the larger set.
compare
is a total ordering function over sets. (Which specific ordering is used is unspecified.)
Time complexity: O(m)
, where m
is the size of the smaller set and n
is the size of the larger set.
val cardinal : set -> int
of_list xs
constructs a set whose elements are the elements of the list xs
.
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 xs
. However, if the list xs
is sorted, then its complexity is only O(n)
. In between these extremes, its complexity degrades gracefully.
to_list s
constructs a list whose elements are the elements of the set s
, in increasing order.
Time complexity: O(n)
, where n
is the size of the set s
.
of_array xs
constructs a set whose elements are the elements of the array xs
.
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 xs
. However, if the array xs
is sorted, then its complexity is only O(n)
. In between these extremes, its complexity degrades gracefully.
to_array s
constructs an array whose elements are the elements of the set s
, in increasing order.
Time complexity: O(n)
, where n
is the size of the set s
.
of_seq xs
constructs a set whose elements are the elements of the sequence xs
. (The whole sequence is immediately consumed.)
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 xs
. However, if the sequence xs
is sorted, then its complexity is only O(n)
. In between these extremes, its complexity degrades gracefully.
add_seq xs s
constructs a set whose elements are the elements of the sequence xs
and the elements of the set s
.
It is equivalent to union (of_seq xs) s
.
Its time complexity is the combined time complexity of of_seq
and union
.
to_seq s
constructs a (persistent) increasing sequence whose elements are the elements of the set s
.
The time complexity of consuming the entire sequence is O(n)
, where n
is the size of the set s
. The worst-case time complexity of demanding one element is O(\log n)
.
to_seq_from x s
constructs a (persistent) increasing sequence whose elements are the elements of the set s
that are greater than or equal to x
.
The time complexity of consuming the entire sequence is O(n)
, where n
is the size of the set s
. The time complexity of demanding one element is O(\log n)
.
to_rev_seq s
constructs a (persistent) decreasing sequence whose elements are the elements of the set s
.
The time complexity of consuming the entire sequence is O(n)
, where n
is the size of the set s
. The time complexity of demanding one element is O(\log n)
.
iter yield s
produces an increasing sequence whose elements are the elements of the set s
.
This is achieved by applying the function yield
in turn to each element of the sequence.
Time complexity: O(n)
, where n
is the size of the set s
.
fold yield s accu
produces an increasing sequence whose elements are the elements of the set s
.
This is achieved by applying the function yield
in turn to each element of the sequence. An accumulator, whose initial value is accu
, is threaded through this sequence of function invocations.
Time complexity: O(n)
, where n
is the size of the set s
.
for_all p s
tests whether all elements x
of the set s
satisfy p x = true
.
Time complexity: O(n)
, where n
is the size of the set s
.
exists p s
tests whether at least one element x
of the set s
satisfies p x = true
.
Time complexity: O(n)
, where n
is the size of the set s
.
find_first f s
requires the function f
to be a monotonically increasing function of elements to Boolean values. It returns the least element x
of the set s
such that f x
is true
, if there is such an element. If there is none, it raises Not_found
.
In other words, when the elements of the set are enumerated as an increasing sequence, find_first f s
returns the first element of the sequence that follows the threshold of the function f
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
find_first_opt f s
requires the function f
to be a monotonically increasing function of elements to Boolean values. It returns Some x
, where x
is the least element of the set s
such that f x
is true
, if there is such an element. If there is none, it returns None
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
find_last f s
requires the function f
to be a monotonically decreasing function of elements to Boolean values. It returns the greatest element x
of the set s
such that f x
is true
, if there is such an element. If there is none, it raises Not_found
.
In other words, when the elements of the set are enumerated as an increasing sequence, find_last f s
returns the last element of the sequence that precedes the threshold of the function f
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
find_last_opt f s
requires the function f
to be a monotonically decreasing function of elements to Boolean values. It returns Some x
, where x
is the greatest element of the set s
such that f x
is true
, if there is such an element. If there is none, it returns None
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
map f s
computes the image of the set s
through the function f
, that is, in mathematical notation, the set \{ y \mid y = f(x) \wedge x \in s \}
.
If, for every element x
of the set s
, f x
is x
, then the result is physically equal to s
.
If the function f
is monotonically increasing, then the time complexity is O(n)
, where n
is the size of the set s
; otherwise, it is O(n.\log n)
.
filter p s
returns the set of the elements x
of the set s
such that p x
is true
.
If, for every element x
of the set s
, p x
is true
, then the result of filter p s
is physically equal to s
.
Time complexity: O(n)
, where n
is the size of the set s
.
filter_map f s
computes the set \{ y \mid \mathit{Some}\; y = f(x) \wedge x \in s \}
.
If, for every element x
of the set s
, f x
is Some x
, then the result is physically equal to s
.
If the function f
(restricted to the elements that it retains) is monotonically increasing, then the time complexity is O(n)
, where n
is the size of the set s
; otherwise, it is O(n.\log n)
.
partition p s
returns a pair (s1, s2)
, where s1
is the set of the elements x
of s
such that p x
is true
, and s2
is the set of the elements of s
such that p x
is false
.
Time complexity: O(n)
, where n
is the size of the set s
.
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 set is viewed as an increasing sequence of elements. Thus, the index of an element is its index in the sequence. The valid indices in a set s
are the integers in the semi-open interval of 0
to cardinal s
.
get s i
requires 0 <= i && i < cardinal s
. It returns the element that lies at index i
in the set s
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
If x
is a member of the set s
, then index x s
returns the index i
where this element lies in the set s
. (Thus, get s i
is x
.) Otherwise, it raises Not_found
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
cut s i
requires 0 <= i && i <= cardinal s
. It returns a pair (s1, s2)
, where s1
is the set of the elements of s
whose index is less than i
, and s2
is the set of the elements of s
whose index is greater than or equal to i
.
Time complexity: O(\log n)
, where n
is the size of the set s
.
cut_and_get s i
requires 0 <= i && i < cardinal s
. It returns a triple (s1, x, s2)
, where s1
is the set of the elements of s
whose index is less than i
, x
is the element of s
at index i
, and s2
is the set of the elements of s
whose index is greater than i
.
Time complexity: O(\log n)
, where n
is the size of the set s
.