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

import Agda.Syntax.Literal (Literal)
import Agda.Syntax.Concrete.Name (Name, QName)
import Agda.Syntax.Position

data Keyword
	= KwLet | KwIn | KwWhere | KwData | KwCoData
	| KwPostulate | KwMutual | KwAbstract | KwPrivate
	| KwOpen | KwImport | KwModule | KwPrimitive
	| KwInfix | KwInfixL | KwInfixR | KwWith | KwRewrite
	| KwSet | KwProp | KwForall | KwRecord | KwConstructor | KwField
	| KwHiding | KwUsing | KwRenaming | KwTo | KwPublic
	| KwOPTIONS | KwBUILTIN | KwLINE
        | KwCOMPILED_DATA | KwCOMPILED_TYPE | KwCOMPILED | KwIMPORT
        | KwIMPOSSIBLE
    deriving (Eq, Show)

layoutKeywords :: [Keyword]
layoutKeywords =
    [ KwLet, KwWhere, KwPostulate, KwMutual, KwAbstract, KwPrivate, KwPrimitive, KwField ]

data Symbol
	= SymDot | SymSemi | SymVirtualSemi | SymBar
	| SymColon | SymArrow | SymEqual | SymLambda
	| SymUnderscore	| SymQuestionMark   | SymAs
	| SymOpenParen	      | SymCloseParen
	| SymOpenBrace	      | SymCloseBrace
	| SymOpenVirtualBrace | SymCloseVirtualBrace
	| SymOpenPragma	      | SymClosePragma | SymEllipsis
    deriving (Eq, Show)

data Token
	  -- Keywords
	= TokKeyword Keyword Interval
	  -- Identifiers and operators
	| TokId		(Interval, String)
	| TokQId	[(Interval, String)] -- non empty namespace
	  -- Literals
	| TokLiteral	Literal
	  -- Special symbols
	| TokSymbol Symbol Interval
	  -- Other tokens
	| TokString (Interval, String)  -- arbitrary string, used in pragmas
	| TokSetN (Interval, Integer)
	| TokTeX (Interval, String)
        | TokComment (Interval, String)
	| TokDummy	-- Dummy token to make Happy not complain
			-- about overlapping cases.
	| 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