The `ORDTABLE` signature

Overview

Ordered tables are tables which are ordered by their keys. This interface is nearly identical to TABLE except for the ordered table functions starting with first, Key now ascribing to ORDKEY, and Set now ascribing to ORDSET.

Interface

structure Key : ORDKEY
structure Seq : SEQUENCE

type α t
type α table = α t

exception Order

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

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

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

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

val map : (α → β) → α table → β table
val mapKey : (Key.t * α → β) → α table → β table
val filter : (α → bool) → α table → α table
val filterKey : (Key.t * α → bool) → α table → α table

val reduce : (α * α → α) → α → α table → α
val iterate : (β * α → β) → β → α table → β
val iteratePrefixes : (β * α → β) → β → α table → (β table * β)

val union : (α * α → α) → α table * α table → α table
val intersection : (α * β → γ) → α table * β table → γ table
val difference : α table * β table → α table

val restrict : α table * Set.t → α table
val subtract : α table * Set.t → α table

val $ : (Key.t * α) → α table

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

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

val split : α table * Key.t → α table * α option * α table
val join : α table * α table → α table

val getRange : α table → Key.t * Key.t → α table

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

Substructures

structure Key : ORDKEY: The Key substructure defines the key type of tables, providing equality and other useful functions.
structure Seq : SEQUENCE: The Seq substructure defines the sequence type to and from which tables can be converted.
structure Set : ORDSET where Key = Key and Seq = Seq: The Set substructure contains operations on sets with elements of type Key.t.

Types

type α t: The abstract table type.
type α table = α t: An alias for α t, for readability.

Exceptions

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

Values

