Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Parser.Tokens

Synopsis

data Token where
- TokKeyword Keyword Interval
- TokId (Interval, String)
- TokQId [(Interval, String)]
- TokQual_ QualifiedToken
- TokLiteral RLiteral
- TokSymbol Symbol Interval
- TokString (Interval, String)
- TokTeX (Interval, String)
- TokMarkup (Interval, String)
- TokComment (Interval, String)
- TokDummy
- TokEOF Interval
- pattern TokQual :: QualifiableToken -> [(Interval, String)] -> Interval -> Token
data QualifiableToken
- = QualDo
- | QualEmptyIdiom
- | QualOpenIdiom Bool
data QualifiedToken = QualifiedToken QualifiableToken [(Interval, String)] Interval
data Keyword
- = KwLet
- | KwIn
- | KwWhere
- | KwData
- | KwCoData
- | KwDo
- | KwPostulate
- | KwAbstract
- | KwPrivate
- | KwInstance
- | KwInterleaved
- | KwMutual
- | KwOverlap
- | KwOpen
- | KwImport
- | KwModule
- | KwPrimitive
- | KwMacro
- | KwInfix
- | KwInfixL
- | KwInfixR
- | KwWith
- | KwRewrite
- | KwForall
- | KwRecord
- | KwConstructor
- | KwField
- | KwInductive
- | KwCoInductive
- | KwEta
- | KwNoEta
- | KwHiding
- | KwUsing
- | KwRenaming
- | KwTo
- | KwPublic
- | KwOpaque
- | KwUnfolding
- | KwOPTIONS
- | KwBUILTIN
- | KwLINE
- | KwFOREIGN
- | KwCOMPILE
- | KwIMPOSSIBLE
- | KwSTATIC
- | KwINJECTIVE
- | KwINJECTIVE_FOR_INFERENCE
- | KwINLINE
- | KwNOINLINE
- | KwETA
- | KwNO_TERMINATION_CHECK
- | KwTERMINATING
- | KwNON_TERMINATING
- | KwNOT_PROJECTION_LIKE
- | KwNON_COVERING
- | KwWARNING_ON_USAGE
- | KwWARNING_ON_IMPORT
- | KwMEASURE
- | KwDISPLAY
- | KwREWRITE
- | KwOVERLAPPABLE
- | KwOVERLAPPING
- | KwOVERLAPS
- | KwINCOHERENT
- | KwQuote
- | KwQuoteTerm
- | KwUnquote
- | KwUnquoteDecl
- | KwUnquoteDef
- | KwSyntax
- | KwPatternSyn
- | KwTactic
- | KwCATCHALL
- | KwVariable
- | KwNO_POSITIVITY_CHECK
- | KwPOLARITY
- | KwNO_UNIVERSE_CHECK
layoutKeywords :: [Keyword]
data Symbol
- = SymDot
- | SymSemi
- | SymVirtualSemi
- | SymBar
- | SymColon
- | SymArrow
- | SymEqual
- | SymLambda
- | SymUnderscore
- | SymQuestionMark
- | SymAs
- | SymOpenParen
- | SymCloseParen
- | SymEmptyIdiomBracket
- | SymOpenIdiomBracket Bool
- | SymCloseIdiomBracket Bool
- | SymDoubleOpenBrace Bool
- | SymDoubleCloseBrace Bool
- | SymOpenBrace
- | SymCloseBrace
- | SymOpenVirtualBrace
- | SymCloseVirtualBrace
- | SymOpenPragma
- | SymClosePragma
- | SymEllipsis
- | SymDotDot
- | SymEndComment

Documentation

data Token Source #

Constructors

TokKeyword Keyword Interval
TokId (Interval, String)
TokQId [(Interval, String)]
TokQual_ QualifiedToken
TokLiteral RLiteral
TokSymbol Symbol Interval
TokString (Interval, String)	Arbitrary string (not enclosed in double quotes), used in pragmas.
TokTeX (Interval, String)
TokMarkup (Interval, String)
TokComment (Interval, String)
TokDummy
TokEOF Interval

Bundled Patterns

pattern TokQual :: QualifiableToken -> [(Interval, String)] -> Interval -> Token

Instances

Instances details

HasRange Token Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods getRange :: Token -> Range Source #
HasRangeWithoutFile Token Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods getRangeWithoutFile :: Token -> RangeWithoutFile Source #
Show Token Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> Token -> ShowS # show :: Token -> String # showList :: [Token] -> ShowS #
Eq Token Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Token -> Token -> Bool # (/=) :: Token -> Token -> Bool #

data QualifiableToken Source #

