The AUG_BST signature

« 210 Library Documentation

Overview

The AUG_BST signature is an interface for an augmented binary search tree with fixed key and value types. This signature is nearly identical to BST except for the addition of reduceVal, the Val substructure, and the lack of polymorphism.

Interface

structure Key : ORDKEY
structure Val : MONOID

type t
type bst = t

datatype view =
LEAF
| NODE of { key : Key.t
				, value : Val.t
				, left : bst
				, right : bst }

exception Order

val expose : bst → view
val size : bst → int
val reduceVal : bst -> Val.t

val empty : unit → bst
val singleton : Key.t * Val.t → bst

val join : bst * bst → bst
val joinMid : bst * (Key.t * Val.t) * bst → bst

val split : bst * Key.t → bst * Val.t option * bst

val $ : Key.t * Val.t → bst

Substructures

structure Key : ORDKEY
The Key substructure defines the key type of a binary search tree, providing comparison and other useful functions on keys.
structure Val : MONOID
The Val substructure defines the value type of a binary search tree. It also contains values $f$ and $I$, which are a reducing function and corresponding identity such that Val is a monoid. These values are using to maintain a reduced value which can be retrieved via reduceVal.

Types

type t
The abstract tree type.
type bst = t
An alias, for readability.
type view = LEAF | NODE of {key : Key.t, value : Val.t, left : bst, right : bst}
A one-layer view of a tree, which is either a leaf (containing no data) or an interior node with a key, value, and two children.

Exceptions

exception Order
Order is raised whenever tree operations would violate the ordering invariant.

Values

val expose : bst → view
Expose a view of the root node of the tree.
val size : bst → int
Return the number of nodes in the tree.
val reduceVal : bst → Val.t
Return the reduced value of the tree, which is logically equivalent to a reduce over the values of the tree with Val.f as the reducing function and Val.I as the identity.
val empty : unit → bst
Construct an empty tree.
val singleton : Key.t * Val.t → bst
Construct a tree containing a single node with the given key and value.
val join : bst * bst → bst
Given trees $A$ and $B$ where all keys in $A$ are strictly less than all keys in $B$, (join (A, B)) evaluates to the union of $A$ and $B$.
val joinMid : bst * (Key.t * Val.t) * bst → bst
(joinMid (A, (k, v), B)) is logically equivalent to (join (A, join (singleton (k, v), B))).
val split : bst * Key.t → bst * Val.t option * bst
(split (T, k)) evaluates to $(L, x, R)$ where $L$ is a bst containing all keys less than $k$, $R$ is a bst containing all keys greater than $k$, and $x$ is the value associated with $k$ (or NONE, if $k \not\in T$).
val $ : Key.t * Val.t → bst
An alias for singleton.