{-|
Copyright   :  (C) 2019, Myrtle Software Ltd
License     :  BSD2 (see the file LICENSE)
Maintainer  :  Christiaan Baaij <christiaan.baaij@gmail.com>

Tools to convert a 'Term' into its "real" representation
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}

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

module Clash.Core.TermLiteral
  ( TermLiteral
  , termToData
  , termToDataError
  , uncheckedTermToData
  ) 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.Typeable                   (Typeable, typeRep)
import           GHC.Natural
import           GHC.Stack

import           Clash.Core.Term                 (Term(Literal), collectArgs)
import           Clash.Core.Literal
import           Clash.Core.Pretty               (showPpr)
import qualified Clash.Util.Interpolate          as I
import qualified Clash.Verification.Internal     as Cv

import           Clash.Core.TermLiteral.TH

-- | Tools to deal with literals encoded as a "Term".
class Typeable a => 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.

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
t = String -> Text
Text.pack (String -> Text) -> Either Term String -> Either Term Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Either Term String
forall a. (TermLiteral a, HasCallStack) => Term -> Either Term a
termToData 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 (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 (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

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

instance TermLiteral a => TermLiteral (Maybe a) where
  termToData :: Term -> Either Term (Maybe a)
termToData = $(deriveTermToData ''Maybe)

instance TermLiteral Bool where
  termToData :: Term -> Either Term Bool
termToData = $(deriveTermToData ''Bool)

instance TermLiteral Cv.RenderAs where
  termToData :: Term -> Either Term RenderAs
termToData = $(deriveTermToData ''Cv.RenderAs)

instance TermLiteral a => TermLiteral (Cv.Assertion' a) where
  termToData :: Term -> Either Term (Assertion' a)
termToData = $(deriveTermToData ''Cv.Assertion')

instance TermLiteral a => TermLiteral (Cv.Property' a) where
  termToData :: Term -> Either Term (Property' a)
termToData = $(deriveTermToData ''Cv.Property')

-- | 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 p. PrettyPrec p => p -> 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
  typ :: String
typ = TypeRep -> String
forall a. Show a => a -> String
show (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))

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

      #{showPpr failedTerm}

    In the full term:

      #{showPpr term}

    While trying to interpret something to type:

      #{typ}
  |]

-- | Same as 'termToData', but errors hard if it can't translate a given term
-- to data.
uncheckedTermToData :: TermLiteral a => Term -> a
uncheckedTermToData :: Term -> a
uncheckedTermToData = (String -> a) -> (a -> a) -> Either String a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> a
forall a. HasCallStack => String -> a
error a -> a
forall a. a -> a
id (Either String a -> a) -> (Term -> Either String a) -> Term -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Either String a
forall a. TermLiteral a => Term -> Either String a
termToDataError