This module defines parsers for HTTP/1.1 request and response lines, headers, and body framing. The reference used is https://httpwg.org/specs/rfc9112.html.

def Std.Http.Protocol.H1.parseRequestLine (limits : Config) : Internal.Parsec.ByteArray.Parser Request.Head

Parses a request line and returns a fully-typed Request.Head. request-line = method SP request-target SP HTTP-version

Equations

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

def Std.Http.Protocol.H1.parseRequestLineRawVersion (limits : Config) : Internal.Parsec.ByteArray.Parser (Method × RequestTarget × Option Version)

Parses a request line and returns the recognized HTTP method and version when available.

request-line = method SP request-target SP HTTP-version

Equations

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

def Std.Http.Protocol.H1.parseSingleHeader (limits : Config) : Internal.Parsec.ByteArray.Parser (Option (String × String))

Parses a single header field line, or returns none when it sees the blank line that terminates the header section.

field-line = field-name ":" OWS field-value OWS CRLF

Equations

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

def Std.Http.Protocol.H1.parseChunkSize (limits : Config) : Internal.Parsec.ByteArray.Parser (Nat × Array (Chunk.ExtensionName × Option Chunk.ExtensionValue))

Parses the size and extensions of a chunk.

Equations

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

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

Result of parsing partial or complete information.

• complete (data : ByteSlice) : TakeResult
• incomplete (data : ByteSlice) (remaining : Nat) : TakeResult

def Std.Http.Protocol.H1.parseChunkPartial (limits : Config) : Internal.Parsec.ByteArray.Parser (Option (Nat × Array (Chunk.ExtensionName × Option Chunk.ExtensionValue) × ByteSlice))

Parses a single chunk in chunked transfer encoding.

Equations

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

def Std.Http.Protocol.H1.parseFixedSizeData (size : Nat) : Internal.Parsec.ByteArray.Parser TakeResult

Parses fixed-size data that can be incomplete.

Equations

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

def Std.Http.Protocol.H1.parseChunkSizedData (size : Nat) : Internal.Parsec.ByteArray.Parser TakeResult

Parses fixed-size chunk data that can be incomplete.

Equations

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

def Std.Http.Protocol.H1.parseTrailers (limits : Config) : Internal.Parsec.ByteArray.Parser (Array (String × String))

Parses trailer headers after a chunked body and returns them as an array of name-value pairs.

This is exposed for callers that need the trailer values directly (e.g. clients). The internal protocol machine uses parseLastChunkBody instead, which discards trailer values.

Equations

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

def Std.Http.Protocol.H1.parseStatusLine (limits : Config) : Internal.Parsec.ByteArray.Parser Response.Head

Parses a status line and returns a fully-typed Response.Head. status-line = HTTP-version SP status-code SP [ reason-phrase ] Accepts only HTTP/1.1. For parsing where the version may be unrecognized and must be mapped to an error event, use parseStatusLineRawVersion.

Equations

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

def Std.Http.Protocol.H1.parseStatusLineRawVersion (limits : Config) : Internal.Parsec.ByteArray.Parser (Status × Option Version)

Parses a status line and returns the status code plus recognized HTTP version when available. Consumes and discards the reason phrase.

status-line = HTTP-version SP status-code SP [ reason-phrase ] CRLF

Equations

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

def Std.Http.Protocol.H1.parseLastChunkBody (limits : Config) : Internal.Parsec.ByteArray.Parser Unit

Parses the trailer section that follows the last chunk size line (0\r\n).

Equations

• Std.Http.Protocol.H1.parseLastChunkBody limits = do discard (Std.Http.Protocol.H1.manyItems✝ (Std.Http.Protocol.H1.parseTrailerHeader✝ limits) limits.maxTrailerHeaders) Std.Http.Protocol.H1.crlf✝