Parameter Make.1-SChunk
module EChunk : Sek__.PrivateSignatures.ECHUNK
type 'a chunk
= 'a EChunk.t
type view
= EChunk.View.view
type 'a t
A schunk is either shared or uniquely owned. When it is shared, it cannot be modified. When it is uniquely owned, it can be modified. As far as the user is concerned, this is transparent: the user does not decide whether to allocate a new schunk or modify an existing schunk in place.
However, the user is responsible for presenting an appropriate owner identity
o
when creating or using a schunk. (This will not be repeated in the specification of every operation.)A schunk records the identity of its creator. It is considered uniquely owned by its creator unless its creator is
Owner.none
, in which case it is considered shared. Later on, when an operation is performed on this schunk with identityo
, the functionOwner.is_uniquely_owned
is used to compare the schunk's creator witho
. The outcome of this test determines whether the schunk is uniquely owned or shared, therefore can or cannot be modified in place.
type 'a measure
=
|
MUnit : 'a measure
|
MSWeight : 'a t measure
Being able to test whether a measure is the unit measure -- which maps every element to a weight of one -- is useful. This allows optimizations in some functions, such as
reach
. For this reason, instead of defining the type'a measure
as a synonym for'a -> weight
, we define it as a (generalized) algebraic data type.
val apply : 'a measure -> 'a -> Sek__.PrivateSignatures.weight
apply m x
applies the measurex
to the elementx
and returns its weight.
val check : 'a measure -> Sek__.PrivateSignatures.owner -> 'a t -> unit
check m o p
verifies that the schunkp
is valid, i.e., that its internal invariant is satisfied. This check is relative to the measurem
and to the identityo
with which this schunk is accessed.
val is_uniquely_owned : 'a t -> Sek__.PrivateSignatures.owner -> bool
is_uniquely_owned p o
determines whether the schunkp
is uniquely owned by ownero
.
val default : 'a t -> 'a
default p
returns the default element that was provided when the schunkp
was created.
val length : 'a t -> Sek__.PublicTypeAbbreviations.length
length p
is the length of the sequencep
. A dummy schunk has length 0.
val weight : 'a t -> Sek__.PrivateSignatures.weight
weight p
is the total weight of the elements of the sequencep
.
val data : 'a t -> 'a array
data p
is the raw array that underlies the chunkp
. This function is dangerous; it should be used only to implement efficient iterators.
val capacity : 'a t -> Sek__.PublicTypeAbbreviations.capacity
capacity p
is the capacity of the chunkp
, that is, the maximum number of elements that this chunk can hold.
val is_empty : 'a t -> bool
is_empty p
is equivalent tolength p = 0
.
val is_full : 'a t -> bool
is_full p
is equivalent tolength p = capacity p
.
val create : 'a -> Sek__.PublicTypeAbbreviations.capacity -> Sek__.PrivateSignatures.owner -> 'a t
create d n v
creates a schunk with default elementd
, capacityn
, and ownero
.
val dummy : 'a -> 'a t
dummy d
creates a dummy (invalid!) schunk.
val is_dummy : 'a t -> bool
is_dummy p
tells whetherp
is a dummy schunk, that is, whether it has been built bydummy
.
val copy : 'a t -> Sek__.PrivateSignatures.owner -> 'a t
copy p o
creates a copy of the schunkp
. The copy is owned byo
.
val of_chunk_destructive : 'a chunk -> Sek__.PrivateSignatures.owner -> 'a t
of_chunk_destructive c o
creates a new schunk, based on the ephemeral chunkc
, with ownero
. The ownership of the chunkc
is lost. The elements of the chunkc
are assumed to have unit weight.
val to_chunk : 'a t -> Sek__.PrivateSignatures.owner -> 'a chunk
to_chunk p o
converts the schunkp
to an ephemeral chunk. Ifp
is uniquely owned byo
, then it is destroyed and its support is re-used directly; no copy is required. Ifp
is shared, then a copy is performed and a new chunk is allocated. Likeof_chunk
, this operation assumes that every element has unit weight.
val of_array_segment : 'a -> Sek__.PublicTypeAbbreviations.capacity -> 'a array -> Sek__.PublicTypeAbbreviations.index -> Sek__.PublicTypeAbbreviations.length -> Sek__.PrivateSignatures.owner -> 'a t
of_array_segment d n a head size o
creates a schunk with ownero
by copying data from the array segment defined by the arraya
, the start indexhead
, and the sizesize
. The schunk has capacityn
and default valued
.size
must be less than or equal ton
. The elements are assumed to have unit weight.
val make : 'a -> Sek__.PublicTypeAbbreviations.capacity -> Sek__.PublicTypeAbbreviations.length -> 'a -> Sek__.PrivateSignatures.owner -> 'a t
make d n k v o
creates a schunk that containsk
copies of the valuev
. The schunk has default valued
, capacityn
, and ownero
. The elements are assumed to have unit weight.
val init : 'a -> Sek__.PublicTypeAbbreviations.capacity -> Sek__.PublicTypeAbbreviations.length -> Sek__.PublicTypeAbbreviations.index -> (Sek__.PublicTypeAbbreviations.index -> 'a) -> Sek__.PrivateSignatures.owner -> 'a t
init d n k i f o
creates a fresh schunk that contains the sequence of values produced by the callsf i
,f (i+1)
, ...f (i+k-1)
, in this order. The schunk has default valued
, capacityn
, and ownero
. The elements are assumed to have unit weight.
val peek : Sek__.PrivateSignatures.pov -> 'a t -> 'a
peek pov p
returns the first or last element of the schunkp
, depending on the point-of-viewpov
.p
must be nonempty.
val push : Sek__.PrivateSignatures.pov -> 'a t -> 'a -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a t
push pov p x m v
pushes the elementx
at the front (resp. back) of the schunkp
, depending on the point-of-viewpov
.p
must not be full. Eitherp
is updated in place, or a new schunk is allocated; this is transparent.
val pop : Sek__.PrivateSignatures.pov -> 'a t -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a * 'a t
pop pov p m v
pops an element off the front (resp. back) of the schunkp
, depending on the point-of-viewpov
.p
must not be empty. Eitherp
is updated in place, or a new schunk is allocated; this is transparent.
val get : 'a t -> Sek__.PublicTypeAbbreviations.index -> 'a
get p i
returns the element found at indexi
in the sequencep
.i
must be comprised between 0 included andlength p
excluded.
val concat : 'a t -> 'a t -> Sek__.PrivateSignatures.owner -> 'a t
concat p1 p2 o
concatenates the sequencesp1
andp2
, yielding a sequence. The schunksp1
andp2
must have the same capacity. The length of the concatenated sequence must not exceed this capacity: that is,length p1 + length p2 <= capacity p1
must hold.
val reach : 'a measure -> 'a t -> Sek__.PrivateSignatures.weight -> Sek__.PrivateSignatures.weight * Sek__.PublicTypeAbbreviations.index
reach m p w
returns a pair of the total weight of the elements that precedex
in the sequencep
and the index in the sequence of the elementx
within which the weightw
falls. The weight indexw
must be comprised between 0 included andweight p
excluded.
val reach_from : 'a measure -> 'a t -> Sek__.PublicTypeAbbreviations.index -> Sek__.PrivateSignatures.weight -> Sek__.PrivateSignatures.weight -> Sek__.PrivateSignatures.weight * Sek__.PublicTypeAbbreviations.index
reach_from m p pindex pwindex w
is a generalization ofreach
. Compared withreach
, it takes two extra arguments, an indexpindex
and a corresponding weight indexpwindex
, which describe a starting position in the schunkp
. (pwindex
must be consistent withpindex
: that is, it must be the sum of the weights of the elements whose index is less thanpindex
.) The schunkp
is scanned from the positionpindex
: it is scanned forward ifpwindex <= w
holds, and backwards ifw < pwindex
holds.
val get_by_weight : 'a measure -> 'a t -> Sek__.PrivateSignatures.weight -> Sek__.PrivateSignatures.weight * 'a
get_by_weight m p w
finds the elementx
at weight-indexw
in the schunkp
. It returns a pair of an adjusted weight-index (namelyw
minus the weight of the elements that precedex
) and the elementx
.
val update_by_weight : 'a measure -> Sek__.PrivateSignatures.owner -> 'a Sek__.PrivateSignatures.update -> 'a t Sek__.PrivateSignatures.update
update_by_weight m o f p w
finds the elementx
at weight-indexw
in the schunkp
, adjusts the weight-indexw
by subtracting from it the weight of the elements that precedex
, then passesx
andw
to the update functionf
, which produces a new elementx'
. The elementx
is then replaced withx'
in the schunk. The elementsx
andx'
must have the same weight.
val three_way_split : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a t * 'a * 'a t
three_way_split p i m o
splits the sequencep
into a sequencep1
, followed with an elementx
, followed with a sequencep2
, such that the weighti
falls within the elementx
, that is,weight p1 <= i < weight p1 + apply m x
holds. The weighti
must be comprised between 0 included andweight p
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 triplep1, x, p2
, it returns a pairp1, 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 triplep1, x, p2
, it returns a pairx, p2
.
val remaining_length : Sek__.PrivateSignatures.pov -> Sek__.PublicTypeAbbreviations.index -> 'a t -> Sek__.PublicTypeAbbreviations.length
remaining_length pov i p
returns the number of elements found ahead of the element at indexi
(included).
val segment : Sek__.PrivateSignatures.pov -> Sek__.PublicTypeAbbreviations.index -> Sek__.PublicTypeAbbreviations.length -> 'a t -> 'a Sek__.PublicTypeAbbreviations.segment
segment pov i k p
returns the description of a segment of at mostk
consecutive elements, starting from the one at indexi
and progressing in the directionpov
. The argumentk
must be no greater thanremaining_length pov i p
.For additional details, see the documentation of
segment
in the signatureECHUNK
above.
val segment_max : Sek__.PrivateSignatures.pov -> Sek__.PublicTypeAbbreviations.index -> 'a t -> 'a Sek__.PublicTypeAbbreviations.segment
segment_max pov i s
is a shorthand forsegment pov i k s
wherek
takes its maximum permitted value, that is,remaining_length pov i p
.
val iter_segments : Sek__.PrivateSignatures.pov -> 'a t -> 'a Sek__.PublicTypeAbbreviations.segments
iter_segments pov p
returns a sequence of one or two array segments that store the data of the schunkp
.
val iteri_segments_front : 'a t -> (Sek__.PublicTypeAbbreviations.index -> ('a array * Sek__.PublicTypeAbbreviations.index * Sek__.PublicTypeAbbreviations.length) -> unit) -> unit
iteri_segments_front
iterates over the segments in a schunk, while maintaining the index (with respect to the schunk) of the head of the current segment. It is restricted to theFront
direction.