Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Syntax.Parser.LookAhead

Contents

- The LookAhead monad
- Operations

Description

When lexing by hands (for instance string literals) we need to do some looking ahead. The `LookAhead` monad keeps track of the position we are currently looking at, and provides facilities to synchronise the look-ahead position with the actual position of the `Parser` monad (see `sync` and `rollback`).

Synopsis

- data LookAhead a
- runLookAhead :: (forall b. String -> LookAhead b) -> LookAhead a -> Parser a
- getInput :: LookAhead AlexInput
- setInput :: AlexInput -> LookAhead ()
- liftP :: Parser a -> LookAhead a
- nextChar :: LookAhead Char
- eatNextChar :: LookAhead Char
- sync :: LookAhead ()
- rollback :: LookAhead ()
- match :: [(String, LookAhead a)] -> LookAhead a -> LookAhead a
- match' :: Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a

# The LookAhead monad

data LookAhead a

The LookAhead monad is basically a state monad keeping with an extra `AlexInput`, wrapped around the `Parser` monad.

Instances

Monad LookAhead |

runLookAhead :: (forall b. String -> LookAhead b) -> LookAhead a -> Parser a

Run a `LookAhead` computation. The first argument is the error function.

# Operations

getInput :: LookAhead AlexInput

Get the current look-ahead position.

setInput :: AlexInput -> LookAhead ()

Set the look-ahead position.

liftP :: Parser a -> LookAhead a

Lift a computation in the `Parser` monad to the `LookAhead` monad.

nextChar :: LookAhead Char

Look at the next character. Fails if there are no more characters.

eatNextChar :: LookAhead Char

Consume the next character. Does `nextChar` followed by `sync`.

sync :: LookAhead ()

Consume all the characters up to the current look-ahead position.

rollback :: LookAhead ()

Undo look-ahead. Restores the input from the `ParseState`.

match :: [(String, LookAhead a)] -> LookAhead a -> LookAhead a

Do a case on the current input string. If any of the given strings match we move past it and execute the corresponding action. If no string matches, we execute a default action, advancing the input one character. This function only affects the look-ahead position.

match' :: Char -> [(String, LookAhead a)] -> LookAhead a -> LookAhead a

Same as `match` but takes the initial character from the first argument instead of reading it from the input. Consequently, in the default case the input is not advanced.