The `TABLE` signature

« 210 Library Documentation

Overview


  functor MkTreapTable

A table is a set of key-value pairs where the keys are unique. For this reason, we often think of it as a mapping that associates each key with a value. Since tables are sets, standard set operations apply on them.

If $T$ is a table with $n$ elements, we may denote $T$ with the notation $\{(k_1\mapsto v_1),(k_2\mapsto v_2),\ldots,(k_n\mapsto v_n)\}$ where $k_1,\ldots,k_n$ are $n$ distinct keys, each $k_i$ maps to $v_i$ for $i\in[n]$, and the size of $T$ is written $|T|=n$. We say that a key $k$ is present in a table $T$, written as $k\in_m T$, if there exists a value $v$ such that $(k\mapsto v)\in T$.

Interface


  structure Key : EQKEY

  structure Seq : SEQUENCE

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



  type 'a table

  type 'a seq = 'a Seq.seq

  type key = Key.t

  type set = Set.t



  val size : 'a table -> int

  val domain : 'a table -> set

  val range : 'a table -> 'a seq

  val toString :
    ('a -> string) -> 'a table -> string

  val toSeq : 'a table -> (key * 'a) seq



  val find : 'a table -> key -> 'a option

  val insert :
    ('a * 'a -> 'a) -> (key * 'a) -> 'a table -> 'a table

  val delete : key -> 'a table -> 'a table



  val empty : unit -> 'a table

  val singleton : key * 'a -> 'a table

  val tabulate : (key -> 'a) -> set -> 'a table

  val collect : (key * 'a) seq -> 'a seq table

  val fromSeq : (key * 'a) seq -> 'a table



  val map    :
    ('a -> 'b) -> 'a table -> 'b table

  val mapk   :
    (key * 'a -> 'b) -> 'a table -> 'b table

  val filter :
    ('a -> bool) -> 'a table -> 'a table

  val filterk :
    (key * 'a -> bool) -> 'a table -> 'a table



  val iter   :
    ('b * (key * 'a) -> 'b) -> 'b -> 'a table -> 'b

  val iterh  :
    ('b * (key * 'a) -> 'b) -> 'b -> 'a table -> ('b table * 'b)

  val reduce :
    ('a * 'a -> 'a) -> 'a -> 'a table -> 'a



  val merge   :
    ('a * 'a -> 'a) -> ('a table * 'a table) -> 'a table

  val extract : 'a table * set -> 'a table

  val erase   : 'a table * set -> 'a table



  val $ : (key * 'a) -> 'a table

Substructures

structure Key : EQKEY: The Key substructure defines the key type of a table, providing equality and toString functions on such keys.
structure Seq : SEQUENCE: The Seq substructure defines the underlying SEQUENCE type to and from which tables can be converted.
structure Set : SET where Key = Key and Seq = Seq: The Set substructure contains operations on sets with values of type key, reinforcing the notion of tables as sets of key-value mappings.

Values

type 'a table: This is the abstract type that represents a table as described in the overview.
type 'a seq = 'a Seq.seq: This type is a shorthand for the abstract 'a Seq.seq type.
type key = Key.t: This indicates that the keys in a table must be of type Key.t.
type set = Set.t: This type is a shorthand for the abstract Set.t type.

Types

val size : 'a table -> int: (size T) evaluates to $|T|$, the number of keys contained in the table $T$.
val domain : 'a table -> set: (domain T) evaluates to the set of keys contained in the table $T$.
val range : 'a table -> 'a seq: (range T) evaluates to a sequence containing all values in the table $T$.
val toString : ('a -> string) -> 'a table -> string: (toString valToStr T) evaluates to a string representation of $T$. This representation begins with “{” and ends with “}”. Each key-value pair is represented as “($k$->$v$)”, where $k$ is the string representation of the key and $v$ is the result of applying valToStr to the value.
val toSeq : 'a table -> (key * 'a) seq: If $T = \{(k_1\mapsto v_1),(k_2\mapsto v_2),\ldots,(k_n\mapsto v_n)\}$, (toSeq T) evaluates to a sequence of all key-value pairs $\langle (k_1,v_1),(k_2,v_2),\ldots,(k_n,v_n) \rangle$. The ordering of the sequence is implementation-defined.
val find : 'a table -> key -> 'a option: If $t$ contains the mapping $(k\mapsto v)$, (find T k) evaluates to (SOME v). Otherwise, it evaluates to NONE.
val insert : ('a * 'a -> 'a) -> (key * 'a) -> 'a table -> 'a table: (insert f (k,v) T) evaluates to $T\cup \{(k\mapsto v)\}$ provided $k\not\in_m T$. Otherwise, if $(k\mapsto v')\in T$, the value associated with $k$ is replaced with the result of applying $f$ on the old value $v'$ and the new value $v$.
val delete : key -> 'a table -> 'a table: (delete k T) evaluates to $\{(k'\mapsto v')\in T : k' \neq k\}$, removing $k$ from the table $t$.
val empty : unit -> 'a table: (empty ()) evaluates to the empty table, $\emptyset$.
val singleton : key * 'a -> 'a table: (singleton (k,v)) evalutes to the singleton table $\{(k\mapsto v)\}$.
val tabulate : (key -> 'a) -> set -> 'a table: If $S$ is the set $\{k_1,k_2,\ldots,k_n\}$, (tabulate f S) evaluates to $\{(k_1\mapsto f(k_1)),(k_2\mapsto f(k_2)),\ldots,(k_n\mapsto f(k_n))\}$.
val collect : (key * 'a) seq -> 'a seq table: If $S$ is a sequence of key-value pairs, (collect S) evaluates to a table where each $(k\mapsto V)$ maps $k$ to a sequence $V$ which results from grouping values of the same key $k$ together while respecting the original sequence ordering.
val fromSeq : (key * 'a) seq -> 'a table: If $S$ is a sequence of key-value pairs $\langle (k_1,v_1),(k_2,v_2),\ldots,(k_n,v_n) \rangle$, (fromSeq S) evaluates to the table $\{(k_1\mapsto v_1),(k_2\mapsto v_2),\ldots,(k_n\mapsto v_n)\}$.
val map : ('a -> 'b) -> 'a table -> 'b table: If $T = \{(k_1\mapsto v_1),(k_2\mapsto v_2),\ldots,(k_n\mapsto v_n)\}$, (map f T) evaluates to $\{(k_1\mapsto f(v_1)),(k_2\mapsto f(v_2)),\ldots, (k_n\mapsto f(v_n))\}$.
val mapk : (key * 'a -> 'b) -> 'a table -> 'b table: If $T = \{(k_1\mapsto v_1),(k_2\mapsto v_2),\ldots,(k_n\mapsto v_n)\}$, (mapk f T) evaluates to $\{(k_1\mapsto f(k_1,v_1)),(k_2\mapsto f(k_2,v_2)),\ldots, (k_n\mapsto f(k_n,v_n))\}$.
val filter : ('a -> bool) -> 'a table -> 'a table: (filter p T) evaluates to the table $T'$ such that $(k\mapsto v)\in T'$ if and only if $(k\mapsto v)\in T$ and $p(v)$ evaluates to true.
val filterk : (key * 'a -> bool) -> 'a table -> 'a table: (filterk p T) evaluates to the table $T'$ such that $(k\mapsto v)\in T'$ if and only if $(k\mapsto v)\in T$ and $p(k,v)$ evaluates to true.
val iter : ('b * (key * 'a) -> 'b) -> 'b -> 'a table ->'b: (iter f b T) iterates $f$ with left-association on the key-value pairs in $T$ with $b$ as the base case. The order of application is implementation-defined.
val iterh : ('b * (key * 'a) -> 'b) -> 'b -> 'a table -> ('b table * 'b): (iterh f b T) evaluates to $(T',v)$, where $v$ is the result of evaluating (iter f b T) and $T'$ is a table containing partial evaluation results. Specifically, $T' = \{(k_i\mapsto r_i): (k_i\mapsto v_i)\in T\}$ where $r_i$ is the result of partial evaluation up to the $i^{th}$ key-value pair $(k_i\mapsto v_i)$ as defined by the implementation.
val reduce : ('a * 'a -> 'a) -> 'a -> 'a table -> 'a: (reduce f b T) is logically equivalent to (Seq.reduce f b (range T)).
val merge : ('a * 'a -> 'a) -> ('a table * 'a table) -> 'a table: merge is a generalization of set union. Specifically, (merge f (S, T)) evaluates to a table with the following properties: (1) it contains all the keys from $S$ and $T$ and (2) for each key $k$, its associated value is inherited from either $S$ or $T$ is $k$ if present in exactly one of them. But if $(k\mapsto v)\in S$ and $(k\mapsto w)\in T$, then the associated value is $f(v,w)$.
val extract : 'a table * set -> 'a table: extract is a generalization of set intersection. Specifically, (extract (T,S)) evaluates to $\{(k\mapsto v)\in T : k\in_m S\}$.
val erase : 'a table * set -> 'a table: erase is a generalization of set difference. Specifically, (erase (T,S)) evaluates to $\{(k\mapsto v)\in T : k\not\in_m S\}$.