0 | module HTTP.API.Path
 1 |
 2 | %default total
 3 |
 4 | ||| Single part in a URI path.
 5 | |||
 6 | ||| This matches either a specific string or one or more variables
 7 | ||| stored at the given position in the path.
 8 | public export
 9 | data Part : Type where
10 |   PScheme : String -> Part
11 |   PAuth   : String -> Part
12 |   PStr    : String -> Part
13 |   PTill   : String -> Part
14 |   Capture : (0 t : Type) -> Part
15 |
16 | public export
17 | FromString Part where fromString = PStr
18 |
19 | ||| Computes the list of types captured by a URI path description.
20 | public export
21 | 0 PartsTypes : List Part -> List Type
22 | PartsTypes []                = []
23 | PartsTypes (PScheme _ :: xs) = PartsTypes xs
24 | PartsTypes (PAuth _   :: xs) = PartsTypes xs
25 | PartsTypes (PStr _    :: xs) = PartsTypes xs
26 | PartsTypes (PTill _   :: xs) = PartsTypes xs
27 | PartsTypes (Capture t :: xs) = t :: PartsTypes xs
28 |
29 | ||| Describes a pattern for matching and extracting
30 | ||| values for the path of the request URI.
31 | public export
32 | record ReqPath where
33 |   constructor Path
34 |   parts : List Part
35 |
36 | public export
37 | path : (scheme, authority : String) -> List Part -> ReqPath
38 | path s a ps = Path $ PScheme s :: PAuth a :: ps
39 |