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

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

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

@[implicit_reducible]

instance Std.Http.Request.instReprHead : Repr Head

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✝)

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

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

@[implicit_reducible]

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

def Std.Http.Request.new : Builder

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

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

Sets the HTTP method for the request being built.

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

Sets the HTTP version for the request being built.

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

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

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

Sets the request target/URI for the request being built

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

Sets the headers for the request being built

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

Adds a single header to the request being built.

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.

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.

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.

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

Inserts a typed extension value into the request being built.

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.

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

Creates a new HTTP GET Request with the specified URI.

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

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

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

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

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

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

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

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

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

Creates a new HTTP HEAD Request builder with the specified 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.

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.

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

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