# 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 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 hide export Show ParseError where show (MkParseError state message) = let (line, col) = positionPair state (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}" 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 ```idris public export Parser : Type -> Type Parser a = Eff [ParserState, Except ParseError] 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 f ``` Provide wrappers for `rundownFirst` for evaluating it in various contexts. ```idris export runFirstIO : HasIO io => MonadRec io => (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] export runFirstIODebug : (f : Parser a) -> String -> IO (Either ParseError a) runFirstIODebug f str = do Just state <- newInternalIO str | _ => pure . Left $ BeforeParse "Empty input" runEff (rundownFirst f) [handleParserStateIODebug 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 ### 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) ``` Attempt to parse one of the given input parsers, in the provided order, invoking the provided error action on failure. The state will not be modified when an input parser fails ```idris export oneOfE : (err : String) -> List (Parser a) -> Parser a oneOfE err xs = do start <- save oneOfE' err start [] xs where 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 ```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 -- TODO: Rename these export liftString : Parser (List Char) -> Parser String liftString x = do xs <- x pure $ pack xs export liftString' : Parser (List1 Char) -> Parser String liftString' x = liftString $ map forget x ``` Attempt to parse a specified character ```idris export charExact : Char -> Parser Char charExact c = do result <- charExact' c case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected \{show c}" EndOfInput => throwParseError "End of input" ``` Attempt to parse one of a list of chars ```idris export theseChars : List Char -> Parser Char theseChars cs = do pnote "Parsing one of: \{show cs}" result <- charPredicate (\x => any (== x) cs) case result of GotChar char => pure char GotError err => throwParseError "Got \{show err} Expected one of \{show cs}" EndOfInput => throwParseError "End of input" ``` Attempt to parse an exact string ```idris export exactString : String -> Parser String exactString str with (asList str) exactString "" | [] = do pnote "Parsing the empty string" pure "" exactString input@(strCons c str) | (c :: x) = do pnote "Parsing exact string \{show input}" GotChar next <- charPredicate (== c) | GotError err => throwParseError "Got \{show err} expected \{show c}" | EndOfInput => throwParseError "End of input" rest <- exactString str | x pure input ``` Wrap a parser in delimiter characters, discarding the value of the delimiters ```idris export delimited : (before, after : Char) -> Parser a -> Parser a delimited before after x = do pnote "Parsing delimited by \{show before} \{show after}" starting_state <- save _ <- charExact before Right val <- tryEither x | Left err => do load starting_state throw err Just _ <- tryMaybe $ charExact after | _ => do load starting_state throw $ MkParseError starting_state "Unmatched delimiter \{show before}" pure val ``` Consume any number of characters of the provided character class and discard the result. Also a version for doing so on both sides of a provided parser ```idris export nom : Parser Char -> Parser () nom x = do pnote "Nomming" _ <- many x pure () export surround : (around : Parser Char) -> (item : Parser a) -> Parser a surround around item = do pnote "Surrounding" nom around val <- item nom around pure val ``` ### 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 ```