core: Factor parseExactChar into the effect

This commit is contained in:
Nathan McCarty 2025-01-26 21:06:22 -05:00
parent 08a2f263bb
commit 93d4d876d9
2 changed files with 12 additions and 2 deletions

View file

@ -235,8 +235,7 @@ Attempt to parse a specified character
export export
parseExactChar : Char -> Parser Char parseExactChar : Char -> Parser Char
parseExactChar c = do parseExactChar c = do
pnote "Parsing exact char: \{show c}" result <- parseExactChar' c
result <- parseChar (== c)
case result of case result of
GotChar char => pure char GotChar char => pure char
GotError err => throwParseError "Got \{show err} Expected \{show c}" GotError err => throwParseError "Got \{show err} Expected \{show c}"

View file

@ -211,6 +211,7 @@ data ParserState : Type -> Type where
-- TODO: Maybe add a ParseString that parses a string of characters as a -- TODO: Maybe add a ParseString that parses a string of characters as a
-- string using efficent slicing? -- string using efficent slicing?
ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult
ParseExactChar : (char : Char) -> ParserState ParseCharResult
ParseEoF : ParserState Bool ParseEoF : ParserState Bool
Note : Lazy String -> ParserState () Note : Lazy String -> ParserState ()
``` ```
@ -220,6 +221,7 @@ Show (ParserState t) where
show Save = "Saving state" show Save = "Saving state"
show (Load pi) = "Loading state \{show pi}" show (Load pi) = "Loading state \{show pi}"
show (ParseChar predicate) = "Parsing char" show (ParseChar predicate) = "Parsing char"
show (ParseExactChar char) = "Parsing char \{show char}"
show ParseEoF = "Parsing EoF" show ParseEoF = "Parsing EoF"
show (Note _) = "Note" show (Note _) = "Note"
--> -->
@ -245,6 +247,11 @@ parseChar : Has ParserState fs => (predicate : Char -> Bool)
-> Eff fs ParseCharResult -> Eff fs ParseCharResult
parseChar predicate = send $ ParseChar predicate 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 ||| "Parse" the end of input, returning `True` if the parser state is currently
||| at the end of the input ||| at the end of the input
export export
@ -289,6 +296,9 @@ handleParserStateIO pi (ParseChar predicate) = do
Just (Element next _) => do Just (Element next _) => do
writeIORef pi.position $ MkIndex next writeIORef pi.position $ MkIndex next
pure $ GotChar char pure $ GotChar char
handleParserStateIO pi (ParseExactChar chr) = do
-- TODO: do this directly?
handleParserStateIO pi (ParseChar (== chr))
handleParserStateIO pi ParseEoF = do handleParserStateIO pi ParseEoF = do
pi <- readIORef pi pi <- readIORef pi
readIORef pi.end_of_input readIORef pi.end_of_input
@ -340,6 +350,7 @@ unPS pi (ParseChar predicate) =
Just (Element next _) => Just (Element next _) =>
(GotChar char, {position := MkIndex next} pi) (GotChar char, {position := MkIndex next} pi)
else (GotError char, pi) else (GotError char, pi)
unPS pi (ParseExactChar chr) = unPS pi (ParseChar (== chr))
unPS pi ParseEoF = (pi.end_of_input, pi) unPS pi ParseEoF = (pi.end_of_input, pi)
unPS pi (Note _) = ((), pi) unPS pi (Note _) = ((), pi)