    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 Agda.Syntax.TopLevelModuleName.Boot (TopLevelModuleName')
    import Agda.Syntax.Position (Range)
    import Agda.Utils.Float ( doubleDenotEq, doubleDenotOrd )
    import Agda.Syntax.Common.Pretty

    type RLiteral = Ranged Literal
    data Literal
      = LitNat    !Integer
      | LitWord64 !Word64
      | LitFloat  !Double
      | LitString !Text
      | LitChar   !Char
      | LitQName  !QName
      | LitMeta   !(TopLevelModuleName' Range) !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)     = Doc -> Doc
    hlNumber (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Integer -> Doc
    forall a. Pretty a => a -> Doc
    pretty Integer
    n
        pretty (LitWord64 Word64
    n)  = Doc -> Doc
    hlNumber (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Doc
    forall a. Pretty a => a -> Doc
    pretty Word64
    n
        pretty (LitFloat Double
    d)   = Doc -> Doc
    hlNumber (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Double -> Doc
    forall a. Pretty a => a -> Doc
    pretty Double
    d
        pretty (LitString Text
    s)  = Doc -> Doc
    hlString (Doc -> Doc) -> (String -> Doc) -> String -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Text -> ShowS
    showText Text
    s String
    ""
        pretty (LitChar Char
    c)    = Doc -> Doc
    hlString (Doc -> Doc) -> (String -> Doc) -> String -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Doc
    forall a. String -> Doc a
    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' Range
    _ 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' Range
    f MetaId
    x == LitMeta TopLevelModuleName' Range
    g MetaId
    y = (TopLevelModuleName' Range
    f, MetaId
    x) (TopLevelModuleName' Range, MetaId)
    -> (TopLevelModuleName' Range, MetaId) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (TopLevelModuleName' Range
    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' Range
    f MetaId
    x `compare` LitMeta TopLevelModuleName' Range
    g MetaId
    y = (TopLevelModuleName' Range
    f, MetaId
    x) (TopLevelModuleName' Range, MetaId)
    -> (TopLevelModuleName' Range, MetaId) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` (TopLevelModuleName' Range
    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 t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> Literal
    LitQName QName
    x
      killRange (LitMeta TopLevelModuleName' Range
    m MetaId
    x) = TopLevelModuleName' Range -> MetaId -> Literal
    LitMeta (KillRangeT (TopLevelModuleName' Range)
    forall a. KillRange a => KillRangeT a
    killRange TopLevelModuleName' Range
    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' Range
    m MetaId
    _  ) = TopLevelModuleName' Range -> ()
    forall a. NFData a => a -> ()
    rnf TopLevelModuleName' Range
    m