{-# 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 Typeable Literal
DataType
Constr
Typeable Literal
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Literal -> c Literal)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Literal)
-> (Literal -> Constr)
-> (Literal -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Literal))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal))
-> ((forall b. Data b => b -> b) -> Literal -> Literal)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r)
-> (forall u. (forall d. Data d => d -> u) -> Literal -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal)
-> Data Literal
Literal -> DataType
Literal -> Constr
(forall b. Data b => b -> b) -> Literal -> Literal
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
forall u. (forall d. Data d => d -> u) -> Literal -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Literal)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
$cLitMeta :: Constr
$cLitQName :: Constr
$cLitChar :: Constr
$cLitString :: Constr
$cLitFloat :: Constr
$cLitWord64 :: Constr
$cLitNat :: Constr
$tLiteral :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Literal -> m Literal
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
gmapMp :: (forall d. Data d => d -> m d) -> Literal -> m Literal
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
gmapM :: (forall d. Data d => d -> m d) -> Literal -> m Literal
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
$cgmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Literal)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Literal)
dataTypeOf :: Literal -> DataType
$cdataTypeOf :: Literal -> DataType
toConstr :: Literal -> Constr
$ctoConstr :: Literal -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
$cp1Data :: Typeable Literal
Data

instance Show Literal where
  showsPrec :: Int -> Literal -> ShowS
showsPrec Int
p Literal
l = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Literal
l of
    LitNat Range
_ Integer
n    -> String -> Integer -> ShowS
forall a. Show a => String -> a -> ShowS
sh String
"LitNat _" Integer
n
    LitWord64 Range
_ Word64
n -> String -> Word64 -> ShowS
forall a. Show a => String -> a -> ShowS
sh String
"LitWord64 _" Word64
n
    LitFloat Range
_ Double
x  -> String -> Double -> ShowS
forall a. Show a => String -> a -> ShowS
sh String
"LitFloat _" Double
x
    LitString Range
_ String
s -> String -> String -> ShowS
forall a. Show a => String -> a -> ShowS
sh String
"LitString _" String
s
    LitChar Range
_ Char
c   -> String -> Char -> ShowS
forall a. Show a => String -> a -> ShowS
sh String
"LitChar _" Char
c
    LitQName Range
_ QName
q  -> String -> QName -> ShowS
forall a. Show a => String -> a -> ShowS
sh String
"LitQName _" QName
q
    LitMeta Range
_ AbsolutePath
_ MetaId
x -> String -> MetaId -> ShowS
forall a. Show a => String -> a -> ShowS
sh String
"LitMeta _ _" MetaId
x
    where
      sh :: Show a => String -> a -> ShowS
      sh :: String -> a -> ShowS
