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