module Agda.Syntax.Literal where

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

import Data.Data (Data)
import Data.Text (Text)
import qualified Data.Text as T

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import Agda.Utils.FileName
import Agda.Utils.Float ( doubleDenotEq, doubleDenotOrd )
import Agda.Utils.Pretty

type RLiteral = Ranged Literal
data Literal
  = LitNat    !Integer
  | LitWord64 !Word64
  | LitFloat  !Double
  | LitString !Text
  | LitChar   !Char
  | LitQName  !QName
  | LitMeta   AbsolutePath MetaId
  deriving (Typeable Literal
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 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Int -> Literal -> ShowS
[Literal] -> ShowS
Literal -> String
(Int -> Literal -> ShowS)
-> (Literal -> String) -> ([Literal] -> ShowS) -> Show Literal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Literal] -> ShowS
$cshowList :: [Literal] -> ShowS
show :: Literal -> String
$cshow :: Literal -> String
showsPrec :: Int -> Literal -> ShowS
$cshowsPrec :: Int -> Literal -> ShowS
Show)

instance Pretty Literal where
    pretty :: Literal -> Doc
pretty (LitNat Integer
n)     = Integer -> Doc
forall a. Pretty a => a -> Doc
pretty Integer
n
    pretty (LitWord64 Word64
n)  = Word64 -> Doc
forall a. Pretty a => a -> Doc
pretty Word64
n
    pretty (LitFloat Double
d)   = Double -> Doc
forall a. Pretty a => a -> Doc
pretty Double
d
    pretty (LitString Text
s)  = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Text -> ShowS
showText Text
s String
""
    pretty (LitChar 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 QName
x)   = QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
    pretty (LitMeta AbsolutePath
_ MetaId
x)  = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x

showText :: Text -> ShowS
showText :: Text -> ShowS
showText Text
s = String -> ShowS
showString String
"\""
           ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> ShowS -> ShowS) -> ShowS -> Text -> ShowS
forall a. (Char -> a -> a) -> a -> Text -> a
T.foldr (\ Char
c -> (Char -> ShowS
showChar' Char
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)) ShowS
forall a. a -> a
id Text
s
           ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Integer
n    == :: Literal -> Literal -> Bool
== LitNat 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 Word64
n == LitWord64 Word64
m = Word64
n Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
m
  LitFloat Double
x  == LitFloat Double
y  = Double -> Double -> Bool
doubleDenotEq Double
x Double
y
  LitString Text
s == LitString Text
t = Text
s Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
t
  LitChar Char
c   == LitChar Char
d   = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
d
  LitQName QName
x  == LitQName QName
y  = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
  LitMeta AbsolutePath
f MetaId
x == LitMeta AbsolutePath
g MetaId
y = (AbsolutePath
f, MetaId
x) (AbsolutePath, MetaId) -> (AbsolutePath, MetaId) -> Bool
forall a. Eq a => a -> a -> Bool
== (AbsolutePath
g, MetaId
y)
  Literal
_           == Literal
_             = Bool
False

instance Ord Literal where
  LitNat Integer
n    compare :: Literal -> Literal -> Ordering
`compare` LitNat Integer
m    = Integer
n Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Integer
m
  LitWord64 Word64
n `compare` LitWord64 Word64
m = Word64
n Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Word64
m
  LitFloat Double
x  `compare` LitFloat Double
y  = Double -> Double -> Ordering
doubleDenotOrd Double
x Double
y
  LitString Text
s `compare` LitString Text
t = Text
s Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Text
t
  LitChar Char
c   `compare` LitChar Char
d   = Char
c Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Char
d
  LitQName QName
x  `compare` LitQName QName
y  = QName
x QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QName
y
  LitMeta AbsolutePath
f MetaId
x `compare` LitMeta 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

instance KillRange Literal where
  killRange :: Literal -> Literal
killRange (LitNat    Integer
x) = Integer -> Literal
LitNat    Integer
x
  killRange (LitWord64 Word64
x) = Word64 -> Literal
LitWord64 Word64
x
  killRange (LitFloat  Double
x) = Double -> Literal
LitFloat  Double
x
  killRange (LitString Text
x) = Text -> Literal
LitString Text
x
  killRange (LitChar   Char
x) = Char -> Literal
LitChar   Char
x
  killRange (LitQName  QName
x) = (QName -> Literal) -> QName -> Literal
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 QName -> Literal
LitQName QName
x
  killRange (LitMeta AbsolutePath
f MetaId
x) = AbsolutePath -> MetaId -> Literal
LitMeta AbsolutePath
f MetaId
x

-- | Ranges are not forced.

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