0 | module HTTP.API.Client.Interface
 1 |
 2 | import public HTTP.API
 3 | import public HTTP.API.Client.Request
 4 |
 5 | %default total
 6 |
 7 | public export
 8 | interface Receive (0 a : Type) where
 9 |   ||| Auto-implicit argument required by and passed to the
10 |   ||| utility functions of this interface.
11 |   0 RecConstraint : a -> Type
12 |
13 |   ||| Types of values extracted from the HTTP request
14 |   ||| in function `fromRequest`.
15 |   0 RecTypes : a -> List Type
16 |
17 |   ||| `TList` representation of `RecTypes`. This is required
18 |   ||| to split the `RecTypes` of several endpoint descriptions and
19 |   ||| pass each of them to the proper description.
20 |   recs       : (v : a) -> TList (RecTypes v)
21 |
22 |   adjRequest :
23 |        (v : a)
24 |     -> {auto con : RecConstraint v}
25 |     -> HList (RecTypes v)
26 |     -> HTTPRequest
27 |     -> HTTPRequest
28 |
29 | public export
30 | Receive ReqEnv where
31 |   RecConstraint _ = ()
32 |   RecTypes _ = []
33 |   recs _ = []
34 |   adjRequest _ _ r = r
35 |
36 | public export
37 | interface GetResponse (0 a : Type) where
38 |   0 RespEncodings : a -> List Type
39 |   0 RespTypes : a -> List Type
40 |
41 | --------------------------------------------------------------------------------
42 | -- Type-level Utilities
43 | --------------------------------------------------------------------------------
44 |
45 | public export
46 | 0 AllRespTypes : All GetResponse ts => (endpoint : HList ts) -> List Type
47 | AllRespTypes @{[]}   []      = []
48 | AllRespTypes @{_::_} (v::vs) = RespTypes v ++ AllRespTypes vs
49 |
50 | public export
51 | 0 AllRespEncodings : All GetResponse ts => (endpoint : HList ts) -> List Type
52 | AllRespEncodings @{[]}   []      = []
53 | AllRespEncodings @{_::_} (v::vs) = RespEncodings v ++ AllRespEncodings vs
54 |
55 | ||| Computes the list of type of values used to adjust the HTTP request
56 | ||| by a single endpoint description.
57 | public export
58 | 0 AllRecTypes : All Receive ts => (endpoint : HList ts) -> List Type
59 | AllRecTypes @{[]}   []      = []
60 | AllRecTypes @{_::_} (v::vs) = RecTypes v ++ AllRecTypes vs
61 |
62 | ||| Computes the list of type of constraints used to adjust the HTTP request
63 | ||| by a single endpoint description.
64 | public export
65 | 0 AllRecConstraints : All Receive ts => (endpoint : HList ts) -> List Type
66 | AllRecConstraints @{[]}   []      = []
67 | AllRecConstraints @{_::_} (v::vs) = RecConstraint v :: AllRecConstraints vs
68 |
69 | export
70 | endpointRequest :
71 |      (endpoint  : HList ts)
72 |   -> {auto all  : All Receive ts}
73 |   -> {auto cons : HList (AllRecConstraints endpoint)}
74 |   -> HList (AllRecTypes endpoint)
75 |   -> HTTPRequest
76 |   -> HTTPRequest
77 | endpointRequest []                      _  r = r
78 | endpointRequest (v::vs) @{_::_} @{_::_} hl r =
79 |  let (ts,rem) := splitHList (recs v) hl
80 |   in endpointRequest vs rem (adjRequest v ts r)
81 |