{-|
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), 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 :: 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 (Proxy a
forall k (t :: k). Proxy t
Proxy @a))

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

instance TermLiteral String where
  termToData :: 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 :: 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 (collectArgs -> (_, [ Left (Literal (ByteArrayLiteral (BA.ByteArray ba)))
                                 , Left (Literal (IntLiteral off))
                                 , Left (Literal (IntLiteral len))])) =
    Right (Text.Text (Text.ByteArray ba) (fromInteger off) (fromInteger 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 :: 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 a. (Num a, KnownNat n) => a
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 :: 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 :: 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 :: Term -> Either Term Integer
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 :: 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 :: Term -> Either Term Natural
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 Natural
forall a b. a -> Either a b
Left Term
t
    | Bool
otherwise = Natural -> Either Term Natural
forall a b. b -> Either a b
Right (Integer -> Natural
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))])) =
    Natural -> Either Term Natural
forall a b. b -> Either a b
Right (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n)
  termToData Term
t = Term -> Either Term Natural
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 :: Term -> Either Term (SNat n)
termToData = \case
    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 :: 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
a' <- Term -> Either Term a
forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
termToData Term
a
    b
b' <- Term -> Either Term b
forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
termToData Term
b
    (a, b) -> Either Term (a, b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (a
a', b
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 (Proxy a
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 (Proxy b
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 :: Term -> Either Term (Vec n a)
termToData Term
term = do
    Maybe (Vec n a)
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 Maybe (Vec n a)
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 :: forall a. Name a -> Text
nameOcc :: 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
                a
c1 <- Term -> Either Term a
forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
termToData @a Term
c0
                [a]
cs1 <- Term -> Either Term [a]
go Term
cs0
                [a] -> Either Term [a]
forall a b. b -> Either a b
Right (a
c1a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
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 (KnownNat n => Integer
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 (Proxy a
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 :: Term -> Either String a
termToDataError Term
term = (Term -> String) -> (a -> a) -> Either Term a -> Either String a
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 (Proxy a
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}
  |]