module Agda.Syntax.Parser.LexActions
(
lexToken
, token
, withInterval, withInterval', withInterval_
, withLayout
, begin, end, beginWith, endWith
, begin_, end_
, lexError
, keyword, symbol, identifier, literal
, followedBy, eof, inState
) where
import Data.Char
import Agda.Syntax.Parser.Lexer
import Agda.Syntax.Parser.Alex
import Agda.Syntax.Parser.Monad
import Agda.Syntax.Parser.Tokens
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Tuple
returnEOF :: AlexInput -> Parser Token
returnEOF inp =
do setLastPos $ lexPos inp
setPrevToken "<EOF>"
return TokEOF
skipTo :: AlexInput -> Parser Token
skipTo inp = setLexInput inp >> lexToken
lexToken :: Parser Token
lexToken =
do inp <- getLexInput
lss@(ls:_) <- getLexState
flags <- getParseFlags
case alexScanUser (lss, flags) (foolAlex inp) ls of
AlexEOF -> returnEOF inp
AlexSkip inp' len -> skipTo (newInput inp inp' len)
AlexToken inp' len action -> fmap postToken $ action inp (newInput inp inp' len) len
AlexError i -> parseError $ concat
[ "Lexical error"
, case headMaybe $ lexInput i of
Just '\t' -> " (you may want to replace tabs with spaces)"
Just c | not (isPrint c) -> " (unprintable character)"
_ -> ""
, ":"
]
postToken :: Token -> Token
postToken (TokId (r, "\x03bb")) = TokSymbol SymLambda r
postToken (TokId (r, "\x2026")) = TokSymbol SymEllipsis r
postToken (TokId (r, "\x2192")) = TokSymbol SymArrow r
postToken (TokId (r, "\x2983")) = TokSymbol SymDoubleOpenBrace r
postToken (TokId (r, "\x2984")) = TokSymbol SymDoubleCloseBrace r
postToken (TokId (r, "\x2987")) = TokSymbol SymOpenIdiomBracket r
postToken (TokId (r, "\x2988")) = TokSymbol SymCloseIdiomBracket r
postToken (TokId (r, "\x2200")) = TokKeyword KwForall r
postToken (TokId (r, s))
| set == "Set" && all isSub n = TokSetN (r, readSubscript n)
where
(set, n) = splitAt 3 s
isSub c = '\x2080' <= c && c <= '\x2089'
readSubscript = read . map (\c -> toEnum (fromEnum c - 0x2080 + fromEnum '0'))
postToken t = t
newInput :: PreviousInput -> CurrentInput -> TokenLength -> CurrentInput
newInput inp inp' len =
case drop (len - 1) (lexInput inp) of
c:s' -> inp' { lexInput = s'
, lexPrevChar = c
}
[] -> inp' { lexInput = [] }
foolAlex :: AlexInput -> AlexInput
foolAlex = over lensLexInput $ map $ \ c ->
case c of
_ | isSpace c && not (c `elem` "\t\n") -> ' '
_ | isAscii c -> c
_ | isPrint c -> if isAlpha c then 'z' else '+'
_ | otherwise -> '\1'
token :: (String -> Parser tok) -> LexAction tok
token action inp inp' len =
do setLexInput inp'
setPrevToken t
setLastPos $ lexPos inp
action t
where
t = take len $ lexInput inp
withInterval :: ((Interval, String) -> tok) -> LexAction tok
withInterval f = token $ \s -> do
r <- getParseInterval
return $ f (r,s)
withInterval' :: (String -> a) -> ((Interval, a) -> tok) -> LexAction tok
withInterval' f t = withInterval (t . (id -*- f))
withInterval_ :: (Interval -> r) -> LexAction r
withInterval_ f = withInterval (f . fst)
withLayout :: LexAction r -> LexAction r
withLayout a i1 i2 n =
do pushLexState layout
a i1 i2 n
begin :: LexState -> LexAction Token
begin code _ _ _ =
do pushLexState code
lexToken
begin_ :: LexState -> LexAction Token
begin_ code _ inp' _ =
do pushLexState code
skipTo inp'
end_ :: LexAction Token
end_ _ inp' _ =
do popLexState
skipTo inp'
beginWith :: LexState -> LexAction a -> LexAction a
beginWith code a inp inp' n =
do pushLexState code
a inp inp' n
endWith :: LexAction a -> LexAction a
endWith a inp inp' n =
do popLexState
a inp inp' n
end :: LexAction Token
end _ _ _ =
do popLexState
lexToken
keyword :: Keyword -> LexAction Token
keyword k = layout $ withInterval_ (TokKeyword k)
where
layout | elem k layoutKeywords = withLayout
| otherwise = id
symbol :: Symbol -> LexAction Token
symbol s = withInterval_ (TokSymbol s)
literal :: Read a => (Range -> a -> Literal) -> LexAction Token
literal lit =
withInterval' read (TokLiteral . uncurry lit . mapFst getRange)
identifier :: LexAction Token
identifier = qualified (either TokId TokQId)
qualified :: (Either (Interval, String) [(Interval, String)] -> a) -> LexAction a
qualified tok =
token $ \s ->
do i <- getParseInterval
case mkName i $ wordsBy (=='.') s of
[] -> lexError "lex error on .."
[x] -> return $ tok $ Left x
xs -> return $ tok $ Right xs
where
mkName :: Interval -> [String] -> [(Interval, String)]
mkName _ [] = []
mkName i [x] = [(i, x)]
mkName i (x:xs) = (i0, x) : mkName i1 xs
where
p0 = iStart i
p1 = iEnd i
p' = movePos (movePosByString p0 x) '.'
i0 = Interval p0 p'
i1 = Interval p' p1
followedBy :: Char -> LexPredicate
followedBy c' _ _ _ inp =
case lexInput inp of
[] -> False
c:_ -> c == c'
eof :: LexPredicate
eof _ _ _ inp = null $ lexInput inp
inState :: LexState -> LexPredicate
inState s (ls, _) _ _ _ = s `elem` ls