-- editorconfig-checker-disable-file
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module PlutusTx.Lift.Class
  ( Typeable (..)
  , Lift (..)
  , RTCompile
  ) where

import PlutusIR
import PlutusIR.Compiler.Definitions

import PlutusCore qualified as PLC
import PlutusCore.Crypto.BLS12_381.G1 (Element)
import PlutusCore.Crypto.BLS12_381.G2 (Element)
import PlutusCore.Crypto.BLS12_381.Pairing (MlResult)
import PlutusCore.Data
import PlutusCore.Quote
import PlutusCore.Value
import PlutusIR.MkPir
import PlutusTx.Builtins
import PlutusTx.Builtins.HasBuiltin (FromBuiltin, HasFromBuiltin)
import PlutusTx.Builtins.Internal
  ( BuiltinInteger
  , BuiltinList
  , BuiltinPair
  , BuiltinUnit
  , BuiltinValue
  )

import Language.Haskell.TH qualified as TH hiding (newName)

import Data.ByteString qualified as BS
import Data.Kind qualified as GHC
import Data.Proxy
import Data.Text qualified as T
import Data.Vector.Strict qualified as Strict
import GHC.TypeLits (ErrorMessage (..), TypeError)

-- We do not use qualified import because the whole module contains off-chain code
import Prelude as Haskell

{- Note [Compiling at TH time and runtime]
We want to reuse PIR's machinery for defining datatypes. However, one cannot
get a PLC Type consisting of the compiled PIR type, because the compilation of the
definitions is done by making a *term*.

So we use the abstract support for handling definitions in PIR, MonadDefs. Typeable
then has `typeRep :: Proxy a -> RTCompile uni fun (Type TyName uni ())`,
which says that you can get the type in some compilation monad (which
you will later have to discharge yourself).

This means that the TH expressions we are generating are not for `Type`s directly, but rather
for monadic expressions that will, at runtime, compute types. We are effectively generating
a specialized compiler.

We thus have two pieces of compilation going on here:
- At TH time, we reify information about datatypes, and construct specialized compilation expressions
  for the various parts.
- At runtime, we actually run these and create definitions etc.

The interplay between the parts happening at TH time and the parts happening at runtime is somewhat
awkward, but I couldn't think of a better way of doing it.

A particularly awkward feature is that the typeclass constraints required by the code in each
instance are going to be different, and so we can't use reusable functions, instead we need to
inline all the definitions so that the overall expression can have the right constraints inferred.
-}

type RTCompile uni fun = DefT TH.Name uni fun () Quote

{-| Class for types which have a corresponding Plutus IR type. Instances should always be derived,
do not write your own instance! -}
class Typeable uni (a :: k) where
  -- | Get the Plutus IR type corresponding to this type.
  typeRep :: Proxy a -> RTCompile uni fun (Type TyName uni ())

{-| Class for types which can be lifted into Plutus IR. Instances should be derived, do not write
your own instance! -}
class Lift uni a where
  -- | Get a Plutus IR term corresponding to the given value.
  lift :: a -> RTCompile uni fun (Term TyName Name uni fun ())

-- 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 :: GHC.Type -> k), Typeable uni (a :: GHC.Type)) => Typeable uni (f a) where
  typeRep :: forall fun. 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 ())
-> DefT Name uni fun () Quote (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 -> DefT Name uni fun () Quote (Type TyName uni ())
forall fun. 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 ())
-> DefT Name uni fun () Quote (Type TyName uni ())
-> DefT Name uni fun () Quote (Type TyName uni ())
forall a b.
DefT Name uni fun () Quote (a -> b)
-> DefT Name uni fun () Quote a -> DefT Name uni fun () Quote b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Proxy a -> DefT Name uni fun () Quote (Type TyName uni ())
forall fun. 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 :: forall fun. Proxy (->) -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy (->)
_ = do
    TyName
