Message

This module provides types and operations for HTTP/1.1 messages, centered around the Direction type which models the server's role in message exchange: Direction.receiving for parsing incoming requests from clients, and Direction.sending for generating outgoing responses to clients. The Message.Head type is parameterized by Direction and resolves to Request.Head or Response.Head accordingly, enabling generic code that works uniformly across both phases while exposing common operations such as headers, version, and shouldKeepAlive

inductive Std.Http.Protocol.H1.Direction : Type

Direction of message flow from the server's perspective.

• receiving : Direction

  Receiving and parsing incoming requests from clients.

• sending : Direction

  Client perspective: writing outgoing requests and reading incoming responses.

@[implicit_reducible]

instance Std.Http.Protocol.H1.instBEqDirection : BEq Direction

Equations

• Std.Http.Protocol.H1.instBEqDirection = { beq := Std.Http.Protocol.H1.instBEqDirection.beq }

def Std.Http.Protocol.H1.instBEqDirection.beq : Direction → Direction → Bool

Equations

• Std.Http.Protocol.H1.instBEqDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[reducible, inline]

abbrev Std.Http.Protocol.H1.Direction.swap : Direction → Direction

Inverts the message direction.

Equations

• Std.Http.Protocol.H1.Direction.receiving.swap = Std.Http.Protocol.H1.Direction.sending
• Std.Http.Protocol.H1.Direction.sending.swap = Std.Http.Protocol.H1.Direction.receiving

def Std.Http.Protocol.H1.Message.Head : Direction → Type

Gets the message head type based on direction.

Equations

• Std.Http.Protocol.H1.Message.Head Std.Http.Protocol.H1.Direction.receiving = Std.Http.Request.Head
• Std.Http.Protocol.H1.Message.Head Std.Http.Protocol.H1.Direction.sending = Std.Http.Response.Head

def Std.Http.Protocol.H1.Message.Head.headers {dir : Direction} (m : Head dir) : Headers

Gets the headers of a Message.

Equations

• m_2.headers = m_2.headers
• m_2.headers = m_2.headers

def Std.Http.Protocol.H1.Message.Head.setHeaders {dir : Direction} (m : Head dir) (headers : Headers) : Head dir

Returns a copy of the message head with the headers replaced.

Equations

• m_2.setHeaders headers = { method := m_2.method, version := m_2.version, uri := m_2.uri, headers := headers }
• m_2.setHeaders headers = { status := m_2.status, version := m_2.version, headers := headers }

def Std.Http.Protocol.H1.Message.Head.version {dir : Direction} (m : Head dir) : Version

Gets the version of a Message.

Equations

• m_2.version = m_2.version
• m_2.version = m_2.version

def Std.Http.Protocol.H1.Message.Head.getSize {dir : Direction} (message : Head dir) (allowEOFBody : Bool) : Option Body.Length

Determines the message body size based on the Content-Length header and the Transfer-Encoding (chunked) flag.

Equations

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

def Std.Http.Protocol.H1.Message.Head.shouldKeepAlive {dir : Direction} (message : Head dir) : Bool

Checks whether the message indicates that the connection should be kept alive.

Equations

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

@[implicit_reducible]

instance Std.Http.Protocol.H1.instReprHead {dir : Direction} : Repr (Message.Head dir)

Equations

• Std.Http.Protocol.H1.instReprHead = { reprPrec := Std.Http.Protocol.H1.instReprHead._aux_1 }
• Std.Http.Protocol.H1.instReprHead = { reprPrec := Std.Http.Protocol.H1.instReprHead._aux_3 }

@[implicit_reducible]

instance Std.Http.Protocol.H1.instEncodeV11Head {dir : Direction} : Internal.Encode Version.v11 (Message.Head dir)

Equations

• Std.Http.Protocol.H1.instEncodeV11Head = { encode := Std.Http.Protocol.H1.instEncodeV11Head._aux_1 }
• Std.Http.Protocol.H1.instEncodeV11Head = { encode := Std.Http.Protocol.H1.instEncodeV11Head._aux_3 }

@[implicit_reducible]

instance Std.Http.Protocol.H1.instEmptyCollectionHead {dir : Direction} : EmptyCollection (Message.Head dir)

Equations

• Std.Http.Protocol.H1.instEmptyCollectionHead = { emptyCollection := { method := Std.Http.Method.get, version := Std.Http.Version.v11 } }
• Std.Http.Protocol.H1.instEmptyCollectionHead = { emptyCollection := { } }