    {-# LANGUAGE DeriveDataTypeable #-}
    module Agda.Syntax.Literal where

    import Data.Generics (Typeable, Data)

    import Agda.Syntax.Position

    data Literal = LitInt    Range Integer
                 | LitLevel  Range Integer
    	     | LitFloat  Range Double
    	     | LitString Range String
    	     | LitChar   Range Char
      deriving (Typeable, Data, Show)

    instance Eq Literal where
      LitLevel _ n  == LitLevel _ m  = n == m
      LitInt _ n    == LitInt _ m    = n == m
      LitFloat _ x  == LitFloat _ y  = x == y
      LitString _ s == LitString _ t = s == t
      LitChar _ c   == LitChar _ d   = c == d
      _             == _             = False

    instance Ord Literal where
      LitLevel _ n  `compare` LitLevel _ m  = n `compare` m
      LitInt _ n    `compare` LitInt _ m    = n `compare` m
      LitFloat _ x  `compare` LitFloat _ y  = x `compare` y
      LitString _ s `compare` LitString _ t = s `compare` t
      LitChar _ c   `compare` LitChar _ d   = c `compare` d
      compare LitLevel{}    _ = LT
      compare _ LitLevel{} = GT
      compare LitInt{}    _ = LT
      compare _ LitInt{} = GT
      compare LitFloat{}  _ = LT
      compare _ LitFloat{} = GT
      compare LitString{} _ = LT
      compare _ LitString{} = GT

    instance HasRange Literal where
      getRange (LitLevel  r _) = r
      getRange (LitInt    r _) = r
      getRange (LitFloat  r _) = r
      getRange (LitString r _) = r
      getRange (LitChar   r _) = r

    instance SetRange Literal where
      setRange r (LitLevel  _ x) = LitLevel  r x
      setRange r (LitInt    _ x) = LitInt    r x
      setRange r (LitFloat  _ x) = LitFloat  r x
      setRange r (LitString _ x) = LitString r x
      setRange r (LitChar   _ x) = LitChar   r x

    instance KillRange Literal where
      killRange (LitLevel  r x) = LitLevel  (killRange r) x
      killRange (LitInt    r x) = LitInt    (killRange r) x
      killRange (LitFloat  r x) = LitFloat  (killRange r) x
      killRange (LitString r x) = LitString (killRange r) x
      killRange (LitChar   r x) = LitChar   (killRange r) x