The ORDTABLE signature

Overview

The ORDTABLE interface specifies a mapping from keys to values, written as $\{k_1 \mapsto v_1, k_2 \mapsto v_2, \dots \}$.

•   The Key substructure now ascribes to ORDKEY.
•   The Set substructure now ascribes to ORDSET.
•   There is additional functionality relying upon the ordering of keys, such as split, join, and getRange.

•   The toSeq function now specifies that it returns keys in sorted order.

Interface

structure Key : ORDKEY
structure Seq : SEQUENCE

type 'a t
type 'a table = 'a t

exception Order

structure Set : ORDSET where Key = Key and Seq = Seq

val size : 'a table → int
val domain : 'a table → Set.t
val range : 'a table → 'a Seq.t
val toString : ('a → string) → 'a table → string
val toSeq : 'a table → (Key.t * 'a) Seq.t

val find : 'a table → Key.t → 'a option
val insert : 'a table * (Key.t * 'a) → 'a table
val insertWith : ('a * 'a → 'a) → 'a table * (Key.t * 'a) → 'a table
val delete : 'a table * Key.t → 'a table

val empty : unit → 'a table
val singleton : Key.t * 'a → 'a table
val tabulate : (Key.t → 'a) → Set.t → 'a table
val collect : (Key.t * 'a) Seq.t → 'a Seq.t table
val fromSeq : (Key.t * 'a) Seq.t → 'a table

val map : ('a → 'b) → 'a table → 'b table
val mapKey : (Key.t * 'a → 'b) → 'a table → 'b table
val filter : ('a → bool) → 'a table → 'a table
val filterKey : (Key.t * 'a → bool) → 'a table → 'a table

val reduce : ('a * 'a → 'a) → 'a → 'a table → 'a
val iterate : ('b * 'a → 'b) → 'b → 'a table → 'b
val iteratePrefixes : ('b * 'a → 'b) → 'b → 'a table → ('b table * 'b)

val union : ('a * 'a → 'a) → 'a table * 'a table → 'a table
val intersection : ('a * 'b → 'c) → 'a table * 'b table → 'c table
val difference : 'a table * 'b table → 'a table

val restrict : 'a table * Set.t → 'a table
val subtract : 'a table * Set.t → 'a table

val $ : (Key.t * 'a) → 'a table

val first : 'a table → (Key.t * 'a) option
val last : 'a table → (Key.t * 'a) option

val prev : 'a table * Key.t → (Key.t * 'a) option
val next : 'a table * Key.t → (Key.t * 'a) option

val split : 'a table * Key.t → 'a table * 'a option * 'a table
val join : 'a table * 'a table → 'a table

val getRange : 'a table → Key.t * Key.t → 'a table

val rank : 'a table * Key.t → int
val select : 'a table * int → (Key.t * 'a) option
val splitRank : 'a table * int → 'a table * 'a table

Substructures

structure Key : ORDKEY

The Key substructure defines the key type of tables, which are totally ordered according to the provided comparison function.

structure Seq : SEQUENCE

The Seq substructure defines the underlying sequence type, so that we may convert tables to and from sequences.

structure Set : ORDSET where Key = Key and Seq = Seq

The Set substructure contains operations on sets with elements of type Key.t.

Types

type 'a t

type 'a table = 'a t

The abstract table type with values of type 'a. The type table is for readability in the signature.

Exceptions

exception Order

Order is raised when the ordering invariant would be violated.

Values

val size : 'a table → int

The number of key-value pairs in a table.

val domain : 'a table → Set.t

Return the set of all keys in a table.

val range : 'a table → 'a Seq.t

Return a sequence of all values in a table in sorted order of the keys they were associated with.

val toString : ('a → string) → 'a table → string

toString f t returns a string representation of $t$. Each key is converted to a string via Key.toString and each value is converted via $f$.

val toSeq : 'a table → (Key.t * 'a) Seq.t

Return a sequence of all key-value pairs in a table, sorted by key.

val find : 'a table → Key.t → 'a option

find t k returns (SOME $v$) if $(k \mapsto v) \in t$, and NONE otherwise.

val insert : 'a table * (Key.t * 'a) → 'a table

insert (t, (k, v)) returns the table $t \cup \{(k \mapsto v)\}$. If $k$ is already in $t$, then the new value $v$ is given precedence. It is logically equivalent to insertWith (fn (_, v) => v) (t, (k,v)) .

val insertWith : ('a * 'a → 'a) → 'a table * (Key.t * 'a) → 'a table

insertWith f (t, (k, v)) returns the table $t \cup \{(k \mapsto v)\}$ if $k$ is not already a member of $t$, and otherwise it returns $t \cup \{(k \mapsto f (v', v))\}$ where $(k \mapsto v')$ is already in $t$.

val delete : 'a table * Key.t → 'a table

delete (t, k) removes the key $k$ from $t$ only if $k$ is a member of $t$. That is, if $(k \mapsto v) \in t$ then it returns $t \setminus \{(k \mapsto v)\}$, otherwise it returns $t$.

val empty : unit → 'a table

Construct the empty table.

val singleton : Key.t * 'a → 'a table

singleton (k, v) constructs the singleton table $\{(k \mapsto v)\}$.

val tabulate : (Key.t → 'a) → Set.t → 'a table

tabulate f s evaluates to the table $\{ (k \mapsto f(k)) : k \in s \}$.

val collect : (Key.t * 'a) Seq.t → 'a Seq.t table

collect s takes a sequence of key-value pairs and produces a table where each unique key $k$ is paired with $\langle v : (k', v) \in s | k' = k \rangle$.

val fromSeq : (Key.t * 'a) Seq.t → 'a table

Return the table representation of a sequence of key-value pairs. If there are duplicate keys, then take the value associated with the first occurence in the sequence.

val map : ('a → 'b) → 'a table → 'b table

map f t returns the table $\{ (k \mapsto f(v)) : (k \mapsto v) \in t \}$.

val mapKey : (Key.t * 'a → 'b) → 'a table → 'b table

mapKey f t returns the table $\{ (k \mapsto f(k, v)) : (k \mapsto v) \in t \}$.

val filter : ('a → bool) → 'a table → 'a table

filter p t produces a table containing all $(k \mapsto v) \in t$ which satisfies $p(v)$.

val filterKey : (Key.t * 'a → bool) → 'a table → 'a table

filterKey p t returns the table containing every $(k \mapsto v) \in t$ which satisfies $p(k, v)$.

val reduce : ('a * 'a → 'a) → 'a → 'a table → 'a

reduce f b t is logically equivalent to Seq.reduce f b (range t).

val iterate : ('b * 'a → 'b) → 'b → 'a table → 'b

iterate f b t is logically equivalent to Seq.iterate f b (range t).

val iteratePrefixes : ('b * 'a → 'b) → 'b → 'a table → ('b table * 'b)

iteratePrefixes f b t is logically equivalent to (fromSeq p, x) where $(p, x)$ = Seq.iteratePrefixes f b (range t).

val union : ('a * 'a → 'a) → 'a table * 'a table → 'a table

union f (a, b) evaluates to $a \cup b$. For keys $k$ where $(k \mapsto v) \in a$ and $(k \mapsto w) \in b$, we have $(k \mapsto f (v, w))$ in the resulting table.

val intersection : ('a * 'b → 'c) → 'a table * 'b table → 'c table

intersection f (a, b) evaluates to the table $a \cap b$. Every intersecting key $k$ is mapped to $f (v, w)$, where $(k \mapsto v) \in a$ and $(k \mapsto w) \in b$.

val difference : 'a table * 'b table → 'a table

difference (a, b) evaluates to the table $a \setminus b$.

val restrict : 'a table * Set.t → 'a table

restrict returns the table of $\{ (k \mapsto v) \in t | k \in s \}$. It is therefore essentially an intersection. The name is motivated by the notion of restricting a function to a smaller domain, where we interpret a table as a function.

val subtract : 'a table * Set.t → 'a table

subtract returns the table of $\{ (k \mapsto v) \in t | k \notin s \}$. The name is motivated by the notion of a domain subtraction on a function.

val $ : (Key.t * 'a) → 'a table

An alias for singleton.

val first : 'a table → (Key.t * 'a) option

Return the smallest key of a table (together with its associated value), or NONE if the table is empty.

val last : 'a table → (Key.t * 'a) option

Return the largest key of a table (together with its associated value), or NONE if the table is empty.

val prev : 'a table * Key.t → (Key.t * 'a) option

prev (t, k) returns the largest key (together with its associated value) in $t$ which is strictly less than $k$, or NONE if there is no such key.

val next : 'a table * Key.t → (Key.t * 'a) option

next (t, k) evaluates to the smallest key (together with its associated value) in $t$ which is strictly greater than $k$, or NONE if there is no such key.

val split : 'a table * Key.t → 'a table * 'a option * 'a table

split (t, k) evaluates to $(l, v, r)$, where $l$ consists of all key-value pairs with keys strictly smaller than $k$, $r$ consists of all key-value pairs with keys strictly greater than $k$, and $v$ is $k$'s associated value in $t$ (or NONE if $k$ is not present in $t$).

val join : 'a table * 'a table → 'a table

Given tables $a$ and $b$ where every key in $a$ is strictly smaller than every element in $b$, (join (a, b)) evaluates to $a \cup b$. Otherwise, it raises Order.

val getRange : 'a table → Key.t * Key.t → 'a table

getRange t (x, y) evaluates to $\{ (k \mapsto v) \in t\ |\ x \leq k \leq y \}$.

val rank : 'a table * Key.t → int

rank (t, k) evaluates to the number of keys in $t$ which are strictly smaller than $k$.

val select : 'a table * int → (Key.t * 'a) option

select (t, i) evaluates to the $i^\text{th}$ smallest key (together with its associated value) in $t$, or NONE if either $i < 0$ or $i \geq |t|$.

val splitRank : 'a table * int → 'a table * 'a table

splitRank (t, i) evaluates to $(l, r)$, where $l$ consists of the $i$ smallest keys of $t$, and $r$ is the set of the $|t| - i$ largest keys of $t$. Raises Fail if $i < 0$ or $i \geq |t|$.