Idris2Doc : HTTP.API.Server.Interface

HTTP.API.Server.Interface

(source)
Reexports
import public HTTP.API
import public HTTP.Prog
import public HTTP.Request
import public HTTP.Response
Definitions
interface Serve : Type -> Type
  Interface for integrating a partial description of a
  HTTP endpoint and using to extract variables from the
  HTTP request and make adjustments to the server response.

  Parameters: a
Methods:
  
0 Constraint : a -> Type
  Auto-implicit argument required by and passed to the
  utility functions of this interface.
  
0 InTypes : a -> List Type
  Types of values extracted from the HTTP request
  in function `fromRequest`.
  
0 OutTypes : a -> List Type
  Types of values needed to adjust the HTTP response
  in `adjResponse`.
  
outs : (v : a) -> TList (OutTypes v)
  `TList` representation of `OutTypes`. This is required
  to split the `OutTypes` of several endpoint descriptions and
  pass each of them to the proper description.
  
canHandle : (v : a) -> Constraint v => Request -> Bool
  Returns `True`, if this endpoint description can process
  the current HTTP request.
  
  In general, a HTTP server consists of many endpoints, and
  the first, for which `canHandle` returns `True`, will
  get to process the request. If it then fails to do so
  (by failing with a `RequestErr` in `fromRequest` or `adjResposnse`,
  the request is considered to be invalid and no other endpoint
  handler is tried. Instead, a proper error response is sent to
  the client.
  
fromRequest : (v : a) -> Constraint v => Request -> Handler (HList (InTypes v))
  Tries to analyze the current HTTP request and extract
  a heterogeneous list of `InTypes` from it.
  
adjResponse : (v : a) -> Constraint v => HList (OutTypes v) -> Request -> Response -> Handler Response
  Takes the `OutTypes` and uses them to adjust the HTTP response.

Implementations:
  
Serve ReqContent
  
Serve ReqEnv
  
Serve ReqHeaders
  
Serve ReqMethod
  
Serve ReqPath
  
Serve ReqQuery
0 Constraint : Serve a => a -> Type
  Auto-implicit argument required by and passed to the
  utility functions of this interface.

  Totality: total
  Visibility: public export
0 InTypes : Serve a => a -> List Type
  Types of values extracted from the HTTP request
  in function `fromRequest`.

  Totality: total
  Visibility: public export
0 OutTypes : Serve a => a -> List Type
  Types of values needed to adjust the HTTP response
  in `adjResponse`.

  Totality: total
  Visibility: public export
outs : {auto __con : Serve a} -> (v : a) -> TList (OutTypes v)
  `TList` representation of `OutTypes`. This is required
  to split the `OutTypes` of several endpoint descriptions and
  pass each of them to the proper description.

  Totality: total
  Visibility: public export
canHandle : {auto __con : Serve a} -> (v : a) -> Constraint v => Request -> Bool
  Returns `True`, if this endpoint description can process
  the current HTTP request.
  
  In general, a HTTP server consists of many endpoints, and
  the first, for which `canHandle` returns `True`, will
  get to process the request. If it then fails to do so
  (by failing with a `RequestErr` in `fromRequest` or `adjResposnse`,
  the request is considered to be invalid and no other endpoint
  handler is tried. Instead, a proper error response is sent to
  the client.

  Totality: total
  Visibility: public export
fromRequest : {auto __con : Serve a} -> (v : a) -> Constraint v => Request -> Handler (HList (InTypes v))
  Tries to analyze the current HTTP request and extract
  a heterogeneous list of `InTypes` from it.

  Totality: total
  Visibility: public export
adjResponse : {auto __con : Serve a} -> (v : a) -> Constraint v => HList (OutTypes v) -> Request -> Response -> Handler Response
  Takes the `OutTypes` and uses them to adjust the HTTP response.

  Totality: total
  Visibility: public export
0 Constraints : All Serve ts => HList ts -> List Type
  Computes the list of constraints required to process a
  single endpoint description.

  Totality: total
  Visibility: public export
0 AllInTypes : All Serve ts => HList ts -> List Type
  Computes the list of types of values extracted from the HTTP request
  by a single endpoint description.

  Totality: total
  Visibility: public export
0 AllOutTypes : All Serve ts => HList ts -> List Type
  Computes the list of type of values used to adjust the HTTP response
  by a single endpoint description.

  Totality: total
  Visibility: public export
allOuts : {auto {conArg:17993} : All Serve ts} -> (endpoint : HList ts) -> TList (AllOutTypes endpoint)
  Computes a `TList` representation of the outtypes of an entpoint.

  Totality: total
  Visibility: public export
0 EndpointHandler : All Serve ts => HList ts -> Type
  Function type for the handler of a single endpoint of a HTTP server.

  Totality: total
  Visibility: public export
canServe : {auto all : All Serve ts} -> (endpoint : HList ts) -> HList (Constraints endpoint) => Request -> Bool
  Returns `True` if the given endpoint can serve the current
  HTTP request

  Totality: total
  Visibility: export
serveEndpoint : {auto all : All Serve ts} -> (endpoint : HList ts) -> HList (Constraints endpoint) => EndpointHandler endpoint -> Request -> Handler Response
  Processes a HTTP request at the given HTTP endpoint.
  
  This proceeds in three steps:
  
  1. The necessary values are extracted from the request
     by invoking all `fromRequest` functions and concatenating
     the results.
  
  2. The extracted values are passed to the endpoint handler
     (of type `EndpointHandler endpoint`), which produces the values
     required to make adjustments to the HTTP response.
  
  3. The values from (2) are split up and passed to the individual
     `adjResponse` runctions, which adjust the (initially empty)
     HTTP response accordingly.

  Totality: total
  Visibility: export