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.

• parse : Value → Option α

  Parses a header value into the typed representation.

• serialize : α → Name × Value

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

• 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.

• 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 = if (v.value.isEmpty || !v.value.all Char.isDigit) = true then none else 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.

• codings : Array String

  The ordered list of transfer codings.

• isValid : Validate self.codings = true

  Proof that the transfer codings satisfy the chunked placement rules.

• isValid : Validate self.codings = true

  Proof that the transfer codings satisfy the chunked placement rules.

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

Equations

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

@[implicit_reducible]

instance Std.Http.Header.instReprTransferEncoding : Repr TransferEncoding

Equations

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

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.

• tokens : Array String

  The normalized connection-option tokens.

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

  Proof that all tokens satisfy isToken.

• 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 }

structure Std.Http.Header.Host : Type

The Host header.

Represents the authority component of a URI: host [ ":" port ]

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-host-and-authority

• host : URI.Host

  Host name (reg-name, IPv4, or IPv6 literal).

• port : URI.Port

  Optional port.

@[implicit_reducible]

instance Std.Http.Header.instReprHost : Repr Host

Equations

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

def Std.Http.Header.instReprHost.repr : Host → Nat → Format

Equations

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

@[implicit_reducible]

instance Std.Http.Header.instBEqHost : BEq Host

Equations

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

def Std.Http.Header.instBEqHost.beq : Host → Host → Bool

Equations

• Std.Http.Header.instBEqHost.beq { host := a, port := a_1 } { host := b, port := b_1 } = (a == b && a_1 == b_1)
• Std.Http.Header.instBEqHost.beq x✝¹ x✝ = false

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

Parses a Host header value.

Equations

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

def Std.Http.Header.Host.serialize (host : Host) : Name × Value

Serializes a Host header back to a name and a value.

Equations

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

@[implicit_reducible]

instance Std.Http.Header.Host.inst : Header Host

Equations

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

structure Std.Http.Header.Expect : Type

The Expect header.

Represents an expectation token. The only standardized expectation is 100-continue.

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

def Std.Http.Header.instReprExpect.repr : Expect → Nat → Format

Equations

• Std.Http.Header.instReprExpect.repr x✝ prec✝ = Std.Format.bracket "{ " Std.Format.nil " }"

@[implicit_reducible]

instance Std.Http.Header.instReprExpect : Repr Expect

Equations

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

def Std.Http.Header.instBEqExpect.beq : Expect → Expect → Bool

Equations

• Std.Http.Header.instBEqExpect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Std.Http.Header.instBEqExpect : BEq Expect

Equations

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

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

Parses an Expect header.

Succeeds only if the value is exactly 100-continue (case-insensitive, trimmed).

Equations

• Std.Http.Header.Expect.parse v = if (v.value.trimAscii.toString.toLower == "100-continue") = true then some { } else none

def Std.Http.Header.Expect.serialize : Expect → Name × Value

Serializes an Expect header.

Equations

• x✝.serialize = (Std.Http.Header.Name.expect, Std.Http.Header.Value.ofString! "100-continue")

@[implicit_reducible]

instance Std.Http.Header.Expect.inst : Header Expect

Equations

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