module Agda.Syntax.Parser.Alex
(
AlexInput(..)
, alexInputPrevChar
, alexGetChar
, LexAction, LexPredicate
, (.&&.), (.||.), not'
, PreviousInput, CurrentInput, TokenLength
, getLexInput, setLexInput
)
where
import Control.Monad.State
import Agda.Syntax.Position
import Agda.Syntax.Parser.Monad
import Agda.Utils.Monad
data AlexInput = AlexInput
{ lexPos :: !Position
, lexInput :: String
, lexPrevChar :: !Char
}
alexInputPrevChar :: AlexInput -> Char
alexInputPrevChar = lexPrevChar
alexGetChar :: AlexInput -> Maybe (Char, AlexInput)
alexGetChar (AlexInput { lexInput = [] }) = Nothing
alexGetChar (AlexInput { lexInput = c:s, lexPos = p }) =
Just (c, AlexInput
{ lexInput = s
, lexPos = movePos p c
, lexPrevChar = c
}
)
getLexInput :: Parser AlexInput
getLexInput = getInp <$> get
where
getInp s = AlexInput
{ lexPos = parsePos s
, lexInput = parseInp s
, lexPrevChar = parsePrevChar s
}
setLexInput :: AlexInput -> Parser ()
setLexInput inp = modify upd
where
upd s = s { parsePos = lexPos inp
, parseInp = lexInput inp
, parsePrevChar = lexPrevChar inp
}
type PreviousInput = AlexInput
type CurrentInput = AlexInput
type TokenLength = Int
type LexAction r = PreviousInput -> CurrentInput -> TokenLength -> Parser r
type LexPredicate = ([LexState], ParseFlags) -> PreviousInput -> TokenLength -> CurrentInput -> Bool
(.&&.) :: LexPredicate -> LexPredicate -> LexPredicate
p1 .&&. p2 = \x y z u -> p1 x y z u && p2 x y z u
(.||.) :: LexPredicate -> LexPredicate -> LexPredicate
p1 .||. p2 = \x y z u -> p1 x y z u || p2 x y z u
not' :: LexPredicate -> LexPredicate
not' p = \x y z u -> not (p x y z u)