Tokens which may appear qualified.

Constructors

QualDo	qualified `do`
QualEmptyIdiom	qualified `(\|)` or `⦇⦈`
QualOpenIdiom Bool	qualified `(\|` or `⦇`, `True` if unicode

Instances

Instances details

Show QualifiableToken Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> QualifiableToken -> ShowS # show :: QualifiableToken -> String # showList :: [QualifiableToken] -> ShowS #
Eq QualifiableToken Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: QualifiableToken -> QualifiableToken -> Bool # (/=) :: QualifiableToken -> QualifiableToken -> Bool #

data QualifiedToken Source #

A "qualified token", i.e. a sequence of (module) names followed by one of the allowed (QualifiableToken) keywords/symbols.

Constructors

QualifiedToken
Fields QualifiableToken The token itself. [(Interval, String)] Parts for the qualifying identifier, together with their ranges. Interval Range of the token being qualified.

Instances

Instances details

HasRange QualifiedToken Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods getRange :: QualifiedToken -> Range Source #
Show QualifiedToken Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> QualifiedToken -> ShowS # show :: QualifiedToken -> String # showList :: [QualifiedToken] -> ShowS #
Eq QualifiedToken Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: QualifiedToken -> QualifiedToken -> Bool # (/=) :: QualifiedToken -> QualifiedToken -> Bool #

data Keyword Source #

Constructors

KwLet
KwIn
KwWhere
KwData
KwCoData
KwDo
KwPostulate
KwAbstract
KwPrivate
KwInstance
KwInterleaved
KwMutual
KwOverlap
KwOpen
KwImport
KwModule
KwPrimitive
KwMacro
KwInfix
KwInfixL
KwInfixR
KwWith
KwRewrite
KwForall
KwRecord
KwConstructor
KwField
KwInductive
KwCoInductive
KwEta
KwNoEta
KwHiding
KwUsing
KwRenaming
KwTo
KwPublic
KwOpaque
KwUnfolding
KwOPTIONS
KwBUILTIN
KwLINE
KwFOREIGN
KwCOMPILE
KwIMPOSSIBLE
KwSTATIC
KwINJECTIVE
KwINJECTIVE_FOR_INFERENCE
KwINLINE
KwNOINLINE
KwETA
KwNO_TERMINATION_CHECK
KwTERMINATING
KwNON_TERMINATING
KwNOT_PROJECTION_LIKE
KwNON_COVERING
KwWARNING_ON_USAGE
KwWARNING_ON_IMPORT
KwMEASURE
KwDISPLAY
KwREWRITE
KwOVERLAPPABLE
KwOVERLAPPING
KwOVERLAPS
KwINCOHERENT
KwQuote
KwQuoteTerm
KwUnquote
KwUnquoteDecl
KwUnquoteDef
KwSyntax
KwPatternSyn
KwTactic
KwCATCHALL
KwVariable
KwNO_POSITIVITY_CHECK
KwPOLARITY
KwNO_UNIVERSE_CHECK

Instances

Instances details

Show Keyword Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> Keyword -> ShowS # show :: Keyword -> String # showList :: [Keyword] -> ShowS #
Eq Keyword Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Keyword -> Keyword -> Bool # (/=) :: Keyword -> Keyword -> Bool #

layoutKeywords :: [Keyword] Source #

Unconditional layout keywords.

Some keywords introduce layout only in certain circumstances, these are not included here.

data Symbol Source #

Constructors

SymDot	.
SymSemi	;
SymVirtualSemi	layout-implied `;`
SymBar	\|
SymColon	:
SymArrow	`->` or `→`
SymEqual	=
SymLambda	`@ or` λ@
SymUnderscore	_
SymQuestionMark	?
SymAs	@@@
SymOpenParen	(
SymCloseParen	)
SymEmptyIdiomBracket	`(\|)` or `⦇⦈`
SymOpenIdiomBracket Bool	`(\|` or `⦇`, `True` if unicode
SymCloseIdiomBracket Bool	`\|)` or `⦈`, `True` if unicode
SymDoubleOpenBrace Bool	`{{` or `⦃`, `True` if unicode
SymDoubleCloseBrace Bool	`{{` or `⦄`, `True` if unicode
SymOpenBrace	{
SymCloseBrace	}
SymOpenVirtualBrace	layout-implied `{`
SymCloseVirtualBrace	layout-implied `}`
SymOpenPragma	{-#
SymClosePragma	#-}
SymEllipsis	`...` or `…`
SymDotDot	..
SymEndComment	A misplaced end-comment "-}".

Instances

Instances details

Show Symbol Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
Eq Symbol Source #
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #