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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Parser.LookAhead

Contents

- The LookAhead monad
- Operations

Description

When lexing by hand (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
- lookAheadError :: String -> LookAhead 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 Source #

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

#### Instances

Instances details

Applicative LookAhead Source # |
Instance details Defined in Agda.Syntax.Parser.LookAhead Methods pure :: a -> LookAhead a Source # (<*>) :: LookAhead (a -> b) -> LookAhead a -> LookAhead b Source # liftA2 :: (a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c Source # (*>) :: LookAhead a -> LookAhead b -> LookAhead b Source # (<*) :: LookAhead a -> LookAhead b -> LookAhead a Source #
Functor LookAhead Source # |
Instance details Defined in Agda.Syntax.Parser.LookAhead Methods fmap :: (a -> b) -> LookAhead a -> LookAhead b Source # (<$) :: a -> LookAhead b -> LookAhead a Source #
Monad LookAhead Source # |
Instance details Defined in Agda.Syntax.Parser.LookAhead Methods (>>=) :: LookAhead a -> (a -> LookAhead b) -> LookAhead b Source # (>>) :: LookAhead a -> LookAhead b -> LookAhead b Source # return :: a -> LookAhead a Source #

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

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

# Operations

lookAheadError :: String -> LookAhead a Source #

Throw an error message according to the supplied method.

getInput :: LookAhead AlexInput Source #

Get the current look-ahead position.

setInput :: AlexInput -> LookAhead () Source #

Set the look-ahead position.

liftP :: Parser a -> LookAhead a Source #

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

nextChar :: LookAhead Char Source #

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

eatNextChar :: LookAhead Char Source #

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

sync :: LookAhead () Source #

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

rollback :: LookAhead () Source #

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

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

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 Source #

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.