`Baby.CORE`

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 : tree`

`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.

`val weight : tree -> int`

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`

.

`val cardinal : tree -> int`

`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.

`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 -> unit`

`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.