package baby

Keys, or elements.

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 key, 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 key 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 key v is not necessarily found at the root of the new tree.

join_neighbors l v r is analogous to join l v r. Like join, it requires l < v < r. Furthermore, it assumes that the trees l and r have been obtained by taking two siblings in a well-formed tree and by adding or removing one element in one of them.

join_weight_balanced l v r is analogous to join l v r. Like join, it requires l < v < r. Furthermore, it assumes that the weights of the trees l and r differ by at most one.

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.

doubleton x y requires x < y. It constructs a tree whose elements are x and y.

tripleton x y z requires x < y < z. It constructs a tree whose elements are x, y, and z.

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.