| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

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

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

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.
Produced by Haddock version 2.4.2