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

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

@[reducible, inline]

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

Inverts the message direction.

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

Gets the message head type based on direction.

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

Gets the headers of a Message.

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.

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

Gets the version of a Message.

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.

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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