module Agda.Syntax.Parser.Alex
(
AlexInput(..)
, lensLexInput
, alexInputPrevChar
, alexGetChar, alexGetByte
, LexAction, LexPredicate
, (.&&.), (.||.), not'
, PreviousInput, CurrentInput, TokenLength
, getLexInput, setLexInput
)
where
import Control.Monad.State
import Data.Char
import Data.Word
import Agda.Syntax.Position
import Agda.Syntax.Parser.Monad
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Tuple
data AlexInput = AlexInput
{ lexSrcFile :: !SrcFile
, lexPos :: !PositionWithoutFile
, lexInput :: String
, lexPrevChar :: !Char
}
lensLexInput :: Lens' String AlexInput
lensLexInput f r = f (lexInput r) <&> \ s -> r { lexInput = s }
alexInputPrevChar :: AlexInput -> Char
alexInputPrevChar = lexPrevChar
alexGetChar :: AlexInput -> Maybe (Char, AlexInput)
alexGetChar (AlexInput { lexInput = [] }) = Nothing
alexGetChar inp@(AlexInput { lexInput = c:s, lexPos = p }) =
Just (c, AlexInput
{ lexSrcFile = lexSrcFile inp
, lexInput = s
, lexPos = movePos p c
, lexPrevChar = c
}
)
alexGetByte :: AlexInput -> Maybe (Word8, AlexInput)
alexGetByte ai =
mapFst (fromIntegral . fromEnum . toASCII) <$> alexGetChar ai
where
toASCII c
| isSpace c && c /= '\t' && c /= '\n' = ' '
| isAscii c = c
| isPrint c = if isAlpha c then 'z'
else '+'
| otherwise = '\1'
getLexInput :: Parser AlexInput
getLexInput = getInp <$> get
where
getInp s = AlexInput
{ lexSrcFile = parseSrcFile s
, lexPos = parsePos s
, lexInput = parseInp s
, lexPrevChar = parsePrevChar s
}
setLexInput :: AlexInput -> Parser ()
setLexInput inp = modify upd
where
upd s = s { parseSrcFile = lexSrcFile inp
, 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)