Text.Parser.Core


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