val size : α table → int: Return the number of key-value pairs in a table.
val domain : α table → Set.t: Return the set of all keys in a table.
val range : α table → α Seq.t: Return a sequence of all values in a table in sorted order of the keys they were associated with.
val toString : (α → string) → α table → string: (toString f t) evaluates to a string representation of $t$ where each key is converted to a string with Key.toString and each value is converted with $f$. For example, the table $\{ (1 \mapsto 2), (3 \mapsto 42) \}$ might be represented by the string “{(1->2),(3->42)}“. The ordering of key-value pairs in the resulting string is sorted by key.
val toSeq : α table → (Key.t * α) Seq.t: Return a sequence of all key-value pairs in a table, sorted by key.
val find : α table → Key.t → α option: (find t k) returns (SOME $v$) if $(k \mapsto v) \in t$, and NONE otherwise.
val insert : α table * (Key.t * α) → α table: (insert (t, (k, v))) returns the table $t \cup \{(k \mapsto v)\}$ where $v$ is given precedence over $v'$ if there already exists a $(k \mapsto v') \in t$.
val insertWith : (α * α → α) → α table * (Key.t * α) → α table: (insertWith f (t, (k, v))) returns the table $t \cup \{(k \mapsto v)\}$ if $k$ is not already a member of $t$, otherwise it returns $t \cup \{(k \mapsto f (v', v))\}$ where $(k \mapsto v') \in t$.
val delete : α table * Key.t → α table: (delete (t, k)) deletes $k$ only if it is present in $t$. That is, it evaluates to $t \setminus \{(k \mapsto v)\}$ if $(k \mapsto v) \in t$. Otherwise, it evaluates to $t$.
val empty : unit → α table: Construct the empty table.
val singleton : Key.t * α → α table: (singleton (k, v)) evaluates to the singleton table $\{(k \mapsto v)\}$.
val tabulate : (Key.t → α) → Set.t → α table: (tabulate f x) evaluates to the table $\{ (k \mapsto f(k)) : k \in x \}$.
val collect : (Key.t * α) Seq.t → α Seq.t table: (collect s) is logically equivalent to (fromSeq (Seq.collect Key.compare s)).
val fromSeq : (Key.t * α) Seq.t → α 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 : (α → β) → α table → β table: (map f t) returns the table $\{ (k \mapsto f(v)) : (k \mapsto v) \in t \}$.
val mapKey : (Key.t * α → β) → α table → β table: (mapKey f t) returns the table $\{ (k \mapsto f(k, v)) : (k \mapsto v) \in t \}$.
val filter : (α → bool) → α table → α table: (filter p t) returns the table containing every $(k \mapsto v) \in t$ which satisfies $p(v)$.
val filterKey : (Key.t * α → bool) → α table → α table: (filterKey p t) returns the table containing every $(k \mapsto v) \in t$ which satisfies $p(k, v)$.
val reduce : (α * α → α) → α → α table → α: (reduce f b t) is logically equivalent to (Seq.reduce f b (range t)).
val iterate : (β * α → β) → β → α table → β: (iterate f b t) is logically equivalent to (Seq.iterate f b (range t)).
val iteratePrefixes : (β * α → β) → β → α table → (β table * β): (iteratePrefixes f b t) is logically equivalent to (fromSeq p, x) where $(p, x)$ = (Seq.iteratePrefixes f b (range t)).
val union : (α * α → α) → α table * α table → α 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 : (α * β → γ) → α table * β table → γ 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 : α table * β table → α table: (difference (a, b)) evaluates to the table $a \setminus b$.
val restrict : α table * Set.t → α table: restrict is basically an alias for intersection in that it restricts a table's domain by the elements of a set. The name is motivated by the interpretation of a table as a function, and therefore (restrict (t, x)) evaluates to $t\,|_x$.
val subtract : α table * Set.t → α table: subtract is basically an alias for difference in that it removes all mappings whose keys are given in a set. The name is once again motivated by the interpretation of a table as a function, where (subtract (t, x)) performs the domain subtraction of $t$ by $x$. This is also sometimes referred to as the domain anti-restriction.
val $ : (Key.t * α) → α table: An alias for singleton.
val first : α table → (Key.t * α) option: Return the least key of a table along with its associated value, or NONE if the table is empty.
val last : α table → (Key.t * α) option: Return the greatest key of a table along with its associated value, or NONE if the table is empty.
val prev : α table * Key.t → (Key.t * α) option: (prev (t, k)) evaluates to the maximum key (paired with its associated value) in $t$ which is strictly less than $k$, or NONE if there is no such key.
val next : α table * Key.t → (Key.t * α) option: (next (t, k)) evaluates to the minimum key (paired with its associated value) in $t$ which is strictly greater than $k$, or NONE if there is no such key.
val split : α table * Key.t → α table * α option * α table: (split (t, k)) evaluates to $(l, v, r)$, where $l = \{ (k' \mapsto v') \in t\ |\ k' < k \}$, $r = \{ (k' \mapsto v') \in t\ |\ k' > k \}$, and $v$ is $k$'s associated value, or NONE if $k \not\in t$.
val join : α table * α table → α table: Given tables $x$ and $y$ where every key in $x$ is strictly less than every element in $y$, (join (x, y)) evaluates to $x \cup y$.
val getRange : α table → Key.t * Key.t → α table: (getRange t (a, b)) evaluates to $\{ (k \mapsto v) \in t\ |\ a \leq k \leq b \}$.
val rank : α table * Key.t → int: (rank (t, k)) evaluates to $\big|\{ (k' \mapsto v') \in t\ |\ k' < k \}\big|$.
val select : α table * int → (Key.t * α) option: (select (t, i)) evaluates to the $i^\text{th}$ largest key (paired with its associated value) in $t$, or NONE if either $i < 0$ or $i \geq |t|$.
val splitRank : α table * int → α table * α table: (splitRank (t, i)) evaluates to $(l, r)$ such that $|l| = i$, $|r| = |t| - i$, every key in $l$ is strictly less than every key in $r$, and their union is $t$. Raises Fail if $i < 0$ or $i \geq |t|$.