    {-|
    Copyright   :  (C) 2019, Myrtle Software Ltd,
                       2021, QBayLogic B.V.
                       2022, Google Inc.
    License     :  BSD2 (see the file LICENSE)
    Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>

    Tools to convert a 'Term' into its "real" representation
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE QuasiQuotes #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE NamedFieldPuns #-}

    --{-# OPTIONS_GHC -ddump-splices #-}

    module Clash.Core.TermLiteral
      ( TermLiteral
      , showsTypePrec
      , showType
      , termToData
      , termToDataError
      , deriveTermLiteral
      ) where

    import           Data.Bifunctor                  (bimap)
    import           Data.Either                     (lefts)
    import           Data.Proxy                      (Proxy(..))
    import           Data.Text                       (Text)
    import qualified Data.Text                       as Text
    import           Data.Text.Extra                 (showt)
    #if MIN_VERSION_ghc(9,4,0)
    import qualified Data.Text.Internal              as Text
    import qualified Data.Text.Array                 as Text
    import qualified Data.Primitive.ByteArray        as BA
    #endif
    import           Data.Typeable                   (Typeable, typeRep)
    import           GHC.Natural
    import           GHC.Stack
    import           GHC.TypeNats (KnownNat)
    import           Text.Show.Pretty                (ppShow)

    import           Clash.Annotations.SynthesisAttributes (Attr)
    import           Clash.Core.DataCon              (DataCon(..))
    import           Clash.Core.Literal
    import           Clash.Core.Name                 (Name(..))
    import           Clash.Core.Pretty               (showPpr)
    import           Clash.Core.Term                 (Term(Literal, Data, Tick), collectArgs)
    import           Clash.Promoted.Nat
    import           Clash.Promoted.Nat.Unsafe
    import           Clash.Sized.Index               (Index)
    import           Clash.Sized.Vector              (Vec (Nil, Cons), fromList)
    import qualified Clash.Util.Interpolate          as I
    import qualified Clash.Verification.Internal     as Cv

    import           Clash.Core.TermLiteral.TH

    -- | Pretty print type @a@
    showType :: TermLiteral a => Proxy a -> String
    showType :: forall a. TermLiteral a => Proxy a -> String
    showType Proxy a
    proxy = Int -> Proxy a -> ShowS
    forall a. TermLiteral a => Int -> Proxy a -> ShowS
    showsTypePrec Int
    0 Proxy a
    proxy String
    ""

    -- | Tools to deal with literals encoded as a 'Term'.
    class TermLiteral a where
      -- | Convert 'Term' to the constant it represents. Will return an error if
      -- (one of the subterms) fail to translate.
      termToData
        :: HasCallStack
        => Term
        -- ^ Term to convert
        -> Either Term a
        -- ^ 'Left' indicates a failure, containing the (sub)term that failed to
        -- translate. 'Right' indicates a success.

      -- | Pretty print the type of a term (for error messages). Its default implementation
      -- uses 'Typeable' to print the type. Note that this method is there to allow
      -- an instance for 'SNat' to exist (and other GADTs imposing
      -- t'GHC.TypeNats.KnownNat'). Without it, GHC would ask for a @KnownNat@
      -- constraint on the instance, which would defeat the purpose of it.
      showsTypePrec ::
        -- | The operator precedence of the enclosing context (a number from @0@ to
        -- @11@). Function application has precedence @10@. Used to determine whether
        -- the result should be wrapped in parentheses.
        Int ->
        -- | Proxy for a term whose type needs to be pretty printed
        Proxy a ->
        ShowS

      default showsTypePrec :: Typeable a => Int -> Proxy a -> ShowS
      showsTypePrec Int
    n Proxy a
    _ = Int -> TypeRep -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    n (Proxy a -> TypeRep
    forall {k} (proxy :: k -> Type) (a :: k).
    Typeable a =>
    proxy a -> TypeRep
    typeRep (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a))

    instance TermLiteral Term where
      termToData :: HasCallStack => Term -> Either Term Term
    termToData = Term -> Either Term Term
    forall a. a -> Either Term a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure

    instance TermLiteral String where
      termToData :: HasCallStack => Term -> Either Term String
    termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Left (Literal (StringLiteral String
    s))])) = String -> Either Term String
    forall a b. b -> Either a b
    Right String
    s
      termToData Term
    t = Term -> Either Term String
    forall a b. a -> Either a b
    Left Term
    t

    instance TermLiteral Text where
      termToData :: HasCallStack => Term -> Either Term Text
    termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Left (Literal (StringLiteral String
    s))])) =
        Text -> Either Term Text
    forall a b. b -> Either a b
    Right (String -> Text
    Text.pack String
    s)
    #if MIN_VERSION_ghc(9,4,0)
      termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [ Left (Literal (ByteArrayLiteral (BA.ByteArray ByteArray#
    ba)))
                                     , Left (Literal (IntLiteral Integer
    off))
                                     , Left (Literal (IntLiteral Integer
    len))])) =
        Text -> Either Term Text
    forall a b. b -> Either a b
    Right (ByteArray -> Int -> Int -> Text
    Text.Text (ByteArray# -> ByteArray
    Text.ByteArray ByteArray#
    ba) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    off) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    len))
    #endif
      termToData Term
    t = Term -> Either Term Text
    forall a b. a -> Either a b
    Left Term
    t

    instance KnownNat n => TermLiteral (Index n) where
      termToData :: HasCallStack => Term -> Either Term (Index n)
    termToData t :: Term
    t@(Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Either Term Type
    _, Either Term Type
    _, Left (Literal (IntegerLiteral Integer
    n))]))
        | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 = Term -> Either Term (Index n)
    forall a b. a -> Either a b
    Left Term
    t
        | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= forall (n :: Nat) a. (Num a, KnownNat n) => a
    natToNum @n = Term -> Either Term (Index n)
    forall a b. a -> Either a b
    Left Term
    t
        | Bool
    otherwise = Index n -> Either Term (Index n)
    forall a b. b -> Either a b
    Right (Integer -> Index n
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)
      termToData Term
    t = Term -> Either Term (Index n)
    forall a b. a -> Either a b
    Left Term
    t

    instance TermLiteral Int where
      termToData :: HasCallStack => Term -> Either Term Int
    termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Left (Literal (IntLiteral Integer
    n))])) =
        Int -> Either Term Int
    forall a b. b -> Either a b
    Right (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)
      termToData Term
    t = Term -> Either Term Int
    forall a b. a -> Either a b
    Left Term
    t

    instance TermLiteral Word where
      termToData :: HasCallStack => Term -> Either Term Word
    termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Left (Literal (WordLiteral Integer
    n))])) =
        Word -> Either Term Word
    forall a b. b -> Either a b
    Right (Integer -> Word
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)
      termToData Term
    t = Term -> Either Term Word
    forall a b. a -> Either a b
    Left Term
    t

    instance TermLiteral Integer where
      termToData :: HasCallStack => Term -> Either Term Integer
    termToData (Tick TickInfo
    _ Term
    e) = Term -> Either Term Integer
    forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
    termToData Term
    e
      termToData (Literal (IntegerLiteral Integer
    n)) = Integer -> Either Term Integer
    forall a b. b -> Either a b
    Right Integer
    n
      termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Left (Literal (IntegerLiteral Integer
    n))])) = Integer -> Either Term Integer
    forall a b. b -> Either a b
    Right Integer
    n
      termToData Term
    t = Term -> Either Term Integer
    forall a b. a -> Either a b
    Left Term
    t

    instance TermLiteral Char where
      termToData :: HasCallStack => Term -> Either Term Char
    termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Left (Literal (CharLiteral Char
    c))])) = Char -> Either Term Char
    forall a b. b -> Either a b
    Right Char
    c
      termToData Term
    t = Term -> Either Term Char
    forall a b. a -> Either a b
    Left Term
    t

    instance TermLiteral Natural where
      termToData :: HasCallStack => Term -> Either Term Nat
    termToData (Tick TickInfo
    _ Term
    e) = Term -> Either Term Nat
    forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
    termToData Term
    e
      termToData t :: Term
    t@(Literal (NaturalLiteral Integer
    n))
        | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 = Term -> Either Term Nat
    forall a b. a -> Either a b
    Left Term
    t
        | Bool
    otherwise = Nat -> Either Term Nat
    forall a b. b -> Either a b
    Right (Integer -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    n)
      termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Left (Literal (NaturalLiteral Integer
    n))])) =
        Nat -> Either Term Nat
    forall a b. b -> Either a b
    Right (Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)
      termToData Term
    t = Term -> Either Term Nat
    forall a b. a -> Either a b
    Left Term
    t

    -- | Unsafe warning: If you use this instance in a monomorphic context (e.g.,
    -- @TermLiteral (SNat 5)@), you need to make very sure that the term corresponds
    -- to the literal. If you don't, there will be a mismatch between type level
    -- variables and the proof carried in 'SNat's 'KnownNat'. Typical usage of this
    -- instance will therefore leave the /n/ polymorphic.
    --
    instance TermLiteral (SNat n) where
      termToData :: HasCallStack => Term -> Either Term (SNat n)
    termToData = \case
        Tick TickInfo
    _ Term
    e                   -> Term -> Either Term (SNat n)
    forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
    termToData Term
    e
        Literal (NaturalLiteral Integer
    n) -> SNat n -> Either Term (SNat n)
    forall a b. b -> Either a b
    Right (Integer -> SNat n
    forall (k :: Nat). Integer -> SNat k
    unsafeSNat Integer
    n)
        Term
    t                          -> Term -> Either Term (SNat n)
    forall a b. a -> Either a b
    Left Term
    t

      showsTypePrec :: Int -> Proxy (SNat n) -> ShowS
    showsTypePrec Int
    n Proxy (SNat n)
    _
        -- We don't know the literal /n/ at this point. However, we can't simply put
        -- and /n/ here either, as it might collide with other type variables. To
        -- prevent confusion, we put an underscore. This is obviously "wrong", but
        -- good enough for error messages - the main purpose of this function.
        = Bool -> ShowS -> ShowS
    showParen (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String -> ShowS
    showString String
    "SNat _"

    instance (TermLiteral a, TermLiteral b) => TermLiteral (a, b) where
      termToData :: HasCallStack => Term -> Either Term (a, b)
    termToData (Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    _, [Either Term Type] -> [Term]
    forall a b. [Either a b] -> [a]
    lefts -> [Term
    a, Term
    b])) = do
        a' <- Term -> Either Term a
    forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
    termToData Term
    a
        b' <- termToData b
        pure (a', b')
      termToData Term
    t = Term -> Either Term (a, b)
    forall a b. a -> Either a b
    Left Term
    t

      showsTypePrec :: Int -> Proxy (a, b) -> ShowS
    showsTypePrec Int
    _ Proxy (a, b)
    _ =
        -- XXX: We pass in 11 here, but should really be passing in 0. We never want
        --      any parentheses for fields in tuples. However, Typeable's show
        --      implementation does put parentheses around tuple fields - so we
        --      replicate that behavior here for ease of testing.
          Char -> ShowS
    showChar Char
    '('
        ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Proxy a -> ShowS
    forall a. TermLiteral a => Int -> Proxy a -> ShowS
    showsTypePrec Int
    11 (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)
        ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    ","
        ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Proxy b -> ShowS
    forall a. TermLiteral a => Int -> Proxy a -> ShowS
    showsTypePrec Int
    11 (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b)
        ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ')'

    instance (TermLiteral a, KnownNat n) => TermLiteral (Vec n a) where
      termToData :: HasCallStack => Term -> Either Term (Vec n a)
    termToData Term
    term = do
        res <- [a] -> Maybe (Vec n a)
    forall (n :: Nat) a. KnownNat n => [a] -> Maybe (Vec n a)
    fromList ([a] -> Maybe (Vec n a))
    -> Either Term [a] -> Either Term (Maybe (Vec n a))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> Either Term [a]
    go Term
    term
        -- Check whether length of list constructed in 'go' corresponds to the
        -- @KnownNat n@ we've been given
        case res of
          Maybe (Vec n a)
    Nothing -> Term -> Either Term (Vec n a)
    forall a b. a -> Either a b
    Left Term
    term
          Just Vec n a
    v -> Vec n a -> Either Term (Vec n a)
    forall a b. b -> Either a b
    Right Vec n a
    v
       where
        -- Construct a list from given term
        go :: Term -> Either Term [a]
    go t :: Term
    t@(Term -> (Term, [Either Term Type])
    collectArgs -> (Term
    constr, [Either Term Type]
    args)) =
          case Term
    constr of
            Data (MkData{dcName :: DataCon -> DcName
    dcName=Name{Text
    nameOcc :: Text
    nameOcc :: forall a. Name a -> Text
    nameOcc}})
              | Text
    nameOcc Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> Text
    forall a. Show a => a -> Text
    showt 'Nil -> [a] -> Either Term [a]
    forall a b. b -> Either a b
    Right []
              | Text
    nameOcc Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> Text
    forall a. Show a => a -> Text
    showt 'Cons ->
                case [Either Term Type] -> [Term]
    forall a b. [Either a b] -> [a]
    lefts [Either Term Type]
    args of
                  [Term
    _gadtProof, Term
    c0, Term
    cs0] -> do
                    c1 <- forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
    termToData @a Term
    c0
                    cs1 <- go cs0
                    Right (c1:cs1)
                  [Term]
    _ -> Term -> Either Term [a]
    forall a b. a -> Either a b
    Left Term
    t
            Term
    _ -> Term -> Either Term [a]
    forall a b. a -> Either a b
    Left Term
    t

      showsTypePrec :: Int -> Proxy (Vec n a) -> ShowS
    showsTypePrec Int
    n Proxy (Vec n a)
    _ =
        Bool -> ShowS -> ShowS
    showParen (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
            String -> ShowS
    showString String
    "Vec"
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ' '
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString (Integer -> String
    forall a. Show a => a -> String
    show (forall (n :: Nat). KnownNat n => Integer
    natToInteger @n))
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ' '
          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Proxy a -> ShowS
    forall a. TermLiteral a => Int -> Proxy a -> ShowS
    showsTypePrec Int
    11 (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)

    deriveTermLiteral ''Bool
    deriveTermLiteral ''Maybe
    deriveTermLiteral ''Either
    deriveTermLiteral ''Cv.RenderAs
    deriveTermLiteral ''Cv.Assertion'
    deriveTermLiteral ''Cv.Property'
    deriveTermLiteral ''Attr

    -- | Same as 'termToData', but returns printable error message if it couldn't
    -- translate a term.
    termToDataError :: forall a. TermLiteral a => Term -> Either String a
    termToDataError :: forall a. TermLiteral a => Term -> Either String a
    termToDataError Term
    term = (Term -> String) -> (a -> a) -> Either Term a -> Either String a
    forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
    forall (p :: Type -> Type -> Type) a b c d.
    Bifunctor p =>
    (a -> b) -> (c -> d) -> p a c -> p b d
    bimap Term -> String
    forall {a}. (PrettyPrec a, Show a) => a -> String
    err a -> a
    forall a. a -> a
    id (Term -> Either Term a
    forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
    termToData Term
    term)
     where
      -- XXX: If we put this construct in the quasiquoted part, it yields a parse
      --      error on some platforms. This is likely related to some older version
      --      of dependencies. In the interested of time yours truly just moved it
      --      outside of the quasiquoter.
      shownType :: String
    shownType = Proxy a -> String
    forall a. TermLiteral a => Proxy a -> String
    showType (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)

      err :: a -> String
    err a
    failedTerm = [I.i|
        Failed to translate term to literal. Term that failed to translate:

          #{showPpr failedTerm}

        In its non-pretty-printed form:

          #{ppShow failedTerm}

        In the full term:

          #{showPpr term}

        While trying to interpret something to type:

          #{shownType}
      |]