diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index fe13c13..00818ae 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -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 ``` ## 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