core: runFirstIO

This commit is contained in:
Nathan McCarty 2025-01-25 00:08:01 -05:00
parent 38c69c0ae3
commit 1658e15487

View file

@ -19,10 +19,9 @@ Combine the parser state at time of error with an error message.
```idris
public export
record ParseError where
constructor MkParseError
state : ParserInternal Id
message : String
data ParseError : Type where
MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
BeforeParse : (message : String) -> ParseError
```
<!-- idris
@ -33,6 +32,8 @@ Show ParseError where
(line, col) = (show line, show col)
position = show state.position.index
in "Error at line \{line}, column \{col} (\{position}): \{message}"
show (BeforeParse message) =
"Error before parsing: \{message}"
-->
## Type Alias
@ -95,6 +96,17 @@ rundownFirst f =
runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f
```
Provide wrappers for `rundownFirst` for evaluating it in various contexts.
```idris
export
runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a)
runFirstIO f str = do
Just state <- newInternalIO str
| _ => pure . Left $ BeforeParse "Empty input"
runEff (rundownFirst f) [handleParserStateIO state]
```
## Utility functionality
### Parser combinators