    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Syntax.Parser.Tokens
        ( Token(..)
        , Keyword(..)
        , layoutKeywords
        , Symbol(..)
        ) where

    import Data.Functor (void)

    import Agda.Syntax.Literal (RLiteral)
    import Agda.Syntax.Position

    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
        deriving (Keyword -> Keyword -> Bool
    (Keyword -> Keyword -> Bool)
    -> (Keyword -> Keyword -> Bool) -> Eq Keyword
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Keyword -> Keyword -> Bool
    == :: Keyword -> Keyword -> Bool
    $c/= :: Keyword -> Keyword -> Bool
    /= :: Keyword -> Keyword -> Bool
    Eq, Int -> Keyword -> ShowS
    [Keyword] -> ShowS
    Keyword -> String
    (Int -> Keyword -> ShowS)
    -> (Keyword -> String) -> ([Keyword] -> ShowS) -> Show Keyword
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Keyword -> ShowS
    showsPrec :: Int -> Keyword -> ShowS
    $cshow :: Keyword -> String
    show :: Keyword -> String
    $cshowList :: [Keyword] -> ShowS
    showList :: [Keyword] -> ShowS
    Show)

    -- | Unconditional layout keywords.
    --
    -- Some keywords introduce layout only in certain circumstances,
    -- these are not included here.
    --
    layoutKeywords :: [Keyword]
    layoutKeywords :: [Keyword]
    layoutKeywords =
        [ Keyword
    KwAbstract
        , Keyword
    KwDo
        , Keyword
    KwField
        , Keyword
    KwInstance
        , Keyword
    KwLet
        , Keyword
    KwMacro
        , Keyword
    KwMutual
        , Keyword
    KwPostulate
        , Keyword
    KwPrimitive
        , Keyword
    KwPrivate
        , Keyword
    KwVariable
        , Keyword
    KwWhere
        , Keyword
    KwOpaque
        ]

    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 -- ^ A misplaced end-comment "-}".
        deriving (Symbol -> Symbol -> Bool
    (Symbol -> Symbol -> Bool)
    -> (Symbol -> Symbol -> Bool) -> Eq Symbol
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Symbol -> Symbol -> Bool
    == :: Symbol -> Symbol -> Bool
    $c/= :: Symbol -> Symbol -> Bool
    /= :: Symbol -> Symbol -> Bool
    Eq, Int -> Symbol -> ShowS
    [Symbol] -> ShowS
    Symbol -> String
    (Int -> Symbol -> ShowS)
    -> (Symbol -> String) -> ([Symbol] -> ShowS) -> Show Symbol
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Symbol -> ShowS
    showsPrec :: Int -> Symbol -> ShowS
    $cshow :: Symbol -> String
    show :: Symbol -> String
    $cshowList :: [Symbol] -> ShowS
    showList :: [Symbol] -> ShowS
    Show)

    data Token
              -- Keywords
            = TokKeyword Keyword Interval
              -- Identifiers and operators
            | TokId         (Interval, String)
            | TokQId        [(Interval, String)]
                            -- Non-empty namespace. The intervals for
                            -- "A.B.x" correspond to "A.", "B." and "x".
              -- Literals
            | TokLiteral    RLiteral
              -- Special symbols
            | TokSymbol Symbol Interval
              -- Other tokens
            | TokString (Interval, String)
                -- ^ Arbitrary string (not enclosed in double quotes), used in pragmas.
            | TokTeX (Interval, String)
            | TokMarkup (Interval, String)
            | TokComment (Interval, String)
            | TokDummy      -- Dummy token to make Happy not complain
                            -- about overlapping cases.
            | TokEOF Interval
        deriving (Token -> Token -> Bool
    (Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Token -> Token -> Bool
    == :: Token -> Token -> Bool
    $c/= :: Token -> Token -> Bool
    /= :: Token -> Token -> Bool
    Eq, Int -> Token -> ShowS
    [Token] -> ShowS
    Token -> String
    (Int -> Token -> ShowS)
    -> (Token -> String) -> ([Token] -> ShowS) -> Show Token
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Token -> ShowS
    showsPrec :: Int -> Token -> ShowS
    $cshow :: Token -> String
    show :: Token -> String
    $cshowList :: [Token] -> ShowS
    showList :: [Token] -> ShowS
    Show)

    instance HasRange Token where
      getRange :: Token -> Range
    getRange (TokKeyword Keyword
    _ Interval
    i)    = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
      getRange (TokId (Interval
    i, String
    _))      = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
      getRange (TokQId [(Interval, String)]
    iss)        = [Interval] -> Range
    forall a. HasRange a => a -> Range
    getRange (((Interval, String) -> Interval)
    -> [(Interval, String)] -> [Interval]
    forall a b. (a -> b) -> [a] -> [b]
    map (Interval, String) -> Interval
    forall a b. (a, b) -> a
    fst [(Interval, String)]
    iss)
      getRange (TokLiteral RLiteral
    lit)    = RLiteral -> Range
    forall a. HasRange a => a -> Range
    getRange RLiteral
    lit
      getRange (TokSymbol Symbol
    _ Interval
    i)     = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
      getRange (TokString (Interval
    i, String
    _))  = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
      getRange (TokTeX (Interval
    i, String
    _))     = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
      getRange (TokMarkup (Interval
    i, String
    _))  = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
      getRange (TokComment (Interval
    i, String
    _)) = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
      getRange Token
    TokDummy            = Range
    forall a. Range' a
    noRange
      getRange (TokEOF Interval
    i)          = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i

    instance HasRangeWithoutFile Token where
      getRangeWithoutFile :: Token -> RangeWithoutFile
    getRangeWithoutFile = Range -> RangeWithoutFile
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (Range -> RangeWithoutFile)
    -> (Token -> Range) -> Token -> RangeWithoutFile
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Token -> Range
    forall a. HasRange a => a -> Range
    getRange