The `SORTED_DICT` signature

Overview

The SORTED_DICT interface specifies a persistent mapping from keys to values, written as $\{k_1 \mapsto v_1, k_2 \mapsto v_2, \dots \}$. Dictionaries do not have duplicate keys, so there is a unique associated value for each key. Keys are kept in sorted order, which first, split and getRange rely upon. The key type is given by the Key substructure, and the value type is polymorphic.

No operation modifies its arguments: an update returns a new dictionary.

Interface

structure Key : ORDKEY
structure Seq : SEQUENCE

type 'a t
type 'a dict = 'a t

exception Order

val empty : unit → 'a dict
val singleton : Key.t * 'a → 'a dict
val fromSeq : (Key.t * 'a) Seq.t → 'a dict
val toSeq : 'a dict → (Key.t * 'a) Seq.t
val toString : ('a → string) → 'a dict → string

val size : 'a dict → int
val find : 'a dict → Key.t → 'a option
val insert : 'a dict * (Key.t * 'a) → 'a dict
val remove : 'a dict * Key.t → 'a dict

val union : 'a dict * 'a dict → 'a dict
val intersection : 'a dict * 'a dict → 'a dict
val difference : 'a dict * 'a dict → 'a dict
val filter : (Key.t * 'a → bool) → 'a dict → 'a dict

val first : 'a dict → (Key.t * 'a) option
val last : 'a dict → (Key.t * 'a) option
val prev : 'a dict * Key.t → (Key.t * 'a) option
val next : 'a dict * Key.t → (Key.t * 'a) option

val split : 'a dict * Key.t → 'a dict * 'a option * 'a dict
val join : 'a dict * 'a dict → 'a dict
val getRange : 'a dict → Key.t * Key.t → 'a dict

val rank : 'a dict * Key.t → int
val select : 'a dict * int → (Key.t * 'a) option

Substructures

structure Key : ORDKEY: The Key substructure defines the key type of dictionaries, 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 dictionaries to and from sequences.

Types

type 'a t
type 'a dict = 'a t: The abstract dictionary type with values of type 'a. The type dict is for readability in the signature.

Exceptions

exception Order: Order is raised when join detects that its arguments would violate the ordering invariant.

Values

val empty : unit → 'a dict: Construct the empty dictionary.
val singleton : Key.t * 'a → 'a dict: singleton (k, v) constructs the singleton dictionary $\{k \mapsto v\}$.
val fromSeq : (Key.t * 'a) Seq.t → 'a dict: Return the dictionary of a sequence of key-value pairs, which may be in any order. If a key appears more than once, the value of its first occurrence in the sequence is kept.
val toSeq : 'a dict → (Key.t * 'a) Seq.t: Return a sequence of all key-value pairs in a dictionary, sorted by key.
val toString : ('a → string) → 'a dict → string: toString f d returns a string representation of $d$, sorted by key. Each key is converted to a string via Key.toString and each value via $f$.
val size : 'a dict → int: The number of key-value pairs in a dictionary.
val find : 'a dict → Key.t → 'a option: find d k returns (SOME $v$) if $(k \mapsto v) \in d$, and NONE otherwise.
val insert : 'a dict * (Key.t * 'a) → 'a dict: insert (d, (k, v)) returns the dictionary $d$ with $k$ mapped to $v$. If $k$ is already in $d$, its value is replaced by $v$.
val remove : 'a dict * Key.t → 'a dict: remove (d, k) returns the dictionary $d$ without the key $k$. If $k$ is not in $d$, it returns $d$.
val union : 'a dict * 'a dict → 'a dict: union (a, b) evaluates to $a \cup b$. A key in both $a$ and $b$ keeps its value from $a$.
val intersection : 'a dict * 'a dict → 'a dict: intersection (a, b) evaluates to the key-value pairs of $a$ whose keys are also in $b$.
val difference : 'a dict * 'a dict → 'a dict: difference (a, b) evaluates to the key-value pairs of $a$ whose keys are not in $b$.
val filter : (Key.t * 'a → bool) → 'a dict → 'a dict: filter p d returns the dictionary containing every $(k \mapsto v) \in d$ which satisfies $p(k, v)$.
val first : 'a dict → (Key.t * 'a) option: Return the smallest key of a dictionary (together with its associated value), or NONE if the dictionary is empty.
val last : 'a dict → (Key.t * 'a) option: Return the largest key of a dictionary (together with its associated value), or NONE if the dictionary is empty.
val prev : 'a dict * Key.t → (Key.t * 'a) option: prev (d, k) returns the largest key (together with its value) in $d$ which is strictly less than $k$, or NONE if there is no such key. $k$ need not be in $d$.
val next : 'a dict * Key.t → (Key.t * 'a) option: next (d, k) returns the smallest key (together with its value) in $d$ which is strictly greater than $k$, or NONE if there is no such key. $k$ need not be in $d$.
val split : 'a dict * Key.t → 'a dict * 'a option * 'a dict: split (d, 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 $d$ (or NONE if $k$ is not present in $d$).
val join : 'a dict * 'a dict → 'a dict: Given dictionaries $a$ and $b$ where every key in $a$ is strictly smaller than every key in $b$, join (a, b) evaluates to $a \cup b$.
val getRange : 'a dict → Key.t * Key.t → 'a dict: getRange d (x, y) evaluates to $\{ (k \mapsto v) \in d\ |\ x \leq k < y \}$. The range includes $x$ but not $y$.
val rank : 'a dict * Key.t → int: rank (d, k) evaluates to the number of keys in $d$ which are strictly smaller than $k$. $k$ need not be in $d$.
val select : 'a dict * int → (Key.t * 'a) option: select (d, i) evaluates to the key of rank $i$ (together with its associated value), or NONE if either $i < 0$ or $i \geq |d|$. Ranks start at zero, so select (d, 0) is the smallest key.