0 | module HTTP.API.Server.Interface
  1 |
  2 | import public HTTP.API
  3 | import public HTTP.I18n
  4 | import public HTTP.Prog
  5 | import public HTTP.Request
  6 | import public HTTP.Response
  7 |
  8 | %default total
  9 |
 10 | ||| Interface for integrating a partial description of a
 11 | ||| HTTP endpoint and using to extract variables from the
 12 | ||| HTTP request and make adjustments to the server response.
 13 | public export
 14 | interface Serve (0 a : Type) where
 15 |
 16 |   ||| Auto-implicit argument required by and passed to the
 17 |   ||| utility functions of this interface.
 18 |   0 Constraint : a -> Type
 19 |
 20 |   ||| Types of values extracted from the HTTP request
 21 |   ||| in function `fromRequest`.
 22 |   0 InTypes    : a -> List Type
 23 |
 24 |   ||| Types of values needed to adjust the HTTP response
 25 |   ||| in `adjResponse`.
 26 |   0 OutTypes   : a -> List Type
 27 |
 28 |   ||| `TList` representation of `OutTypes`. This is required
 29 |   ||| to split the `OutTypes` of several endpoint descriptions and
 30 |   ||| pass each of them to the proper description.
 31 |   outs         : (v : a) -> TList (OutTypes v)
 32 |
 33 |   ||| Returns `True`, if this endpoint description can process
 34 |   ||| the current HTTP request.
 35 |   |||
 36 |   ||| In general, a HTTP server consists of many endpoints, and
 37 |   ||| the first, for which `canHandle` returns `True`, will
 38 |   ||| get to process the request. If it then fails to do so
 39 |   ||| (by failing with a `RequestErr` in `fromRequest` or `adjResposnse`,
 40 |   ||| the request is considered to be invalid and no other endpoint
 41 |   ||| handler is tried. Instead, a proper error response is sent to
 42 |   ||| the client.
 43 |   canHandle    : (v : a) -> (con : Constraint v) => Request -> Bool
 44 |
 45 |   ||| Tries to analyze the current HTTP request and extract
 46 |   ||| a heterogeneous list of `InTypes` from it.
 47 |   fromRequest  :
 48 |        (v : a)
 49 |     -> {auto con : Constraint v}
 50 |     -> Request
 51 |     -> Handler (HList $ InTypes v)
 52 |
 53 |   ||| Takes the `OutTypes` and uses them to adjust the HTTP response.
 54 |   adjResponse  :
 55 |        (v : a)
 56 |     -> {auto con : Constraint v}
 57 |     -> HList (OutTypes v)
 58 |     -> Request
 59 |     -> Response
 60 |     -> Handler Response
 61 |
 62 | --------------------------------------------------------------------------------
 63 | -- Type-level Utilities
 64 | --------------------------------------------------------------------------------
 65 |
 66 | ||| Computes the list of constraints required to process a
 67 | ||| single endpoint description.
 68 | public export
 69 | 0 Constraints : All Serve ts => (endpoint : HList ts) -> List Type
 70 | Constraints @{[]}   []      = []
 71 | Constraints @{_::_} (v::vs) = Constraint v :: Constraints vs
 72 |
 73 | ||| Computes the list of types of values extracted from the HTTP request
 74 | ||| by a single endpoint description.
 75 | public export
 76 | 0 AllInTypes : All Serve ts => (endpoint : HList ts) -> List Type
 77 | AllInTypes @{[]}   []      = []
 78 | AllInTypes @{_::_} (v::vs) = InTypes v ++ AllInTypes vs
 79 |
 80 | ||| Computes the list of type of values used to adjust the HTTP response
 81 | ||| by a single endpoint description.
 82 | public export
 83 | 0 AllOutTypes : All Serve ts => (endpoint : HList ts) -> List Type
 84 | AllOutTypes @{[]}   []      = []
 85 | AllOutTypes @{_::_} (v::vs) = OutTypes v ++ AllOutTypes vs
 86 |
 87 | ||| Computes a `TList` representation of the outtypes of an entpoint.
 88 | public export
 89 | allOuts : All Serve ts => (endpoint : HList ts) -> TList (AllOutTypes endpoint)
 90 | allOuts @{[]}   []      = []
 91 | allOuts @{_::_} (v::vs) = outs v ++ allOuts vs
 92 |
 93 | ||| Function type for the handler of a single endpoint of a HTTP server.
 94 | public export
 95 | 0 EndpointHandler : All Serve ts => (endpoint : HList ts) -> Type
 96 | EndpointHandler vs =
 97 |   Fun (AllInTypes vs) (Handler (ResultType $ AllOutTypes vs))
 98 |
 99 | --------------------------------------------------------------------------------
100 | -- Server Implementation
101 | --------------------------------------------------------------------------------
102 |
103 | ||| Returns `True` if the given endpoint can serve the current
104 | ||| HTTP request
105 | export
106 | canServe :
107 |      {auto all : All Serve ts}
108 |   -> (endpoint : HList ts)
109 |   -> {auto con : HList (Constraints endpoint)}
110 |   -> Request -> Bool
111 | canServe @{[]}   []      @{[]}   req = True
112 | canServe @{_::_} (v::vs) @{_::_} req = canHandle v req && canServe vs req
113 |
114 | -- extracts all required values from the HTTP request at a given
115 | -- endpoint
116 | getIns :
117 |      {auto all : All Serve ts}
118 |   -> (endpoint : HList ts)
119 |   -> {auto con : HList (Constraints endpoint)}
120 |   -> Request
121 |   -> Handler (HList $ AllInTypes endpoint)
122 | getIns @{[]}   []      @{[]}   req = pure []
123 | getIns @{_::_} (v::vs) @{_::_} req = Prelude.do
124 |   rs  <- fromRequest v req
125 |   rem <- getIns vs req
126 |   pure (rs ++ rem)
127 |
128 | -- uses the values generated by the endpoint handler to make
129 | -- adjustments to the HTTP response.
130 | putOuts :
131 |      {auto all : All Serve ts}
132 |   -> (endpoint : HList ts)
133 |   -> {auto con : HList (Constraints endpoint)}
134 |   -> HList (AllOutTypes endpoint)
135 |   -> Request
136 |   -> Response
137 |   -> Handler Response
138 | putOuts @{[]}   []      [] @{[]}   req resp = pure resp
139 | putOuts @{_::_} (x::xs) vs @{_::_} req resp = Prelude.do
140 |   let (ts,rem) := splitHList (outs x) vs
141 |   r2 <- adjResponse x ts req resp
142 |   putOuts xs rem req r2
143 |
144 | ||| Processes a HTTP request at the given HTTP endpoint.
145 | |||
146 | ||| This proceeds in three steps:
147 | |||
148 | ||| 1. The necessary values are extracted from the request
149 | |||    by invoking all `fromRequest` functions and concatenating
150 | |||    the results.
151 | |||
152 | ||| 2. The extracted values are passed to the endpoint handler
153 | |||    (of type `EndpointHandler endpoint`), which produces the values
154 | |||    required to make adjustments to the HTTP response.
155 | |||
156 | ||| 3. The values from (2) are split up and passed to the individual
157 | |||    `adjResponse` runctions, which adjust the (initially empty)
158 | |||    HTTP response accordingly.
159 | export
160 | serveEndpoint :
161 |      {auto all : All Serve ts}
162 |   -> (endpoint : HList ts)
163 |   -> {auto con : HList (Constraints endpoint)}
164 |   -> EndpointHandler endpoint
165 |   -> Request
166 |   -> Handler Response
167 | serveEndpoint endpoint f req = Prelude.do
168 |   ins  <- getIns endpoint req
169 |   outs <- applyHList ins f
170 |   putOuts endpoint (wrapResult (allOuts endpoint) outs) req empty
171 |