diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 00818ae..17c4ff9 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -105,6 +105,18 @@ runFirstIO f str = do Just state <- newInternalIO str | _ => pure . Left $ BeforeParse "Empty input" runEff (rundownFirst f) [handleParserStateIO state] + +export +runFirst : (f : Parser a) -> String -> Eff fs (Either ParseError a) +runFirst f str = do + Just state <- pure $ newInternal str + | _ => pure . Left $ BeforeParse "Empty input" + (result, _) <- lift . runParserState state . rundownFirst $ f + pure result + +export +runFirst' : (f : Parser a) -> String -> Either ParseError a +runFirst' f str = extract $ runFirst f str {fs = []} ``` ## Utility functionality diff --git a/src/Parser/ParserState.md b/src/Parser/ParserState.md index 323b6d5..2a06858 100644 --- a/src/Parser/ParserState.md +++ b/src/Parser/ParserState.md @@ -281,6 +281,36 @@ newInternalIO str = do map Just $ newIORef internal ``` +### State context + +```idris +unPS : ParserInternal Id -> ParserState a -> (a, ParserInternal Id) +unPS pi Save = (pi, pi) +unPS pi (Load pj) = ((), pi) +unPS pi (ParseChar predicate err) = + if pi.end_of_input + then (EndOfInput, pi) + else let + char = assert_total $ strIndex pi.input (cast pi.position.index) + in if predicate char + then case refine0 (pi.position.index + 1) {p = IsIndex pi.length} of + Nothing => + (GotChar char, {end_of_input := True} pi) + Just (Element next _) => + (GotChar char, {position := MkIndex next} pi) + else (GotError $ err char, pi) +unPS pi ParseEoF = (pi.end_of_input, pi) + +export +runParserState : Has ParserState fs => + (s : ParserInternal Id) -> Eff fs t + -> Eff (fs - ParserState) (t, ParserInternal Id) +runParserState s = + handleRelayS s (\x, y => pure (y, x)) $ \s2,ps,f => + let (a, st) = unPS s2 ps + in f st a +``` + ## Footnotes [^1]: https://github.com/stefan-hoeck/idris2-barbies