a <- Quote TyName -> DefT Name uni fun () Quote TyName
forall a. Quote a -> DefT Name uni fun () Quote a
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 a. Quote a -> DefT Name uni fun () Quote a
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 a. a -> DefT Name uni fun () Quote a
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 k (a :: k) uni fun
   . uni `PLC.HasTypeLevel` a
  => Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin :: forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (Proxy a
_ :: Proxy a) = Type TyName uni ()
-> DefT Name uni fun () Quote (Type TyName uni ())
forall a. a -> DefT Name uni fun () Quote a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni ()
 -> DefT Name uni fun () Quote (Type TyName uni ()))
-> Type TyName uni ()
-> DefT Name uni fun () Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @a ()

liftBuiltin
  :: forall a uni fun
   . uni `PLC.HasTermLevel` a
  => a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin :: forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin = Term TyName Name uni fun ()
-> DefT Name uni fun () Quote (Term TyName Name uni fun ())
forall a. a -> DefT Name uni fun () Quote a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ()
 -> DefT Name uni fun () Quote (Term TyName Name uni fun ()))
-> (a -> Term TyName Name uni fun ())
-> a
-> DefT Name uni fun () Quote (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, HasTermLevel 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 = [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 :: forall fun. 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.HasTypeLevel` Integer => Typeable uni BuiltinInteger where
  typeRep :: forall fun.
Proxy BuiltinInteger -> RTCompile uni fun (Type TyName uni ())
typeRep = Proxy BuiltinInteger -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTermLevel` Integer => Lift uni BuiltinInteger where
  lift :: forall fun.
BuiltinInteger -> RTCompile uni fun (Term TyName Name uni fun ())
lift = BuiltinInteger -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` BS.ByteString => Typeable uni BuiltinByteString where
  typeRep :: forall fun.
Proxy BuiltinByteString -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinByteString
_ = Proxy ByteString -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @BS.ByteString)

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTermLevel` BS.ByteString => Lift uni BuiltinByteString where
  lift :: forall fun.
BuiltinByteString
-> RTCompile uni fun (Term TyName Name uni fun ())
lift = ByteString -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (ByteString -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinByteString -> ByteString)
-> BuiltinByteString
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinByteString -> ByteString
BuiltinByteString -> FromBuiltin BuiltinByteString
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` T.Text => Typeable uni BuiltinString where
  typeRep :: forall fun.
Proxy BuiltinString -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinString
_ = Proxy Text -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @T.Text)

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTermLevel` T.Text => Lift uni BuiltinString where
  lift :: forall fun.
BuiltinString -> RTCompile uni fun (Term TyName Name uni fun ())
lift = Text -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Text -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinString -> Text)
-> BuiltinString
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinString -> Text
BuiltinString -> FromBuiltin BuiltinString
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` () => Typeable uni BuiltinUnit where
  typeRep :: forall fun.
Proxy BuiltinUnit -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinUnit
_ = Proxy () -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @())

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTermLevel` () => Lift uni BuiltinUnit where
  lift :: forall fun.
BuiltinUnit -> RTCompile uni fun (Term TyName Name uni fun ())
lift = () -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (() -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinUnit -> ())
-> BuiltinUnit
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinUnit -> ()
BuiltinUnit -> FromBuiltin BuiltinUnit
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` Bool => Typeable uni Bool where
  typeRep :: forall fun. Proxy Bool -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy Bool
_ = Proxy Bool -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Bool)

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTermLevel` Bool => Lift uni Bool where
  lift :: forall fun. Bool -> RTCompile uni fun (Term TyName Name uni fun ())
lift = Bool -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Bool -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (Bool -> Bool)
-> Bool
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
Bool -> FromBuiltin Bool
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` [] => Typeable uni BuiltinList where
  typeRep :: forall fun.
Proxy BuiltinList -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinList
_ = Proxy [] -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @[])

-- See Note [Lift and Typeable instances for builtins]
instance
  (HasFromBuiltin arep, uni `PLC.HasTermLevel` [FromBuiltin arep])
  => Lift uni (BuiltinList arep)
  where
  lift :: forall fun.
BuiltinList arep -> RTCompile uni fun (Term TyName Name uni fun ())
lift = [FromBuiltin arep]
-> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin ([FromBuiltin arep]
 -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinList arep -> [FromBuiltin arep])
-> BuiltinList arep
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinList arep -> [FromBuiltin arep]
BuiltinList arep -> FromBuiltin (BuiltinList arep)
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` Strict.Vector => Typeable uni BuiltinArray where
  typeRep :: forall fun.
Proxy BuiltinArray -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinArray
_ = Proxy Vector -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @Strict.Vector)

