Module type PrivateSignatures.SCHUNK

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 identity o, the function Owner.is_uniquely_owned is used to compare the schunk's creator with o. The outcome of this test determines whether the schunk is uniquely owned or shared, therefore can or cannot be modified in place.

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.

apply m x applies the measure x to the element x and returns its weight.

check m o p verifies that the schunk p is valid, i.e., that its internal invariant is satisfied. This check is relative to the measure m and to the identity o with which this schunk is accessed.

is_uniquely_owned p o determines whether the schunk p is uniquely owned by owner o.

default p returns the default element that was provided when the schunk p was created.

length p is the length of the sequence p. A dummy schunk has length 0.

weight p is the total weight of the elements of the sequence p.

data p is the raw array that underlies the chunk p. This function is dangerous; it should be used only to implement efficient iterators.

capacity p is the capacity of the chunk p, that is, the maximum number of elements that this chunk can hold.

is_empty p is equivalent to length p = 0.

is_full p is equivalent to length p = capacity p.

create d n v creates a schunk with default element d, capacity n, and owner o.

dummy d creates a dummy (invalid!) schunk.

is_dummy p tells whether p is a dummy schunk, that is, whether it has been built by dummy.

support p returns the chunk that supports the schunk p.

copy p o creates a copy of the schunk p. The copy is owned by o.

of_chunk_destructive c o creates a new schunk, based on the ephemeral chunk c, with owner o. The ownership of the chunk c is lost. The elements of the chunk c are assumed to have unit weight.

to_chunk p o converts the schunk p to an ephemeral chunk. If p is uniquely owned by o, then it is destroyed and its support is re-used directly; no copy is required. If p is shared, then a copy is performed and a new chunk is allocated. Like of_chunk, this operation assumes that every element has unit weight.

of_array_segment d n a head size o creates a schunk with owner o by copying data from the array segment defined by the array a, the start index head, and the size size. The schunk has capacity n and default value d. size must be less than or equal to n. The elements are assumed to have unit weight.

make d n k v o creates a schunk that contains k copies of the value v. The schunk has default value d, capacity n, and owner o. The elements are assumed to have unit weight.

init d n k i f o creates a fresh schunk that contains the sequence of values produced by the calls f i, f (i+1), ... f (i+k-1), in this order. The schunk has default value d, capacity n, and owner o. The elements are assumed to have unit weight.

peek pov p returns the first or last element of the schunk p, depending on the point-of-view pov. p must be nonempty.

push pov p x m v pushes the element x at the front (resp. back) of the schunk p, depending on the point-of-view pov. p must not be full. Either p is updated in place, or a new schunk is allocated; this is transparent.

pop pov p m v pops an element off the front (resp. back) of the schunk p, depending on the point-of-view pov. p must not be empty. Either p is updated in place, or a new schunk is allocated; this is transparent.

get p i returns the element found at index i in the sequence p. i must be comprised between 0 included and length p excluded.

concat p1 p2 o concatenates the sequences p1 and p2, yielding a sequence. The schunks p1 and p2 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.

reach m p w returns a pair of the total weight of the elements that precede x in the sequence p and the index in the sequence of the element x within which the weight w falls. The weight index w must be comprised between 0 included and weight p excluded.

reach_from m p pindex pwindex w is a generalization of reach. Compared with reach, it takes two extra arguments, an index pindex and a corresponding weight index pwindex, which describe a starting position in the schunk p. (pwindex must be consistent with pindex: that is, it must be the sum of the weights of the elements whose index is less than pindex.) The schunk p is scanned from the position pindex: it is scanned forward if pwindex <= w holds, and backwards if w < pwindex holds.

get_by_weight m p w finds the element x at weight-index w in the schunk p. It returns a pair of an adjusted weight-index (namely w minus the weight of the elements that precede x) and the element x.

update_by_weight m o f p w finds the element x at weight-index w in the schunk p, adjusts the weight-index w by subtracting from it the weight of the elements that precede x, then passes x and w to the update function f, which produces a new element x'. The element x is then replaced with x' in the schunk. The elements x and x' must have the same weight.

three_way_split p i m o splits the sequence p into a sequence p1, followed with an element x, followed with a sequence p2, such that the weight i falls within the element x, that is, weight p1 <= i < weight p1 + apply m x holds. The weight i must be comprised between 0 included and weight p excluded.

take is a specialized version of three_way_split. Instead of returning a triple p1, x, p2, it returns a pair p1, x.

drop is a specialized version of three_way_split. Instead of returning a triple p1, x, p2, it returns a pair x, p2.

remaining_length pov i p returns the number of elements found ahead of the element at index i (included).

segment pov i k p returns the description of a segment of at most k consecutive elements, starting from the one at index i and progressing in the direction pov. The argument k must be no greater than remaining_length pov i p.

For additional details, see the documentation of segment in the signature ECHUNK above.

segment_max pov i s is a shorthand for segment pov i k s where k takes its maximum permitted value, that is, remaining_length pov i p.

iter_segments pov p returns a sequence of one or two array segments that store the data of the schunk p.

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 the Front direction.

print is a schunk printer, parameterized with an element printer. It is intended to be used only while debugging.