{-# LANGUAGE CPP #-}
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
#include "undefined.h"
import Agda.Utils.Impossible
returnEOF :: AlexInput -> Parser Token
returnEOF AlexInput{ lexSrcFile, lexPos } = do
setPrevToken "<EOF>"
return $ TokEOF $ posToInterval lexSrcFile lexPos lexPos
skipTo :: AlexInput -> Parser Token
skipTo inp = do
setLexInput inp
lexToken
lexToken :: Parser Token
lexToken =
do inp <- getLexInput
lss <- getLexState
flags <- getParseFlags
case alexScanUser (lss, flags) inp (headWithDefault __IMPOSSIBLE__ lss) of
AlexEOF -> returnEOF inp
AlexSkip inp' len -> skipTo inp'
AlexToken inp' len action -> fmap postToken $ action inp inp' 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)"
_ -> ""
, ":"
]
isSub :: Char -> Bool
isSub c = '\x2080' <= c && c <= '\x2089'
readSubscript :: [Char] -> Integer
readSubscript = read . map (\c -> toEnum (fromEnum c - 0x2080 + fromEnum '0'))
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
postToken (TokId (r, s))
| prop == "Prop" && all isSub n = TokPropN (r, readSubscript n)
where
(prop, n) = splitAt 4 s
postToken t = t
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