
  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 |   PStr       : String -> Part
 11 |   PTill      : String -> Part
 12 |   Capture    : (0 t : Type) -> Part
 13 | 
 14 | public export
 15 | FromString Part where fromString = PStr
 16 | 
 17 | ||| Computes the list of types captured by a URI path description.
 18 | public export
 19 | 0 PartsTypes : List Part -> List Type
 20 | PartsTypes []                = []
 21 | PartsTypes (PStr _    :: xs) = PartsTypes xs
 22 | PartsTypes (PTill _   :: xs) = PartsTypes xs
 23 | PartsTypes (Capture t :: xs) = t :: PartsTypes xs
 24 | 
 25 | ||| Describes a pattern for matching and extracting
 26 | ||| values for the path of the request URI.
 27 | public export
 28 | record ReqPath where
 29 |   constructor Path
 30 |   parts : List Part
 31 |