{-# 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
Constr
DataType
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 -> Constr
Literal -> DataType
(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 p :: Int
p l :: Literal
l = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Literal
l of
LitNat _ n :: Integer
n -> String -> Integer -> ShowS
forall a. Show a => String -> a -> ShowS
sh "LitNat _" Integer
n
LitWord64 _ n :: Word64
n -> String -> Word64 -> ShowS
forall a. Show a => String -> a -> ShowS
sh "LitWord64 _" Word64
n
LitFloat _ x :: Double
x -> String -> Double -> ShowS
forall a. Show a => String -> a -> ShowS
sh "LitFloat _" Double
x
LitString _ s :: String
s -> String -> String -> ShowS
forall a. Show a => String -> a -> ShowS
sh "LitString _" String
s
LitChar _ c :: Char
c -> String -> Char -> ShowS
forall a. Show a => String -> a -> ShowS
sh "LitChar _" Char
c
LitQName _ q :: QName
q -> String -> QName -> ShowS
forall a. Show a => String -> a -> ShowS
sh "LitQName _" QName
q
LitMeta _ _ x :: MetaId
x -> String -> MetaId -> ShowS
forall a. Show a => String -> a -> ShowS
sh "LitMeta _ _" MetaId
x
where
sh :: Show a => String -> a -> ShowS
sh :: String -> a -> ShowS
sh c :: String
c x :: a
x = String -> ShowS
showString (String
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ") 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 _ n :: 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 _ n :: 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 _ d :: 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 _ s :: String
s) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString' String
s ""
pretty (LitChar _ c :: Char
c) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> ShowS
showChar' Char
c "'"
pretty (LitQName _ x :: QName
x) = QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
pretty (LitMeta _ _ x :: MetaId
x) = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x
showString' :: String -> ShowS
showString' :: String -> ShowS
showString' s :: 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 "\"" ] [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 "\"" ]
showChar' :: Char -> ShowS
showChar' :: Char -> ShowS
showChar' '"' = String -> ShowS
showString "\\\""
showChar' c :: Char
c
| Char -> Bool
escapeMe Char
c = Char -> ShowS
showLitChar Char
c
| Bool
otherwise = String -> ShowS
showString [Char
c]
where
escapeMe :: Char -> Bool
escapeMe c :: 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
== '\\'
instance Eq Literal where
LitNat _ n :: Integer
n == :: Literal -> Literal -> Bool
== LitNat _ m :: Integer
m = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
m
LitWord64 _ n :: Word64
n == LitWord64 _ m :: Word64
m = Word64
n Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
m
LitFloat _ x :: Double
x == LitFloat _ y :: 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 _ s :: String
s == LitString _ t :: String
t = String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
t
LitChar _ c :: Char
c == LitChar _ d :: Char
d = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
d
LitQName _ x :: QName
x == LitQName _ y :: QName
y = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
LitMeta _ f :: AbsolutePath
f x :: MetaId
x == LitMeta _ g :: AbsolutePath
g y :: MetaId
y = (AbsolutePath
f, MetaId
x) (AbsolutePath, MetaId) -> (AbsolutePath, MetaId) -> Bool
forall a. Eq a => a -> a -> Bool
== (AbsolutePath
f, MetaId
y)
_ == _ = Bool
False
instance Ord Literal where
LitNat _ n :: Integer
n compare :: Literal -> Literal -> Ordering
`compare` LitNat _ m :: Integer
m = Integer
n Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Integer
m
LitWord64 _ n :: Word64
n `compare` LitWord64 _ m :: Word64
m = Word64
n Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Word64
m
LitFloat _ x :: Double
x `compare` LitFloat _ y :: Double
y = Double -> Double -> Ordering
compareFloat Double
x Double
y
LitString _ s :: String
s `compare` LitString _ t :: String
t = String
s String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` String
t
LitChar _ c :: Char
c `compare` LitChar _ d :: Char
d = Char
c Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Char
d
LitQName _ x :: QName
x `compare` LitQName _ y :: QName
y = QName
x QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QName
y
LitMeta _ f :: AbsolutePath
f x :: MetaId
x `compare` LitMeta _ g :: AbsolutePath
g y :: 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{} _ = Ordering
LT
compare _ LitNat{} = Ordering
GT
compare LitWord64{} _ = Ordering
LT
compare _ LitWord64{} = Ordering
GT
compare LitFloat{} _ = Ordering
LT
compare _ LitFloat{} = Ordering
GT
compare LitString{} _ = Ordering
LT
compare _ LitString{} = Ordering
GT
compare LitChar{} _ = Ordering
LT
compare _ LitChar{} = Ordering
GT
compare LitQName{} _ = Ordering
LT
compare _ LitQName{} = Ordering
GT
compareFloat :: Double -> Double -> Ordering
compareFloat :: Double -> Double -> Ordering
compareFloat x :: Double
x y :: 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 z :: a
z = a
z a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< 0 Bool -> Bool -> Bool
&& a -> Bool
forall a. RealFloat a => a -> Bool
isInfinite a
z
instance HasRange Literal where
getRange :: Literal -> Range
getRange (LitNat r :: Range
r _) = Range
r
getRange (LitWord64 r :: Range
r _) = Range
r
getRange (LitFloat r :: Range
r _) = Range
r
getRange (LitString r :: Range
r _) = Range
r
getRange (LitChar r :: Range
r _) = Range
r
getRange (LitQName r :: Range
r _) = Range
r
getRange (LitMeta r :: Range
r _ _) = Range
r
instance SetRange Literal where
setRange :: Range -> Literal -> Literal
setRange r :: Range
r (LitNat _ x :: Integer
x) = Range -> Integer -> Literal
LitNat Range
r Integer
x
setRange r :: Range
r (LitWord64 _ x :: Word64
x) = Range -> Word64 -> Literal
LitWord64 Range
r Word64
x
setRange r :: Range
r (LitFloat _ x :: Double
x) = Range -> Double -> Literal
LitFloat Range
r Double
x
setRange r :: Range
r (LitString _ x :: String
x) = Range -> String -> Literal
LitString Range
r String
x
setRange r :: Range
r (LitChar _ x :: Char
x) = Range -> Char -> Literal
LitChar Range
r Char
x
setRange r :: Range
r (LitQName _ x :: QName
x) = Range -> QName -> Literal
LitQName Range
r QName
x
setRange r :: Range
r (LitMeta _ f :: AbsolutePath
f x :: MetaId
x) = Range -> AbsolutePath -> MetaId -> Literal
LitMeta Range
r AbsolutePath
f MetaId
x
instance KillRange Literal where
killRange :: Literal -> Literal
killRange (LitNat r :: Range
r x :: Integer
x) = Range -> Integer -> Literal
LitNat (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Integer
x
killRange (LitWord64 r :: Range
r x :: Word64
x) = Range -> Word64 -> Literal
LitWord64 (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Word64
x
killRange (LitFloat r :: Range
r x :: Double
x) = Range -> Double -> Literal
LitFloat (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Double
x
killRange (LitString r :: Range
r x :: String
x) = Range -> String -> Literal
LitString (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) String
x
killRange (LitChar r :: Range
r x :: Char
x) = Range -> Char -> Literal
LitChar (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Char
x
killRange (LitQName r :: Range
r x :: 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 r :: Range
r f :: AbsolutePath
f x :: MetaId
x) = Range -> AbsolutePath -> MetaId -> Literal
LitMeta (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) AbsolutePath
f MetaId
x
instance NFData Literal where
rnf :: Literal -> ()
rnf (LitNat _ _) = ()
rnf (LitWord64 _ _) = ()
rnf (LitFloat _ _) = ()
rnf (LitString _ a :: String
a) = String -> ()
forall a. NFData a => a -> ()
rnf String
a
rnf (LitChar _ _) = ()
rnf (LitQName _ a :: QName
a) = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
rnf (LitMeta _ _ x :: MetaId
x) = MetaId -> ()
forall a. NFData a => a -> ()
rnf MetaId
x