AUG_ORDTABLE signature
The AUG_ORDTABLE signature is an interface for an augmented,
ordered table with fixed key and value types. This signature is nearly
identical to
ORDTABLE except for the addition of
reduceVal, the
Val substructure, and the lack of
polymorphism.
structure Key : ORDKEY
structure Val : MONOID
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 → Val.t Seq.t
val toString : table → string
val toSeq : table → (Key.t * Val.t) Seq.t
val find : table → Key.t → Val.t option
val insert : table * (Key.t * Val.t) → table
val insertWith : (Val.t * Val.t → Val.t) → table * (Key.t * Val.t) → table
val delete : table * Key.t → table
val empty : unit → table
val singleton : Key.t * Val.t → table
val tabulate : (Key.t → Val.t) → Set.t → table
val fromSeq : (Key.t * Val.t) Seq.t → table
val map : (Val.t → Val.t) → table → table
val mapKey : (Key.t * Val.t → Val.t) → table → table
val filter : (Val.t → bool) → table → table
val filterKey : (Key.t * Val.t → bool) → table → table
val reduce : (Val.t * Val.t → Val.t) → Val.t → table → Val.t
val iterate : (α * Val.t → α) → α → table → α
val union : (Val.t * Val.t → Val.t) → table * table → table
val intersection : (Val.t * Val.t → Val.t) → table * table → table
val difference : table * table → table
val restrict : table * Set.t → table
val subtract : table * Set.t → table
val $ : (Key.t * Val.t) → table
val first : table → (Key.t * Val.t) option
val last : table → (Key.t * Val.t) option
val prev : table * Key.t → (Key.t * Val.t) option
val next : table * Key.t → (Key.t * Val.t) option
val split : table * Key.t → table * Val.t 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 * Val.t) option
val splitRank : table * int → table * table
val reduceVal : table → Val.tstructure Key :
ORDKEYKey substructure defines the key type of
tables, providing equality and other useful functions.
structure Val : MONOIDVal substructure defines the value type of a table.
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.
structure Seq :
SEQUENCESeq substructure defines the sequence type to
and from which tables can be converted.
structure Set :
ORDSET where Key = Key and Seq = SeqSet substructure contains operations on
sets with elements of type Key.t.
type ttype table =
tt, for readability.
exception OrderOrder is raised whenever table operations would violate the ordering invariant.val size :
table → int
val domain :
table → Set.t
val range :
table → Val.t Seq.t
val toString :
table → string
(toString 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 Val.toString. 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 * Val.t) Seq.t
val find :
table → Key.t → Val.t option
(find t k) returns (SOME $v$) if
$(k \mapsto v) \in t$, and NONE otherwise.
val insert :
table * (Key.t * Val.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 :
(Val.t * Val.t → Val.t) → table * (Key.t * Val.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
val singleton :
Key.t * Val.t → table
(singleton (k, v)) evaluates to the singleton table
$\{(k \mapsto v)\}$.
val tabulate :
(Key.t → Val.t) → Set.t → table
(tabulate f x) evaluates to the table
$\{ (k \mapsto f(k)) : k \in x \}$.
val fromSeq :
(Key.t * Val.t) Seq.t → table
val map :
(Val.t → Val.t) → table → table
(map f t) returns the table
$\{ (k \mapsto f(v)) : (k \mapsto v) \in t \}$.
val mapKey :
(Key.t * Val.t → Val.t) → table → table
(mapKey f t) returns the table
$\{ (k \mapsto f(k, v)) : (k \mapsto v) \in t \}$.
val filter :
(Val.t → bool) → table → table
(filter p t) returns the table containing every
$(k \mapsto v) \in t$ which satisfies $p(v)$.
val filterKey :
(Key.t * Val.t → bool) → table → table
(filterKey p t) returns the table containing every
$(k \mapsto v) \in t$ which satisfies $p(k, v)$.
val reduce :
(Val.t * Val.t → Val.t) → Val.t → table → Val.t
(reduce f b t) is logically equivalent to
(Seq.reduce f b (range t)).
val iterate :
(α * Val.t → α) → α → table → α
(iterate f b t) is logically equivalent to
(Seq.iterate f b (range t)).
val union :
(Val.t * Val.t → Val.t) → 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 :
(Val.t * Val.t → Val.t) → 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 * Val.t) → table
singleton.
val first :
table → (Key.t * Val.t) optionNONE if the table is empty.
val last :
table → (Key.t * Val.t) optionNONE if the table is empty.
val prev :
table * Key.t → (Key.t * Val.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 * Val.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 * Val.t 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(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 * Val.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|$.
val reduceVal :
table → Val.t(reduceVal t) is logically equivalent to
(Seq.reduce Val.f Val.I (range t)).