mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-28 22:22:10 +03:00
383 lines
15 KiB
Idris
383 lines
15 KiB
Idris
module Text.Parser.Core
|
|
|
|
import Data.Bool
|
|
import Data.List
|
|
import Data.List1
|
|
|
|
import public Control.Delayed
|
|
import public Text.Bounded
|
|
|
|
%default total
|
|
|
|
-- TODO: Add some primitives for helping with error messages.
|
|
-- e.g. perhaps set a string to state what we're currently trying to
|
|
-- parse, or to say what the next expected token is in words
|
|
|
|
||| Description of a language's grammar. The `tok` parameter is the type
|
|
||| of tokens, and the `consumes` flag is True if the language is guaranteed
|
|
||| to be non-empty - that is, successfully parsing the language is guaranteed
|
|
||| to consume some input.
|
|
export
|
|
data Grammar : (state : Type) -> (tok : Type) -> (consumes : Bool) -> Type -> Type where
|
|
Empty : (val : ty) -> Grammar state tok False ty
|
|
Terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
|
|
NextIs : String -> (tok -> Bool) -> Grammar state tok False tok
|
|
EOF : Grammar state tok False ()
|
|
|
|
Fail : (location : Maybe Bounds) -> (fatal : Bool) -> String -> Grammar state tok c ty
|
|
Try : Grammar state tok c ty -> Grammar state tok c ty
|
|
|
|
Commit : Grammar state tok False ()
|
|
MustWork : Grammar state tok c a -> Grammar state tok c a
|
|
|
|
SeqEat : {c2 : Bool} ->
|
|
Grammar state tok True a -> Inf (a -> Grammar state tok c2 b) ->
|
|
Grammar state tok True b
|
|
SeqEmpty : {c1, c2 : Bool} ->
|
|
Grammar state tok c1 a -> (a -> Grammar state tok c2 b) ->
|
|
Grammar state tok (c1 || c2) b
|
|
|
|
ThenEat : {c2 : Bool} ->
|
|
Grammar state tok True () -> Inf (Grammar state tok c2 a) ->
|
|
Grammar state tok True a
|
|
ThenEmpty : {c1, c2 : Bool} ->
|
|
Grammar state tok c1 () -> Grammar state tok c2 a ->
|
|
Grammar state tok (c1 || c2) a
|
|
|
|
Alt : {c1, c2 : Bool} ->
|
|
Grammar state tok c1 ty -> Lazy (Grammar state tok c2 ty) ->
|
|
Grammar state tok (c1 && c2) ty
|
|
Bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
|
|
Position : Grammar state tok False Bounds
|
|
|
|
Act : state -> Grammar state tok False ()
|
|
|
|
||| Sequence two grammars. If either consumes some input, the sequence is
|
|
||| guaranteed to consume some input. If the first one consumes input, the
|
|
||| second is allowed to be recursive (because it means some input has been
|
|
||| consumed and therefore the input is smaller)
|
|
export %inline
|
|
(>>=) : {c1, c2 : Bool} ->
|
|
Grammar state tok c1 a ->
|
|
inf c1 (a -> Grammar state tok c2 b) ->
|
|
Grammar state tok (c1 || c2) b
|
|
(>>=) {c1 = False} = SeqEmpty
|
|
(>>=) {c1 = True} = SeqEat
|
|
|
|
||| Sequence two grammars. If either consumes some input, the sequence is
|
|
||| guaranteed to consume some input. If the first one consumes input, the
|
|
||| second is allowed to be recursive (because it means some input has been
|
|
||| consumed and therefore the input is smaller)
|
|
public export %inline %tcinline
|
|
(>>) : {c1, c2 : Bool} ->
|
|
Grammar state tok c1 () ->
|
|
inf c1 (Grammar state tok c2 a) ->
|
|
Grammar state tok (c1 || c2) a
|
|
(>>) {c1 = False} = ThenEmpty
|
|
(>>) {c1 = True} = ThenEat
|
|
|
|
||| Sequence two grammars. If either consumes some input, the sequence is
|
|
||| guaranteed to consume input. This is an explicitly non-infinite version
|
|
||| of `>>=`.
|
|
export %inline
|
|
seq : {c1,c2 : Bool} ->
|
|
Grammar state tok c1 a ->
|
|
(a -> Grammar state tok c2 b) ->
|
|
Grammar state tok (c1 || c2) b
|
|
seq = SeqEmpty
|
|
|
|
||| Sequence a grammar followed by the grammar it returns.
|
|
export %inline
|
|
join : {c1,c2 : Bool} ->
|
|
Grammar state tok c1 (Grammar state tok c2 a) ->
|
|
Grammar state tok (c1 || c2) a
|
|
join {c1 = False} p = SeqEmpty p id
|
|
join {c1 = True} p = SeqEat p id
|
|
|
|
||| Allows the result of a grammar to be mapped to a different value.
|
|
export
|
|
{c : _} ->
|
|
Functor (Grammar state tok c) where
|
|
map f (Empty val) = Empty (f val)
|
|
map f (Fail bd fatal msg) = Fail bd fatal msg
|
|
map f (Try g) = Try (map f g)
|
|
map f (MustWork g) = MustWork (map f g)
|
|
map f (Terminal msg g) = Terminal msg (map f . g)
|
|
map f (Alt x y) = Alt (map f x) (map f y)
|
|
map f (SeqEat act next)
|
|
= SeqEat act (\val => map f (next val))
|
|
map f (SeqEmpty act next)
|
|
= SeqEmpty act (\ val => map f (next val))
|
|
map f (ThenEat act next)
|
|
= ThenEat act (map f next)
|
|
map f (ThenEmpty act next)
|
|
= ThenEmpty act (map f next)
|
|
map {c} f (Bounds act)
|
|
= rewrite sym $ orFalseNeutral c in
|
|
SeqEmpty (Bounds act) (Empty . f) -- Bounds (map f act)
|
|
-- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
|
|
-- so a sequence must be used.
|
|
map {c = False} f p = SeqEmpty p (Empty . f)
|
|
|
|
||| Give two alternative grammars. If both consume, the combination is
|
|
||| guaranteed to consume.
|
|
export %inline
|
|
(<|>) : {c1,c2 : Bool} ->
|
|
Grammar state tok c1 ty ->
|
|
Lazy (Grammar state tok c2 ty) ->
|
|
Grammar state tok (c1 && c2) ty
|
|
(<|>) = Alt
|
|
|
|
infixr 2 <||>
|
|
||| Take the tagged disjunction of two grammars. If both consume, the
|
|
||| combination is guaranteed to consume.
|
|
export
|
|
(<||>) : {c1,c2 : Bool} ->
|
|
Grammar state tok c1 a ->
|
|
Lazy (Grammar state tok c2 b) ->
|
|
Grammar state tok (c1 && c2) (Either a b)
|
|
(<||>) p q = (Left <$> p) <|> (Right <$> q)
|
|
|
|
||| Sequence a grammar with value type `a -> b` and a grammar
|
|
||| with value type `a`. If both succeed, apply the function
|
|
||| from the first grammar to the value from the second grammar.
|
|
||| Guaranteed to consume if either grammar consumes.
|
|
export %inline
|
|
(<*>) : {c1, c2 : Bool} ->
|
|
Grammar state tok c1 (a -> b) ->
|
|
Grammar state tok c2 a ->
|
|
Grammar state tok (c1 || c2) b
|
|
(<*>) x y = SeqEmpty x (\f => map f y)
|
|
|
|
||| Sequence two grammars. If both succeed, use the value of the first one.
|
|
||| Guaranteed to consume if either grammar consumes.
|
|
export %inline
|
|
(<*) : {c1,c2 : Bool} ->
|
|
Grammar state tok c1 a ->
|
|
Grammar state tok c2 b ->
|
|
Grammar state tok (c1 || c2) a
|
|
(<*) x y = map const x <*> y
|
|
|
|
||| Sequence two grammars. If both succeed, use the value of the second one.
|
|
||| Guaranteed to consume if either grammar consumes.
|
|
export %inline
|
|
(*>) : {c1,c2 : Bool} ->
|
|
Grammar state tok c1 a ->
|
|
Grammar state tok c2 b ->
|
|
Grammar state tok (c1 || c2) b
|
|
(*>) x y = map (const id) x <*> y
|
|
|
|
export %inline
|
|
act : state -> Grammar state tok False ()
|
|
act = Act
|
|
|
|
||| Produce a grammar that can parse a different type of token by providing a
|
|
||| function converting the new token type into the original one.
|
|
export
|
|
mapToken : (a -> b) -> Grammar state b c ty -> Grammar state a c ty
|
|
mapToken f (Empty val) = Empty val
|
|
mapToken f (Terminal msg g) = Terminal msg (g . f)
|
|
mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . f)) (Empty . f)
|
|
mapToken f EOF = EOF
|
|
mapToken f (Fail bd fatal msg) = Fail bd fatal msg
|
|
mapToken f (Try g) = Try (mapToken f g)
|
|
mapToken f (MustWork g) = MustWork (mapToken f g)
|
|
mapToken f Commit = Commit
|
|
mapToken f (SeqEat act next)
|
|
= SeqEat (mapToken f act) (\x => mapToken f (next x))
|
|
mapToken f (SeqEmpty act next)
|
|
= SeqEmpty (mapToken f act) (\x => mapToken f (next x))
|
|
mapToken f (ThenEat act next)
|
|
= ThenEat (mapToken f act) (mapToken f next)
|
|
mapToken f (ThenEmpty act next)
|
|
= ThenEmpty (mapToken f act) (mapToken f next)
|
|
mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
|
|
mapToken f (Bounds act) = Bounds (mapToken f act)
|
|
mapToken f Position = Position
|
|
mapToken f (Act action) = Act action
|
|
|
|
||| Always succeed with the given value.
|
|
export %inline
|
|
pure : (val : ty) -> Grammar state tok False ty
|
|
pure = Empty
|
|
|
|
||| Check whether the next token satisfies a predicate
|
|
export %inline
|
|
nextIs : String -> (tok -> Bool) -> Grammar state tok False tok
|
|
nextIs = NextIs
|
|
|
|
||| Look at the next token in the input
|
|
export %inline
|
|
peek : Grammar state tok False tok
|
|
peek = nextIs "Unrecognised token" (const True)
|
|
|
|
||| Succeeds if running the predicate on the next token returns Just x,
|
|
||| returning x. Otherwise fails.
|
|
export %inline
|
|
terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
|
|
terminal = Terminal
|
|
|
|
||| Always fail with a message
|
|
export %inline
|
|
fail : String -> Grammar state tok c ty
|
|
fail = Fail Nothing False
|
|
|
|
||| Always fail with a message and a location
|
|
export %inline
|
|
failLoc : Bounds -> String -> Grammar state tok c ty
|
|
failLoc b = Fail (Just b) False
|
|
|
|
||| Fail with no possibility for recovery (i.e.
|
|
||| no alternative parsing can succeed).
|
|
export %inline
|
|
fatalError : String -> Grammar state tok c ty
|
|
fatalError = Fail Nothing True
|
|
|
|
||| Fail with no possibility for recovery (i.e.
|
|
||| no alternative parsing can succeed).
|
|
export %inline
|
|
fatalLoc : Bounds -> String -> Grammar state tok c ty
|
|
fatalLoc b = Fail (Just b) True
|
|
|
|
||| Catch a fatal error
|
|
export %inline
|
|
try : Grammar state tok c ty -> Grammar state tok c ty
|
|
try = Try
|
|
|
|
||| Succeed if the input is empty
|
|
export %inline
|
|
eof : Grammar state tok False ()
|
|
eof = EOF
|
|
|
|
||| Commit to an alternative; if the current branch of an alternative
|
|
||| fails to parse, no more branches will be tried
|
|
export %inline
|
|
commit : Grammar state tok False ()
|
|
commit = Commit
|
|
|
|
||| If the parser fails, treat it as a fatal error
|
|
export %inline
|
|
mustWork : {c : Bool} -> Grammar state tok c ty -> Grammar state tok c ty
|
|
mustWork = MustWork
|
|
|
|
export %inline
|
|
bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
|
|
bounds = Bounds
|
|
|
|
export %inline
|
|
position : Grammar state tok False Bounds
|
|
position = Position
|
|
|
|
public export
|
|
data ParsingError tok = Error String (Maybe Bounds)
|
|
|
|
export
|
|
Show tok => Show (ParsingError tok) where
|
|
show (Error s Nothing) = "PARSING ERROR: " ++ s
|
|
show (Error s (Just (MkBounds startLine startCol endLine endCol))) =
|
|
"PARSING ERROR: "
|
|
++ s
|
|
++ " @ L\{show startLine}:\{show startCol}-L\{show endLine}:\{show endCol}"
|
|
|
|
data ParseResult : Type -> Type -> Type -> Type where
|
|
Failure : (committed : Bool) -> (fatal : Bool) ->
|
|
List1 (ParsingError tok) -> ParseResult state tok ty
|
|
Res : state -> (committed : Bool) ->
|
|
(val : WithBounds ty) -> (more : List (WithBounds tok)) -> ParseResult state tok ty
|
|
|
|
mergeWith : WithBounds ty -> ParseResult state tok sy -> ParseResult state tok sy
|
|
mergeWith x (Res s committed val more) = Res s committed (mergeBounds x val) more
|
|
mergeWith x v = v
|
|
|
|
doParse : Semigroup state => state -> (commit : Bool) ->
|
|
(act : Grammar state tok c ty) ->
|
|
(xs : List (WithBounds tok)) ->
|
|
ParseResult state tok ty
|
|
doParse s com (Empty val) xs = Res s com (irrelevantBounds val) xs
|
|
doParse s com (Fail location fatal str) xs
|
|
= Failure com fatal (Error str (location <|> (bounds <$> head' xs)) ::: Nil)
|
|
doParse s com (Try g) xs = case doParse s com g xs of
|
|
-- recover from fatal match but still propagate the 'commit'
|
|
Failure com _ errs => Failure com False errs
|
|
res => res
|
|
doParse s com Commit xs = Res s True (irrelevantBounds ()) xs
|
|
doParse s com (MustWork g) xs =
|
|
case assert_total (doParse s com g xs) of
|
|
Failure com' _ errs => Failure com' True errs
|
|
res => res
|
|
doParse s com (Terminal err f) [] = Failure com False (Error "End of input" Nothing ::: Nil)
|
|
doParse s com (Terminal err f) (x :: xs) =
|
|
case f x.val of
|
|
Nothing => Failure com False (Error err (Just x.bounds) ::: Nil)
|
|
Just a => Res s com (const a <$> x) xs
|
|
doParse s com EOF [] = Res s com (irrelevantBounds ()) []
|
|
doParse s com EOF (x :: xs) = Failure com False (Error "Expected end of input" (Just x.bounds) ::: Nil)
|
|
doParse s com (NextIs err f) [] = Failure com False (Error "End of input" Nothing ::: Nil)
|
|
doParse s com (NextIs err f) (x :: xs)
|
|
= if f x.val
|
|
then Res s com (removeIrrelevance x) (x :: xs)
|
|
else Failure com False (Error err (Just x.bounds) ::: Nil)
|
|
doParse s com (Alt {c1} {c2} x y) xs
|
|
= case doParse s False x xs of
|
|
Failure com' fatal errs
|
|
=> if com' || fatal
|
|
-- If the alternative had committed, don't try the
|
|
-- other branch (and reset commit flag)
|
|
then Failure com fatal errs
|
|
else case (assert_total doParse s False y xs) of
|
|
(Failure com'' fatal' errs') => if com'' || fatal'
|
|
-- Only add the errors together if the second branch
|
|
-- is also non-committed and non-fatal.
|
|
then Failure com'' fatal' errs'
|
|
else Failure com False (errs ++ errs')
|
|
(Res s _ val xs) => Res s com val xs
|
|
-- Successfully parsed the first option, so use the outer commit flag
|
|
Res s _ val xs => Res s com val xs
|
|
doParse s com (SeqEmpty act next) xs
|
|
= case assert_total (doParse s com act xs) of
|
|
Failure com fatal errs => Failure com fatal errs
|
|
Res s com v xs =>
|
|
mergeWith v (assert_total $ doParse s com (next v.val) xs)
|
|
doParse s com (SeqEat act next) xs
|
|
= case assert_total (doParse s com act xs) of
|
|
Failure com fatal errs => Failure com fatal errs
|
|
Res s com v xs =>
|
|
mergeWith v (assert_total $ doParse s com (next v.val) xs)
|
|
doParse s com (ThenEmpty act next) xs
|
|
= case assert_total (doParse s com act xs) of
|
|
Failure com fatal errs => Failure com fatal errs
|
|
Res s com v xs =>
|
|
mergeWith v (assert_total $ doParse s com next xs)
|
|
doParse s com (ThenEat act next) xs
|
|
= case assert_total (doParse s com act xs) of
|
|
Failure com fatal errs => Failure com fatal errs
|
|
Res s com v xs =>
|
|
mergeWith v (assert_total $ doParse s com next xs)
|
|
doParse s com (Bounds act) xs
|
|
= case assert_total (doParse s com act xs) of
|
|
Failure com fatal errs => Failure com fatal errs
|
|
Res s com v xs => Res s com (const v <$> v) xs
|
|
doParse s com Position [] = Failure com False (Error "End of input" Nothing ::: Nil)
|
|
doParse s com Position (x :: xs)
|
|
= Res s com (irrelevantBounds x.bounds) (x :: xs)
|
|
doParse s com (Act action) xs = Res (s <+> action) com (irrelevantBounds ()) xs
|
|
|
|
||| Parse a list of tokens according to the given grammar. If successful,
|
|
||| returns a pair of the parse result and the unparsed tokens (the remaining
|
|
||| input).
|
|
export
|
|
parse : {c : Bool} -> (act : Grammar () tok c ty) -> (xs : List (WithBounds tok)) ->
|
|
Either (List1 (ParsingError tok)) (ty, List (WithBounds tok))
|
|
parse act xs
|
|
= case doParse neutral False act xs of
|
|
Failure _ _ errs => Left errs
|
|
Res _ _ v rest => Right (v.val, rest)
|
|
|
|
export
|
|
parseWith : Monoid state => {c : Bool} -> (act : Grammar state tok c ty) -> (xs : List (WithBounds tok)) ->
|
|
Either (List1 (ParsingError tok)) (state, ty, List (WithBounds tok))
|
|
parseWith act xs
|
|
= case doParse neutral False act xs of
|
|
Failure _ _ errs => Left errs
|
|
Res s _ v rest => Right (s, v.val, rest)
|