module Agda.Syntax.Parser.Tokens
( Token(..)
, Keyword(..)
, layoutKeywords
, Symbol(..)
) where
import Agda.Syntax.Literal (Literal)
import Agda.Syntax.Position
data Keyword
= KwLet | KwIn | KwWhere | KwData | KwCoData
| KwPostulate | KwMutual | KwAbstract | KwPrivate | KwInstance
| KwOpen | KwImport | KwModule | KwPrimitive
| KwInfix | KwInfixL | KwInfixR | KwWith | KwRewrite
| KwSet | KwProp | KwForall | KwRecord | KwConstructor | KwField
| KwInductive | KwCoInductive
| KwHiding | KwUsing | KwRenaming | KwTo | KwPublic
| KwOPTIONS | KwBUILTIN | KwLINE
| KwCOMPILED_DATA | KwCOMPILED_TYPE | KwCOMPILED | KwCOMPILED_EXPORT
| KwCOMPILED_EPIC | KwCOMPILED_JS
| KwIMPORT | KwIMPOSSIBLE | KwETA | KwSTATIC
| KwNO_TERMINATION_CHECK | KwTERMINATING | KwNON_TERMINATING
| KwMEASURE
| KwREWRITE
| KwQuoteGoal | KwQuoteContext | KwQuote | KwQuoteTerm | KwUnquote | KwUnquoteDecl | KwSyntax
| KwPatternSyn | KwTactic
deriving (Eq, Show)
layoutKeywords :: [Keyword]
layoutKeywords =
[ KwLet, KwWhere, KwPostulate, KwMutual, KwAbstract, KwPrivate, KwInstance, KwPrimitive, KwField ]
data Symbol
= SymDot | SymSemi | SymVirtualSemi | SymBar
| SymColon | SymArrow | SymEqual | SymLambda
| SymUnderscore | SymQuestionMark | SymAs
| SymOpenParen | SymCloseParen
| SymDoubleOpenBrace | SymDoubleCloseBrace
| SymOpenBrace | SymCloseBrace
| SymOpenVirtualBrace | SymCloseVirtualBrace
| SymOpenPragma | SymClosePragma | SymEllipsis | SymDotDot
| SymEndComment
deriving (Eq, Show)
data Token
= TokKeyword Keyword Interval
| TokId (Interval, String)
| TokQId [(Interval, String)]
| TokLiteral Literal
| TokSymbol Symbol Interval
| TokString (Interval, String)
| TokSetN (Interval, Integer)
| TokTeX (Interval, String)
| TokComment (Interval, String)
| TokDummy
| TokEOF
deriving (Eq, Show)
instance HasRange Token where
getRange (TokKeyword _ i) = getRange i
getRange (TokId (i, _)) = getRange i
getRange (TokQId iss) = Range $ map fst iss
getRange (TokLiteral lit) = getRange lit
getRange (TokSymbol _ i) = getRange i
getRange (TokString (i, _)) = getRange i
getRange (TokSetN (i, _)) = getRange i
getRange (TokTeX (i, _)) = getRange i
getRange (TokComment (i, _)) = getRange i
getRange TokDummy = noRange
getRange TokEOF = noRange