-- See Note [Lift and Typeable instances for builtins]
instance
  ( HasFromBuiltin arep
  , uni `PLC.HasTermLevel` Strict.Vector (FromBuiltin arep)
  )
  => Lift uni (BuiltinArray arep)
  where
  lift :: forall fun.
BuiltinArray arep
-> RTCompile uni fun (Term TyName Name uni fun ())
lift = Vector (FromBuiltin arep)
-> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Vector (FromBuiltin arep)
 -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinArray arep -> Vector (FromBuiltin arep))
-> BuiltinArray arep
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinArray arep -> Vector (FromBuiltin arep)
BuiltinArray arep -> FromBuiltin (BuiltinArray arep)
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

instance uni `PLC.HasTypeLevel` (,) => Typeable uni BuiltinPair where
  typeRep :: forall fun.
Proxy BuiltinPair -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinPair
_ = Proxy (,) -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall {k} (t :: k). Proxy t
forall (t :: * -> * -> *). Proxy t
Proxy @(,))

instance
  ( HasFromBuiltin arep
  , HasFromBuiltin brep
  , uni `PLC.HasTermLevel` (FromBuiltin arep, FromBuiltin brep)
  )
  => Lift uni (BuiltinPair arep brep)
  where
  lift :: forall fun.
BuiltinPair arep brep
-> RTCompile uni fun (Term TyName Name uni fun ())
lift = (FromBuiltin arep, FromBuiltin brep)
-> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin ((FromBuiltin arep, FromBuiltin brep)
 -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinPair arep brep -> (FromBuiltin arep, FromBuiltin brep))
-> BuiltinPair arep brep
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinPair arep brep -> (FromBuiltin arep, FromBuiltin brep)
BuiltinPair arep brep -> FromBuiltin (BuiltinPair arep brep)
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` Data => Typeable uni BuiltinData where
  typeRep :: forall fun.
Proxy BuiltinData -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinData
_ = Proxy Data -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Data)

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTypeLevel` Value => Typeable uni BuiltinValue where
  typeRep :: forall fun.
