diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index ddf26c5..d9c2db2 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -235,8 +235,7 @@ Attempt to parse a specified character export parseExactChar : Char -> Parser Char parseExactChar c = do - pnote "Parsing exact char: \{show c}" - result <- parseChar (== c) + result <- parseExactChar' c case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected \{show c}" diff --git a/src/Parser/ParserState.md b/src/Parser/ParserState.md index 703e5a7..8668a16 100644 --- a/src/Parser/ParserState.md +++ b/src/Parser/ParserState.md @@ -211,6 +211,7 @@ data ParserState : Type -> Type where -- TODO: Maybe add a ParseString that parses a string of characters as a -- string using efficent slicing? ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult + ParseExactChar : (char : Char) -> ParserState ParseCharResult ParseEoF : ParserState Bool Note : Lazy String -> ParserState () ``` @@ -220,6 +221,7 @@ Show (ParserState t) where show Save = "Saving state" show (Load pi) = "Loading state \{show pi}" show (ParseChar predicate) = "Parsing char" + show (ParseExactChar char) = "Parsing char \{show char}" show ParseEoF = "Parsing EoF" show (Note _) = "Note" --> @@ -245,6 +247,11 @@ parseChar : Has ParserState fs => (predicate : Char -> Bool) -> Eff fs ParseCharResult parseChar predicate = send $ ParseChar predicate +||| Parse a char by exact value +export +parseExactChar' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult +parseExactChar' chr = send $ ParseExactChar chr + ||| "Parse" the end of input, returning `True` if the parser state is currently ||| at the end of the input export @@ -289,6 +296,9 @@ handleParserStateIO pi (ParseChar predicate) = do Just (Element next _) => do writeIORef pi.position $ MkIndex next pure $ GotChar char +handleParserStateIO pi (ParseExactChar chr) = do + -- TODO: do this directly? + handleParserStateIO pi (ParseChar (== chr)) handleParserStateIO pi ParseEoF = do pi <- readIORef pi readIORef pi.end_of_input @@ -340,6 +350,7 @@ unPS pi (ParseChar predicate) = Just (Element next _) => (GotChar char, {position := MkIndex next} pi) else (GotError char, pi) +unPS pi (ParseExactChar chr) = unPS pi (ParseChar (== chr)) unPS pi ParseEoF = (pi.end_of_input, pi) unPS pi (Note _) = ((), pi)