The ORDTABLE signature

« 210 Library Documentation

Overview

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

Tables do not have duplicate keys, so there is a unique associated value for each key in the domain of a table. The key type is given by the Key substructure, and the value type is polymorphic.

This interface is nearly identical to SET except for the following:

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