{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module PlutusTx.Lift.Instances () where

import PlutusCore qualified as PLC

import PlutusCore.Data
import PlutusTx.Builtins
import PlutusTx.Builtins.Internal (BuiltinList)
import PlutusTx.Lift.Class


import PlutusIR
import PlutusIR.MkPir

import Data.ByteString qualified as BS
import Data.Kind qualified as GHC
import Data.Proxy
import Data.Text qualified as Text

import GHC.TypeLits (ErrorMessage (..), TypeError)

-- We do not use qualified import because the whole module contains off-chain code
import PlutusTx.Builtins.Class (FromBuiltin)
import Prelude as Haskell

-- Derived instances

-- This instance ensures that we can apply typeable type constructors to typeable arguments and get a typeable
-- type. We need the kind variable, so that partial application of type constructors works.
instance (Typeable uni (f :: * -> k), Typeable uni (a :: *)) => Typeable uni (f a) where
    typeRep :: Proxy (f a) -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy (f a)
_ = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (Type TyName uni () -> Type TyName uni () -> Type TyName uni ())
-> RTCompile uni fun (Type TyName uni ())
-> DefT
     Name uni fun () Quote (Type TyName uni () -> Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy f -> RTCompile uni fun (Type TyName uni ())
forall k (uni :: * -> *) (a :: k) fun.
Typeable uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRep (Proxy f
forall k (t :: k). Proxy t
Proxy :: Proxy f) DefT
  Name uni fun () Quote (Type TyName uni () -> Type TyName uni ())
-> RTCompile uni fun (Type TyName uni ())
-> RTCompile uni fun (Type TyName uni ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Proxy a -> RTCompile uni fun (Type TyName uni ())
forall k (uni :: * -> *) (a :: k) fun.
Typeable uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRep (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)

{- Note [Typeable instances for function types]
Surely there is an obvious 'Typeable' instance for 'a -> b': we just turn it directly
into a 'TyFun'!

However, if you write this instance, you find that it overlaps with the instance for applied
type constructors. For is not '(->) a' an applied type constructor?

Vexing. However, if we run with this, we can define a 'Typeable' instance for '(->)' directly.
What is this? Well, it's something like '\a b . a -> b' as a type function. Which is a rather
silly thing to write, but it does work.
-}
-- See Note [Typeable instances for function types]
instance Typeable uni (->) where
    typeRep :: Proxy (->) -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy (->)
_ = do
        TyName
a <- Quote TyName -> DefT Name uni fun () Quote TyName
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
PLC.liftQuote (Quote TyName -> DefT Name uni fun () Quote TyName)
-> Quote TyName -> DefT Name uni fun () Quote TyName
forall a b. (a -> b) -> a -> b
$ Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
PLC.freshTyName Text
"a"
        TyName
b <- Quote TyName -> DefT Name uni fun () Quote TyName
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
PLC.liftQuote (Quote TyName -> DefT Name uni fun () Quote TyName)
-> Quote TyName -> DefT Name uni fun () Quote TyName
forall a b. (a -> b) -> a -> b
$ Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
PLC.freshTyName Text
"b"
        let tvda :: TyVarDecl TyName ()
tvda = () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            tvdb :: TyVarDecl TyName ()
tvdb = () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        Type TyName uni () -> RTCompile uni fun (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> RTCompile uni fun (Type TyName uni ()))
-> Type TyName uni () -> RTCompile uni fun (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ [TyVarDecl TyName ()] -> Type TyName uni () -> Type TyName uni ()
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam [TyVarDecl TyName ()
tvda, TyVarDecl TyName ()
tvdb] (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () TyVarDecl TyName ()
tvda) (() -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () TyVarDecl TyName ()
tvdb)

-- Primitives

typeRepBuiltin
    :: forall (a :: GHC.Type) uni fun. uni `PLC.Includes` a
    => Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin :: Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (Proxy a
_ :: Proxy a) = Type TyName uni () -> RTCompile uni fun (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> RTCompile uni fun (Type TyName uni ()))
-> Type TyName uni () -> RTCompile uni fun (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> Type TyName uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @a ()

liftBuiltin
    :: forall a uni fun. uni `PLC.Includes` a
    => a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin :: a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin = Term TyName Name uni fun ()
-> RTCompile uni fun (Term TyName Name uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ()
 -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (a -> Term TyName Name uni fun ())
-> a
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> a -> Term TyName Name uni fun ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, Includes uni a) =>
ann -> a -> term ann
mkConstant ()

instance (TypeError ('Text "Int is not supported, use Integer instead"))
    => Typeable uni Int where
    typeRep :: Proxy Int -> RTCompile uni fun (Type TyName uni ())
typeRep = [Char] -> Proxy Int -> RTCompile uni fun (Type TyName uni ())
forall a. HasCallStack => [Char] -> a
Haskell.error [Char]
"unsupported"

instance (TypeError ('Text "Int is not supported, use Integer instead"))
    => Lift uni Int where
    lift :: Int -> RTCompile uni fun (Term TyName Name uni fun ())
lift = [Char] -> Int -> RTCompile uni fun (Term TyName Name uni fun ())
forall a. HasCallStack => [Char] -> a
Haskell.error [Char]
"unsupported"

instance uni `PLC.Includes` Integer => Typeable uni Integer where
    typeRep :: Proxy Integer -> RTCompile uni fun (Type TyName uni ())
typeRep = Proxy Integer -> RTCompile uni fun (Type TyName uni ())
forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin

instance uni `PLC.Includes` Integer => Lift uni Integer where
    lift :: Integer -> RTCompile uni fun (Term TyName Name uni fun ())
lift = Integer -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin

instance uni `PLC.Includes` BS.ByteString => Typeable uni BS.ByteString where
    typeRep :: Proxy ByteString -> RTCompile uni fun (Type TyName uni ())
typeRep = Proxy ByteString -> RTCompile uni fun (Type TyName uni ())
forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin

instance uni `PLC.Includes` BS.ByteString => Lift uni BS.ByteString where
    lift :: ByteString -> RTCompile uni fun (Term TyName Name uni fun ())
lift = ByteString -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin

instance uni `PLC.Includes` Data => Typeable uni BuiltinData where
    typeRep :: Proxy BuiltinData -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinData
_ = Proxy Data -> RTCompile uni fun (Type TyName uni ())
forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (Proxy Data
forall k (t :: k). Proxy t
Proxy @Data)

instance uni `PLC.Includes` Data => Lift uni BuiltinData where
    lift :: BuiltinData -> RTCompile uni fun (Term TyName Name uni fun ())
lift BuiltinData
d = Data -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (BuiltinData -> Data
builtinDataToData BuiltinData
d)

instance uni `PLC.Includes` BS.ByteString => Typeable uni BuiltinByteString where
    typeRep :: Proxy BuiltinByteString -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinByteString
_proxyPByteString = Proxy ByteString -> RTCompile uni fun (Type TyName uni ())
forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (Proxy ByteString
forall k (t :: k). Proxy t
Proxy @BS.ByteString)

instance uni `PLC.Includes` BS.ByteString => Lift uni BuiltinByteString where
    lift :: BuiltinByteString
-> RTCompile uni fun (Term TyName Name uni fun ())
lift BuiltinByteString
b = ByteString -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (ByteString -> RTCompile uni fun (Term TyName Name uni fun ()))
-> ByteString -> RTCompile uni fun (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ BuiltinByteString -> ByteString
forall arep a. FromBuiltin arep a => arep -> a
fromBuiltin BuiltinByteString
b

instance uni `PLC.Includes` Text.Text => Typeable uni BuiltinString where
    typeRep :: Proxy BuiltinString -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinString
_proxyPByteString = Proxy Text -> RTCompile uni fun (Type TyName uni ())
forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (Proxy Text
forall k (t :: k). Proxy t
Proxy @Text.Text)

instance uni `PLC.Includes` Text.Text => Lift uni BuiltinString where
    lift :: BuiltinString -> RTCompile uni fun (Term TyName Name uni fun ())
lift BuiltinString
b = Text -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Text -> RTCompile uni fun (Term TyName Name uni fun ()))
-> Text -> RTCompile uni fun (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ BuiltinString -> Text
forall arep a. FromBuiltin arep a => arep -> a
fromBuiltin BuiltinString
b

instance (FromBuiltin arep a, uni `PLC.Includes` [a]) => Lift uni (BuiltinList arep) where
    lift :: BuiltinList arep -> RTCompile uni fun (Term TyName Name uni fun ())
lift BuiltinList arep
b = [a] -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin ([a] -> RTCompile uni fun (Term TyName Name uni fun ()))
-> [a] -> RTCompile uni fun (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ BuiltinList arep -> [a]
forall arep a. FromBuiltin arep a => arep -> a
fromBuiltin BuiltinList arep
b

-- Standard types
-- These need to be in a separate file for TH staging reasons

makeLift ''Bool
makeLift ''Maybe
makeLift ''Either
makeLift ''[]
makeLift ''()
-- include a few tuple instances for convenience
makeLift ''(,)
makeLift ''(,,)
makeLift ''(,,,)
makeLift ''(,,,,)
makeLift ''Data