Proxy BuiltinValue -> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinValue
_ = Proxy Value -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Value)

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTermLevel` Data => Lift uni BuiltinData where
  lift :: forall fun.
BuiltinData -> RTCompile uni fun (Term TyName Name uni fun ())
lift = Data -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Data -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinData -> Data)
-> BuiltinData
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinData -> Data
BuiltinData -> FromBuiltin BuiltinData
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance uni `PLC.HasTermLevel` Value => Lift uni BuiltinValue where
  lift :: forall fun.
BuiltinValue -> RTCompile uni fun (Term TyName Name uni fun ())
lift = Value -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Value -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinValue -> Value)
-> BuiltinValue
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinValue -> Value
BuiltinValue -> FromBuiltin BuiltinValue
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance
  uni `PLC.HasTypeLevel` PlutusCore.Crypto.BLS12_381.G1.Element
  => Typeable uni BuiltinBLS12_381_G1_Element
  where
  typeRep :: forall fun.
Proxy BuiltinBLS12_381_G1_Element
-> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinBLS12_381_G1_Element
_ = Proxy Element -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @PlutusCore.Crypto.BLS12_381.G1.Element)

-- See Note [Lift and Typeable instances for builtins]
instance
  uni `PLC.HasTermLevel` PlutusCore.Crypto.BLS12_381.G1.Element
  => Lift uni BuiltinBLS12_381_G1_Element
  where
  lift :: forall fun.
BuiltinBLS12_381_G1_Element
-> RTCompile uni fun (Term TyName Name uni fun ())
lift = Element -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Element -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinBLS12_381_G1_Element -> Element)
-> BuiltinBLS12_381_G1_Element
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinBLS12_381_G1_Element -> Element
BuiltinBLS12_381_G1_Element
-> FromBuiltin BuiltinBLS12_381_G1_Element
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance
  uni `PLC.HasTypeLevel` PlutusCore.Crypto.BLS12_381.G2.Element
  => Typeable uni BuiltinBLS12_381_G2_Element
  where
  typeRep :: forall fun.
Proxy BuiltinBLS12_381_G2_Element
-> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinBLS12_381_G2_Element
_ = Proxy Element -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @PlutusCore.Crypto.BLS12_381.G2.Element)

-- See Note [Lift and Typeable instances for builtins]
instance
  uni `PLC.HasTermLevel` PlutusCore.Crypto.BLS12_381.G2.Element
  => Lift uni BuiltinBLS12_381_G2_Element
  where
  lift :: forall fun.
BuiltinBLS12_381_G2_Element
-> RTCompile uni fun (Term TyName Name uni fun ())
lift = Element -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (Element -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinBLS12_381_G2_Element -> Element)
-> BuiltinBLS12_381_G2_Element
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinBLS12_381_G2_Element -> Element
BuiltinBLS12_381_G2_Element
-> FromBuiltin BuiltinBLS12_381_G2_Element
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

-- See Note [Lift and Typeable instances for builtins]
instance
  uni `PLC.HasTypeLevel` PlutusCore.Crypto.BLS12_381.Pairing.MlResult
  => Typeable uni BuiltinBLS12_381_MlResult
  where
  typeRep :: forall fun.
Proxy BuiltinBLS12_381_MlResult
-> RTCompile uni fun (Type TyName uni ())
typeRep Proxy BuiltinBLS12_381_MlResult
_ = Proxy MlResult -> RTCompile uni fun (Type TyName uni ())
forall k (a :: k) (uni :: * -> *) fun.
HasTypeLevel uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
typeRepBuiltin (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @PlutusCore.Crypto.BLS12_381.Pairing.MlResult)

-- See Note [Lift and Typeable instances for builtins]
instance
  uni `PLC.HasTermLevel` PlutusCore.Crypto.BLS12_381.Pairing.MlResult
  => Lift uni BuiltinBLS12_381_MlResult
  where
  lift :: forall fun.
BuiltinBLS12_381_MlResult
-> RTCompile uni fun (Term TyName Name uni fun ())
lift = MlResult -> RTCompile uni fun (Term TyName Name uni fun ())
forall a (uni :: * -> *) fun.
HasTermLevel uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
liftBuiltin (MlResult -> RTCompile uni fun (Term TyName Name uni fun ()))
-> (BuiltinBLS12_381_MlResult -> MlResult)
-> BuiltinBLS12_381_MlResult
-> RTCompile uni fun (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinBLS12_381_MlResult -> MlResult
BuiltinBLS12_381_MlResult -> FromBuiltin BuiltinBLS12_381_MlResult
forall arep. HasFromBuiltin arep => arep -> FromBuiltin arep
fromBuiltin

{- Note [Lift and Typeable instances for builtins]
We can, generally, lift builtin values. We just make a constant with the value inside.
However, in Plutus Tx we use opaque types for most builtin types to avoid people
trying to pattern match on them. So the types don't quite match up with what we need
to put inside the constant.

Fortunately, we have To/FromBuiltin, which happen to do what we want.
See Note [Built-in types and their Haskell counterparts].
This is arguably slightly an abuse: the versions of the types that we want in
Plutus Tx source code and the versions that we use as the implementations of
the builtin types in the universe could be different. But in practice they
aren't. So we can write fairly straightforward instances for most types.

Similarly, for Typeable we may have to use a different type from the opaque one.
-}