0 | ||| Define the API.
 1 | module Pact.API
 2 |
 3 | import public Pact.API.Operator
 4 | import public Pact.API.Verb
 5 | import public Pact.API.MimeRender
 6 | import public Pact.API.Accept
 7 | import public Pact.API.HttpApiData
 8 | import public Pact.API.Component
 9 |
10 | import Data.Vect
11 | import public Data.Vect.Quantifiers
12 |
13 | public export
14 | record API where
15 |   constructor (:>)
16 |   { types : Vect typesLen Type }
17 |   { auto prf : All FromHttpApiData types }
18 |   paths : Component lastType types reqBody
19 |   verb : Verb
20 |
21 | public export
22 | ApiReqBody : API -> Type
23 | ApiReqBody (path :> _) = PathReqBody path
24 |
25 |
26 | ||| Get the type of the handler.
27 | ||| @m The type of the monad.
28 | ||| @ts The types of the path parameters.
29 | ||| @path The path.
30 | ||| @epType The type of the endpoint.
31 | |||
32 | ||| Returns the type of the handler.
33 | public export
34 | GetHandlerType : (m : Type -> Type) -> API -> Type
35 | GetHandlerType m (path :> ep) = GetPathType path $ (m (VerbResponse ep))
36 |
37 | ||| Get the type of the endpoint.
38 | ||| @m The type of the monad.
39 | ||| @ts The types of the path parameters.
40 | ||| @path The path.
41 | ||| @epType The type of the endpoint.
42 | |||
43 | ||| Returns the type of the endpoint.
44 | public export
45 | GetEPFromAPI : (m : Type -> Type) -> API -> Type
46 | GetEPFromAPI m (path :> ep) = m (VerbResponse ep)
47 |
48 | ||| Get the type of the endpoint result.
49 | ||| @ts The types of the path parameters.
50 | ||| @path The path.
51 | ||| @epType The type of the endpoint.
52 | |||
53 | ||| Returns the type of the endpoint result.
54 | public export
55 | GetEpResultTypeFromAPI : API -> Type
56 | GetEpResultTypeFromAPI (path :> ep) = VerbResponse ep