sh String
c a
x = String -> ShowS
showString (String
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ") ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShowS
forall a. Show a => a -> ShowS
shows a
x

instance Pretty Literal where
    pretty :: Literal -> Doc
pretty (LitNat Range
_ Integer
n)     = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
n
    pretty (LitWord64 Range
_ Word64
n)  = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Word64 -> String
forall a. Show a => a -> String
show Word64
n
    pretty (LitFloat Range
_ Double
d)   = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Double -> String
forall a. Show a => a -> String
show Double
d
    pretty (LitString Range
_ String
s)  = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString' String
s String
""
    pretty (LitChar Range
_ Char
c)    = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> ShowS
showChar' Char
c String
"'"
    pretty (LitQName Range
_ QName
x)   = QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
    pretty (LitMeta Range
_ AbsolutePath
_ MetaId
x)  = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x

showString' :: String -> ShowS
showString' :: String -> ShowS
showString' String
s =
    (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id ([ShowS] -> ShowS) -> [ShowS] -> ShowS
forall a b. (a -> b) -> a -> b
$ [ String -> ShowS
showString String
"\"" ] [ShowS] -> [ShowS] -> [ShowS]
forall a. [a] -> [a] -> [a]
++ (Char -> ShowS) -> String -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map Char -> ShowS
showChar' String
s [ShowS] -> [ShowS] -> [ShowS]
forall a. [a] -> [a] -> [a]
++ [ String -> ShowS
showString String
"\"" ]

showChar' :: Char -> ShowS
showChar' :: Char -> ShowS
showChar' Char
'"'   = String -> ShowS
showString String
"\\\""
showChar' Char
c
    | Char -> Bool
escapeMe Char
c = Char -> ShowS
showLitChar Char
c
    | Bool
otherwise  = String -> ShowS
showString [Char
c]
    where
        escapeMe :: Char -> Bool
escapeMe Char
c = Bool -> Bool
not (Char -> Bool
isPrint Char
c) Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\\'

instance Eq Literal where
  LitNat Range
_ Integer
n    == :: Literal -> Literal -> Bool
== LitNat Range
_ Integer
m    = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
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 Range
_ Word64
n == LitWord64 Range
_ Word64
m = Word64
n Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
m
  LitFloat Range
_ Double
x  == LitFloat Range
_ Double
y  = Double -> Double -> Bool
forall a. IEEE a => a -> a -> Bool
identicalIEEE Double
x Double
y Bool -> Bool -> Bool
|| (Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x Bool -> Bool -> Bool
&& Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
y)
  LitString Range
_ String
s == LitString Range
_ String
t = String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
t
  LitChar Range
_ Char
c   == LitChar Range
_ Char
d   = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
d
  LitQName Range
_ QName
x  == LitQName Range
_ QName
y  = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
  LitMeta Range
_ AbsolutePath
f MetaId
x == LitMeta Range
_ AbsolutePath
g MetaId
y = (AbsolutePath
f, MetaId
x) (AbsolutePath, MetaId) -> (AbsolutePath, MetaId) -> Bool
forall a. Eq a => a -> a -> Bool
== (AbsolutePath
f, MetaId
y)
  Literal
_             == Literal
_             = Bool
False

instance Ord Literal where
  LitNat Range
_ Integer
n    compare :: Literal -> Literal -> Ordering
`compare` LitNat Range
_ Integer
m    = Integer
n Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Integer
m
  LitWord64 Range
_ Word64
n `compare` LitWord64 Range
_ Word64
m = Word64
n Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Word64
m
  LitFloat Range
_ Double
x  `compare` LitFloat Range
_ Double
y  = Double -> Double -> Ordering
compareFloat Double
x Double
y
  LitString Range
_ String
s `compare` LitString Range
_ String
t = String
s String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` String
t
  LitChar Range
_ Char
c   `compare` LitChar Range
_ Char
d   = Char
c Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Char
d
  LitQName Range
_ QName
x  `compare` LitQName Range
_ QName
y  = QName
x QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QName
y
  LitMeta Range
_ AbsolutePath
f MetaId
x `compare` LitMeta Range
_ AbsolutePath
g MetaId
y = (AbsolutePath
f, MetaId
x) (AbsolutePath, MetaId) -> (AbsolutePath, MetaId) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` (AbsolutePath
g, MetaId
y)
  compare LitNat{}    Literal
_ = Ordering
LT
  compare Literal
_ LitNat{}    = Ordering
GT
  compare LitWord64{} Literal
_ = Ordering
LT
  compare Literal
_ LitWord64{} = Ordering
GT
  compare LitFloat{}  Literal
_ = Ordering
LT
  compare Literal
_ LitFloat{}  = Ordering
GT
  compare LitString{} Literal
_ = Ordering
LT
  compare Literal
_ LitString{} = Ordering
GT
  compare LitChar{} Literal
_   = Ordering
LT
  compare Literal
_ LitChar{}   = Ordering
GT
  compare LitQName{} Literal
_  = Ordering
LT
  compare Literal
_ LitQName{}  = Ordering
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 :: Double -> Double -> Ordering
compareFloat Double
x Double
y
  | Double -> Double -> Bool
forall a. IEEE a => a -> a -> Bool
identicalIEEE Double
x Double
y          = Ordering
EQ
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegInf Double
x                 = Ordering
LT
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegInf Double
y                 = Ordering
GT
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x Bool -> Bool -> Bool
&& Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
y         = Ordering
EQ
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x                    = Ordering
LT
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
y                    = Ordering
GT
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Double
x Bool -> Bool -> Bool
&& Double
x Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
y = Ordering
LT
  | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Double
y Bool -> Bool -> Bool
&& Double
x Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
y = Ordering
GT
  | Bool
otherwise                  = Double -> Double -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Double
x Double
y
  where
    isNegInf :: a -> Bool
isNegInf a
z = a
z a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
&& a -> Bool
forall a. RealFloat a => a -> Bool
isInfinite a
z

instance HasRange Literal where
  getRange :: Literal -> Range
getRange (LitNat    Range
r Integer
_) = Range
r
  getRange (LitWord64 Range
r Word64
_) = Range
r
  getRange (LitFloat  Range
r Double
_) = Range
r
  getRange (LitString Range
r String
_) = Range
r
  getRange (LitChar   Range
r Char
_) = Range
r
  getRange (LitQName  Range
r QName
_) = Range
r
  getRange (LitMeta Range
r AbsolutePath
_ MetaId
_) = Range
r

instance SetRange Literal where
  setRange :: Range -> Literal -> Literal
setRange Range
r (LitNat    Range
_ Integer
x) = Range -> Integer -> Literal
LitNat    Range
r Integer
x
  setRange Range
r (LitWord64 Range
_ Word64
x) = Range -> Word64 -> Literal
LitWord64 Range
r Word64
x
  setRange Range
r (LitFloat  Range
_ Double
x) = Range -> Double -> Literal
LitFloat  Range
r Double
x
  setRange Range
r (LitString Range
_ String
x) = Range -> String -> Literal
LitString Range
r String
x
  setRange Range
r (LitChar   Range
_ Char
x) = Range -> Char -> Literal
LitChar   Range
r Char
x
  setRange Range
r (LitQName  Range
_ QName
x) = Range -> QName -> Literal
LitQName  Range
r QName
x
  setRange Range
r (LitMeta Range
_ AbsolutePath
f MetaId
x) = Range -> AbsolutePath -> MetaId -> Literal
LitMeta   Range
r AbsolutePath
f MetaId
x

instance KillRange Literal where
  killRange :: Literal -> Literal
killRange (LitNat    Range
r Integer
x) = Range -> Integer -> Literal
LitNat    (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Integer
x
  killRange (LitWord64 Range
r Word64
x) = Range -> Word64 -> Literal
LitWord64 (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Word64
x
  killRange (LitFloat  Range
r Double
x) = Range -> Double -> Literal
LitFloat  (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Double
x
  killRange (LitString Range
r String
x) = Range -> String -> Literal
LitString (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) String
x
  killRange (LitChar   Range
r Char
x) = Range -> Char -> Literal
LitChar   (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Char
x
  killRange (LitQName  Range
r QName
x) = (Range -> QName -> Literal) -> Range -> QName -> Literal
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 Range -> QName -> Literal
LitQName Range
r QName
x
  killRange (LitMeta Range
r AbsolutePath
f MetaId
x) = Range -> AbsolutePath -> MetaId -> Literal
LitMeta   (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) AbsolutePath
f MetaId
x

-- | Ranges are not forced.

instance NFData Literal where
  rnf :: Literal -> ()
rnf (LitNat Range
_ Integer
_)    = ()
  rnf (LitWord64 Range
_ Word64
_) = ()
  rnf (LitFloat Range
_ Double
_)  = ()
  rnf (LitString Range
_ String
a) = String -> ()
forall a. NFData a => a -> ()
rnf String
a
  rnf (LitChar Range
_ Char
_)   = ()
  rnf (LitQName Range
_ QName
a)  = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
  rnf (LitMeta Range
_ AbsolutePath
_ MetaId
x) = MetaId -> ()
forall a. NFData a => a -> ()
rnf MetaId
x