Kot.Buffer8include Signatures.BUFFERval empty : 'a bufferval length : 'a buffer -> intval is_empty : 'a buffer -> boolval first : 'a buffer -> 'afirst b returns the first element of the buffer b, which must be nonempty. It is equivalent to fst (pop b).
val last : 'a buffer -> 'alast b returns the last element of the buffer b, which must be nonempty. It is equivalent to snd (eject b).
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a buffer -> 'bval fold_right : ('a -> 'b -> 'b) -> 'a buffer -> 'b -> 'bval doubleton : 'a -> 'a -> 'a bufferdoubleton x y constructs a buffer whose length is 2 and whose elements are x and y.
val has_length_3 : 'a buffer -> boolhas_length_3 b is equivalent to length b = 3.
val has_length_6 : 'a buffer -> boolhas_length_6 b is equivalent to length b = 6.
val has_length_8 : 'a buffer -> boolhas_length_8 b is equivalent to length b = 8.
move_left_1_33 b1 b2 requires the buffers b1 and b2 to have length 3. One element is moved from b2 to b1. The concatenation of the buffers b1 and b2 is unchanged.
move_right_1_33 b1 b2 requires the buffers b1 and b2 to have length 3. One element is moved from b1 to b2. The concatenation of the buffers b1 and b2 is unchanged.
double_move_left_323 expects three buffers whose lengths are 3, 2, and 3. It moves one element from the middle buffer into the first buffer and one element from the last buffer into the middle buffer.
val double_move_right_323 :
'a buffer ->
'a buffer ->
'a buffer ->
'a buffer * 'a buffer * 'a bufferdouble_move_right_323 expects three buffers whose lengths are 3, 2, and 3. It moves one element from the first buffer into the middle buffer and one element from the middle buffer into the last buffer.
double_move_left_32x expects three buffers whose lengths are 3, 2, and X, where X is comprised between 4 and 6. It moves one element from the middle buffer into the first buffer and one element from the last buffer into the middle buffer.
val double_move_right_x23 :
'a buffer ->
'a buffer ->
'a buffer ->
'a buffer * 'a buffer * 'a bufferdouble_move_right_x23 expects three buffers whose lengths are X, 2, and 3, where X is comprised between 4 and 6. It moves one element from the first buffer into the middle buffer and one element from the middle buffer into the last buffer.
concat23 concatenates two buffers whose lengths are 2 and 3.
concat32 concatenates two buffers whose lengths are 3 and 2.
concat323 concatenates three buffers whose lengths are 3, 2, and 3.
split23l expects a buffer whose length is comprised between 2 and 5. This buffer is split into two buffers b1 and b2 such that b1 has length 2 or 3 and b2 has length 0 or 2 or 3.
split23r expects a buffer whose length is comprised between 2 and 5. This buffer is split into two buffers b1 and b2 such that b1 has length 0 or 2 or 3 and b2 has length 2 or 3.
split8 expects a buffer of length 8. This buffer is split into three buffers whose lengths are 3, 2, and 3.