
  0 | module HTTP.API
  1 | 
  2 | import public Data.Buffer
  3 | import public Data.ByteString
  4 | import public Data.List.Quantifiers
  5 | import public Data.Maybe0
  6 | 
  7 | import public HTTP.API.Content
  8 | import public HTTP.API.Endpoints
  9 | import public HTTP.API.Decode
 10 | import public HTTP.API.Encode
 11 | import public HTTP.API.Env
 12 | import public HTTP.API.Header
 13 | import public HTTP.API.Method
 14 | import public HTTP.API.Path
 15 | import public HTTP.API.Query
 16 | import public HTTP.API.TList
 17 | 
 18 | import public HTTP.Header
 19 | import public HTTP.Method
 20 | import public HTTP.RequestErr
 21 | import public HTTP.Status
 22 | import public HTTP.URI
 23 | 
 24 | %default total
 25 | 
 26 | ||| Computes a function type from a list of argument types and a result type.
 27 | |||
 28 | ||| This is used to compute the function type of handler of a single
 29 | ||| server endpoint.
 30 | public export
 31 | 0 Fun : List Type -> Type -> Type
 32 | Fun []        r = r
 33 | Fun (t :: ts) r = t -> Fun ts r
 34 | 
 35 | ||| Computes the result type the handler of a server endpoint.
 36 | |||
 37 | ||| For convenience in downstream code, we only return a heterogeneous list
 38 | ||| in case several values are required to make adjustments to the HTTP
 39 | ||| response. In case of no value or a single value being required, we return
 40 | ||| `Unit` or the a single value, respectively.
 41 | public export
 42 | 0 ResultType : List Type -> Type
 43 | ResultType []  = ()
 44 | ResultType [t] = t
 45 | ResultType ts  = HList ts
 46 | 
 47 | export
 48 | applyHList : HList ts -> Fun ts r -> r
 49 | applyHList []        r = r
 50 | applyHList (v :: vs) f = applyHList vs (f v)
 51 | 
 52 | ||| converts a `ResultType` to a heterogeneous list
 53 | export
 54 | wrapResult : TList ts -> ResultType ts -> HList ts
 55 | wrapResult []        r = []
 56 | wrapResult [t]       r = [r]
 57 | wrapResult (_::_::_) r = r
 58 |