{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Syntax.Parser.Tokens
    ( Token(.., TokQual)
    , QualifiableToken(..), QualifiedToken(..)
    , 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  -- ^ 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 "-}".
  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)

-- | "Tokens" which may appear qualified.
data QualifiableToken
  = QualDo              -- ^ qualified @do@
  | QualEmptyIdiom      -- ^ qualified @(|)@ or @⦇⦈@
  | QualOpenIdiom  Bool -- ^ qualified @(|@ or @⦇@, 'True' if unicode
  deriving (QualifiableToken -> QualifiableToken -> Bool
(QualifiableToken -> QualifiableToken -> Bool)
-> (QualifiableToken -> QualifiableToken -> Bool)
-> Eq QualifiableToken
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QualifiableToken -> QualifiableToken -> Bool
== :: QualifiableToken -> QualifiableToken -> Bool
$c/= :: QualifiableToken -> QualifiableToken -> Bool
/= :: QualifiableToken -> QualifiableToken -> Bool
Eq, Int -> QualifiableToken -> ShowS
[QualifiableToken] -> ShowS
QualifiableToken -> String
(Int -> QualifiableToken -> ShowS)
-> (QualifiableToken -> String)
-> ([QualifiableToken] -> ShowS)
-> Show QualifiableToken
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QualifiableToken -> ShowS
showsPrec :: Int -> QualifiableToken -> ShowS
$cshow :: QualifiableToken -> String
show :: QualifiableToken -> String
$cshowList :: [QualifiableToken] -> ShowS
showList :: [QualifiableToken] -> ShowS
Show)

-- | A "qualified token", i.e. a sequence of (module) names followed by
-- one of the allowed ('QualifiableToken') keywords/symbols.
data QualifiedToken
  = QualifiedToken
      QualifiableToken     -- ^ The token itself.
      [(Interval, String)] -- ^ Parts for the qualifying identifier, together with their ranges.
      Interval             -- ^ Range of the token being qualified.
  deriving (QualifiedToken -> QualifiedToken -> Bool
(QualifiedToken -> QualifiedToken -> Bool)
-> (QualifiedToken -> QualifiedToken -> Bool) -> Eq QualifiedToken
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QualifiedToken -> QualifiedToken -> Bool
== :: QualifiedToken -> QualifiedToken -> Bool
$c/= :: QualifiedToken -> QualifiedToken -> Bool
/= :: QualifiedToken -> QualifiedToken -> Bool
Eq, Int -> QualifiedToken -> ShowS
[QualifiedToken] -> ShowS
QualifiedToken -> String
(Int -> QualifiedToken -> ShowS)
-> (QualifiedToken -> String)
-> ([QualifiedToken] -> ShowS)
-> Show QualifiedToken
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QualifiedToken -> ShowS
showsPrec :: Int -> QualifiedToken -> ShowS
$cshow :: QualifiedToken -> String
show :: QualifiedToken -> String
$cshowList :: [QualifiedToken] -> ShowS
showList :: [QualifiedToken] -> 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".
        | TokQual_      QualifiedToken
          -- 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)

pattern TokQual :: QualifiableToken -> [(Interval, String)] -> Interval -> Token
pattern $mTokQual :: forall {r}.
Token
-> (QualifiableToken -> [(Interval, String)] -> Interval -> r)
-> ((# #) -> r)
-> r
$bTokQual :: QualifiableToken -> [(Interval, String)] -> Interval -> Token
TokQual clz iss j = TokQual_ (QualifiedToken clz iss j)

{-# COMPLETE TokKeyword, TokId, TokQId, TokQual, TokLiteral, TokSymbol, TokString, TokTeX, TokMarkup, TokComment, TokDummy, TokEOF #-}

instance HasRange QualifiedToken where
  getRange :: QualifiedToken -> Range
getRange (QualifiedToken QualifiableToken
_ [(Interval, String)]
iss Interval
j) = ([Interval], 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, Interval
j)

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 (TokQual_ QualifiedToken
q)        = QualifiedToken -> Range
forall a. HasRange a => a -> Range
getRange QualifiedToken
q
  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