Request

This module provides the Request type, which represents an HTTP request. It also defines ways to build a Request using functions that make it easier.

References:

• https://httpwg.org/specs/rfc9112.html#request.line

structure Std.Http.Request.Head : Type

The main parts of a request containing the HTTP method, version, and request target URI.

Reference: https://httpwg.org/specs/rfc9112.html#request.line

• method : Method

  The HTTP method (GET, POST, PUT, DELETE, etc.) for the request

  Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.3.1

• version : Version

  The HTTP protocol version for the request (e.g. HTTP/1.1, HTTP/2.0, HTTP/3.0).

  Reference: https://httpwg.org/specs/rfc9112.html#http.version

• uri : RequestTarget

  The raw request-target string (commonly origin-form path/query, "*", or authority-form).

• headers : Headers

  Collection of HTTP headers for the request (Content-Type, Authorization, etc.).

@[implicit_reducible]

instance Std.Http.Request.instInhabitedHead : Inhabited Head

Equations

• Std.Http.Request.instInhabitedHead = { default := Std.Http.Request.instInhabitedHead.default }

def Std.Http.Request.instInhabitedHead.default : Head

Equations

• Std.Http.Request.instInhabitedHead.default = { method := default, version := default, uri := default, headers := default }

def Std.Http.Request.instReprHead.repr : Head → Nat → Format

Equations

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

@[implicit_reducible]

instance Std.Http.Request.instReprHead : Repr Head

Equations

• Std.Http.Request.instReprHead = { reprPrec := Std.Http.Request.instReprHead.repr }

structure Std.Http.Request (t : Type) : Type

HTTP request structure parameterized by body type.

• line : Head

  The request line information (method, version, and request-target uri).

• body : t

  The request body content of type t.

• extensions : Extensions

  Optional dynamic metadata attached to the request.

@[implicit_reducible]

instance Std.Http.instInhabitedRequest {a✝ : Type} [Inhabited a✝] : Inhabited (Request a✝)

Equations

• Std.Http.instInhabitedRequest = { default := Std.Http.instInhabitedRequest.default }

def Std.Http.instInhabitedRequest.default {a✝ : Type} [Inhabited a✝] : Request a✝

Equations

• Std.Http.instInhabitedRequest.default = { line := default, body := default, extensions := default }

structure Std.Http.Request.Builder : Type

Builds an HTTP Request.

• line : Head

  The request-line of an HTTP request.

• extensions : Extensions

  Optional dynamic metadata attached to the request.

@[implicit_reducible]

instance Std.Http.Request.instToStringHead : ToString Head

Equations

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

@[implicit_reducible]

instance Std.Http.Request.instEncodeV11Head : Internal.Encode Version.v11 Head

Equations

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

def Std.Http.Request.new : Builder

Creates a new HTTP request builder with the default head (method: GET, version: HTTP/1.1, target: *).

Equations

• Std.Http.Request.new = { }

def Std.Http.Request.Builder.method (builder : Builder) (method : Method) : Builder

Sets the HTTP method for the request being built.

Equations

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

def Std.Http.Request.Builder.version (builder : Builder) (version : Version) : Builder

Sets the HTTP version for the request being built.

Equations

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

def Std.Http.Request.Builder.uri (builder : Builder) (uri : RequestTarget) : Builder

Sets the request target/URI for the request being built.

Equations

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

def Std.Http.Request.Builder.uri! (builder : Builder) (uri : String) : Builder

Sets the request target/URI for the request being built

Equations

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

def Std.Http.Request.Builder.headers (builder : Builder) (headers : Headers) : Builder

Sets the headers for the request being built

Equations

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

def Std.Http.Request.Builder.header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder

Adds a single header to the request being built.

Equations

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

def Std.Http.Request.Builder.header! (builder : Builder) (key value : String) : Builder

Adds a single header to the request being built, panics if the header is invalid.

Equations

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

def Std.Http.Request.Builder.header? (builder : Builder) (key value : String) : Option Builder

Adds a single header to the request being built. Returns none if the header name or value is invalid.

Equations

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

def Std.Http.Request.Builder.headerOpt (builder : Builder) (key : Header.Name) (value : Option Header.Value) : Builder

Adds a header to the request being built only if the Option Header.Value is some.

Equations

• builder.headerOpt key (some v) = builder.header key v
• builder.headerOpt key none = builder

def Std.Http.Request.Builder.extension {α : Type u_1} (builder : Builder) [TypeName α] (data : α) : Builder

Inserts a typed extension value into the request being built.

Equations

• builder.extension data = { line := builder.line, extensions := builder.extensions.insert data }

def Std.Http.Request.Builder.body {t : Type} (builder : Builder) (body : t) : Request t

Builds and returns the final HTTP Request with the specified body.

Equations

• builder.body body = { line := builder.line, body := body, extensions := builder.extensions }

def Std.Http.Request.get (uri : RequestTarget) : Builder

Creates a new HTTP GET Request with the specified URI.

Equations

• Std.Http.Request.get uri = (Std.Http.Request.new.method Std.Http.Method.get).uri uri

def Std.Http.Request.post (uri : RequestTarget) : Builder

Creates a new HTTP POST Request builder with the specified URI.

Equations

• Std.Http.Request.post uri = (Std.Http.Request.new.method Std.Http.Method.post).uri uri

def Std.Http.Request.put (uri : RequestTarget) : Builder

Creates a new HTTP PUT Request builder with the specified URI.

Equations

• Std.Http.Request.put uri = (Std.Http.Request.new.method Std.Http.Method.put).uri uri

def Std.Http.Request.delete (uri : RequestTarget) : Builder

Creates a new HTTP DELETE Request builder with the specified URI.

Equations

• Std.Http.Request.delete uri = (Std.Http.Request.new.method Std.Http.Method.delete).uri uri

def Std.Http.Request.patch (uri : RequestTarget) : Builder

Creates a new HTTP PATCH Request builder with the specified URI.

Equations

• Std.Http.Request.patch uri = (Std.Http.Request.new.method Std.Http.Method.patch).uri uri

def Std.Http.Request.head (uri : RequestTarget) : Builder

Creates a new HTTP HEAD Request builder with the specified URI.

Equations

• Std.Http.Request.head uri = (Std.Http.Request.new.method Std.Http.Method.head).uri uri

def Std.Http.Request.options (uri : RequestTarget) : Builder

Creates a new HTTP OPTIONS Request builder with the specified URI. Use Request.options (RequestTarget.asteriskForm) for server-wide OPTIONS.

Equations

• Std.Http.Request.options uri = (Std.Http.Request.new.method Std.Http.Method.options).uri uri

def Std.Http.Request.connect (uri : RequestTarget) : Builder

Creates a new HTTP CONNECT Request builder with the specified URI. Typically used with RequestTarget.authorityForm for tunneling.

Equations

• Std.Http.Request.connect uri = (Std.Http.Request.new.method Std.Http.Method.connect).uri uri

def Std.Http.Request.trace (uri : RequestTarget) : Builder

Creates a new HTTP TRACE Request builder with the specified URI.

Equations

• Std.Http.Request.trace uri = (Std.Http.Request.new.method Std.Http.Method.trace).uri uri