Parameter Make.1-SSeq
type 'a schunk
type 'a measure
=
|
MUnit : 'a measure
|
MSWeight : 'a schunk measure
type 'a t
=
|
Zero of
{
default : 'a;
}
|
One of
{
default : 'a;
x : 'a;
}
|
Short of
{
default : 'a;
a : 'a array;
}
|
Level of
{
weight : Sek__.PrivateSignatures.weight;
front : 'a schunk;
middle : 'a schunk t;
back : 'a schunk;
}
This is the structure of a shareable sequence.
val create : 'a -> 'a t
create default
is an empty sequence.
val make : 'a -> Sek__.PublicTypeAbbreviations.length -> 'a -> Sek__.PrivateSignatures.owner -> 'a t
make default n v o
creates a sequence that consists ofn
copies of the valuev
. This sequence has depth0
.
val init : 'a -> Sek__.PublicTypeAbbreviations.length -> (Sek__.PublicTypeAbbreviations.index -> 'a) -> Sek__.PrivateSignatures.owner -> 'a t
init default n f o
creates a sequence that consists of the values produced by the callsf 0
,f 1
, ...f (n-1)
, in this order. This sequence has depth0
.
val nonempty_level : Sek__.PrivateSignatures.pov -> Sek__.PrivateSignatures.weight -> 'a schunk -> 'a schunk t -> 'a schunk -> 'a t
nonempty_level pov weight this middle that
constructs a nonempty sequence whose front (resp. back) isthis
, whose middle ismiddle
, and whose back (resp. front) isthat
.weight
must be the total weight of the elements in the sequence, and must be nonzero.
val create_middle : 'a -> 'a schunk t
val default : 'a t -> 'a
default s
returns a default element. (This element was provided as a default element in one of the operations that contributed to the construction ofs
.)
val weight : 'a t -> Sek__.PrivateSignatures.weight
weight s
is the total weight of the elements of the sequences
.
val is_empty : 'a t -> bool
is_empty s
determines whether the sequences
is empty.
val dummy : 'a t -> 'a schunk
dummy s
extracts a dummy schunk out ofs
, if possible; otherwise, it creates a fresh one.
val check : 'a t -> 'a measure -> Sek__.PrivateSignatures.owner -> Sek__.PublicTypeAbbreviations.depth -> unit
check s m o depth
verifies that the sequences
is valid with respect to measurem
, ownero
, and depthdepth
.
val check_middle : 'a schunk t -> 'a measure -> Sek__.PrivateSignatures.owner -> Sek__.PublicTypeAbbreviations.depth -> unit
check_middle middle m o depth
verifies that the sequencemiddle
is valid with respect to measurem
, ownero
, and depthdepth
. This includes checking that it is a valid sequence, checking that its elements are valid schunks, and verifing that the density invariant holds.
val push : Sek__.PrivateSignatures.pov -> 'a t -> 'a -> 'a measure -> Sek__.PrivateSignatures.owner -> Sek__.PublicTypeAbbreviations.depth -> 'a t
push pov s x m o depth
constructs and returns a new sequence obtained by pushing the elementx
onto the front or back end of the sequences
.
val pop : Sek__.PrivateSignatures.pov -> 'a t -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a * 'a t
If the sequence
s
is nonempty, thenpop pov s m o
returns a pair of the elementx
found at the front or back end of the sequences
and of the sequences
deprived ofx
. If the sequences
is empty, the exceptionEmpty
is raised.
val peek : Sek__.PrivateSignatures.pov -> 'a t -> 'a
If the sequence
s
is nonempty, thenpeek pov s
reads the elementx
found at the front or back end of the sequences
and returnsx
. If the sequences
is empty, the exceptionEmpty
is raised.
val get : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.weight * 'a
get s i m
is equivalent tolet s1, x, s2 = three_way_split s i m o in (i - weight s1, x)
. Thus, it returns a pair of the elementx
within which the weighti
falls and the indexi
minus the weight of the elements located towards the left ofx
.
val set : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a -> 'a t
set s i m o x
returns a new sequence obtained by replacing the element within which the weighti
falls with the new elementx
. The old and new element must have the same weight.
val update : 'a measure -> Sek__.PrivateSignatures.owner -> 'a Sek__.PrivateSignatures.update -> 'a t Sek__.PrivateSignatures.update
update m o f s i
applies the updatef
at weight-indexi
in the sequences
. The update functionf
is itself parameterized with the weight-index at which the update should be applied.
val fuse_back : 'a schunk t -> 'a schunk -> Sek__.PrivateSignatures.owner -> Sek__.PublicTypeAbbreviations.depth -> 'a schunk t
fuse_back middle p o depth
pushes the schunkp
onto the back ofmiddle
, which is a sequence of schunks. If possible, the last schunk of the sequence and the schunkp
are fused into a single schunk. By convention, passdepth
, notdepth + 1
--fuse_back
takes care of adding one.
val fuse : 'a schunk t -> 'a schunk t -> Sek__.PrivateSignatures.owner -> Sek__.PublicTypeAbbreviations.depth -> 'a schunk t
fuse s1 s2 o depth
concatenates the sequencess1
ands2
, which are sequences of schunks. It attempts to fuse the last schunk ofs1
and the first schunk ofs2
, so as to preserve the fill invariant. By convention, passdepth
, notdepth + 1
--fuse
takes care of adding one.
val concat : 'a t -> 'a t -> Sek__.PrivateSignatures.owner -> Sek__.PublicTypeAbbreviations.depth -> 'a t
concat s1 s2 o depth
concatenates the sequencess1
ands2
.
val three_way_split : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a t * 'a * 'a t
three_way_split s i m o
splits the sequences
into a sequences1
, followed with an elementx
, followed with a sequences2
, such that the weighti
falls within the elementx
, that is,weight s1 <= i < weight s1 + apply m x
holds. The weighti
must be comprised between 0 included andweight s
excluded.
val take : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a t * 'a
take
is a specialized version ofthree_way_split
. Instead of returning a triples1, x, s2
, it returns a pairs1, x
.
val drop : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a * 'a t
drop
is a specialized version ofthree_way_split
. Instead of returning a triples1, x, s2
, it returns a pairx, s2
.
val to_array : 'a t -> 'a array
to_array s
returns a fresh array whose elements are the elements of the sequences
.
val of_array_segment : 'a -> 'a array -> Sek__.PublicTypeAbbreviations.index -> Sek__.PublicTypeAbbreviations.length -> Sek__.PrivateSignatures.owner -> 'a t
of_array_segment default a head size o
creates a sequence out of the array segment defined by the arraya
, the start indexhead
, and the sizesize
. This function only makes sense at depth0
.
val iter : Sek__.PrivateSignatures.pov -> ('a -> unit) -> 'a t -> unit
iter pov f s
applies the functionf
in turn to every element in the sequences
, in the order specified by the point-of-viewpov
.
val iter_segments : Sek__.PrivateSignatures.pov -> 'a t -> 'a Sek__.PublicTypeAbbreviations.segments
iter_segments pov s
returns a sequence of array segments that store the data of the sequences
.