
   0 | module Libraries.Text.Parser.Core
   1 | 
   2 | import Data.Bool
   3 | import Data.List
   4 | import Data.List1
   5 | 
   6 | import public Libraries.Control.Delayed
   7 | import public Libraries.Text.Bounded
   8 | 
   9 | %default total
  10 | 
  11 | %hide Prelude.(>>)
  12 | 
  13 | -- TODO: Add some primitives for helping with error messages.
  14 | -- e.g. perhaps set a string to state what we're currently trying to
  15 | -- parse, or to say what the next expected token is in words
  16 | 
  17 | ||| Description of a language's grammar. The `tok` parameter is the type
  18 | ||| of tokens, and the `consumes` flag is True if the language is guaranteed
  19 | ||| to be non-empty - that is, successfully parsing the language is guaranteed
  20 | ||| to consume some input.
  21 | export
  22 | data Grammar : (state : Type) -> (tok : Type) -> (consumes : Bool) -> Type -> Type where
  23 |      Empty : (val : ty) -> Grammar state tok False ty
  24 |      Terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
  25 |      NextIs : String -> (tok -> Bool) -> Grammar state tok False tok
  26 |      EOF : Grammar state tok False ()
  27 | 
  28 |      Fail : (location : Maybe Bounds) -> (fatal : Bool) -> String -> Grammar state tok c ty
  29 |      Warning : (location : Maybe Bounds) -> String -> Grammar state tok False ()
  30 | 
  31 |      Try : Grammar state tok c ty -> Grammar state tok c ty
  32 | 
  33 |      Commit : Grammar state tok False ()
  34 |      MustWork : Grammar state tok c a -> Grammar state tok c a
  35 | 
  36 |      SeqEat : {c2 : Bool} ->
  37 |               Grammar state tok True a -> Inf (a -> Grammar state tok c2 b) ->
  38 |               Grammar state tok True b
  39 |      SeqEmpty : {c1, c2 : Bool} ->
  40 |                 Grammar state tok c1 a -> (a -> Grammar state tok c2 b) ->
  41 |                 Grammar state tok (c1 || c2) b
  42 | 
  43 |      ThenEat : {c2 : Bool} ->
  44 |                Grammar state tok True () -> Inf (Grammar state tok c2 a) ->
  45 |                Grammar state tok True a
  46 |      ThenEmpty : {c1, c2 : Bool} ->
  47 |                  Grammar state tok c1 () -> Grammar state tok c2 a ->
  48 |                  Grammar state tok (c1 || c2) a
  49 | 
  50 |      Alt : {c1, c2 : Bool} ->
  51 |            Grammar state tok c1 ty -> Lazy (Grammar state tok c2 ty) ->
  52 |            Grammar state tok (c1 && c2) ty
  53 |      Bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
  54 |      Position : Grammar state tok False Bounds
  55 | 
  56 |      Act : state -> Grammar state tok False ()
  57 | 
  58 | ||| Sequence two grammars. If either consumes some input, the sequence is
  59 | ||| guaranteed to consume some input. If the first one consumes input, the
  60 | ||| second is allowed to be recursive (because it means some input has been
  61 | ||| consumed and therefore the input is smaller)
  62 | export %inline
  63 | (>>=) : {c1, c2 : Bool} ->
  64 |         Grammar state tok c1 a ->
  65 |         inf c1 (a -> Grammar state tok c2 b) ->
  66 |         Grammar state tok (c1 || c2) b
  67 | (>>=) {c1 = False} = SeqEmpty
  68 | (>>=) {c1 = True}  = SeqEat
  69 | 
  70 | ||| Sequence two grammars. If either consumes some input, the sequence is
  71 | ||| guaranteed to consume some input. If the first one consumes input, the
  72 | ||| second is allowed to be recursive (because it means some input has been
  73 | ||| consumed and therefore the input is smaller)
  74 | public export %inline %tcinline
  75 | (>>) : {c1, c2 : Bool} ->
  76 |         Grammar state tok c1 () ->
  77 |         inf c1 (Grammar state tok c2 a) ->
  78 |         Grammar state tok (c1 || c2) a
  79 | (>>) {c1 = False} = ThenEmpty
  80 | (>>) {c1 = True} = ThenEat
  81 | 
  82 | ||| Sequence two grammars. If either consumes some input, the sequence is
  83 | ||| guaranteed to consume input. This is an explicitly non-infinite version
  84 | ||| of `>>=`.
  85 | export %inline
  86 | seq : {c1,c2 : Bool} ->
  87 |       Grammar state tok c1 a ->
  88 |       (a -> Grammar state tok c2 b) ->
  89 |       Grammar state tok (c1 || c2) b
  90 | seq = SeqEmpty
  91 | 
  92 | ||| Sequence a grammar followed by the grammar it returns.
  93 | export %inline
  94 | join : {c1,c2 : Bool} ->
  95 |        Grammar state tok c1 (Grammar state tok c2 a) ->
  96 |        Grammar state tok (c1 || c2) a
  97 | join {c1 = False} p = SeqEmpty p id
  98 | join {c1 = True} p = SeqEat p id
  99 | 
 100 | ||| Allows the result of a grammar to be mapped to a different value.
 101 | export
 102 | {c : _} ->
 103 | Functor (Grammar state tok c) where
 104 |   map f (Empty val)  = Empty (f val)
 105 |   map f (Fail bd fatal msg) = Fail bd fatal msg
 106 |   map f (Try g) = Try (map f g)
 107 |   map f (MustWork g) = MustWork (map f g)
 108 |   map f (Terminal msg g) = Terminal msg (map f . g)
 109 |   map f (Alt x y)    = Alt (map f x) (map f y)
 110 |   map f (SeqEat act next)
 111 |       = SeqEat act (\val => map f (next val))
 112 |   map f (SeqEmpty act next)
 113 |       = SeqEmpty act (\ val => map f (next val))
 114 |   map f (ThenEat act next)
 115 |       = ThenEat act (map f next)
 116 |   map f (ThenEmpty act next)
 117 |       = ThenEmpty act (map f next)
 118 |   map {c} f (Bounds act)
 119 |     = rewrite sym $ orFalseNeutral c in
 120 |       SeqEmpty (Bounds act) (Empty . f) -- Bounds (map f act)
 121 |   -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
 122 |   -- so a sequence must be used.
 123 |   map {c = False} f p = SeqEmpty p (Empty . f)
 124 | 
 125 | ||| Give two alternative grammars. If both consume, the combination is
 126 | ||| guaranteed to consume.
 127 | export %inline
 128 | (<|>) : {c1,c2 : Bool} ->
 129 |         Grammar state tok c1 ty ->
 130 |         Lazy (Grammar state tok c2 ty) ->
 131 |         Grammar state tok (c1 && c2) ty
 132 | (<|>) = Alt
 133 | 
 134 | export infixr 2 <||>
 135 | ||| Take the tagged disjunction of two grammars. If both consume, the
 136 | ||| combination is guaranteed to consume.
 137 | export
 138 | (<||>) : {c1,c2 : Bool} ->
 139 |         Grammar state tok c1 a ->
 140 |         Lazy (Grammar state tok c2 b) ->
 141 |         Grammar state tok (c1 && c2) (Either a b)
 142 | (<||>) p q = (Left <$> p) <|> (Right <$> q)
 143 | 
 144 | ||| Sequence a grammar with value type `a -> b` and a grammar
 145 | ||| with value type `a`. If both succeed, apply the function
 146 | ||| from the first grammar to the value from the second grammar.
 147 | ||| Guaranteed to consume if either grammar consumes.
 148 | export %inline
 149 | (<*>) : {c1, c2 : Bool} ->
 150 |         Grammar state tok c1 (a -> b) ->
 151 |         Grammar state tok c2 a ->
 152 |         Grammar state tok (c1 || c2) b
 153 | (<*>) x y = SeqEmpty x (\f => map f y)
 154 | 
 155 | ||| Sequence two grammars. If both succeed, use the value of the first one.
 156 | ||| Guaranteed to consume if either grammar consumes.
 157 | export %inline
 158 | (<*) : {c1,c2 : Bool} ->
 159 |        Grammar state tok c1 a ->
 160 |        Grammar state tok c2 b ->
 161 |        Grammar state tok (c1 || c2) a
 162 | (<*) x y = map const x <*> y
 163 | 
 164 | ||| Sequence two grammars. If both succeed, use the value of the second one.
 165 | ||| Guaranteed to consume if either grammar consumes.
 166 | export %inline
 167 | (*>) : {c1,c2 : Bool} ->
 168 |        Grammar state tok c1 a ->
 169 |        Grammar state tok c2 b ->
 170 |        Grammar state tok (c1 || c2) b
 171 | (*>) x y = map (const id) x <*> y
 172 | 
 173 | export %inline
 174 | act : state -> Grammar state tok False ()
 175 | act = Act
 176 | 
 177 | ||| Produce a grammar that can parse a different type of token by providing a
 178 | ||| function converting the new token type into the original one.
 179 | export
 180 | mapToken : (a -> b) -> Grammar state b c ty -> Grammar state a c ty
 181 | mapToken f (Empty val) = Empty val
 182 | mapToken f (Terminal msg g) = Terminal msg (g . f)
 183 | mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . f)) (Empty . f)
 184 | mapToken f EOF = EOF
 185 | mapToken f (Warning bd msg) = Warning bd msg
 186 | mapToken f (Fail bd fatal msg) = Fail bd fatal msg
 187 | mapToken f (Try g) = Try (mapToken f g)
 188 | mapToken f (MustWork g) = MustWork (mapToken f g)
 189 | mapToken f Commit = Commit
 190 | mapToken f (SeqEat act next)
 191 |   = SeqEat (mapToken f act) (\x => mapToken f (next x))
 192 | mapToken f (SeqEmpty act next)
 193 |   = SeqEmpty (mapToken f act) (\x => mapToken f (next x))
 194 | mapToken f (ThenEat act next)
 195 |   = ThenEat (mapToken f act) (mapToken f next)
 196 | mapToken f (ThenEmpty act next)
 197 |   = ThenEmpty (mapToken f act) (mapToken f next)
 198 | mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
 199 | mapToken f (Bounds act) = Bounds (mapToken f act)
 200 | mapToken f Position = Position
 201 | mapToken f (Act action) = Act action
 202 | 
 203 | ||| Always succeed with the given value.
 204 | export %inline
 205 | pure : (val : ty) -> Grammar state tok False ty
 206 | pure = Empty
 207 | 
 208 | ||| Check whether the next token satisfies a predicate
 209 | export %inline
 210 | nextIs : String -> (tok -> Bool) -> Grammar state tok False tok
 211 | nextIs = NextIs
 212 | 
 213 | ||| Look at the next token in the input
 214 | export %inline
 215 | peek : Grammar state tok False tok
 216 | peek = nextIs "Unrecognised token" (const True)
 217 | 
 218 | ||| Succeeds if running the predicate on the next token returns Just x,
 219 | ||| returning x. Otherwise fails.
 220 | export %inline
 221 | terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
 222 | terminal = Terminal
 223 | 
 224 | ||| Always fail with a message
 225 | export %inline
 226 | fail : String -> Grammar state tok c ty
 227 | fail = Fail Nothing False
 228 | 
 229 | ||| Always fail with a message and a location
 230 | export %inline
 231 | failLoc : Bounds -> String -> Grammar state tok c ty
 232 | failLoc b = Fail (Just b) False
 233 | 
 234 | ||| Fail with no possibility for recovery (i.e.
 235 | ||| no alternative parsing can succeed).
 236 | export %inline
 237 | fatalError : String -> Grammar state tok c ty
 238 | fatalError = Fail Nothing True
 239 | 
 240 | ||| Fail with no possibility for recovery (i.e.
 241 | ||| no alternative parsing can succeed).
 242 | export %inline
 243 | fatalLoc : Bounds -> String -> Grammar state tok c ty
 244 | fatalLoc b = Fail (Just b) True
 245 | 
 246 | ||| Catch a fatal error
 247 | export %inline
 248 | try : Grammar state tok c ty -> Grammar state tok c ty
 249 | try = Try
 250 | 
 251 | ||| Succeed if the input is empty
 252 | export %inline
 253 | eof : Grammar state tok False ()
 254 | eof = EOF
 255 | 
 256 | ||| Commit to an alternative; if the current branch of an alternative
 257 | ||| fails to parse, no more branches will be tried
 258 | export %inline
 259 | commit : Grammar state tok False ()
 260 | commit = Commit
 261 | 
 262 | ||| If the parser fails, treat it as a fatal error
 263 | export %inline
 264 | mustWork : {c : Bool} -> Grammar state tok c ty -> Grammar state tok c ty
 265 | mustWork = MustWork
 266 | 
 267 | ||| If the parser fails, treat it as a fatal error and explain why
 268 | export
 269 | mustWorkBecause :
 270 |   {c : Bool} -> Bounds -> String ->
 271 |   Grammar state tok c ty -> Grammar state tok c ty
 272 | mustWorkBecause {c} loc msg p
 273 |   = rewrite sym (andSameNeutral c) in
 274 |     p <|> fatalLoc loc msg
 275 | 
 276 | export %inline
 277 | bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
 278 | bounds = Bounds
 279 | 
 280 | export
 281 | mustFailBecause :
 282 |   String ->
 283 |   Grammar state tok True ty -> Grammar state tok False Unit
 284 | mustFailBecause msg p
 285 |   = (bounds p >>= \res => fatalLoc {c=False} res.bounds msg) <|> pure ()
 286 | 
 287 | export %inline
 288 | position : Grammar state tok False Bounds
 289 | position = Position
 290 | 
 291 | ||| Warn the user
 292 | export %inline
 293 | withWarning : {c : _} -> String -> Grammar state tok c ty -> Grammar state tok c ty
 294 | withWarning warn p
 295 |     = rewrite sym $ orFalseNeutral c in
 296 |       SeqEmpty (bounds p) $ \ res =>
 297 |       do Warning (Just res.bounds) warn
 298 |          pure res.val
 299 | 
 300 | public export
 301 | data ParsingError tok = Error String (Maybe Bounds)
 302 | 
 303 | public export
 304 | ParsingWarnings : Type
 305 | ParsingWarnings = List (Maybe Bounds, String)
 306 | 
 307 | data ParseResult : Type -> Type -> Type -> Type where
 308 |      Failure : (committed : Bool) -> (fatal : Bool) ->
 309 |                List1 (ParsingError tok) -> ParseResult state tok ty
 310 |      Res : state ->
 311 |            (ws : ParsingWarnings) ->
 312 |            (committed : Bool) ->
 313 |            (val : WithBounds ty) ->
 314 |            (more : List (WithBounds tok)) ->
 315 |            ParseResult state tok ty
 316 | 
 317 | mergeWith : WithBounds ty -> ParseResult state tok sy -> ParseResult state tok sy
 318 | mergeWith x (Res s ws committed val more) = Res s ws committed (mergeBounds x val) more
 319 | mergeWith x v = v
 320 | 
 321 | doParse : Semigroup state =>
 322 |           state -> (ws : ParsingWarnings) ->
 323 |           (commit : Bool) ->
 324 |           (act : Grammar state tok c ty) ->
 325 |           (xs : List (WithBounds tok)) ->
 326 |           ParseResult state tok ty
 327 | doParse s ws com (Empty val) xs = Res s ws com (irrelevantBounds val) xs
 328 | doParse s ws com (Warning mb msg) xs = Res s ((mb, msg) :: ws) com (irrelevantBounds ()) xs
 329 | doParse s ws com (Fail location fatal str) xs
 330 |     = Failure com fatal (Error str (location <|> (bounds <$> head' xs)) ::: Nil)
 331 | doParse s ws com (Try g) xs = case doParse s ws com g xs of
 332 |   -- recover from fatal match but still propagate the 'commit'
 333 |   Failure com _ errs => Failure com False errs
 334 |   res => res
 335 | doParse s ws com Commit xs = Res s ws True (irrelevantBounds ()) xs
 336 | doParse s ws com (MustWork g) xs =
 337 |   case doParse s ws com g xs of
 338 |        Failure com' _ errs => Failure com' True errs
 339 |        res => res
 340 | doParse s ws com (Terminal err f) [] = Failure com False (Error "End of input" Nothing ::: Nil)
 341 | doParse s ws com (Terminal err f) (x :: xs) =
 342 |   case f x.val of
 343 |        Nothing => Failure com False (Error err (Just x.bounds) ::: Nil)
 344 |        Just a => Res s ws com (const a <$> x) xs
 345 | doParse s ws com EOF [] = Res s ws com (irrelevantBounds ()) []
 346 | doParse s ws com EOF (x :: xs) = Failure com False (Error "Expected end of input" (Just x.bounds) ::: Nil)
 347 | doParse s ws com (NextIs err f) [] = Failure com False (Error "End of input" Nothing ::: Nil)
 348 | doParse s ws com (NextIs err f) (x :: xs)
 349 |       = if f x.val
 350 |            then Res s ws com (removeIrrelevance x) (x :: xs)
 351 |            else Failure com False (Error err (Just x.bounds) ::: Nil)
 352 | doParse s ws com (Alt {c1} {c2} x y) xs
 353 |     = case doParse s ws False x xs of
 354 |            Failure com' fatal errs
 355 |               => if com' || fatal
 356 |                         -- If the alternative had committed, don't try the
 357 |                         -- other branch (and reset commit flag)
 358 |                    then Failure com fatal errs
 359 |                    else case doParse s ws False y xs of
 360 |                              (Failure com'' fatal' errs') => if com'' || fatal'
 361 |                                                                      -- Only add the errors together if the second branch
 362 |                                                                      -- is also non-committed and non-fatal.
 363 |                                                              then Failure com'' fatal' errs'
 364 |                                                              else Failure com False (errs ++ errs')
 365 |                              (Res s ws _ val xs) => Res s ws com val xs
 366 |            -- Successfully parsed the first option, so use the outer commit flag
 367 |            Res s ws _ val xs => Res s ws com val xs
 368 | doParse s ws com (SeqEmpty act next) xs
 369 |     = case doParse s ws com act xs of
 370 |            Failure com fatal errs => Failure com fatal errs
 371 |            Res s ws com v xs =>
 372 |              mergeWith v $ doParse s ws com (next v.val) xs
 373 | doParse s ws com (SeqEat act next) xs
 374 |     = case doParse s ws com act xs of
 375 |            Failure com fatal errs => Failure com fatal errs
 376 |            Res s ws com v xs =>
 377 |              mergeWith v $ assert_total doParse s ws com (next v.val) xs
 378 | doParse s ws com (ThenEmpty act next) xs
 379 |     = case doParse s ws com act xs of
 380 |            Failure com fatal errs => Failure com fatal errs
 381 |            Res s ws com v xs =>
 382 |              mergeWith v $ doParse s ws com next xs
 383 | doParse s ws com (ThenEat act next) xs
 384 |     = case doParse s ws com act xs of
 385 |            Failure com fatal errs => Failure com fatal errs
 386 |            Res s ws com v xs =>
 387 |              mergeWith v $ assert_total doParse s ws com next xs
 388 | doParse s ws com (Bounds act) xs
 389 |     = case doParse s ws com act xs of
 390 |            Failure com fatal errs => Failure com fatal errs
 391 |            Res s ws com v xs => Res s ws com (const v <$> v) xs
 392 | doParse s ws com Position [] = Failure com False (Error "End of input" Nothing ::: Nil)
 393 | doParse s ws com Position (x :: xs)
 394 |     = Res s ws com (irrelevantBounds x.bounds) (x :: xs)
 395 | doParse s ws com (Act action) xs
 396 |   = Res (s <+> action) ws com (irrelevantBounds ()) xs
 397 | 
 398 | ||| Parse a list of tokens according to the given grammar. If successful,
 399 | ||| returns a pair of the parse result and the unparsed tokens (the remaining
 400 | ||| input).
 401 | export
 402 | parse : {c : Bool} -> (act : Grammar () tok c ty) -> (xs : List (WithBounds tok)) ->
 403 |         Either (List1 (ParsingError tok))
 404 |                (ParsingWarnings, ty, List (WithBounds tok))
 405 | parse act xs
 406 |     = case doParse neutral [] False act xs of
 407 |            Failure _ _ errs => Left errs
 408 |            Res _ ws _ v rest => Right (ws, v.val, rest)
 409 | 
 410 | export
 411 | parseWith : Monoid state => {c : Bool} -> (act : Grammar state tok c ty) -> (xs : List (WithBounds tok)) ->
 412 |         Either (List1 (ParsingError tok))
 413 |                (state, ParsingWarnings, ty, List (WithBounds tok))
 414 | parseWith act xs
 415 |     = case doParse neutral [] False act xs of
 416 |            Failure _ _ errs => Left errs
 417 |            Res s ws _ v rest => Right (s, ws, v.val, rest)
 418 |