Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Parser.Tokens

Synopsis

- data Token
  - = TokKeyword Keyword Interval
  - | TokId (Interval, String)
  - | TokQId [(Interval, String)]
  - | TokLiteral RLiteral
  - | TokSymbol Symbol Interval
  - | TokString (Interval, String)
  - | TokTeX (Interval, String)
  - | TokMarkup (Interval, String)
  - | TokComment (Interval, String)
  - | TokDummy
  - | TokEOF 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
  - | SymOpenIdiomBracket
  - | SymCloseIdiomBracket
  - | SymEmptyIdiomBracket
  - | SymDoubleOpenBrace
  - | SymDoubleCloseBrace
  - | SymOpenBrace
  - | SymCloseBrace
  - | SymOpenVirtualBrace
  - | SymCloseVirtualBrace
  - | SymOpenPragma
  - | SymClosePragma
  - | SymEllipsis
  - | SymDotDot
  - | SymEndComment

# Documentation

data Token Source #

Constructors

TokKeyword Keyword Interval |
TokId (Interval, String) |
TokQId [(Interval, String)] |
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 |

#### 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 Source # show :: Token -> String Source # showList :: [Token] -> ShowS Source #
Eq Token Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Token -> Token -> Bool Source # (/=) :: Token -> Token -> Bool Source #

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 Source # show :: Keyword -> String Source # showList :: [Keyword] -> ShowS Source #
Eq Keyword Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Keyword -> Keyword -> Bool Source # (/=) :: Keyword -> Keyword -> Bool Source #

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 |
SymBar |
SymColon |
SymArrow |
SymEqual |
SymLambda |
SymUnderscore |
SymQuestionMark |
SymAs |
SymOpenParen |
SymCloseParen |
SymOpenIdiomBracket |
SymCloseIdiomBracket |
SymEmptyIdiomBracket |
SymDoubleOpenBrace |
SymDoubleCloseBrace |
SymOpenBrace |
SymCloseBrace |
SymOpenVirtualBrace |
SymCloseVirtualBrace |
SymOpenPragma |
SymClosePragma |
SymEllipsis |
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 Source # show :: Symbol -> String Source # showList :: [Symbol] -> ShowS Source #
Eq Symbol Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Symbol -> Symbol -> Bool Source # (/=) :: Symbol -> Symbol -> Bool Source #