ChunkedBuffer

This module provides an efficient way to concatenate multiple ByteArrays by deferring the actual concatenation until necessary. This is particularly useful in HTTP response building and streaming scenarios where data is accumulated incrementally.

structure Std.Http.Internal.ChunkedBuffer : Type

A structure that accumulates multiple ByteArrays efficiently by tracking them in an array and maintaining the total size. This allows building large buffers without repeated allocations and copies.

• data : Array ByteArray

  The accumulated byte arrays.

• size : Nat

  The total size in bytes of all accumulated arrays

@[inline]

def Std.Http.Internal.ChunkedBuffer.empty : ChunkedBuffer

An empty ChunkedBuffer.

Equations

• Std.Http.Internal.ChunkedBuffer.empty = { data := #[], size := 0 }

@[inline]

def Std.Http.Internal.ChunkedBuffer.push (c : ChunkedBuffer) (b : ByteArray) : ChunkedBuffer

Append a single ByteArray to the ChunkedBuffer.

Equations

• c.push b = { data := c.data.push b, size := c.size + b.size }

@[inline]

def Std.Http.Internal.ChunkedBuffer.write (buffer : ChunkedBuffer) (data : ByteArray) : ChunkedBuffer

Writes a ByteArray to the ChunkedBuffer.

Equations

• buffer.write data = buffer.push data

@[inline]

def Std.Http.Internal.ChunkedBuffer.append (buffer data : ChunkedBuffer) : ChunkedBuffer

Writes a ChunkedBuffer to the ChunkedBuffer.

Equations

• buffer.append data = { data := buffer.data ++ data.data, size := buffer.size + data.size }

@[inline]

def Std.Http.Internal.ChunkedBuffer.writeChar (buffer : ChunkedBuffer) (data : Char) : ChunkedBuffer

Writes a Char to the ChunkedBuffer. Only the low byte is written (Char.toUInt8), so this is only correct for ASCII characters.

Equations

• buffer.writeChar data = buffer.push { data := #[data.toUInt8] }

@[inline]

def Std.Http.Internal.ChunkedBuffer.writeString (buffer : ChunkedBuffer) (data : String) : ChunkedBuffer

Writes a String to the ChunkedBuffer.

Equations

• buffer.writeString data = buffer.push data.toUTF8

@[inline]

def Std.Http.Internal.ChunkedBuffer.toByteArray (cb : ChunkedBuffer) : ByteArray

Turn the combined structure into a single contiguous ByteArray.

Equations

• cb.toByteArray = if h : 1 = cb.data.size then cb.data[0] else Array.foldl (fun (x1 x2 : ByteArray) => x1 ++ x2) (ByteArray.emptyWithCapacity cb.size) cb.data

@[inline]

def Std.Http.Internal.ChunkedBuffer.ofByteArray (bs : ByteArray) : ChunkedBuffer

Build from a ByteArray directly.

Equations

• Std.Http.Internal.ChunkedBuffer.ofByteArray bs = { data := #[bs], size := bs.size }

@[inline]

def Std.Http.Internal.ChunkedBuffer.ofArray (bs : Array ByteArray) : ChunkedBuffer

Build from an array of ByteArrays directly.

Equations

• Std.Http.Internal.ChunkedBuffer.ofArray bs = { data := bs, size := Array.foldl (fun (x1 : Nat) (x2 : ByteArray) => x1 + x2.size) 0 bs }

@[inline]

def Std.Http.Internal.ChunkedBuffer.isEmpty (bb : ChunkedBuffer) : Bool

Checks whether the buffer is empty.

Equations

• bb.isEmpty = decide (bb.size = 0)

@[implicit_reducible]

instance Std.Http.Internal.ChunkedBuffer.instInhabited : Inhabited ChunkedBuffer

Equations

• Std.Http.Internal.ChunkedBuffer.instInhabited = { default := Std.Http.Internal.ChunkedBuffer.empty }

@[implicit_reducible]

instance Std.Http.Internal.ChunkedBuffer.instEmptyCollection : EmptyCollection ChunkedBuffer

Equations

• Std.Http.Internal.ChunkedBuffer.instEmptyCollection = { emptyCollection := Std.Http.Internal.ChunkedBuffer.empty }

@[implicit_reducible]

instance Std.Http.Internal.ChunkedBuffer.instCoeByteArray : Coe ByteArray ChunkedBuffer

Equations

• Std.Http.Internal.ChunkedBuffer.instCoeByteArray = { coe := Std.Http.Internal.ChunkedBuffer.ofByteArray }

@[implicit_reducible]

instance Std.Http.Internal.ChunkedBuffer.instCoeArrayByteArray : Coe (Array ByteArray) ChunkedBuffer

Equations

• Std.Http.Internal.ChunkedBuffer.instCoeArrayByteArray = { coe := Std.Http.Internal.ChunkedBuffer.ofArray }