Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Parser.LookAhead

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

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

(<*>) :: LookAhead (a -> b) -> LookAhead a -> LookAhead b #

liftA2 :: (a -> b -> c) -> LookAhead a -> LookAhead b -> LookAhead c

(*>) :: LookAhead a -> LookAhead b -> LookAhead b

(<*) :: LookAhead a -> LookAhead b -> LookAhead a

Functor LookAhead Source # 
Instance details

Defined in Agda.Syntax.Parser.LookAhead

Methods

fmap :: (a -> b) -> LookAhead a -> LookAhead b

(<$) :: a -> LookAhead b -> LookAhead a #

Monad LookAhead Source # 
Instance details

Defined in Agda.Syntax.Parser.LookAhead

Methods

(>>=) :: LookAhead a -> (a -> LookAhead b) -> LookAhead b

(>>) :: LookAhead a -> LookAhead b -> LookAhead b

return :: a -> LookAhead a

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.