Header Typeclass and Common Headers

This module defines the Header typeclass for typed HTTP headers and some common header parsers.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-representation-data-and-met

class Std.Http.Header (α : Type) : Type

Typeclass for typed HTTP headers that can be parsed from and serialized to header values.

• parse : Value → Option α

  Parses a header value into the typed representation.

• serialize : α → Name × Value

  Serializes the typed representation back to a name-value pair.

@[implicit_reducible]

instance Std.Http.instEncodeV11OfHeader {α : Type} [h : Header α] : Internal.Encode Version.v11 α

structure Std.Http.Header.ContentLength : Type

The Content-Length header, representing the size of the message body in bytes. Parses only valid natural number values.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-8.6-2

• length : Nat

  The content length in bytes.

def Std.Http.Header.instBEqContentLength.beq : ContentLength → ContentLength → Bool

@[implicit_reducible]

instance Std.Http.Header.instBEqContentLength : BEq ContentLength

def Std.Http.Header.instReprContentLength.repr : ContentLength → Nat → Format

@[implicit_reducible]

instance Std.Http.Header.instReprContentLength : Repr ContentLength

def Std.Http.Header.ContentLength.parse (v : Value) : Option ContentLength

Parses a content length header value.

def Std.Http.Header.ContentLength.serialize (h : ContentLength) : Name × Value

Serializes a content length header back to a name-value pair.

@[implicit_reducible]

instance Std.Http.Header.ContentLength.inst : Header ContentLength

def Std.Http.Header.TransferEncoding.Validate (codings : Array String) : Bool

Validates the chunked placement rules for the Transfer Encoding header. Returns false if the encoding list violates the constraints.

Reference: https://www.rfc-editor.org/rfc/rfc9112#section-6.1

structure Std.Http.Header.TransferEncoding : Type

The Transfer-Encoding header, representing the list of transfer codings applied to the message body.

Validation rules (RFC 9112 Section 6.1):

• "chunked" may appear at most once.
• If "chunked" is present, it must be the last encoding in the list.

Reference: https://www.rfc-editor.org/rfc/rfc9112#section-6.1

• codings : Array String

  The ordered list of transfer codings.

• isValid : Validate self.codings = true

  Proof that the transfer codings satisfy the chunked placement rules.

@[implicit_reducible]

instance Std.Http.Header.instReprTransferEncoding : Repr TransferEncoding

def Std.Http.Header.instReprTransferEncoding.repr : TransferEncoding → Nat → Format

def Std.Http.Header.TransferEncoding.isChunked (te : TransferEncoding) : Bool

Returns true if the transfer encoding ends with chunked.

def Std.Http.Header.TransferEncoding.parse (v : Value) : Option TransferEncoding

Parses a comma-separated list of transfer codings from a header value, validating chunked placement.

def Std.Http.Header.TransferEncoding.serialize (te : TransferEncoding) : Name × Value

Serializes a transfer encoding back to a comma-separated header value.

@[implicit_reducible]

instance Std.Http.Header.TransferEncoding.inst : Header TransferEncoding

structure Std.Http.Header.Connection : Type

The Connection header, represented as a list of connection option tokens.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-connection

• tokens : Array String

  The normalized connection-option tokens.

• valid : self.tokens.all Internal.isToken = true

  Proof that all tokens satisfy isToken.

@[implicit_reducible]

instance Std.Http.Header.instReprConnection : Repr Connection

def Std.Http.Header.instReprConnection.repr : Connection → Nat → Format

def Std.Http.Header.Connection.containsToken (connection : Connection) (token : String) : Bool

Checks whether a specific token is present in the Connection header value.

def Std.Http.Header.Connection.shouldClose (connection : Connection) : Bool

Checks whether the Connection header requests connection close semantics.

def Std.Http.Header.Connection.parse (v : Value) : Option Connection

Parses a Connection header value into normalized tokens.

def Std.Http.Header.Connection.serialize (connection : Connection) : Name × Value

Serializes a Connection header back to a comma-separated value.

@[implicit_reducible]

instance Std.Http.Header.Connection.inst : Header Connection