    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