AUG_ORDTABLE
signature
The AUG_ORDTABLE
interface specifies a mapping from keys to values,
augmented with efficient retrieval of reduced values for ranges of keys.
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. The value type is given by the
Val
substructure.
The AUG_ORDTABLE
signature is nearly identical to ORDTABLE
except for the following.
Val
substructure which fixes the value type,
and specifies how reduced values are computed.reduceVal
function retrieves reduced values.collect
and iteratePrefixes
have been removed,
since these rely upon a polymorphic value type.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 : ('a * Val.t → 'a) → 'a → table → 'a
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.t
structure Key :
ORDKEY
Key
substructure defines the type of keys in a table,
which are totally ordered according to the provided comparison function.
structure Val : MONOID
Val
substructure defines the type of values in a table,
which ascribe to MONOID
,
specifying how reduced values are computed.
structure Seq :
SEQUENCE
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
Set
substructure contains operations on
ordered sets with elements of type Key.t
.
type t
type table =
t
Key.t
and values of type Val.t
The alias table
is for readability in the signature.
exception Order
Order
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
returns a string representation of $t$. Each key is converted
to a string via Key.toString
and each value is converted via Val.toString
.
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 :
'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
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 fromSeq :
(Key.t * 'a) Seq.t → 'a table
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 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
singleton
.
val first :
'a table → (Key.t * 'a) option
NONE
if the table is empty.
val last :
'a table → (Key.t * 'a) option
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
(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|$.
val reduceVal :
table → Val.t
reduceVal t
is logically equivalent to
Seq.reduce Val.f Val.I (range t)
. See MONOID
for more information.