Module type PrivateSignatures.ECHUNK

A chunk is a mutable object, which represents a sequence of elements of type 'a. A chunk has a fixed capacity, which it cannot exceed.

check c verifies that the chunk c is valid, i.e., that its internal invariant is satisfied.

create d n creates a fresh chunk whose capacity is n. The default element d is used to initialize empty slots. If overwrite_empty_slots is true, then it is also used to overwrite a slot that becomes empty, e.g., in pop and carve_back.

make d n k v creates a fresh chunk whose default element is d, whose capacity is n, and which contains a sequence of k copies of the value v. The integer k must be no greater than n.

init d n k i f creates a fresh chunk whose default element is d, whose capacity is n, and which contains the sequence of values produced by the calls f i, f (i+1), ... f (i+k-1), in this order. The integer k must be no greater than n.

dummy d creates a dummy (invalid!) chunk, which can be used as a default element when creating a chunk of chunks. This dummy chunk is invalid and must not be used. As an exception to this rule, it is permitted to apply is_empty and is_full to a dummy chunk; in that case, they both return true.

is_dummy c tells whether c is a dummy chunk, that is, whether it has been built by dummy.

of_array_segment d n a head size creates a chunk by copying data from the array segment defined by the array a, the start index head, and the size size. The chunk has capacity n and default value d. size must be less than or equal to n.

default c returns the default element that was provided when the chunk c was created.

length c is the length of the sequence c.

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

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

is_empty c is equivalent to length c = 0.

is_full c is equivalent to length c = capacity c.

is_empty_or_dummy c is equivalent to is_empty c || is_dummy c.

is_full_or_dummy c is equivalent to is_full c || is_dummy c.

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

set c i x replaces the element found at index i in the sequence c with the value x. i must be comprised between 0 included and length c excluded.

peek pov c returns the first or last element of the chunk c, depending on the point-of-view pov. The chunk c must be nonempty.

push pov c x inserts the element x at the front or back of the chunk c, depending on the point-of-view pov. The chunk c must not be full.

pop pov c extracts and returns the first or last element of the chunk c, depending on the point-of-view pov. The chunk c must be nonempty.

copy c creates and returns a copy of the chunk c. The copy is identical to the original chunk, but is disjoint from c, so an update to the copy does not affect c.

clear c updates the chunk c so that it represents the empty sequence.

carve_back c i splits the sequence c at index i. The index i must be comprised between 0 included and length c included. After this operation, the chunk c is truncated and represents the first part of the sequence, up to index i excluded. A new chunk, which represents the second part of the sequence, beginning at index i, is returned.

take c i truncates the sequence c at index i. The index i must be comprised between 0 included and length c included. After this operation, the chunk c is truncated and represents the first part of the sequence, up to index i excluded.

drop c i truncates the sequence c at index i. The index i must be comprised between 0 included and length c included. After this operation, the chunk c is truncated and represents the second part of the sequence, beginning at index i.

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

view c is a view that covers all of the elements currently found in the chunk c.

iter_segments pov c returns a sequence of up to two array segments that cover the chunk c. It is analogous to View.iter_segments above, but applies to the entire chunk (not to a view). It is permitted to apply iter_segments to a dummy chunk.