module Agda.Syntax.Parser.LexActions
(
lexToken
, token
, withInterval, withInterval', withInterval_
, withLayout
, andThen, skip
, begin, end, beginWith, endWith
, begin_, end_
, lexError
, keyword, symbol, identifier, literal, literal', integer
, followedBy, eof, inState
) where
import Control.Monad.State (modify)
import Data.Bifunctor
import Data.Char
import Data.Foldable (foldl')
import Data.Maybe
import Agda.Syntax.Common (pattern Ranged)
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.List
import Agda.Utils.Impossible
returnEOF :: AlexInput -> Parser Token
returnEOF :: AlexInput -> Parser Token
returnEOF AlexInput{ SrcFile
lexSrcFile :: AlexInput -> SrcFile
lexSrcFile :: SrcFile
lexSrcFile, PositionWithoutFile
lexPos :: AlexInput -> PositionWithoutFile
lexPos :: PositionWithoutFile
lexPos } = do
String -> Parser ()
setPrevToken String
"<EOF>"
Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Parser Token) -> Token -> Parser Token
forall a b. (a -> b) -> a -> b
$ Interval -> Token
TokEOF (Interval -> Token) -> Interval -> Token
forall a b. (a -> b) -> a -> b
$ SrcFile -> PositionWithoutFile -> PositionWithoutFile -> Interval
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
posToInterval SrcFile
lexSrcFile PositionWithoutFile
lexPos PositionWithoutFile
lexPos
skipTo :: AlexInput -> Parser Token
skipTo :: AlexInput -> Parser Token
skipTo AlexInput
inp = do
AlexInput -> Parser ()
setLexInput AlexInput
inp
Parser Token
lexToken
lexToken :: Parser Token
lexToken :: Parser Token
lexToken =
do AlexInput
inp <- Parser AlexInput
getLexInput
[LexState]
lss <- Parser [LexState]
getLexState
ParseFlags
flags <- Parser ParseFlags
getParseFlags
case ([LexState], ParseFlags)
-> AlexInput -> LexState -> AlexReturn (LexAction Token)
alexScanUser ([LexState]
lss, ParseFlags
flags) AlexInput
inp (LexState -> [LexState] -> LexState
forall a. a -> [a] -> a
headWithDefault LexState
forall a. HasCallStack => a
__IMPOSSIBLE__ [LexState]
lss) of
AlexReturn (LexAction Token)
AlexEOF -> AlexInput -> Parser Token
returnEOF AlexInput
inp
AlexSkip AlexInput
inp' LexState
len -> AlexInput -> Parser Token
skipTo AlexInput
inp'
AlexToken AlexInput
inp' LexState
len LexAction Token
action -> Token -> Token
postToken (Token -> Token) -> Parser Token -> Parser Token
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LexAction Token
-> AlexInput -> AlexInput -> LexState -> Parser Token
forall r.
LexAction r -> AlexInput -> AlexInput -> LexState -> Parser r
runLexAction LexAction Token
action AlexInput
inp AlexInput
inp' LexState
len
AlexError AlexInput
i -> String -> Parser Token
forall a. String -> Parser a
parseError (String -> Parser Token) -> String -> Parser Token
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
"Lexical error"
, case String -> Maybe Char
forall a. [a] -> Maybe a
listToMaybe (String -> Maybe Char) -> String -> Maybe Char
forall a b. (a -> b) -> a -> b
$ AlexInput -> String
lexInput AlexInput
i of
Just Char
'\t' -> String
" (you may want to replace tabs with spaces)"
Just Char
c | Bool -> Bool
not (Char -> Bool
isPrint Char
c) -> String
" (unprintable character)"
Maybe Char
_ -> String
""
, String
":"
]
isSub :: Char -> Bool
isSub :: Char -> Bool
isSub Char
c = Char
'\x2080' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'\x2089'
readSubscript :: [Char] -> Integer
readSubscript :: String -> Integer
readSubscript = String -> Integer
forall a. Read a => String -> a
read (String -> Integer) -> (String -> String) -> String -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> LexState -> Char
forall a. Enum a => LexState -> a
toEnum (Char -> LexState
forall a. Enum a => a -> LexState
fromEnum Char
c LexState -> LexState -> LexState
forall a. Num a => a -> a -> a
- LexState
0x2080 LexState -> LexState -> LexState
forall a. Num a => a -> a -> a
+ Char -> LexState
forall a. Enum a => a -> LexState
fromEnum Char
'0'))
postToken :: Token -> Token
postToken :: Token -> Token
postToken (TokId (Interval
r, String
"\x03bb")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymLambda Interval
r
postToken (TokId (Interval
r, String
"\x2026")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymEllipsis Interval
r
postToken (TokId (Interval
r, String
"\x2192")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymArrow Interval
r
postToken (TokId (Interval
r, String
"\x2983")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymDoubleOpenBrace Interval
r
postToken (TokId (Interval
r, String
"\x2984")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymDoubleCloseBrace Interval
r
postToken (TokId (Interval
r, String
"\x2987")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymOpenIdiomBracket Interval
r
postToken (TokId (Interval
r, String
"\x2988")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymCloseIdiomBracket Interval
r
postToken (TokId (Interval
r, String
"\x2987\x2988")) = Symbol -> Interval -> Token
TokSymbol Symbol
SymEmptyIdiomBracket Interval
r
postToken (TokId (Interval
r, String
"\x2200")) = Keyword -> Interval -> Token
TokKeyword Keyword
KwForall Interval
r
postToken Token
t = Token
t
token :: (String -> Parser tok) -> LexAction tok
token :: forall tok. (String -> Parser tok) -> LexAction tok
token String -> Parser tok
action = (AlexInput -> AlexInput -> LexState -> Parser tok) -> LexAction tok
forall r.
(AlexInput -> AlexInput -> LexState -> Parser r) -> LexAction r
LexAction ((AlexInput -> AlexInput -> LexState -> Parser tok)
-> LexAction tok)
-> (AlexInput -> AlexInput -> LexState -> Parser tok)
-> LexAction tok
forall a b. (a -> b) -> a -> b
$ \ AlexInput
inp AlexInput
inp' LexState
len ->
do AlexInput -> Parser ()
setLexInput AlexInput
inp'
let t :: String
t = LexState -> String -> String
forall a. LexState -> [a] -> [a]
take LexState
len (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ AlexInput -> String
lexInput AlexInput
inp
String -> Parser ()
setPrevToken String
t
PositionWithoutFile -> Parser ()
setLastPos (PositionWithoutFile -> Parser ())
-> PositionWithoutFile -> Parser ()
forall a b. (a -> b) -> a -> b
$ AlexInput -> PositionWithoutFile
lexPos AlexInput
inp
String -> Parser tok
action String
t
withInterval :: ((Interval, String) -> tok) -> LexAction tok
withInterval :: forall tok. ((Interval, String) -> tok) -> LexAction tok
withInterval (Interval, String) -> tok
f = (String -> Parser tok) -> LexAction tok
forall tok. (String -> Parser tok) -> LexAction tok
token ((String -> Parser tok) -> LexAction tok)
-> (String -> Parser tok) -> LexAction tok
forall a b. (a -> b) -> a -> b
$ \String
s -> do
Interval
r <- Parser Interval
getParseInterval
tok -> Parser tok
forall (m :: * -> *) a. Monad m => a -> m a
return (tok -> Parser tok) -> tok -> Parser tok
forall a b. (a -> b) -> a -> b
$ (Interval, String) -> tok
f (Interval
r,String
s)
withInterval' :: (String -> a) -> ((Interval, a) -> tok) -> LexAction tok
withInterval' :: forall a tok.
(String -> a) -> ((Interval, a) -> tok) -> LexAction tok
withInterval' String -> a
f (Interval, a) -> tok
t = ((Interval, String) -> tok) -> LexAction tok
forall tok. ((Interval, String) -> tok) -> LexAction tok
withInterval ((Interval, a) -> tok
t ((Interval, a) -> tok)
-> ((Interval, String) -> (Interval, a))
-> (Interval, String)
-> tok
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> a) -> (Interval, String) -> (Interval, a)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second String -> a
f)
withInterval_ :: (Interval -> r) -> LexAction r
withInterval_ :: forall r. (Interval -> r) -> LexAction r
withInterval_ Interval -> r
f = ((Interval, String) -> r) -> LexAction r
forall tok. ((Interval, String) -> tok) -> LexAction tok
withInterval (Interval -> r
f (Interval -> r)
-> ((Interval, String) -> Interval) -> (Interval, String) -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Interval, String) -> Interval
forall a b. (a, b) -> a
fst)
withLayout :: Keyword -> LexAction r -> LexAction r
withLayout :: forall r. Keyword -> LexAction r -> LexAction r
withLayout Keyword
kw LexAction r
a = LexState -> Parser ()
pushLexState LexState
layout Parser () -> LexAction r -> LexAction r
forall r. Parser () -> LexAction r -> LexAction r
`andThen` Parser ()
setLayoutKw Parser () -> LexAction r -> LexAction r
forall r. Parser () -> LexAction r -> LexAction r
`andThen` LexAction r
a
where
setLayoutKw :: Parser ()
setLayoutKw = (ParseState -> ParseState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ParseState -> ParseState) -> Parser ())
-> (ParseState -> ParseState) -> Parser ()
forall a b. (a -> b) -> a -> b
$ \ ParseState
st -> ParseState
st { parseLayKw :: Keyword
parseLayKw = Keyword
kw }
infixr 1 `andThen`
andThen :: Parser () -> LexAction r -> LexAction r
andThen :: forall r. Parser () -> LexAction r -> LexAction r
andThen Parser ()
cmd LexAction r
a = (AlexInput -> AlexInput -> LexState -> Parser r) -> LexAction r
forall r.
(AlexInput -> AlexInput -> LexState -> Parser r) -> LexAction r
LexAction ((AlexInput -> AlexInput -> LexState -> Parser r) -> LexAction r)
-> (AlexInput -> AlexInput -> LexState -> Parser r) -> LexAction r
forall a b. (a -> b) -> a -> b
$ \ AlexInput
inp AlexInput
inp' LexState
n -> do
Parser ()
cmd
LexAction r -> AlexInput -> AlexInput -> LexState -> Parser r
forall r.
LexAction r -> AlexInput -> AlexInput -> LexState -> Parser r
runLexAction LexAction r
a AlexInput
inp AlexInput
inp' LexState
n
revisit :: LexAction Token
revisit :: LexAction Token
revisit = (AlexInput -> AlexInput -> LexState -> Parser Token)
-> LexAction Token
forall r.
(AlexInput -> AlexInput -> LexState -> Parser r) -> LexAction r
LexAction ((AlexInput -> AlexInput -> LexState -> Parser Token)
-> LexAction Token)
-> (AlexInput -> AlexInput -> LexState -> Parser Token)
-> LexAction Token
forall a b. (a -> b) -> a -> b
$ \ AlexInput
_ AlexInput
_ LexState
_ -> Parser Token
lexToken
skip :: LexAction Token
skip :: LexAction Token
skip = (AlexInput -> AlexInput -> LexState -> Parser Token)
-> LexAction Token
forall r.
(AlexInput -> AlexInput -> LexState -> Parser r) -> LexAction r
LexAction ((AlexInput -> AlexInput -> LexState -> Parser Token)
-> LexAction Token)
-> (AlexInput -> AlexInput -> LexState -> Parser Token)
-> LexAction Token
forall a b. (a -> b) -> a -> b
$ \ AlexInput
_ AlexInput
inp' LexState
_ -> AlexInput -> Parser Token
skipTo AlexInput
inp'
begin :: LexState -> LexAction Token
begin :: LexState -> LexAction Token
begin LexState
code = LexState -> LexAction Token -> LexAction Token
forall a. LexState -> LexAction a -> LexAction a
beginWith LexState
code LexAction Token
revisit
end :: LexAction Token
end :: LexAction Token
end = LexAction Token -> LexAction Token
forall a. LexAction a -> LexAction a
endWith LexAction Token
revisit
begin_ :: LexState -> LexAction Token
begin_ :: LexState -> LexAction Token
begin_ LexState
code = LexState -> LexAction Token -> LexAction Token
forall a. LexState -> LexAction a -> LexAction a
beginWith LexState
code LexAction Token
skip
end_ :: LexAction Token
end_ :: LexAction Token
end_ = LexAction Token -> LexAction Token
forall a. LexAction a -> LexAction a
endWith LexAction Token
skip
beginWith :: LexState -> LexAction a -> LexAction a
beginWith :: forall a. LexState -> LexAction a -> LexAction a
beginWith LexState
code LexAction a
a = LexState -> Parser ()
pushLexState LexState
code Parser () -> LexAction a -> LexAction a
forall r. Parser () -> LexAction r -> LexAction r
`andThen` LexAction a
a
endWith :: LexAction a -> LexAction a
endWith :: forall a. LexAction a -> LexAction a
endWith LexAction a
a = Parser ()
popLexState Parser () -> LexAction a -> LexAction a
forall r. Parser () -> LexAction r -> LexAction r
`andThen` LexAction a
a
keyword :: Keyword -> LexAction Token
keyword :: Keyword -> LexAction Token
keyword Keyword
k =
case Keyword
k of
Keyword
_ | Keyword
k Keyword -> [Keyword] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Keyword]
layoutKeywords ->
Keyword -> LexAction Token -> LexAction Token
forall r. Keyword -> LexAction r -> LexAction r
withLayout Keyword
k LexAction Token
cont
Keyword
_ -> LexAction Token
cont
where
cont :: LexAction Token
cont = (Interval -> Token) -> LexAction Token
forall r. (Interval -> r) -> LexAction r
withInterval_ (Keyword -> Interval -> Token
TokKeyword Keyword
k)
symbol :: Symbol -> LexAction Token
symbol :: Symbol -> LexAction Token
symbol Symbol
s = (Interval -> Token) -> LexAction Token
forall r. (Interval -> r) -> LexAction r
withInterval_ (Symbol -> Interval -> Token
TokSymbol Symbol
s)
number :: String -> Integer
number :: String -> Integer
number String
str = case String
str of
Char
'0' : Char
'x' : String
num -> Integer -> String -> Integer
parseNumber Integer
16 String
num
Char
'0' : Char
'b' : String
num -> Integer -> String -> Integer
parseNumber Integer
2 String
num
String
num -> Integer -> String -> Integer
parseNumber Integer
10 String
num
where
parseNumber :: Integer -> String -> Integer
parseNumber :: Integer -> String -> Integer
parseNumber Integer
radix = (Integer -> Char -> Integer) -> Integer -> String -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Integer -> Integer -> Char -> Integer
addDigit Integer
radix) Integer
0
addDigit :: Integer -> Integer -> Char -> Integer
addDigit :: Integer -> Integer -> Char -> Integer
addDigit Integer
radix Integer
n Char
'_' = Integer
n
addDigit Integer
radix Integer
n Char
c = Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
radix Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ LexState -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> LexState
digitToInt Char
c)
integer :: String -> Integer
integer :: String -> Integer
integer = \case
Char
'-' : String
str -> - (String -> Integer
number String
str)
String
str -> String -> Integer
number String
str
literal' :: (String -> a) -> (a -> Literal) -> LexAction Token
literal' :: forall a. (String -> a) -> (a -> Literal) -> LexAction Token
literal' String -> a
read a -> Literal
lit = (String -> a) -> ((Interval, a) -> Token) -> LexAction Token
forall a tok.
(String -> a) -> ((Interval, a) -> tok) -> LexAction tok
withInterval' String -> a
read (((Interval, a) -> Token) -> LexAction Token)
-> ((Interval, a) -> Token) -> LexAction Token
forall a b. (a -> b) -> a -> b
$ \ (Interval
r, a
a) ->
RLiteral -> Token
TokLiteral (RLiteral -> Token) -> RLiteral -> Token
forall a b. (a -> b) -> a -> b
$ Range -> Literal -> RLiteral
forall a. Range -> a -> Ranged a
Ranged (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
r) (Literal -> RLiteral) -> Literal -> RLiteral
forall a b. (a -> b) -> a -> b
$ a -> Literal
lit a
a
literal :: Read a => (a -> Literal) -> LexAction Token
literal :: forall a. Read a => (a -> Literal) -> LexAction Token
literal = (String -> a) -> (a -> Literal) -> LexAction Token
forall a. (String -> a) -> (a -> Literal) -> LexAction Token
literal' String -> a
forall a. Read a => String -> a
read
identifier :: LexAction Token
identifier :: LexAction Token
identifier = (Either (Interval, String) [(Interval, String)] -> Token)
-> LexAction Token
forall a.
(Either (Interval, String) [(Interval, String)] -> a)
-> LexAction a
qualified (((Interval, String) -> Token)
-> ([(Interval, String)] -> Token)
-> Either (Interval, String) [(Interval, String)]
-> Token
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Interval, String) -> Token
TokId [(Interval, String)] -> Token
TokQId)
qualified :: (Either (Interval, String) [(Interval, String)] -> a) -> LexAction a
qualified :: forall a.
(Either (Interval, String) [(Interval, String)] -> a)
-> LexAction a
qualified Either (Interval, String) [(Interval, String)] -> a
tok =
(String -> Parser a) -> LexAction a
forall tok. (String -> Parser tok) -> LexAction tok
token ((String -> Parser a) -> LexAction a)
-> (String -> Parser a) -> LexAction a
forall a b. (a -> b) -> a -> b
$ \String
s ->
do Interval
i <- Parser Interval
getParseInterval
case Interval -> [String] -> [(Interval, String)]
mkName Interval
i ([String] -> [(Interval, String)])
-> [String] -> [(Interval, String)]
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> [String]
forall a. (a -> Bool) -> [a] -> [[a]]
wordsBy (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'.') String
s of
[] -> String -> Parser a
forall a. String -> Parser a
lexError String
"lex error on .."
[(Interval, String)
x] -> a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Parser a) -> a -> Parser a
forall a b. (a -> b) -> a -> b
$ Either (Interval, String) [(Interval, String)] -> a
tok (Either (Interval, String) [(Interval, String)] -> a)
-> Either (Interval, String) [(Interval, String)] -> a
forall a b. (a -> b) -> a -> b
$ (Interval, String)
-> Either (Interval, String) [(Interval, String)]
forall a b. a -> Either a b
Left (Interval, String)
x
[(Interval, String)]
xs -> a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Parser a) -> a -> Parser a
forall a b. (a -> b) -> a -> b
$ Either (Interval, String) [(Interval, String)] -> a
tok (Either (Interval, String) [(Interval, String)] -> a)
-> Either (Interval, String) [(Interval, String)] -> a
forall a b. (a -> b) -> a -> b
$ [(Interval, String)]
-> Either (Interval, String) [(Interval, String)]
forall a b. b -> Either a b
Right [(Interval, String)]
xs
where
mkName :: Interval -> [String] -> [(Interval, String)]
mkName :: Interval -> [String] -> [(Interval, String)]
mkName Interval
_ [] = []
mkName Interval
i [String
x] = [(Interval
i, String
x)]
mkName Interval
i (String
x:[String]
xs) = (Interval
i0, String
x) (Interval, String) -> [(Interval, String)] -> [(Interval, String)]
forall a. a -> [a] -> [a]
: Interval -> [String] -> [(Interval, String)]
mkName Interval
i1 [String]
xs
where
p0 :: Position' SrcFile
p0 = Interval -> Position' SrcFile
forall a. Interval' a -> Position' a
iStart Interval
i
p1 :: Position' SrcFile
p1 = Interval -> Position' SrcFile
forall a. Interval' a -> Position' a
iEnd Interval
i
p' :: Position' SrcFile
p' = Position' SrcFile -> Char -> Position' SrcFile
forall a. Position' a -> Char -> Position' a
movePos (Position' SrcFile -> String -> Position' SrcFile
forall a. Position' a -> String -> Position' a
movePosByString Position' SrcFile
p0 String
x) Char
'.'
i0 :: Interval
i0 = Position' SrcFile -> Position' SrcFile -> Interval
forall a. Position' a -> Position' a -> Interval' a
Interval Position' SrcFile
p0 Position' SrcFile
p'
i1 :: Interval
i1 = Position' SrcFile -> Position' SrcFile -> Interval
forall a. Position' a -> Position' a -> Interval' a
Interval Position' SrcFile
p' Position' SrcFile
p1
followedBy :: Char -> LexPredicate
followedBy :: Char -> LexPredicate
followedBy Char
c' ([LexState], ParseFlags)
_ AlexInput
_ LexState
_ AlexInput
inp =
case AlexInput -> String
lexInput AlexInput
inp of
[] -> Bool
False
Char
c:String
_ -> Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c'
eof :: LexPredicate
eof :: LexPredicate
eof ([LexState], ParseFlags)
_ AlexInput
_ LexState
_ AlexInput
inp = String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ AlexInput -> String
lexInput AlexInput
inp
inState :: LexState -> LexPredicate
inState :: LexState -> LexPredicate
inState LexState
s ([LexState]
ls, ParseFlags
_) AlexInput
_ LexState
_ AlexInput
_ = LexState
s LexState -> [LexState] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [LexState]
ls