266 lines
6.8 KiB
Markdown
266 lines
6.8 KiB
Markdown
# 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
|
|
MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
|
|
BeforeParse : (message : String) -> ParseError
|
|
```
|
|
|
|
<!-- idris
|
|
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}"
|
|
-->
|
|
|
|
## 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
|
|
```
|
|
|
|
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]
|
|
|
|
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)
|
|
|
|
||| 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"
|
|
```
|
|
|
|
Attempt to parse one of a list of chars
|
|
|
|
```idris
|
|
export
|
|
parseTheseChars : List Char -> Parser Char
|
|
parseTheseChars cs = do
|
|
result <- parseChar (\x => any (== x) cs) id
|
|
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
|
|
exactString : String -> Parser String
|
|
exactString str with (asList str)
|
|
exactString "" | [] = pure ""
|
|
exactString input@(strCons c str) | (c :: x) = do
|
|
GotChar next <- parseChar (== c) id
|
|
| GotError err => throwParseError "Got \{show err} expected \{show c}"
|
|
| EndOfInput => throwParseError "End of input"
|
|
rest <- exactString str | x
|
|
pure 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
|
|
```
|