    {-# LANGUAGE DeriveDataTypeable #-}

    module Agda.Syntax.Literal where

    import Control.DeepSeq
    import Data.Char
    import Data.Word

    import Data.Data (Data)

    import Numeric.IEEE ( IEEE(identicalIEEE) )

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Abstract.Name
    import Agda.Utils.Pretty
    import Agda.Utils.FileName

    data Literal = LitNat    Range !Integer
                 | LitWord64 Range !Word64
                 | LitFloat  Range !Double
                 | LitString Range String
                 | LitChar   Range !Char
                 | LitQName  Range QName
                 | LitMeta   Range AbsolutePath MetaId
      deriving Data

    instance Show Literal where
      showsPrec p l = showParen (p > 9) $ case l of
        LitNat _ n    -> sh "LitNat _" n
        LitWord64 _ n -> sh "LitWord64 _" n
        LitFloat _ x  -> sh "LitFloat _" x
        LitString _ s -> sh "LitString _" s
        LitChar _ c   -> sh "LitChar _" c
        LitQName _ q  -> sh "LitQName _" q
        LitMeta _ _ x -> sh "LitMeta _ _" x
        where
          sh :: Show a => String -> a -> ShowS
          sh c x = showString (c ++ " ") . shows x

    instance Pretty Literal where
        pretty (LitNat _ n)     = text $ show n
        pretty (LitWord64 _ n)  = text $ show n
        pretty (LitFloat _ d)   = text $ show d
        pretty (LitString _ s)  = text $ showString' s ""
        pretty (LitChar _ c)    = text $ "'" ++ showChar' c "" ++ "'"
        pretty (LitQName _ x)   = pretty x
        pretty (LitMeta _ _ x)  = pretty x

    showString' :: String -> ShowS
    showString' s =
        foldr (.) id $ [ showString "\"" ] ++ map showChar' s ++ [ showString "\"" ]

    showChar' :: Char -> ShowS
    showChar' '"'   = showString "\\\""
    showChar' c
        | escapeMe c = showLitChar c
        | otherwise  = showString [c]
        where
            escapeMe c = not (isPrint c) || c == '\\'

    instance Eq Literal where
      LitNat _ n    == LitNat _ m    = n == m
      -- ASR (2016-09-29). We use bitwise equality for comparing Double
      -- because Haskell's Eq, which equates 0.0 and -0.0, allows to prove
      -- a contradiction (see Issue #2169).
      LitWord64 _ n == LitWord64 _ m = n == m
      LitFloat _ x  == LitFloat _ y  = identicalIEEE x y || (isNaN x && isNaN y)
      LitString _ s == LitString _ t = s == t
      LitChar _ c   == LitChar _ d   = c == d
      LitQName _ x  == LitQName _ y  = x == y
      LitMeta _ f x == LitMeta _ g y = (f, x) == (f, y)
      _             == _             = False

    instance Ord Literal where
      LitNat _ n    `compare` LitNat _ m    = n `compare` m
      LitWord64 _ n `compare` LitWord64 _ m = n `compare` m
      LitFloat _ x  `compare` LitFloat _ y  = compareFloat x y
      LitString _ s `compare` LitString _ t = s `compare` t
      LitChar _ c   `compare` LitChar _ d   = c `compare` d
      LitQName _ x  `compare` LitQName _ y  = x `compare` y
      LitMeta _ f x `compare` LitMeta _ g y = (f, x) `compare` (g, y)
      compare LitNat{}    _ = LT
      compare _ LitNat{}    = GT
      compare LitWord64{} _ = LT
      compare _ LitWord64{} = GT
      compare LitFloat{}  _ = LT
      compare _ LitFloat{}  = GT
      compare LitString{} _ = LT
      compare _ LitString{} = GT
      compare LitChar{} _   = LT
      compare _ LitChar{}   = GT
      compare LitQName{} _  = LT
      compare _ LitQName{}  = GT
      -- compare LitMeta{} _   = LT
      -- compare _ LitMeta{}   = GT

    -- NOTE: This is not the same ordering as primFloatNumericalEquality!
    -- This ordering must be a total order of all allowed float values,
    -- while primFloatNumericalEquality is only a preorder
    compareFloat :: Double -> Double -> Ordering
    compareFloat x y
      | identicalIEEE x y          = EQ
      | isNegInf x                 = LT
      | isNegInf y                 = GT
      | isNaN x && isNaN y         = EQ
      | isNaN x                    = LT
      | isNaN y                    = GT
      | isNegativeZero x && x == y = LT
      | isNegativeZero y && x == y = GT
      | otherwise                  = compare x y
      where
        isNegInf z = z < 0 && isInfinite z

    instance HasRange Literal where
      getRange (LitNat    r _) = r
      getRange (LitWord64 r _) = r
      getRange (LitFloat  r _) = r
      getRange (LitString r _) = r
      getRange (LitChar   r _) = r
      getRange (LitQName  r _) = r
      getRange (LitMeta r _ _) = r

    instance SetRange Literal where
      setRange r (LitNat    _ x) = LitNat    r x
      setRange r (LitWord64 _ x) = LitWord64 r x
      setRange r (LitFloat  _ x) = LitFloat  r x
      setRange r (LitString _ x) = LitString r x
      setRange r (LitChar   _ x) = LitChar   r x
      setRange r (LitQName  _ x) = LitQName  r x
      setRange r (LitMeta _ f x) = LitMeta   r f x

    instance KillRange Literal where
      killRange (LitNat    r x) = LitNat    (killRange r) x
      killRange (LitWord64 r x) = LitWord64 (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
      killRange (LitQName  r x) = killRange2 LitQName r x
      killRange (LitMeta r f x) = LitMeta   (killRange r) f x

    -- | Ranges are not forced.

    instance NFData Literal where
      rnf (LitNat _ _)    = ()
      rnf (LitWord64 _ _) = ()
      rnf (LitFloat _ _)  = ()
      rnf (LitString _ a) = rnf a
      rnf (LitChar _ _)   = ()
      rnf (LitQName _ a)  = rnf a
      rnf (LitMeta _ _ x) = rnf x