WFURL : Type Well-formed URLs with a valid filesystem path and a list of query parameters
Visibility: public exportallowsBody : Method -> Bool- Visibility: public export
DepBody : Method -> Type -> Type The body of a request depending on the request method used
TODO: remove body for HEAD , TRACE and OPTIONS
Visibility: public exportrecord RichRequest : Type -> Type A request with a well formed url and a dependent body
The fields of `RichRequest` are private the fields are accessible
Totality: total
Visibility: export
Constructor: MkRichReq : (method : Method) -> WFURL -> Version -> List (String, String) -> DepBody method bodyType -> RichRequest bodyType
Projections:
.body : ({rec:0} : RichRequest bodyType) -> DepBody (method {rec:0}) bodyType .method : RichRequest bodyType -> Method .url : RichRequest bodyType -> WFURL .version : RichRequest bodyType -> Version
Hints:
HasHeaders (RichRequest t) HasMethod (RichRequest t) HasURL (RichRequest t) HasVersion (RichRequest t)
.getBody' : RichRequest b -> Maybe b- Visibility: export
MkRichRequest : (m : Method) -> WFURL -> Version -> List (String, String) -> DepBody m body -> RichRequest body Public constructor for `RichRequest`
Visibility: export Interface for accessing headers of a request or response
Parameters: t
Methods:
Implementations:
HasHeaders (Request m u v (List (String, String)) b) HasHeaders (Response v (List (String, String)) b) HasHeaders (RichRequest t)
- Visibility: public export
interface HasVersion : Type -> Type Interface for accessing http version of a request
Parameters: t
Methods:
.version : t -> Version
Implementations:
HasVersion (Request m u Version h b) HasVersion (RichRequest t)
.version : HasVersion t => t -> Version- Visibility: public export
interface HasMethod : Type -> Type Interface for accessing the http method of a request
Parameters: t
Methods:
.method : t -> Method
Implementations:
HasMethod (Request Method u v h b) HasMethod (RichRequest t)
.method : HasMethod t => t -> Method- Visibility: public export
interface HasBody : Type -> Type -> Type Interface for accessing the body of a request or response
Parameters: r, t
Methods:
.body : r -> t
Implementations:
HasBody (Response v h b) b HasBody (Request m u v h b) b
.body : HasBody r t => r -> t- Visibility: public export
interface HasURL : Type -> Type Interface for accessing the url of a request
Parameters: t
Methods:
.url : t -> WFURL
Implementations:
HasURL (Request m WFURL v h b) HasURL (RichRequest t)
.url : HasURL t => t -> WFURL- Visibility: public export
anyGet : (r : RichRequest t) -> allowsBody (r .method) = False => RichRequest s Given a rich GET request, coerce the type of its body to anything else
Visibility: export.getBody : (r : RichRequest t) -> allowsBody (r .method) = True => t Obtain the body of a rich request, requires evidence that the method is _not_ a `GET` request
Visibility: exportGenericHttpResponse : Type -> Type The most generic kind of HTTP request using string headers
Visibility: public exportPlainRequest : Type- Visibility: public export
PlainResponse : Type- Visibility: public export
JSONRequest : Type- Visibility: public export
JSONResponse : Type A JSON response might not contain a response body. For this, we use Maybe.
A `Nothing` response body is an empty body
Visibility: public exportOk : PlainResponse- Visibility: export
Bad : PlainResponse- Visibility: export
BadJSON : JSONResponse- Visibility: export
PlainHTTP : API The HTTP container that represents an http request and its matching http response
Visibility: public exportRichHTTP : API The HTTP container that represents 1 http request and its matching http response
Visibility: public exportJSONHTTP : API The API for requests and responses with JSON request body
Visibility: public exportURLHttpRequest : Type -> Type- Visibility: public export
interface HTTPDebug : Type -> Type A debug interface to avoid conflicting with `Show`.
Parameters: t
Methods:
renderDebug : t -> String
Implementations:
HTTPDebug Buffer HTTPDebug WFURL HTTPDebug (List (String, String)) HTTPDebug JSON HTTPDebug Status HTTPDebug String
renderDebug : HTTPDebug t => t -> String- Visibility: public export