Module `ShareableSequence.Make`

Parameters

Signature

type 'a schunk = 'a SChunk.t
type 'a measure = 'a SChunk.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 of n copies of the value v. This sequence has depth 0.

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 calls f 0, f 1, ... f (n-1), in this order. This sequence has depth 0.

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) is this, whose middle is middle, and whose back (resp. front) is that. 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 of s.)

val weight : 'a t -> Sek__.PrivateSignatures.weight: weight s is the total weight of the elements of the sequence s.

val is_empty : 'a t -> bool: is_empty s determines whether the sequence s is empty.

val dummy : 'a t -> 'a schunk: dummy s extracts a dummy schunk out of s, 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 sequence s is valid with respect to measure m, owner o, and depth depth.

val check_middle : 'a schunk t -> 'a measure -> Sek__.PrivateSignatures.owner -> Sek__.PublicTypeAbbreviations.depth -> unit: check_middle middle m o depth verifies that the sequence middle is valid with respect to measure m, owner o, and depth depth. 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 element x onto the front or back end of the sequence s.

val pop : Sek__.PrivateSignatures.pov -> 'a t -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a * 'a t: If the sequence s is nonempty, then pop pov s m o returns a pair of the element x found at the front or back end of the sequence s and of the sequence s deprived of x. If the sequence s is empty, the exception Empty is raised.

val peek : Sek__.PrivateSignatures.pov -> 'a t -> 'a: If the sequence s is nonempty, then peek pov s reads the element x found at the front or back end of the sequence s and returns x. If the sequence s is empty, the exception Empty is raised.

val get : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.weight * 'a: get s i m is equivalent to let s1, x, s2 = three_way_split s i m o in (i - weight s1, x). Thus, it returns a pair of the element x within which the weight i falls and the index i minus the weight of the elements located towards the left of x.

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 weight i falls with the new element x. 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 update f at weight-index i in the sequence s. The update function f 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 schunk p onto the back of middle, which is a sequence of schunks. If possible, the last schunk of the sequence and the schunk p are fused into a single schunk. By convention, pass depth, not depth + 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 sequences s1 and s2, which are sequences of schunks. It attempts to fuse the last schunk of s1 and the first schunk of s2, so as to preserve the fill invariant. By convention, pass depth, not depth + 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 sequences s1 and s2.

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 sequence s into a sequence s1, followed with an element x, followed with a sequence s2, such that the weight i falls within the element x, that is, weight s1 <= i < weight s1 + apply m x holds. The weight i must be comprised between 0 included and weight s excluded.

val take : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a t * 'a: take is a specialized version of three_way_split. Instead of returning a triple s1, x, s2, it returns a pair s1, x.

val drop : 'a t -> Sek__.PrivateSignatures.weight -> 'a measure -> Sek__.PrivateSignatures.owner -> 'a * 'a t: drop is a specialized version of three_way_split. Instead of returning a triple s1, x, s2, it returns a pair x, s2.

val to_array : 'a t -> 'a array: to_array s returns a fresh array whose elements are the elements of the sequence s.

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 array a, the start index head, and the size size. This function only makes sense at depth 0.

val iter : Sek__.PrivateSignatures.pov -> ('a -> unit) -> 'a t -> unit: iter pov f s applies the function f in turn to every element in the sequence s, in the order specified by the point-of-view pov.

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 sequence s.

val print : 'a measure -> ('a -> PPrint.document) -> 'a t -> PPrint.document: print is a sequence printer, parameterized with an element printer. It is intended to be used only while debugging.