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 α

Equations

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

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

Equations

• Std.Http.Header.instBEqContentLength.beq { length := a } { length := b } = (a == b)
• Std.Http.Header.instBEqContentLength.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.Header.instBEqContentLength : BEq ContentLength

Equations

• Std.Http.Header.instBEqContentLength = { beq := Std.Http.Header.instBEqContentLength.beq }

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

Equations

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

@[implicit_reducible]

instance Std.Http.Header.instReprContentLength : Repr ContentLength

Equations

• Std.Http.Header.instReprContentLength = { reprPrec := Std.Http.Header.instReprContentLength.repr }

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

Parses a content length header value.

Equations

• Std.Http.Header.ContentLength.parse v = Option.map Std.Http.Header.ContentLength.mk v.value.toNat?

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

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

Equations

• h.serialize = (Std.Http.Header.Name.contentLength, Std.Http.Header.Value.ofString! (toString h.length))

@[implicit_reducible]

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

Equations

• Std.Http.Header.ContentLength.inst = { parse := Std.Http.Header.ContentLength.parse, serialize := Std.Http.Header.ContentLength.serialize }

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

Equations

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

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

Equations

• Std.Http.Header.instReprTransferEncoding = { reprPrec := Std.Http.Header.instReprTransferEncoding.repr }

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

Equations

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

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

Returns true if the transfer encoding ends with chunked.

Equations

• te.isChunked = (te.codings.back? == some "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.

Equations

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

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

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

Equations

• te.serialize = (Std.Http.Header.Name.transferEncoding, Std.Http.Header.Value.ofString! (",".intercalate te.codings.toList))

@[implicit_reducible]

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

Equations

• Std.Http.Header.TransferEncoding.inst = { parse := Std.Http.Header.TransferEncoding.parse, serialize := Std.Http.Header.TransferEncoding.serialize }

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

Equations

• Std.Http.Header.instReprConnection = { reprPrec := Std.Http.Header.instReprConnection.repr }

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

Equations

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

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

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

Equations

• connection.containsToken token = connection.tokens.any fun (x : String) => x == token.trimAscii.toString.toLower

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

Checks whether the Connection header requests connection close semantics.

Equations

• connection.shouldClose = connection.containsToken "close"

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

Parses a Connection header value into normalized tokens.

Equations

• Std.Http.Header.Connection.parse v = do let tokens ← Std.Http.Header.parseTokenList✝ v if h : tokens.all Std.Http.Internal.isToken = true then some { tokens := tokens, valid := h } else none

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

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

Equations

• connection.serialize = (Std.Http.Header.Name.connection, Std.Http.Header.Value.ofString! (",".intercalate connection.tokens.toList))

@[implicit_reducible]

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

Equations

• Std.Http.Header.Connection.inst = { parse := Std.Http.Header.Connection.parse, serialize := Std.Http.Header.Connection.serialize }