Module EChunk.View

A view is an immutable object, which represents a certain range in a chunk. It can be thought of as a pair of a head index and a size.

head v is the head of the view v, that is, the index in the underlying chunk of the first element of the view v.

size v is the size of the view v, that is, the number of elements in this view.

check c v verifies that the view v is valid with respect to the chunk v, i.e., that its internal invariant is satisfied.

dummy is a dummy view. It may be invalid and must not be used in any way.

iter_segments pov (c, v) f returns a sequence of up to two array segments that cover the view v of the chunk c.

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

get c v i returns the element found at index i in the view v of the sequence c. v must be a valid view with respect to c, and i must be comprised between 0 included and size v excluded.

set c v i x replaces the element found at index i in the view v of the sequence c with x. v must be a valid view with respect to c, and i must be comprised between 0 included and size v excluded.

three_way_split c v i returns the element x found at index i in the view v of the sequence c, along with two views that cover the elements of v found left and right of x. v must be a valid view with respect to c, and i must be comprised between 0 included and size v excluded.

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

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

is_flush pov c v determines whether the front (resp. back) of the view v coincides with the front (resp. back) of the chunk c.

is_aligned c v determines whether the view v covers all of the sequence c. It is equivalent to is_flush Front c v && is_flush Back c v.

push pov c v is the view obtained by pushing one element in front of (resp. at the back of) the view v. The view v must not cover all of c.

pop pov c v is the view obtained by popping one element in front of (resp. at the back of) the view v. The view v must be nonempty.

restrict c v i k is the view obtained by restricting the view v to the subview defined by the relative index i and the length k.

copy pov c1 v1 c2 v2 copies the data in the view v1 of chunk c1 to the front (resp. back) of view v2 of c2, depending on the point-of-view pov. The view v1 and v2 must be valid with respect to the chunks c1 and c2, respectively. There must be enough room for the data, that is, size v1 + size v2 <= capacity c2 must hold. The function returns a view that is valid with respect to c2 and includes v2 plus the newly-copied data.

sub c v creates a new chunk that contains the data covered by the view v of the chunk c. The copied data is located in view v of the new chunk c', so Chunk.view c' is v.

iter pov f (c, v) applies the function f in turn to every element in view v of chunk c, in the order specified by the point-of-view pov.

fold_left f (c, v) seed applies the function f in turn to every element in view v of chunk c, while maintaining an accumulator.

segment pov i k c v 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 index i is relative to the view v: it must be in the interval [0, size v). The length k must be no greater than the number of elements between index i (included) and the end of the view v in the direction of iteration.

segment Front i k c v returns a triple (a, j, m) such that the elements of the view v in the interval [i, i + m) are stored in the array a in the segment [j, j + m).

segment Back i k c v returns a triple (a, j, m) such that the elements of the view v in the interval (i - m, i] are stored in the array a in the segment [j, j + m).

The value m is the maximal value such that m <= k and the elements starting at index i in the direction of iteration are stored consecutively in memory. If k > 0 holds, then it is guaranteed that m > 0 holds as well.

In the current implementation, all elements of a view can be covered by using at most two segments. Thus, after segment Front i k c v returns (a, j, m), either m = k holds and all elements of the view have been covered, or calling segment Front (i + k) (k - m) c returns a segment that covers all of the remaining elements of the view.

print is a view printer. It is intended to be used only while debugging.