0 | module TyTTP.URL.Path
  1 |
  2 | import Data.List
  3 | import Data.String
  4 | import public Data.Either
  5 | import TyTTP
  6 | import TyTTP.URL.Definition
  7 |
  8 | %default total
  9 |
 10 | data Elem : Type where
 11 |   Literal : List Char -> Elem
 12 |   Param : List Char -> Elem
 13 |   Rest : Elem
 14 |
 15 | Eq Elem where
 16 |   (==) (Literal s1) (Literal s2) = s1 == s2
 17 |   (==) (Param s1) (Param s2) = s1 == s2
 18 |   (==) Rest Rest = True
 19 |   (==) _ _ = False
 20 |
 21 | data ParseState
 22 |   = InLiteral (List Char)
 23 |   | InParam (List Char)
 24 |   | InRest
 25 |
 26 | public export
 27 | data ParseError
 28 |   = EmptyPattern
 29 |   | ParamShouldFollowALiteral String (List Elem)
 30 |   | RestShouldFollowALiteral String (List Elem)
 31 |   | ParamAlreadyDefined String (List Elem)
 32 |   | ParamEmpty String (List Elem)
 33 |   | UnclosedParam String (List Elem)
 34 |   | InvalidStartCharInParam Char (List Elem)
 35 |   | InvalidCharInParam Char (List Elem)
 36 |   | RestShouldBeLast String (List Elem)
 37 |
 38 | export
 39 | data ParsedPattern : (0 s : String) -> Type where
 40 |   MkParsedPattern : List Elem -> ParsedPattern s
 41 |
 42 | public export
 43 | parse : (s : String) -> Either ParseError (ParsedPattern s)
 44 | parse "" = Left EmptyPattern
 45 | parse s = map (MkParsedPattern . reverse) $ go (InLiteral []) [] $ unpack s
 46 |   where
 47 |     isAllowedInParam : Char -> Bool
 48 |     isAllowedInParam c = isAlpha c || c == '-' || c == '_'
 49 |
 50 |     go : ParseState -> List Elem -> List Char -> Either ParseError $ List Elem
 51 |     go (InLiteral []) p r@('{' :: xs) = Left $ ParamShouldFollowALiteral (pack r) $ reverse p
 52 |     go (InLiteral s) p ('{' :: xs) = go (InParam []) (Literal (reverse s) :: p) xs
 53 |     go (InLiteral []) p r@('*' :: xs) = Left $ RestShouldFollowALiteral (pack r) $ reverse p
 54 |     go (InLiteral s) p ('*' :: xs) = go InRest (Literal (reverse s) :: p) xs
 55 |     go (InLiteral []) p ['/'] = Right $ Literal ['/'] :: p
 56 |     go (InLiteral s) p ['/'] = Right $ Literal (reverse s) :: p
 57 |     go (InLiteral []) p [] = Right p
 58 |     go (InLiteral s) p [] = Right $ Literal (reverse s) :: p
 59 |     go (InLiteral s) p (x :: xs) = go (InLiteral $ x :: s) p xs
 60 |     go (InParam s) p r@('}' :: xs) =
 61 |       let name = reverse s
 62 |           param = Param name
 63 |       in do
 64 |         False <- pure $ elem param p
 65 |           | True => Left $ ParamAlreadyDefined (pack name) $ reverse p
 66 |         False <- pure $ null name
 67 |           | True => Left $ ParamEmpty (pack $ '{' :: r) $ reverse p
 68 |         go (InLiteral []) (param :: p) xs
 69 |     go (InParam s) p [] = Left $ UnclosedParam (pack $ reverse s) $ reverse p
 70 |     go (InParam []) p (x :: xs) =
 71 |       if isAlpha x
 72 |       then go (InParam [x]) p xs
 73 |       else Left $ InvalidStartCharInParam x $ reverse p
 74 |     go (InParam s) p (x :: xs) =
 75 |       if isAllowedInParam x
 76 |       then go (InParam (x :: s)) p xs
 77 |       else Left $ InvalidCharInParam x $ reverse p
 78 |     go InRest p [] = Right $ Rest :: p
 79 |     go InRest p r@(x :: _) = Left $ RestShouldBeLast (pack r) $ reverse p
 80 |
 81 | public export
 82 | record Path where
 83 |   constructor MkPath
 84 |   raw : String
 85 |   params : List (String, String)
 86 |   rest : String
 87 |
 88 | matcher : (s : String) -> ParsedPattern str -> Maybe Path
 89 | matcher s (MkParsedPattern ls) = go ls (unpack s) $ MkPath s [] ""
 90 |   where
 91 |
 92 |     consumeLiteral : List Char -> List Char -> Maybe $ List Char
 93 |     consumeLiteral [] xs = Just xs
 94 |     consumeLiteral (_::_) [] = Nothing
 95 |     consumeLiteral (l::ls) (x::xs) =
 96 |       case l == x of
 97 |         True => consumeLiteral ls xs
 98 |         False => Nothing
 99 |
100 |     go : List Elem -> List Char -> Path -> Maybe Path
101 |     go [] [] p = Just p
102 |     go [] xs _ = Nothing
103 |     go (Literal l :: ps) xs p = do
104 |       remaining <- consumeLiteral l xs
105 |       go ps (assert_smaller xs remaining) p
106 |     go (Param param :: Literal l@(f::fs) :: ps) xs p =
107 |         let (value, remaining) = List.break (==f) xs
108 |         in if null value
109 |         then Nothing
110 |         else go (Literal l :: ps) (assert_smaller xs remaining) $ { params $= ((pack param, pack value)::) } p
111 |     go (Param param :: Nil) xs p =
112 |       let (value, remaining) = List.break (=='/') xs
113 |       in if null value || not (null remaining)
114 |       then Nothing
115 |       else Just $ { params $= ((pack param, pack value)::) } p
116 |     go (Rest :: Nil) xs p = Just $ { rest := pack xs } p
117 |     go _ _ _ = Nothing
118 |
119 | export
120 | pattern : Monad m
121 |   => Alternative m
122 |   => (str : String)
123 |   -> {auto 0 ok : IsRight (Path.parse str)}
124 |   -> (
125 |     Context me (URL auth Path s) v h1 st h2 a b
126 |     -> m $ Context me' (URL auth Path s) v' h1' st' h2' a' b'
127 |   )
128 |   -> Context me (URL auth String s) v h1 st h2 a b
129 |   -> m $ Context me' (URL auth String s) v' h1' st' h2' a' b'
130 | pattern str {ok} handler ctx with (Path.parse str)
131 |   _ | Right parsedPattern =
132 |     case matcher ctx.request.url.path parsedPattern of
133 |       Just p => do
134 |         result <- handler $ { request.url := { path := p } ctx.request.url } ctx
135 |         pure $ { request.url := { path := ctx.request.url.path } result.request.url } result
136 |       Nothing => empty
137 |