The AUG_SORTED_DICT signature

Overview

The AUG_SORTED_DICT interface specifies a sorted dictionary augmented with efficient retrieval of the reduced value of all its values. It is identical to SORTED_DICT except for the following:

• Dictionaries are not polymorphic in the type of values associated with keys: values have type value in place of 'a.
• The values combine and identity say how values combine.
• The reducedVal function retrieves reduced values.

The other operations are described on the SORTED_DICT page.

Interface

structure Key : ORDKEY
structure Seq : SEQUENCE

type value
val combine : value * value → value
val identity : value

type t
type dict = t

exception Order

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

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

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

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

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

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

val reducedVal : dict → value

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 value

The type of the values.

type t

type dict = t

The abstract dictionary type with values of type value. The type dict is for readability in the signature.

Values

val combine : value * value → value

An associative function that combines two values.

val identity : value

The identity of combine: combining it with any value $x$, on either side, gives back $x$.

val reducedVal : dict → value

reducedVal d evaluates to $v_1 \oplus v_2 \oplus \cdots \oplus v_n$, where $v_1, \ldots, v_n$ are the values of $d$ in increasing order of their keys and $\oplus$ is combine. It evaluates to identity if $d$ is empty.