
   0 | |||This is a slightly modified copy of the same module from `contrib` package.
   1 | module TyRE.Text.Parser.Core
   2 | 
   3 | import public Control.Delayed
   4 | import public Data.List
   5 | 
   6 | ||| Description of a language's grammar. The `tok` parameter is the type
   7 | ||| of tokens, and the `consumes` flag is True if the language is guaranteed
   8 | ||| to be non-empty - that is, successfully parsing the language is guaranteed
   9 | ||| to consume some input.
  10 | public export
  11 | data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
  12 |      Empty : (val : ty) -> Grammar tok False ty
  13 |      Terminal : String -> (tok -> Maybe a) -> Grammar tok True a
  14 |      NextIs : String -> (tok -> Bool) -> Grammar tok False tok
  15 |      EOF : Grammar tok False ()
  16 | 
  17 |      Fail : Bool -> String -> Grammar tok c ty
  18 |      Commit : Grammar tok False ()
  19 |      MustWork : Grammar tok c a -> Grammar tok c a
  20 | 
  21 |      SeqEat : {c2 : _} -> Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
  22 |               Grammar tok True b
  23 |      SeqEmpty : {c1, c2 : _} -> Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
  24 |                 Grammar tok (c1 || c2) b
  25 | 
  26 |      ThenEat : {c2 : _} -> Grammar tok True () -> Inf (Grammar tok c2 b) ->
  27 |                Grammar tok True b
  28 |      ThenEmpty : {c1, c2 : _} -> Grammar tok c1 () -> Grammar tok c2 b ->
  29 |                  Grammar tok (c1 || c2) b
  30 | 
  31 |      Alt : {c1, c2 : _} -> Grammar tok c1 ty -> Grammar tok c2 ty ->
  32 |            Grammar tok (c1 && c2) ty
  33 | 
  34 | ||| Sequence two grammars. If either consumes some input, the sequence is
  35 | ||| guaranteed to consume some input. If the first one consumes input, the
  36 | ||| second is allowed to be recursive (because it means some input has been
  37 | ||| consumed and therefore the input is smaller)
  38 | %inline %tcinline
  39 | public export
  40 | (>>=) : {c1, c2 : Bool} ->
  41 |         Grammar tok c1 a ->
  42 |         inf c1 (a -> Grammar tok c2 b) ->
  43 |         Grammar tok (c1 || c2) b
  44 | (>>=) {c1 = False} = SeqEmpty
  45 | (>>=) {c1 = True} = SeqEat
  46 | 
  47 | ||| Sequence two grammars. If either consumes some input, the sequence is
  48 | ||| guaranteed to consume some input. If the first one consumes input, the
  49 | ||| second is allowed to be recursive (because it means some input has been
  50 | ||| consumed and therefore the input is smaller)
  51 | %inline %tcinline
  52 | public export
  53 | (>>) : {c1, c2 : Bool} ->
  54 |         Grammar tok c1 () ->
  55 |         inf c1 (Grammar tok c2 a) ->
  56 |         Grammar tok (c1 || c2) a
  57 | (>>) {c1 = False} = ThenEmpty
  58 | (>>) {c1 = True} = ThenEat
  59 | 
  60 | ||| Sequence two grammars. If either consumes some input, the sequence is
  61 | ||| guaranteed to consume input. This is an explicitly non-infinite version
  62 | ||| of `>>=`.
  63 | public export
  64 | seq : {c1, c2 : _} -> Grammar tok c1 a ->
  65 |       (a -> Grammar tok c2 b) ->
  66 |       Grammar tok (c1 || c2) b
  67 | seq = SeqEmpty
  68 | 
  69 | ||| Sequence a grammar followed by the grammar it returns.
  70 | public export
  71 | join : {c1, c2 : Bool} ->
  72 |        Grammar tok c1 (Grammar tok c2 a) ->
  73 |        Grammar tok (c1 || c2) a
  74 | join {c1 = False} p = SeqEmpty p id
  75 | join {c1 = True} p = SeqEat p id
  76 | 
  77 | ||| Give two alternative grammars. If both consume, the combination is
  78 | ||| guaranteed to consume.
  79 | public export
  80 | (<|>) : {c1, c2 : _} ->
  81 |         Grammar tok c1 ty ->
  82 |         Grammar tok c2 ty ->
  83 |         Grammar tok (c1 && c2) ty
  84 | (<|>) = Alt
  85 | 
  86 | ||| Allows the result of a grammar to be mapped to a different value.
  87 | public export
  88 | {c : _} -> Functor (Grammar tok c) where
  89 |   map f (Empty val)  = Empty (f val)
  90 |   map f (Fail fatal msg) = Fail fatal msg
  91 |   map f (MustWork g) = MustWork (map f g)
  92 |   map f (Terminal msg g) = Terminal msg (\t => map f (g t))
  93 |   map f (Alt x y)    = Alt (map f x) (map f y)
  94 |   map f (SeqEat act next)
  95 |       = SeqEat act (\val => map f (next val))
  96 |   map f (SeqEmpty act next)
  97 |       = SeqEmpty act (\val => map f (next val))
  98 |   map f (ThenEat act next)
  99 |       = ThenEat act (map f next)
 100 |   map f (ThenEmpty act next)
 101 |       = ThenEmpty act (map f next)
 102 |   -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
 103 |   -- so a sequence must be used.
 104 |   map {c = False} f p = SeqEmpty p (Empty . f)
 105 | 
 106 | ||| Sequence a grammar with value type `a -> b` and a grammar
 107 | ||| with value type `a`. If both succeed, apply the function
 108 | ||| from the first grammar to the value from the second grammar.
 109 | ||| Guaranteed to consume if either grammar consumes.
 110 | public export
 111 | (<*>) : {c1, c2 : _} ->
 112 |         Grammar tok c1 (a -> b) ->
 113 |         Inf (Grammar tok c2 a) ->
 114 |         Grammar tok (c1 || c2) b
 115 | (<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
 116 | (<*>) {c1 = True } x y = SeqEmpty x (\f => map f (Force y))
 117 | 
 118 | ||| Sequence two grammars. If both succeed, use the value of the first one.
 119 | ||| Guaranteed to consume if either grammar consumes.
 120 | public export
 121 | (<*) : {c1, c2 : _} ->
 122 |        Grammar tok c1 a ->
 123 |        Inf (Grammar tok c2 b) ->
 124 |        Grammar tok (c1 || c2) a
 125 | (<*) x y = map const x <*> y
 126 | 
 127 | ||| Sequence two grammars. If both succeed, use the value of the second one.
 128 | ||| Guaranteed to consume if either grammar consumes.
 129 | public export
 130 | (*>) : {c1, c2 : _} ->
 131 |        Grammar tok c1 a ->
 132 |        Inf (Grammar tok c2 b) ->
 133 |        Grammar tok (c1 || c2) b
 134 | (*>) x y = map (const id) x <*> y
 135 | 
 136 | ||| Produce a grammar that can parse a different type of token by providing a
 137 | ||| function converting the new token type into the original one.
 138 | public export
 139 | mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty
 140 | mapToken f (Empty val) = Empty val
 141 | mapToken f (Terminal msg g) = Terminal msg (g . f)
 142 | mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . f)) (Empty . f)
 143 | mapToken f EOF = EOF
 144 | mapToken f (Fail fatal msg) = Fail fatal msg
 145 | mapToken f (MustWork g) = MustWork (mapToken f g)
 146 | mapToken f Commit = Commit
 147 | mapToken f (SeqEat act next)
 148 |    = SeqEat (mapToken f act) (\x => mapToken f (next x))
 149 | mapToken f (SeqEmpty act next)
 150 |    = SeqEmpty (mapToken f act) (\x => mapToken f (next x))
 151 | mapToken f (ThenEat act next)
 152 |    = ThenEat (mapToken f act) (mapToken f next)
 153 | mapToken f (ThenEmpty act next)
 154 |    = ThenEmpty (mapToken f act) (mapToken f next)
 155 | mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
 156 | 
 157 | ||| Always succeed with the given value.
 158 | public export
 159 | pure : (val : ty) -> Grammar tok False ty
 160 | pure = Empty
 161 | 
 162 | ||| Check whether the next token satisfies a predicate
 163 | public export
 164 | nextIs : String -> (tok -> Bool) -> Grammar tok False tok
 165 | nextIs = NextIs
 166 | 
 167 | ||| Look at the next token in the input
 168 | public export
 169 | peek : Grammar tok False tok
 170 | peek = nextIs "Unrecognised token" (const True)
 171 | 
 172 | ||| Succeeds if running the predicate on the next token returns Just x,
 173 | ||| returning x. Otherwise fails.
 174 | public export
 175 | terminal : String -> (tok -> Maybe a) -> Grammar tok True a
 176 | terminal = Terminal
 177 | 
 178 | ||| Always fail with a message
 179 | public export
 180 | fail : String -> Grammar tok c ty
 181 | fail = Fail False
 182 | 
 183 | public export
 184 | fatalError : String -> Grammar tok c ty
 185 | fatalError = Fail True
 186 | 
 187 | ||| Succeed if the input is empty
 188 | public export
 189 | eof : Grammar tok False ()
 190 | eof = EOF
 191 | 
 192 | ||| Commit to an alternative; if the current branch of an alternative
 193 | ||| fails to parse, no more branches will be tried
 194 | public export
 195 | commit : Grammar tok False ()
 196 | commit = Commit
 197 | 
 198 | ||| If the parser fails, treat it as a fatal error
 199 | public export
 200 | mustWork : Grammar tok c ty -> Grammar tok c ty
 201 | mustWork = MustWork
 202 | 
 203 | public export
 204 | data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
 205 |      Failure : {xs : List tok} ->
 206 |                (committed : Bool) -> (fatal : Bool) ->
 207 |                (err : String) -> (rest : List tok) -> ParseResult xs c ty
 208 |      EmptyRes : (committed : Bool) ->
 209 |                 (val : ty) -> (more : List tok) -> ParseResult more False ty
 210 |      NonEmptyRes : {xs : List tok} ->
 211 |                    (committed : Bool) ->
 212 |                    (val : ty) -> (more : List tok) ->
 213 |                    ParseResult (x :: xs ++ more) c ty
 214 | 
 215 | -- Take the result of an alternative branch, reset the commit flag to
 216 | -- the commit flag from the outer alternative, and weaken the 'consumes'
 217 | -- flag to take both alternatives into account
 218 | public export
 219 | weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
 220 |             (com' : Bool) ->
 221 |             ParseResult xs c ty -> ParseResult xs (whatever && c) ty
 222 | weakenRes com' (Failure com fatal msg ts) = Failure com' fatal msg ts
 223 | weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
 224 | weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
 225 | weakenRes com' (NonEmptyRes {xs} com val more) = NonEmptyRes {xs} com' val more
 226 | 
 227 | public export
 228 | doParse : (commit : Bool) ->
 229 |           (act : Grammar tok c ty) ->
 230 |           (xs : List tok) ->
 231 |           ParseResult xs c ty
 232 | -- doParse com xs act with (sizeAccessible xs)
 233 | doParse com (Empty val) xs = EmptyRes com val xs
 234 | doParse com (Fail fatal str) [] = Failure com fatal str []
 235 | doParse com (Fail fatal str) (x :: xs) = Failure com fatal str (x :: xs)
 236 | doParse com Commit xs = EmptyRes True () xs
 237 | doParse com (MustWork g) xs =
 238 |   let p' = doParse com g xs in
 239 |       case p' of
 240 |            Failure com' _ msg ts => Failure com' True msg ts
 241 |            res => res
 242 | doParse com (Terminal err f) [] = Failure com False "End of input" []
 243 | doParse com (Terminal err f) (x :: xs)
 244 |       = maybe
 245 |            (Failure com False err (x :: xs))
 246 |            (\a => NonEmptyRes com {xs=[]} a xs)
 247 |            (f x)
 248 | doParse com EOF [] = EmptyRes com () []
 249 | doParse com EOF (x :: xs)
 250 |       = Failure com False "Expected end of input" (x :: xs)
 251 | doParse com (NextIs err f) [] = Failure com False "End of input" []
 252 | doParse com (NextIs err f) (x :: xs)
 253 |       = if f x
 254 |            then EmptyRes com x (x :: xs)
 255 |            else Failure com False err (x :: xs)
 256 | doParse com (Alt {c1} {c2} x y) xs
 257 |     = let p' = doParse False x xs in
 258 |           case p' of
 259 |                Failure com' fatal msg ts
 260 |                   => if com' || fatal
 261 |                             -- If the alternative had committed, don't try the
 262 |                             -- other branch (and reset commit flag)
 263 |                        then Failure com fatal msg ts
 264 |                        else weakenRes {whatever = c1} com (doParse False y xs)
 265 |   -- Successfully parsed the first option, so use the outer commit flag
 266 |                EmptyRes _ val xs => EmptyRes com val xs
 267 |                NonEmptyRes {xs=xs'} _ val more => NonEmptyRes {xs=xs'} com val more
 268 | doParse com (SeqEmpty {c1} {c2} act next) xs
 269 |     = let p' = assert_total (doParse {c = c1} com act xs) in
 270 |               case p' of
 271 |                Failure com fatal msg ts => Failure com fatal msg ts
 272 |                EmptyRes com val xs => assert_total (doParse com (next val) xs)
 273 |                NonEmptyRes {x} {xs=ys} com val more =>
 274 |                      case (assert_total (doParse com (next val) more)) of
 275 |                           Failure com' fatal msg ts => Failure com' fatal msg ts
 276 |                           EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
 277 |                           NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
 278 |                                rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
 279 |                                        NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
 280 | doParse com (SeqEat act next) xs with (doParse com act xs)
 281 |   doParse com (SeqEat act next) xs | Failure com' fatal msg ts
 282 |        = Failure com' fatal msg ts
 283 |   doParse com (SeqEat act next) (x :: (ys ++ more)) | (NonEmptyRes {xs=ys} com' val more)
 284 |        = let p' = assert_total (doParse com' (next val) more) in
 285 |              case p' of
 286 |               Failure com' fatal msg ts => Failure com' fatal msg ts
 287 |               EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
 288 |               NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
 289 |                    rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
 290 |                            NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
 291 | doParse com (ThenEmpty {c1} {c2} act next) xs
 292 |     = let p' = assert_total (doParse {c = c1} com act xs) in
 293 |               case p' of
 294 |                Failure com fatal msg ts => Failure com fatal msg ts
 295 |                EmptyRes com val xs => assert_total (doParse com next xs)
 296 |                NonEmptyRes {x} {xs=ys} com val more =>
 297 |                      case (assert_total (doParse com next more)) of
 298 |                           Failure com' fatal msg ts => Failure com' fatal msg ts
 299 |                           EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
 300 |                           NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
 301 |                                rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
 302 |                                        NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
 303 | doParse com (ThenEat act next) xs with (doParse com act xs)
 304 |   doParse com (ThenEat act next) xs | Failure com' fatal msg ts
 305 |        = Failure com' fatal msg ts
 306 |   doParse com (ThenEat act next) (x :: (ys ++ more)) | (NonEmptyRes {xs=ys} com' val more)
 307 |        = let p' = assert_total (doParse com' next more) in
 308 |              case p' of
 309 |               Failure com' fatal msg ts => Failure com' fatal msg ts
 310 |               EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
 311 |               NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
 312 |                    rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
 313 |                            NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
 314 | 
 315 | -- This next line is not strictly necessary, but it stops the coverage
 316 | -- checker taking a really long time and eating lots of memory...
 317 | -- doParse _ _ _ = Failure True True "Help the coverage checker!" []
 318 | 
 319 | public export
 320 | data ParseError tok = Error String (List tok)
 321 | 
 322 | ||| Parse a list of tokens according to the given grammar. If successful,
 323 | ||| returns a pair of the parse result and the unparsed tokens (the remaining
 324 | ||| input).
 325 | public export
 326 | parse : {c : _} -> (act : Grammar tok c ty) -> (xs : List tok) ->
 327 |         Either (ParseError tok) (ty, List tok)
 328 | parse act xs
 329 |     = case doParse False act xs of
 330 |            Failure _ _ msg ts => Left (Error msg ts)
 331 |            EmptyRes _ val rest => pure (val, rest)
 332 |            NonEmptyRes _ val rest => pure (val, rest)
 333 |