ST_SEQUENCE signaturefunctor MkSTSequence
A sequence is as defined in the
SEQUENCE signature.
Single-threaded sequences differ in that they are
only meant to be used in single-threaded applications —
that is to say, updates should only be made on the
most recently modified version of the type.
However, operations on single-threaded sequences are always
well-defined, regardless of context.
structure Seq : SEQUENCE
type 'a stseq
exception Range
val fromSeq : 'a Seq.seq -> 'a stseq
val toSeq : 'a stseq -> 'a Seq.seq
val nth : 'a stseq -> int -> 'a
val update :
(int * 'a) -> 'a stseq -> 'a stseq
val inject :
(int * 'a) Seq.seq -> 'a stseq -> 'a stseq
structure Seq :
SEQUENCESeq substructure defines the underlying
SEQUENCE type to and
from which single-threaded sequences can be converted.type 'a stseqexception RangeRange is raised whenever an
invalid index into a single-threaded sequence is used.val fromSeq :
'a Seq.seq -> 'a stseq(fromSeq S) evaluates to the single-threaded
sequence representation of the sequence $S$.val toSeq :
'a steq -> 'a Seq.seq(toSeq S) converts a single-threaded sequence
$S$ back to sequence representation.val nth :
'a seq -> int -> 'a(nth s i) evaluates to $s_i$,
the $i^{th}$ element of $s$.
Raises Range if $i$ is out-of-bounds.val update :
(int * 'a) -> 'a stseq -> 'a stseq(update (i,v) s) evaluates to a single-threaded
sequence with the value at $i$ updated as $v$. Raises
Range if $i$ is out-of-bounds.val inject :
(int * 'a) Seq.seq -> 'a stseq -> 'a stseq(inject U s) evaluates to a
single-threaded sequence
with updated values of $s$ as given by $U$.
If there are duplicate indices in $U$,
the last one is written and the others are ignored. Raises
Range if any indices are out-of-bounds.