-- editorconfig-checker-disable-file
{-# 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 :: forall fun. Proxy (f a) -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy (f a)
_ = forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (uni :: * -> *) (a :: k) fun.
Typeable uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy f) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k (uni :: * -> *) (a :: k) fun.
Typeable uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRep (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 :: forall fun. Proxy (->) -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy (->)
_ = do
        TyName
a <- forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
PLC.liftQuote forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadQuote m => Text -> m TyName
PLC.freshTyName Text
"a"
        TyName
b <- forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
PLC.liftQuote forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadQuote m => Text -> m TyName
PLC.freshTyName Text
"b"
        let tvda :: TyVarDecl TyName ()
tvda = forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a (forall ann. ann -> Kind ann
Type ())
            tvdb :: TyVarDecl TyName ()
tvdb = forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
b (forall ann. ann -> Kind ann
Type ())
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam [TyVarDecl TyName ()
tvda, TyVarDecl TyName ()
tvdb] forall a b. (a -> b) -> a -> b
$ forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () TyVarDecl TyName ()
tvda) (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 :: forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (Proxy a
_ :: Proxy a) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 :: forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall fun. Proxy Int -> RTCompile uni fun (Type TyName uni ())
typeRep = forall a. HasCallStack => [Char] -> a
Haskell.error [Char]
"unsupported"

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

instance uni `PLC.Includes` Integer => Typeable uni Integer where
    typeRep :: forall fun. Proxy Integer -> RTCompile uni fun (Type TyName uni ())
typeRep = 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 :: forall fun.
Integer -> RTCompile uni fun (Term TyName Name uni fun ())
lift = 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 :: forall fun.
Proxy ByteString -> RTCompile uni fun (Type TyName uni ())
typeRep = 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 :: forall fun.
ByteString -> RTCompile uni fun (Term TyName Name uni fun ())
lift = 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 :: forall fun.
Proxy BuiltinData -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinData
_ = forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall {k} (t :: k). Proxy t
Proxy @Data)

instance uni `PLC.Includes` Data => Lift uni BuiltinData where
    lift :: forall fun.
BuiltinData -> RTCompile uni fun (Term TyName Name uni fun ())
lift BuiltinData
d = 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 :: forall fun.
Proxy BuiltinByteString -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinByteString
_proxyPByteString = forall a (uni :: * -> *) fun.
Includes uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall {k} (t :: k). Proxy t
Proxy @BS.ByteString)

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

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

instance uni `PLC.Includes` Text.Text => Lift uni BuiltinString where
    lift :: forall fun.
BuiltinString -> RTCompile uni fun (Term TyName Name uni fun ())
lift BuiltinString
b = forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin forall a b. (a -> b) -> a -> b
$ 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 :: forall fun.
BuiltinList arep -> RTCompile uni fun (Term TyName Name uni fun ())
lift BuiltinList arep
b = forall a (uni :: * -> *) fun.
Includes uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin forall a b. (a -> b) -> a -> b
$ 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