structure Network.HTTP2.HPACK.DecodeResult (α : Type) : Type

Decode result: parsed value and the number of bytes consumed.

• value : α

  The decoded value.

• consumed : Nat

  Number of bytes consumed from input.

@[implicit_reducible]

instance Network.HTTP2.HPACK.instReprDecodeResult {α✝ : Type} [Repr α✝] : Repr (DecodeResult α✝)

Equations

• Network.HTTP2.HPACK.instReprDecodeResult = { reprPrec := Network.HTTP2.HPACK.instReprDecodeResult.repr }

def Network.HTTP2.HPACK.instReprDecodeResult.repr {α✝ : Type} [Repr α✝] : DecodeResult α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.HPACK.decodeInteger (bs : ByteArray) (offset prefixBits : Nat) : Option (DecodeResult Nat)

Decode an integer with the given prefix size (1-8 bits). Returns the decoded integer and number of bytes consumed.

$$\text{decodeInteger} : \text{ByteArray} \to \text{Nat} \to \text{Nat} \to \text{Option}(\text{DecodeResult}(\text{Nat}))$$

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.HPACK.decodeInteger.go (bs : ByteArray) (offset pos value shift fuel : Nat) : Option (DecodeResult Nat)

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP2.HPACK.decodeInteger.go bs offset pos value shift 0 = none

def Network.HTTP2.HPACK.decodeString (bs : ByteArray) (offset : Nat) : Option (DecodeResult String)

Decode a string from HPACK format. The high bit of the first byte indicates Huffman encoding.

$$\text{decodeString} : \text{ByteArray} \to \text{Nat} \to \text{Option}(\text{DecodeResult}(\text{String}))$$

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP2.HPACK.decodeHeaders (dt : DynamicTable) (bs : ByteArray) : Option (List HeaderField × DynamicTable)

Decode a complete HPACK header block into a list of header fields. Updates the dynamic table as fields with indexing are decoded.

$$\text{decodeHeaders} : \text{DynamicTable} \to \text{ByteArray} \to \text{Option}(\text{List}(\text{HeaderField}) \times \text{DynamicTable})$$

Equations

• Network.HTTP2.HPACK.decodeHeaders dt bs = Network.HTTP2.HPACK.decodeHeaders.go bs 0 dt [] (bs.size + 1)

def Network.HTTP2.HPACK.decodeHeaders.go (bs : ByteArray) (offset : Nat) (dt : DynamicTable) (acc : List HeaderField) (fuel : Nat) : Option (List HeaderField × DynamicTable)

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP2.HPACK.decodeHeaders.go bs offset dt acc 0 = some (acc.reverse, dt)