0 | ||| Define the component of a path.
 1 | module Pact.API.Component
 2 |
 3 | import Pact.API.Operator
 4 | import Pact.API.HttpApiData
 5 | import Pact.API.Verb
 6 |
 7 | import Data.Vect
 8 | import Data.Vect.Quantifiers
 9 |
10 | public export
11 | data Component : Type -> Vect n Type -> (reqBody : Type) -> Type where
12 |   ||| Static path segment, e.g. "users"
13 |   StaticPath : String -> Component () [()] Void
14 |   ||| Captured path segment, e.g. ":id"
15 |   Capture : String -> (a : Type) -> Component a [a] Void
16 |   ||| Request body, e.g. UserCreateRequest
17 |   ReqBody : (a : Type) -> Component () [()] a
18 |   ||| Concatenate two paths, e.g. "users/:id/todos"
19 |   (:/) : Component tl [tl] Void -> Component tr tsr reqBody -> Component tl (tl :: tsr) reqBody
20 |
21 | public export
22 | isReqBody : Component t ts reqBody -> Bool
23 | isReqBody (ReqBody _) = True
24 | isReqBody _ = False
25 |
26 | public export 
27 | PathReqBody : Component t ts reqBody -> Type
28 | PathReqBody (StaticPath _) = Void
29 | PathReqBody (Capture _ _) =  Void
30 | PathReqBody (ReqBody reqBody) =  reqBody
31 | -- PathReqBody (ReqBody reqBody :/ restPath) = reqBody
32 | PathReqBody (path :/ restPath) = PathReqBody restPath
33 |
34 | public export
35 | hasReqBody : Component t ts reqBody -> Bool
36 | hasReqBody (StaticPath _) = False
37 | hasReqBody (Capture _ _) = False
38 | hasReqBody (ReqBody _) = True
39 | hasReqBody (_ :/ restPath) = hasReqBody restPath
40 |
41 |
42 | ||| Get the name of a capture path segment
43 | ||| @ path The path to get the name of
44 | ||| @ return The name of the capture path segment
45 | public export
46 | getCaptureName : Component t _ _ -> String
47 | getCaptureName (Capture s _) = s
48 | getCaptureName _ = "unknown"
49 |
50 | ||| Match a path against a list of path segments.
51 | |||
52 | ||| @path The path to match.
53 | ||| @segs The list of path segments.
54 | ||| @allprf A proof that all the path segments are path parameters.
55 | |||
56 | ||| Returns a list of the parsed path parameters.
57 | public export
58 | matchPath : Component t ts reqBody' -> Vect m String -> { auto allprf : All FromHttpApiData ts } -> Either String (HVect ts)
59 | matchPath (StaticPath s) [seg] = if s == seg then Right [()] else Left "Path mismatch"
60 | matchPath (ReqBody s) [] = Right [()]
61 | matchPath (Capture s t) [seg] { allprf = prf :: restPrf } = case parseUrlPiece seg  of
62 |   Right val => Right [val]
63 |   Left err => Left ("Failed to parse path parameter:" ++ s ++ " " ++ err)
64 | matchPath (StaticPath s :/ restPath) (seg :: segs) { allprf = prf :: restPrf } = if s == seg then map (\xs => () :: xs) (matchPath restPath segs) else Left "Path mismatch"
65 | matchPath (Capture s t :/ restPath) (seg :: segs) { allprf = prf :: restPrf } = case parseUrlPiece seg of
66 |   Right val => case matchPath restPath segs of
67 |     Right vals => Right (val :: vals)
68 |     Left err => Left err
69 |   Left err => Left ("Failed to parse path parameter:" ++ s ++ " " ++ err)
70 | matchPath _ segs = Left ("unknown path" ++ show segs)
71 |
72 | ||| Get the type of the path.
73 | ||| @ts The types of the path parameters.
74 | ||| @path The path.
75 | ||| @epType The type of the endpoint.
76 | |||
77 | ||| Returns the type of the path.
78 | public export
79 | GetPathType : Component _ ts reqBody' -> (epType : Type) -> Type
80 | GetPathType (StaticPath _) epType = epType
81 | GetPathType (Capture _ t) epType = t -> epType
82 | GetPathType (ReqBody reqBody) epType = reqBody -> epType
83 | GetPathType { ts = t :: ts'} (path :/ restPath) epType = let epType' = GetPathType restPath epType in case path of
84 |   StaticPath _ => epType'
85 |   Capture name t => t -> epType'
86 |   -- ReqBody reqBody => reqBody -> epType'
87 |   _ => epType'