def Network.Wai.responseLBS (status : HTTP.Types.Status) (headers : HTTP.Types.ResponseHeaders) (body : String) : Response

Create a simple response from a status, headers, and body ByteArray. $$\text{responseLBS} : \text{Status} \to \text{ResponseHeaders} \to \text{String} \to \text{Response}$$ @since 0.3.0

Equations

• Network.Wai.responseLBS status headers body = Network.Wai.Response.responseBuilder status headers body.toUTF8

def Network.Wai.responseFile' (status : HTTP.Types.Status) (headers : HTTP.Types.ResponseHeaders) (path : String) (part : Option Sendfile.FilePart := none) : Response

Create a file response. @since 2.0.0

Equations

• Network.Wai.responseFile' status headers path part = Network.Wai.Response.responseFile status headers path part

def Network.Wai.responseStream' (status : HTTP.Types.Status) (headers : HTTP.Types.ResponseHeaders) (body : StreamingBody) : Response

Create a streaming response. @since 3.0.0

Equations

• Network.Wai.responseStream' status headers body = Network.Wai.Response.responseStream status headers body

@[inline]

def Network.Wai.getRequestBodyChunk (req : Request) : IO ByteArray

Get the next chunk of the request body. Returns empty ByteArray when the body is fully consumed. Preferred over direct requestBody access. $$\text{getRequestBodyChunk} : \text{Request} \to \text{IO}(\text{ByteArray})$$ @since 3.2.2

Equations

• Network.Wai.getRequestBodyChunk req = req.requestBody

def Network.Wai.setRequestBodyChunks (body : IO ByteArray) (req : Request) : Request

Set the request body chunks IO action on a request. The supplied IO action should return the next chunk each time it is called and empty ByteArray when fully consumed. $$\text{setRequestBodyChunks} : \text{IO}(\text{ByteArray}) \to \text{Request} \to \text{Request}$$ @since 3.2.4

Equations

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

def Network.Wai.requestHeader (name : HTTP.Types.HeaderName) (req : Request) : Option String

Get a header value from a request by name.

Equations

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

def Network.Wai.strictRequestBody (req : Request) : IO ByteArray

Read the entire request body strictly into memory. Returns all chunks concatenated as a single ByteArray.

Warning: This consumes the request body. Future calls return empty. Consider using getRequestBodyChunk for streaming when possible. $$\text{strictRequestBody} : \text{Request} \to \text{IO}(\text{ByteArray})$$ @since 3.0.1

Equations

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

@[reducible, inline]

abbrev Network.Wai.consumeRequestBodyStrict (req : Request) : IO ByteArray

Synonym for strictRequestBody. Name signals the non-idempotent (consuming) nature. @since 3.2.3

Equations

• Network.Wai.consumeRequestBodyStrict = Network.Wai.strictRequestBody

def Network.Wai.defaultRequest : Request

A default, blank request. @since 2.0.0

Equations

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

def Network.Wai.mapRequestHeaders (f : HTTP.Types.RequestHeaders → HTTP.Types.RequestHeaders) (req : Request) : Request

Apply the provided function to the request header list. $$\text{mapRequestHeaders} : (H \to H) \to \text{Request} \to \text{Request}$$ @since 3.2.4

Equations

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

def Network.Wai.idMiddleware : Middleware

The identity middleware (does nothing).

Equations

• Network.Wai.idMiddleware = id

@[inline]

def Network.Wai.composeMiddleware (f g : Middleware) : Middleware

Compose two middlewares. $$\text{composeMiddleware}(f, g) = f \circ g$$

Equations

• Network.Wai.composeMiddleware f g = f ∘ g

def Network.Wai.addHeader (name : HTTP.Types.HeaderName) (val : String) (resp : Response) : Response

Add a header to the response.

Equations

• Network.Wai.addHeader name val resp = Network.Wai.Response.mapResponseHeaders (fun (x : Network.HTTP.Types.ResponseHeaders) => (name, val) :: x) resp

def Network.Wai.modifyRequest (f : Request → Request) : Middleware

Apply a function that modifies a request as a Middleware. $$\text{modifyRequest} : (\text{Request} \to \text{Request}) \to \text{Middleware}$$ @since 3.2.4

Equations

• Network.Wai.modifyRequest f app req respond = app (f req) respond

def Network.Wai.modifyResponse (f : Response → Response) : Middleware

Apply a function that modifies a response as a Middleware. $$\text{modifyResponse} : (\text{Response} \to \text{Response}) \to \text{Middleware}$$ @since 3.0.3.0

Equations

• Network.Wai.modifyResponse f app req respond = app req (respond ∘ f)

def Network.Wai.ifRequest (pred : Request → Bool) (middle : Middleware) : Middleware

Conditionally apply a Middleware based on a request predicate. $$\text{ifRequest}(p, m) = \begin{cases} m & \text{if } p(\text{req}) \\ \text{id} & \text{otherwise} \end{cases}$$ @since 3.0.3.0

Equations

• Network.Wai.ifRequest pred middle app req respond = if pred req = true then middle app req respond else app req respond

theorem Network.Wai.idMiddleware_comp_left (m : Middleware) : composeMiddleware idMiddleware m = m

Identity middleware is left identity for composition. $$\text{id} \circ m = m$$

theorem Network.Wai.idMiddleware_comp_right (m : Middleware) : composeMiddleware m idMiddleware = m

Identity middleware is right identity for composition. $$m \circ \text{id} = m$$

theorem Network.Wai.modifyRequest_id : modifyRequest id = idMiddleware

modifyRequest id is the identity middleware.

theorem Network.Wai.modifyResponse_id : modifyResponse id = idMiddleware

modifyResponse id is the identity middleware.

theorem Network.Wai.ifRequest_false (middle : Middleware) : ifRequest (fun (x : Request) => false) middle = idMiddleware

ifRequest (fun _ => false) always passes through. $$\text{ifRequest}(\bot, m) = \text{id}$$