package baby

Balanced binary search trees.

A view on a balanced binary search tree indicates whether this tree is a leaf or a node, and, if it is a node, gives access to its left child, its value, and its right child. A view does not give access to balancing information, such as the tree's height or weight.

view turns a tree into a view.

leaf is the empty tree; a leaf.

join l v r expects a subtree l, a value v, and a subtree r such that l < v < r holds. It returns a new tree whose elements are the elements of l, v, and r. If needed, it performs rebalancing, so the value v is not necessarily found at the root of the new tree.

siblings t1 t2 determines whether the trees t1 and t2 can be siblings in a well-formed tree, that is, whether they can be the children of a well-formed binary node (without rebalancing). This property is the precondition of join_siblings.

join_siblings l v r is analogous to join l v r. Like join, it requires l < v < r. Furthermore, it requires the trees l and r to be siblings. Two trees are siblings if they could be the children of a well-formed binary node.

join_quasi_siblings l v r is analogous to join l v r. Like join, it requires l < v < r. Furthermore, it requires the trees l and r to be quasi-siblings, that is, siblings where one of the trees has been disturbed by adding or removing one element.

If the weight of a tree can be determined in constant time, then weight t returns the weight of the tree t. If the weight of a tree cannot be efficiently determined, then it is acceptable for weight to always return zero. The function weight is used to implement fast paths in subset and equality tests: it must be the case that subset t1 t2 implies weight t1 <= weight t2.

cardinal t returns the number of elements in the tree. Depending on the internal representation of trees, the function cardinal may have time complexity O(1) or O(n). This is indicated by constant_time_cardinal.

constant_time_cardinal indicates whether cardinal constant time complexity.

singleton x constructs a tree whose sole element is x.

of_sorted_unique_array_slice a i j requires the array slice defined by array a, start index i, and end index j to be sorted and to contain no duplicate elements. It converts this array slice, in linear time, to a tree.

seems_smaller t1 t2 indicates which of the trees t1 and t2 seems smaller, based on height or weight. This function is used as part of a heuristic choice, so no correctness obligation bears on it; its postcondition is true.

check t checks that the tree t is well-formed: that is, t is a balanced binary search tree. This function is used while testing only.