module Agda.Syntax.Literal where

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

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

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import {-# SOURCE #-} Agda.Syntax.TopLevelModuleName
  (TopLevelModuleName)
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   !TopLevelModuleName !MetaId
  deriving 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
$cshowsPrec :: Int -> Literal -> ShowS
showsPrec :: Int -> Literal -> ShowS
$cshow :: Literal -> String
show :: Literal -> String
$cshowList :: [Literal] -> ShowS
showList :: [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 TopLevelModuleName
_ 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 TopLevelModuleName
f MetaId
x == LitMeta TopLevelModuleName
g MetaId
y = (TopLevelModuleName
f, MetaId
x) (TopLevelModuleName, MetaId)
-> (TopLevelModuleName, MetaId) -> Bool
forall a. Eq a => a -> a -> Bool
== (TopLevelModuleName
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 TopLevelModuleName
f MetaId
x `compare` LitMeta TopLevelModuleName
g MetaId
y = (TopLevelModuleName
f, MetaId
x) (TopLevelModuleName, MetaId)
-> (TopLevelModuleName, MetaId) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` (TopLevelModuleName
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 TopLevelModuleName
m MetaId
x) = TopLevelModuleName -> MetaId -> Literal
LitMeta (KillRangeT TopLevelModuleName
forall a. KillRange a => KillRangeT a
killRange TopLevelModuleName
m) 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 TopLevelModuleName
m MetaId
_  ) = TopLevelModuleName -> ()
forall a. NFData a => a -> ()
rnf TopLevelModuleName
m