Module Imandra_util.IO_chunk

Chunks for IO

type t = private {
mutable bs : bytes;

buffer

mutable i : int;

offset of subslice

mutable len : int;

length of subslice

}

A single chunk, for writing or reading.

It can be used as a buffer, with active slice b.[i … i+len-1], or just as a string-like object in an output list.

Some day we might use iovec :-)

type chunk = t
val bytes_len : t -> int

Size of underlying buffer

val len : t -> int

Length of the slice

val free_len : t -> int

Space remaining at the end

val of_bytes : bytes -> t
val of_string : string -> t
val sprintf : ('a, unit, string, t) Stdlib.format4 -> 'a
val to_string : t -> string

Extract content as a string

val clear : t -> unit

Make the chunk empty

val map_buf : f:(bytes -> int -> int -> 'a) -> t -> 'a
val extend_buf : f:(bytes -> int -> int -> int) -> t -> int

extend_buf buf ~f calls f on the free slice at the end of buf, and assumes the return value of f is how many bytes were added.

val create : int -> t

Create a chunk with given bytes_len

val get_char : t -> char

Read and consume one char

val consume : t -> int -> unit

Consume n bytes from the buffer.

val is_empty : t -> bool

Is the buffer empty (i.e. len = 0)?

module Pool : sig ... end
val ensure_free_len : ?⁠pool:Pool.t -> t -> int -> unit

Make sure free_len ch is at least n bytes

val append : ?⁠pool:Pool.t -> t -> into:t -> unit

append c ~into:c2 appends the content of c to c2. Might reallocate the content of c2.

parameter pool

can be used for reallocation

val append_str : ?⁠pool:Pool.t -> t -> string -> unit
module FD : sig ... end