# The interface of a `Parser` ```idris module Parser.Interface import public Data.List1 import public Parser.ParserState import public Control.Eff export infixr 4 >| export infixr 5 >& ``` ## Parser Errors 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 ``` ## Type Alias ```idris public export Parser : Type -> Type Parser a = Eff [ParserState, Except ParseError, Choose] a ``` ## Error Generation Provide a few effectful actions to generate an error from an error message, and either return it or throw it. ```idris export parseError : Has ParserState fs => (message : String) -> Eff fs ParseError parseError message = do state <- save pure $ MkParseError state message export throwParseError : Has ParserState fs => Has (Except ParseError) fs => (message : String) -> Eff fs a throwParseError message = do err <- parseError message throw err export guardMaybe : Has ParserState fs => Has (Except ParseError) fs => (message : String) -> Eff fs (Maybe a) -> Eff fs a guardMaybe message x = do Just x <- x | _ => throwParseError message pure x export replaceError : (message : String) -> Parser (a -> Parser b) replaceError message = do state <- save pure (\_ => throw $ MkParseError state message) ``` ## Running a parser We will use the phrasing "rundown" to refer to running all the effects in the parser effect stack except `ParserState`, which is left in the effect stack to facilitate handling in the context of another monad or effect stack, since it benefits from mutability. Rundown a parser, accepting the first returning parse, which may be failing or succeding, and automatically generating a "no valid parses" message in the event no paths in the `Choice` effect produce a returning parse. ```idris export rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a) rundownFirst f = runExcept . guardMaybe "No returning parses" . runChoose {f = Maybe} $ f ``` ## Utility functionality ### Parser combinators Try to run a computation in the context of the `Parser` effect stack, if it fails (via `Except`), reset the state and resort to the supplied callback Also supply a version specialized to ignore the error value, returning `Just a` if the parse succeeds, and `Nothing` if it fails. ```idris export try : (f : Parser a) -> (err : ParseError -> Parser a) -> Parser a try f err = do starting_state <- save result <- lift . runExcept $ f case result of Left error => do load starting_state err error Right result => pure result export tryMaybe : (f : Parser a) -> Parser (Maybe a) 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 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 where altE : Parser a -> Parser a -> Parser a altE f rest = (tryEmpty f) `alt` rest ``` Attempt to parse 0+ of an item ```idris export many : (f : Parser a) -> Parser (List a) many f = do Just next <- tryMaybe f | _ => pure [] map (next ::) $ many f ``` Attempt to parse 1+ of an item, invoking the supplied error action on failure ```idris export atLeastOne : (err : ParseError -> Parser (List1 a)) -> (f : Parser a) -> Parser (List1 a) atLeastOne err f = do Right next <- tryEither f | Left e => err e map (next :::) $ many f ``` Lift a parser producing a `List` or `List1` of `Char` into a parser producing a `String` ```idris export parseString : Parser (List Char) -> Parser String parseString x = do xs <- x pure $ pack xs export parseString' : Parser (List1 Char) -> Parser String parseString' x = parseString $ map forget x ``` Attempt to parse a specified character ```idris export parseExactChar : Char -> Parser Char parseExactChar c = do result <- parseChar (== c) id case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected \{show c}" EndOfInput => throwParseError "End of input" ``` ### Composition of boolean functions ```idris ||| Return true if both of the predicates evaluate to true public export (>&) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool) (>&) a b x = a x && b x ``` ```idris ||| Return true if either of the predicates evaulates to true public export (>|) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool) (>|) a b x = a x || b x ```