The MkSTSequence functor

« 210 Library Documentation


functor MkSTSequence (structure Seq : SEQUENCE) :> ST_SEQUENCE where Seq = Seq

Implements single-threated sequences via a state ref and history. If the state is CUR a, then the single-threaded sequence is current and $a$ can be accessed immediately. Otherwise, if the state is MOD, the single-threaded sequence needs to be reconstructed from history — that is, by sequentially applying every update to the original sequence from which the single-threaded sequence was created.

ST_SEQUENCE Cost Specifications

Work Span
nth $S\ i$
update $(S, (i, x))$
\[O(1)\] \[O(1)\]
inject $(S, U)$ \[O(|U|)\] \[O(1)\]

The following assumes Seq = ArraySequence. For another choice of Seq, refer directly to the implementations of fromSeq and toSeq.

Work Span
fromSeq $S$
toSeq $S$
\[O(|S|)\] \[O(1)\]