The signature Baby.SET describes an abstract data type of sets, equipped with a wide array of efficient operations.
type t = setA synonym for the type set.
In the following, we usually document the behavior of each operation only in the common case where the relation \leq is a total order. (To find out what this means, see OrderedType.compare.)
In this common case, a value of type set can be thought of as a set in the usual sense.
Outside of this common case, the relation \leq is a total preorder, but not a total order: that is, equivalence does not imply equality. In this general case, a value s of type set can be thought of as a set, with the added property that within s, equivalence implies equality: that is, if x and y are members of s, then x \equiv y implies x = y. In other words, a set s contains at most one element of each equivalence class.
Some operations are useful only in the general case where the relation \leq is not a total order. This is explicitly indicated in the documentation of each such operation.
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.
val empty : setempty 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 less than x, r is the set of the elements of s that are 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 -> boolis_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.
This operation is typically useful when the relation \leq is not a total order.
If the set s contains an element x' such that x' \equiv x holds, then find x s returns x'. Otherwise, it raises Not_found.
Time complexity: O(\log n), where n is the size of the set s.
This operation is typically useful when the relation \leq is not a total order.
If the set s contains an element x' such that x' \equiv x holds, then find_opt x s returns Some x'. 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 -> intof_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 consume s produces an increasing sequence whose elements are the elements of the set s. The function consume is applied in turn to each element of the sequence.
Time complexity: O(n), where n is the size of the set s.
fold consume s init produces an increasing sequence whose elements are the elements of the set s. The function consume is applied in turn to each element of the sequence.
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 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 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 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 \}.
The elements of the set s are passed to the function f in increasing order.
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.