core: oneOfM refactor

This commit is contained in:
Nathan McCarty 2025-01-25 13:37:08 -05:00
parent 59fba4584d
commit 72ea53becf

View file

@ -20,8 +20,11 @@ Combine the parser state at time of error with an error message.
```idris
public export
data ParseError : Type where
-- TODO: Rename this constructor
MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
BeforeParse : (message : String) -> ParseError
NestedErrors : (state : ParserInternal Id) -> (message : String)
-> (rest : List ParseError) -> ParseError
```
<!-- idris
@ -34,6 +37,13 @@ Show ParseError where
in "Error at line \{line}, column \{col} (\{position}): \{message}"
show (BeforeParse message) =
"Error before parsing: \{message}"
show (NestedErrors state message rest) =
let rest = assert_total $joinBy "\n" . map ((" " ++) . show) $ rest
(line, col) = positionPair state
(line, col) = (show line, show col)
position = show state.position.index
first = "Error at line \{line}, column \{col} (\{position}): \{message}"
in "\{first}\n\{rest}"
-->
## Type Alias
@ -41,7 +51,7 @@ Show ParseError where
```idris
public export
Parser : Type -> Type
Parser a = Eff [ParserState, Except ParseError, Choose] a
Parser a = Eff [ParserState, Except ParseError] a
```
## Error Generation
@ -93,7 +103,7 @@ no paths in the `Choice` effect produce a returning parse.
export
rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a)
rundownFirst f =
runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f
runExcept f
```
Provide wrappers for `rundownFirst` for evaluating it in various contexts.
@ -148,27 +158,29 @@ tryMaybe f = try (map Just f) (\_ => pure Nothing)
export
tryEither : (f : Parser a) -> Parser (Either ParseError a)
tryEither f = try (map Right f) (pure . Left)
||| Converts any errors thrown by `f` into silent backtracking within `Choose`
export
tryEmpty : (f : Parser a) -> Parser a
tryEmpty f = try f (\_ => empty)
```
Attempt to parse one of the given input parsers, in the provided order, invoking
the provided error action on failure. This will suppress any errors returned by
the input parsers by mapping them to `empty`.
the provided error action on failure.
The state will not be modified when an input parser fails
```idris
export
oneOfE : Foldable f =>
(err : Parser a) -> f (Parser a) -> Parser a
oneOfE err xs = foldr altE err xs
oneOfE : (err : String) -> List (Parser a) -> Parser a
oneOfE err xs = do
start <- save
oneOfE' err start [] xs
where
altE : Parser a -> Parser a -> Parser a
altE f rest = (tryEmpty f) `alt` rest
oneOfE' : (err : String) -> (start : ParserInternal Id)
-> (errs : List ParseError) -> List (Parser a) -> Parser a
oneOfE' err start errs [] = do
throw $ NestedErrors start err (reverse errs)
oneOfE' err start errs (x :: xs) = do
x <- tryEither x
case x of
Right val => pure val
Left error => oneOfE' err start (error :: errs) xs
```
Attempt to parse 0+ of an item