package baby
Library
Module
Module type
Parameter
Class
Class type
The signature Baby.CORE describes the interface that must be offered by the balancing code to the rest of the balanced binary search tree library. Most operations on binary search tree are built on top of this interface, and are oblivious to the balancing criterion.
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.
val leaf : treeleaf 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.
val weight : tree -> intIf 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.
val cardinal : tree -> intcardinal 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.
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.
val check : tree -> unitcheck 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.