{-# LANGUAGE CPP                   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE ViewPatterns          #-}
module PlutusTx.Lift.Class
    ( Typeable (..)
    , Lift (..)
    , RTCompile
    , makeTypeable
    , makeLift
    , withTyVars
    , LiftError (..)
    ) where

import PlutusTx.Lift.THUtils

import PlutusIR
import PlutusIR.Compiler.Definitions
import PlutusIR.Compiler.Names
import PlutusIR.MkPir

import PlutusCore.Default qualified as PLC
import PlutusCore.MkPlc qualified as PLC
import PlutusCore.Quote

import Control.Monad.Except hiding (lift)
import Control.Monad.Reader hiding (lift)
import Control.Monad.State hiding (lift)
import Control.Monad.Trans qualified as Trans

import Language.Haskell.TH qualified as TH hiding (newName)
import Language.Haskell.TH.Datatype qualified as TH
import Language.Haskell.TH.Syntax qualified as TH hiding (newName)
import Language.Haskell.TH.Syntax.Compat qualified as TH

import Data.Map qualified as Map
import Data.Set qualified as Set

import Control.Exception qualified as Prelude (Exception, throw)
import Data.Foldable
import Data.List (sortBy)
import Data.Maybe
import Data.Proxy
import Data.Text qualified as T
import Data.Traversable
import ErrorCode
import Prettyprinter qualified as PP

-- 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
type RTCompileScope uni fun = ReaderT (LocalVars uni) (RTCompile uni fun)
type THCompile = StateT Deps (ReaderT THLocalVars (ExceptT LiftError TH.Q))

data LiftError = UnsupportedLiftKind TH.Kind
               | UnsupportedLiftType TH.Type
               | UserLiftError T.Text
               | LiftMissingDataCons TH.Name
               | LiftMissingVar TH.Name
               deriving anyclass (Show LiftError
Typeable LiftError
Typeable LiftError
-> Show LiftError
-> (LiftError -> SomeException)
-> (SomeException -> Maybe LiftError)
-> (LiftError -> String)
-> Exception LiftError
SomeException -> Maybe LiftError
LiftError -> String
LiftError -> SomeException
forall e.
Typeable e
-> Show e
-> (e -> SomeException)
-> (SomeException -> Maybe e)
-> (e -> String)
-> Exception e
displayException :: LiftError -> String
$cdisplayException :: LiftError -> String
fromException :: SomeException -> Maybe LiftError
$cfromException :: SomeException -> Maybe LiftError
toException :: LiftError -> SomeException
$ctoException :: LiftError -> SomeException
$cp2Exception :: Show LiftError
$cp1Exception :: Typeable LiftError
Prelude.Exception)

instance PP.Pretty LiftError where
    pretty :: LiftError -> Doc ann
pretty (UnsupportedLiftType Type
t) = Doc ann
"Unsupported lift type: " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Type -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow Type
t
    pretty (UnsupportedLiftKind Type
t) = Doc ann
"Unsupported lift kind: " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Type -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow Type
t
    pretty (UserLiftError Text
t)       = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
t
    pretty (LiftMissingDataCons Name
n) = Doc ann
"Constructors not created for type: " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Name -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow Name
n
    pretty (LiftMissingVar Name
n)      = Doc ann
"Unknown local variable: " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Name -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow Name
n

instance Show LiftError where
    show :: LiftError -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (LiftError -> Doc Any) -> LiftError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftError -> Doc Any
forall a ann. Pretty a => a -> Doc ann
PP.pretty -- for Control.Exception

instance HasErrorCode LiftError where
    errorCode :: LiftError -> ErrorCode
errorCode UnsupportedLiftType {} = Natural -> ErrorCode
ErrorCode Natural
44
    errorCode UnsupportedLiftKind {} = Natural -> ErrorCode
ErrorCode Natural
45
    errorCode UserLiftError {}       = Natural -> ErrorCode
ErrorCode Natural
46
    errorCode LiftMissingDataCons {} = Natural -> ErrorCode
ErrorCode Natural
47
    errorCode LiftMissingVar {}      = Natural -> ErrorCode
ErrorCode Natural
48

{- Note [Impredicative function universe wrappers]
We are completely independent of the function universe. We generate constants (so we care about the type universe),
but we never generate builtin functions.

This is indicated in the fact that e.g. 'typeRep' has type 'forall fun . ...'. Note what this says: the
*caller* of 'typeRep` can decide on 'fun'.

So how do we deal with this? A wrong way is to parameterize our (TH) functions by 'fun'. This is wrong, because
this 'fun' is a type variable at TH-generation time, and we want a type variable in the generated code.
Sometimes this will even appear to work, and I don't know what kind of awful magic is going on in trying to persist
type variables into the quote, but I'm pretty sure it's wrong.

We could use 'InstanceSigs', bind 'fun', and then pass it down and use it in our signatures. But you can't splice
types into signatures in typed TH, you need to go to untyped TH and 'unsafeCoerceTExp' back again, which is pretty ugly.

Alternatively, we can *generate* functions which are parameterized over 'fun', and instantiate them at the top-level.
This is totally fine... except that the representation of expressions in typed TH has a type parameter for the type of
the expression, so we would need to write 'TExp (forall fun . ...)'... which is an impredicative type.

The usual solution is to make a datatype that wraps up the quantification, so you write 'newtype X = X (forall a . ...)',
and then you can write 'TExp X' just fine.

We do this, but annoyingly due to the fact that 'fun' appears inside the *value* of our monadic types (e.g. when we compile
to a term we need to have 'fun' in there) we can't do this generically, and instead we end up with a set of repetitive wrappers
for different variants of this impredicative type. Which is annoying, but does work.
-}

-- See Note [Impredicative function universe wrappers]
newtype CompileType = CompileType { CompileType
-> forall fun. RTCompile DefaultUni fun (Type TyName DefaultUni ())
unCompileType :: forall fun . RTCompile PLC.DefaultUni fun (Type TyName PLC.DefaultUni ()) }
newtype CompileTypeScope = CompileTypeScope { CompileTypeScope
-> forall fun.
   RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
unCompileTypeScope :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ()) }
newtype CompileDeclFun = CompileDeclFun { CompileDeclFun
-> forall fun.
   Type TyName DefaultUni ()
   -> RTCompileScope
        DefaultUni fun (VarDecl TyName Name DefaultUni fun ())
unCompileDeclFun :: forall fun . Type TyName PLC.DefaultUni () -> RTCompileScope PLC.DefaultUni fun (VarDecl TyName Name PLC.DefaultUni fun ()) }

{- Note [Type variables]
We handle types in almost exactly the same way when we are constructing Typeable
instances and when we are constructing Lift instances. However, there is one key difference
in how we handle type variables.

In the Typeable case, the type variables we see will be the type variables of the
datatype, which we want to map into the variable declarations that we construct. This requires
us to do some mapping between them at *runtime*, and keep a scope around to map between the TH names
and the PLC types.

In the Lift case, type variables will be free type variables in the instance, and should be handled
by appropriate Typeable constraints for those variables. We get the PLC types by just calling
typeRep.

However, for simplicity we always act as though we have a local scope, and fall back to Typeable,
but in the Lift case we will never populate the local scope.
-}

-- | A scope for type variables. See note [Type variables].
type LocalVars uni = Map.Map TH.Name (Type TyName uni ())
type THLocalVars = Set.Set TH.Name

withTyVars :: (MonadReader (LocalVars uni) m) => [(TH.Name, TyVarDecl TyName ())] -> m a -> m a
withTyVars :: [(Name, TyVarDecl TyName ())] -> m a -> m a
withTyVars [(Name, TyVarDecl TyName ())]
mappings = (Map Name (Type TyName uni ()) -> Map Name (Type TyName uni ()))
-> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Map Name (Type TyName uni ())
scope -> (Map Name (Type TyName uni ())
 -> (Name, TyVarDecl TyName ()) -> Map Name (Type TyName uni ()))
-> Map Name (Type TyName uni ())
-> [(Name, TyVarDecl TyName ())]
-> Map Name (Type TyName uni ())
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map Name (Type TyName uni ())
acc (Name
n, TyVarDecl TyName ()
tvd) -> Name
-> Type TyName uni ()
-> Map Name (Type TyName uni ())
-> Map Name (Type TyName uni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (() -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () TyVarDecl TyName ()
tvd) Map Name (Type TyName uni ())
acc) Map Name (Type TyName uni ())
scope [(Name, TyVarDecl TyName ())]
mappings)

thWithTyVars :: (MonadReader THLocalVars m) => [TH.Name] -> m a -> m a
thWithTyVars :: [Name] -> m a -> m a
thWithTyVars [Name]
names = (Set Name -> Set Name) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Set Name
scope -> (Name -> Set Name -> Set Name) -> Set Name -> [Name] -> Set Name
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.insert Set Name
scope [Name]
names)

{- Note [Lifting newtypes]
Newtypes are handled differently in the compiler, in that we identify them with their underlying type.
See Note [Coercions and newtypes] for details.

So we need to do the same here. This means two things:
- For Typeable, we look for the unique field of the unique constructor, and then make a type lambda
  binding the type variables whose body is that type.
- For Lift, we assert that all constructors must have precisely one argument (as newtypes do), and we
  simply call lift on that.

Since we don't "compile" all the way, rather relying on the typeclass system, lifting recursive
newtypes will hang a runtime. Don't do that. (This is worse than what we do in the compiler, see
Note [Occurrences of recursive names])
-}

-- Dependencies at TH time

{- Note [Tracking dependencies]
While running at TH time, we track the requirements that we need in order to be able to compile
the given type/term, which are things like "must be able to type the constructor argument types".

These are then cashed out into constraints on the instance.
-}

data Dep = TypeableDep TH.Type | LiftDep TH.Type deriving stock (Int -> Dep -> ShowS
[Dep] -> ShowS
Dep -> String
(Int -> Dep -> ShowS)
-> (Dep -> String) -> ([Dep] -> ShowS) -> Show Dep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Dep] -> ShowS
$cshowList :: [Dep] -> ShowS
show :: Dep -> String
$cshow :: Dep -> String
showsPrec :: Int -> Dep -> ShowS
$cshowsPrec :: Int -> Dep -> ShowS
Show, Dep -> Dep -> Bool
(Dep -> Dep -> Bool) -> (Dep -> Dep -> Bool) -> Eq Dep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Dep -> Dep -> Bool
$c/= :: Dep -> Dep -> Bool
== :: Dep -> Dep -> Bool
$c== :: Dep -> Dep -> Bool
Eq, Eq Dep
Eq Dep
-> (Dep -> Dep -> Ordering)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Dep)
-> (Dep -> Dep -> Dep)
-> Ord Dep
Dep -> Dep -> Bool
Dep -> Dep -> Ordering
Dep -> Dep -> Dep
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Dep -> Dep -> Dep
$cmin :: Dep -> Dep -> Dep
max :: Dep -> Dep -> Dep
$cmax :: Dep -> Dep -> Dep
>= :: Dep -> Dep -> Bool
$c>= :: Dep -> Dep -> Bool
> :: Dep -> Dep -> Bool
$c> :: Dep -> Dep -> Bool
<= :: Dep -> Dep -> Bool
$c<= :: Dep -> Dep -> Bool
< :: Dep -> Dep -> Bool
$c< :: Dep -> Dep -> Bool
compare :: Dep -> Dep -> Ordering
$ccompare :: Dep -> Dep -> Ordering
$cp1Ord :: Eq Dep
Ord)
type Deps = Set.Set Dep

-- | Get all the named types which we depend on to define the current type.
-- Note that this relies on dependencies having been added with type synonyms
-- resolved!
getTyConDeps :: Deps -> Set.Set TH.Name
getTyConDeps :: Deps -> Set Name
getTyConDeps Deps
deps = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList ([Name] -> Set Name) -> [Name] -> Set Name
forall a b. (a -> b) -> a -> b
$ (Dep -> Maybe Name) -> [Dep] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Dep -> Maybe Name
typeableDep ([Dep] -> [Name]) -> [Dep] -> [Name]
forall a b. (a -> b) -> a -> b
$ Deps -> [Dep]
forall a. Set a -> [a]
Set.toList Deps
deps
    where
        typeableDep :: Dep -> Maybe Name
typeableDep (TypeableDep (TH.ConT Name
n)) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
        typeableDep Dep
_                         = Maybe Name
forall a. Maybe a
Nothing

addTypeableDep :: TH.Type -> THCompile ()
addTypeableDep :: Type -> THCompile ()
addTypeableDep Type
ty = do
    Type
ty' <- Type -> THCompile Type
normalizeAndResolve Type
ty
    (Deps -> Deps) -> THCompile ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Deps -> Deps) -> THCompile ()) -> (Deps -> Deps) -> THCompile ()
forall a b. (a -> b) -> a -> b
$ Dep -> Deps -> Deps
forall a. Ord a => a -> Set a -> Set a
Set.insert (Dep -> Deps -> Deps) -> Dep -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ Type -> Dep
TypeableDep Type
ty'

addLiftDep :: TH.Type -> THCompile ()
addLiftDep :: Type -> THCompile ()
addLiftDep Type
ty = do
    Type
ty' <- Type -> THCompile Type
normalizeAndResolve Type
ty
    (Deps -> Deps) -> THCompile ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Deps -> Deps) -> THCompile ()) -> (Deps -> Deps) -> THCompile ()
forall a b. (a -> b) -> a -> b
$ Dep -> Deps -> Deps
forall a. Ord a => a -> Set a -> Set a
Set.insert (Dep -> Deps -> Deps) -> Dep -> Deps -> Deps
forall a b. (a -> b) -> a -> b
$ Type -> Dep
LiftDep Type
ty'

-- Constraints

-- | Make a 'Typeable' constraint.
typeablePir :: TH.Type -> TH.Type -> TH.Type
typeablePir :: Type -> Type -> Type
typeablePir Type
uni Type
ty = Name -> [Type] -> Type
TH.classPred ''Typeable [Type
uni, Type
ty]

-- | Make a 'Lift' constraint.
liftPir :: TH.Type -> TH.Type -> TH.Type
liftPir :: Type -> Type -> Type
liftPir Type
uni Type
ty = Name -> [Type] -> Type
TH.classPred ''Lift [Type
uni, Type
ty]

toConstraint :: TH.Type -> Dep -> TH.Pred
toConstraint :: Type -> Dep -> Type
toConstraint Type
uni = \case
    TypeableDep Type
n -> Type -> Type -> Type
typeablePir Type
uni Type
n
    LiftDep Type
ty    -> Type -> Type -> Type
liftPir Type
uni Type
ty

{- Note [Closed constraints]
There is no point adding constraints that are "closed", i.e. don't mention any of the
instance type variables. These will either be satisfied by other instances in scope
(in which case GHC will complain at you), or be unsatisfied in which case the user will
get a useful error anyway.
-}

isClosedConstraint :: TH.Pred -> Bool
isClosedConstraint :: Type -> Bool
isClosedConstraint = [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Name] -> Bool) -> (Type -> [Name]) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Name]
forall a. TypeSubstitution a => a -> [Name]
TH.freeVariables

-- | Convenience wrapper around 'normalizeType' and 'TH.resolveTypeSynonyms'.
normalizeAndResolve :: TH.Type -> THCompile TH.Type
normalizeAndResolve :: Type -> THCompile Type
normalizeAndResolve Type
ty = Type -> Type
normalizeType (Type -> Type) -> THCompile Type -> THCompile Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ReaderT (Set Name) (ExceptT LiftError Q) Type -> THCompile Type
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ReaderT (Set Name) (ExceptT LiftError Q) Type -> THCompile Type)
-> ReaderT (Set Name) (ExceptT LiftError Q) Type -> THCompile Type
forall a b. (a -> b) -> a -> b
$ ExceptT LiftError Q Type
-> ReaderT (Set Name) (ExceptT LiftError Q) Type
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ExceptT LiftError Q Type
 -> ReaderT (Set Name) (ExceptT LiftError Q) Type)
-> ExceptT LiftError Q Type
-> ReaderT (Set Name) (ExceptT LiftError Q) Type
forall a b. (a -> b) -> a -> b
$ Q Type -> ExceptT LiftError Q Type
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (Q Type -> ExceptT LiftError Q Type)
-> Q Type -> ExceptT LiftError Q Type
forall a b. (a -> b) -> a -> b
$ Type -> Q Type
TH.resolveTypeSynonyms Type
ty)

-- See Note [Ordering of constructors]
sortedCons :: TH.DatatypeInfo -> [TH.ConstructorInfo]
sortedCons :: DatatypeInfo -> [ConstructorInfo]
sortedCons TH.DatatypeInfo{datatypeName :: DatatypeInfo -> Name
TH.datatypeName=Name
tyName, datatypeCons :: DatatypeInfo -> [ConstructorInfo]
TH.datatypeCons=[ConstructorInfo]
cons} =
    -- We need to compare 'TH.Name's on their string name *not* on the unique
    let sorted :: [ConstructorInfo]
sorted = (ConstructorInfo -> ConstructorInfo -> Ordering)
-> [ConstructorInfo] -> [ConstructorInfo]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(ConstructorInfo -> Name
TH.constructorName -> (TH.Name OccName
o1 NameFlavour
_)) (ConstructorInfo -> Name
TH.constructorName -> (TH.Name OccName
o2 NameFlavour
_)) -> OccName -> OccName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare OccName
o1 OccName
o2) [ConstructorInfo]
cons
    in if Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Bool Bool -> Bool -> Bool
|| Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''[] then [ConstructorInfo] -> [ConstructorInfo]
forall a. [a] -> [a]
reverse [ConstructorInfo]
sorted else [ConstructorInfo]
sorted

#if MIN_VERSION_template_haskell(2,17,0)
tvNameAndKind :: TH.TyVarBndrUnit -> THCompile (TH.Name, Kind ())
tvNameAndKind = \case
    TH.KindedTV name _ kind -> do
        kind' <- (compileKind <=< normalizeAndResolve) kind
        pure (name, kind')
    -- TODO: is this what PlainTV actually means? That it's of kind Type?
    TH.PlainTV name _ -> pure (name, Type ())
#else
tvNameAndKind :: TH.TyVarBndr -> THCompile (TH.Name, Kind ())
tvNameAndKind :: TyVarBndr -> THCompile (Name, Kind ())
tvNameAndKind = \case
    TH.KindedTV Name
name Type
kind -> do
        Kind ()
kind' <- (Type -> THCompile (Kind ())
compileKind (Type -> THCompile (Kind ()))
-> (Type -> THCompile Type) -> Type -> THCompile (Kind ())
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type -> THCompile Type
normalizeAndResolve) Type
kind
        (Name, Kind ()) -> THCompile (Name, Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, Kind ()
kind')
    -- TODO: is this what PlainTV actually means? That it's of kind Type?
    TH.PlainTV Name
name -> (Name, Kind ()) -> THCompile (Name, Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, () -> Kind ()
forall ann. ann -> Kind ann
Type ())
#endif

------------------
-- Types and kinds
------------------

-- Note: we can actually do this entirely at TH-time, which is nice
compileKind :: TH.Kind -> THCompile (Kind ())
compileKind :: Type -> THCompile (Kind ())
compileKind = \case
    Type
TH.StarT                          -> Kind () -> THCompile (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> THCompile (Kind ())) -> Kind () -> THCompile (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    TH.AppT (TH.AppT Type
TH.ArrowT Type
k1) Type
k2 -> () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (Kind () -> Kind () -> Kind ())
-> THCompile (Kind ())
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (Kind () -> Kind ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> THCompile (Kind ())
compileKind Type
k1 StateT
  Deps
  (ReaderT (Set Name) (ExceptT LiftError Q))
  (Kind () -> Kind ())
-> THCompile (Kind ()) -> THCompile (Kind ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> THCompile (Kind ())
compileKind Type
k2
    Type
k                                 -> LiftError -> THCompile (Kind ())
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError -> THCompile (Kind ()))
-> LiftError -> THCompile (Kind ())
forall a b. (a -> b) -> a -> b
$ Type -> LiftError
UnsupportedLiftKind Type
k

compileType :: TH.Type -> THCompile (TH.TExpQ CompileTypeScope)
compileType :: Type -> THCompile (TExpQ CompileTypeScope)
compileType = \case
    TH.AppT Type
t1 Type
t2 -> do
        TExpQ CompileTypeScope
t1' <- Type -> THCompile (TExpQ CompileTypeScope)
compileType Type
t1
        TExpQ CompileTypeScope
t2' <- Type -> THCompile (TExpQ CompileTypeScope)
compileType Type
t2
        TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> (TExpQ CompileTypeScope -> TExpQ CompileTypeScope)
-> TExpQ CompileTypeScope
-> THCompile (TExpQ CompileTypeScope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TExpQ CompileTypeScope -> TExpQ CompileTypeScope
forall (m :: * -> *) a. Splice m a -> Splice m a
TH.examineSplice (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ [|| CompileTypeScope (TyApp () <$> unCompileTypeScope ($$(TH.liftSplice t1')) <*> unCompileTypeScope ($$(TH.liftSplice t2'))) ||]
    t :: Type
t@(TH.ConT Name
name) -> Type -> Name -> THCompile (TExpQ CompileTypeScope)
compileTypeableType Type
t Name
name
    -- See note [Type variables]
    t :: Type
t@(TH.VarT Name
name) -> do
        Bool
isLocal <- (Set Name -> Bool)
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
name)
        if Bool
isLocal
        then TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> (TExpQ CompileTypeScope -> TExpQ CompileTypeScope)
-> TExpQ CompileTypeScope
-> THCompile (TExpQ CompileTypeScope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TExpQ CompileTypeScope -> TExpQ CompileTypeScope
forall (m :: * -> *) a. Splice m a -> Splice m a
TH.examineSplice (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ [||
              CompileTypeScope $ do
                  vars <- ask
                  case Map.lookup name vars of
                      Just ty -> pure ty
                      Nothing -> Prelude.throw $ LiftMissingVar name
             ||]
        else Type -> Name -> THCompile (TExpQ CompileTypeScope)
compileTypeableType Type
t Name
name
    Type
t -> LiftError -> THCompile (TExpQ CompileTypeScope)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError -> THCompile (TExpQ CompileTypeScope))
-> LiftError -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ Type -> LiftError
UnsupportedLiftType Type
t

-- | Compile a type with the given name using 'typeRep' and incurring a corresponding 'Typeable' dependency.
compileTypeableType :: TH.Type -> TH.Name -> THCompile (TH.TExpQ CompileTypeScope)
compileTypeableType :: Type -> Name -> THCompile (TExpQ CompileTypeScope)
compileTypeableType Type
ty Name
name = do
    Type -> THCompile ()
addTypeableDep Type
ty
    -- We need the `unsafeTExpCoerce` since this will necessarily involve
    -- types we don't know now: the type which this instance is for (which
    -- appears in the proxy argument). However, since we know the type of
    -- `typeRep` we can get back into typed land quickly.
    let trep :: TH.TExpQ CompileType
        trep :: TExpQ CompileType
trep = Q Exp -> TExpQ CompileType
forall a. Q Exp -> Q (TExp a)
TH.unsafeTExpCoerce [| CompileType (typeRep (Proxy :: Proxy $(pure ty))) |]
    TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> (TExpQ CompileTypeScope -> TExpQ CompileTypeScope)
-> TExpQ CompileTypeScope
-> THCompile (TExpQ CompileTypeScope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TExpQ CompileTypeScope -> TExpQ CompileTypeScope
forall (m :: * -> *) a. Splice m a -> Splice m a
TH.examineSplice (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ [||
          let trep' :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
              trep' = Trans.lift $ unCompileType ($$(TH.liftSplice trep))
          in CompileTypeScope $ do
              maybeType <- lookupType () name
              case maybeType of
                  Just t  -> pure t
                  -- this will need some additional constraints in scope
                  Nothing -> trep'
          ||]

-----------
-- Typeable
-----------

-- TODO: try and make this work with type applications
-- | 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 ())

-- Just here so we can pin down the type variables without using TypeApplications in the generated code
recordAlias' :: TH.Name -> RTCompileScope PLC.DefaultUni fun ()
recordAlias' :: Name -> RTCompileScope DefaultUni fun ()
recordAlias' = Name -> RTCompileScope DefaultUni fun ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> m ()
recordAlias

-- Just here so we can pin down the type variables without using TypeApplications in the generated code
defineDatatype' :: TH.Name -> DatatypeDef TyName Name PLC.DefaultUni fun () -> Set.Set TH.Name -> RTCompileScope PLC.DefaultUni fun ()
defineDatatype' :: Name
-> DatatypeDef TyName Name DefaultUni fun ()
-> Set Name
-> RTCompileScope DefaultUni fun ()
defineDatatype' = Name
-> DatatypeDef TyName Name DefaultUni fun ()
-> Set Name
-> RTCompileScope DefaultUni fun ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> DatatypeDef TyName Name uni fun ann -> Set key -> m ()
defineDatatype

-- TODO: there is an unpleasant amount of duplication between this and the main compiler, but
-- I'm not sure how to unify them better
compileTypeRep :: TH.DatatypeInfo -> THCompile (TH.TExpQ CompileType)
compileTypeRep :: DatatypeInfo -> THCompile (TExpQ CompileType)
compileTypeRep dt :: DatatypeInfo
dt@TH.DatatypeInfo{datatypeName :: DatatypeInfo -> Name
TH.datatypeName=Name
tyName, datatypeVars :: DatatypeInfo -> [TyVarBndr]
TH.datatypeVars=[TyVarBndr]
tvs} = do
    [(Name, Kind ())]
tvNamesAndKinds <- (TyVarBndr -> THCompile (Name, Kind ()))
-> [TyVarBndr]
-> StateT
     Deps (ReaderT (Set Name) (ExceptT LiftError Q)) [(Name, Kind ())]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TyVarBndr -> THCompile (Name, Kind ())
tvNameAndKind [TyVarBndr]
tvs
    -- annoyingly th-abstraction doesn't give us a kind we can compile here
    let typeKind :: Kind ()
typeKind = ((Name, Kind ()) -> Kind () -> Kind ())
-> Kind () -> [(Name, Kind ())] -> Kind ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
_, Kind ()
k) Kind ()
acc -> () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k Kind ()
acc) (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) [(Name, Kind ())]
tvNamesAndKinds
    let cons :: [ConstructorInfo]
cons = DatatypeInfo -> [ConstructorInfo]
sortedCons DatatypeInfo
dt

    [Name]
-> THCompile (TExpQ CompileType) -> THCompile (TExpQ CompileType)
forall (m :: * -> *) a.
MonadReader (Set Name) m =>
[Name] -> m a -> m a
thWithTyVars (((Name, Kind ()) -> Name) -> [(Name, Kind ())] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Kind ()) -> Name
forall a b. (a, b) -> a
fst [(Name, Kind ())]
tvNamesAndKinds) (THCompile (TExpQ CompileType) -> THCompile (TExpQ CompileType))
-> THCompile (TExpQ CompileType) -> THCompile (TExpQ CompileType)
forall a b. (a -> b) -> a -> b
$ if DatatypeInfo -> Bool
isNewtype DatatypeInfo
dt
    then do
        -- Extract the unique field of the unique constructor
        TExpQ CompileTypeScope
argTy <- case [ConstructorInfo]
cons of
            [ TH.ConstructorInfo {constructorFields :: ConstructorInfo -> [Type]
TH.constructorFields=[Type
argTy]} ] -> (Type -> THCompile (TExpQ CompileTypeScope)
compileType (Type -> THCompile (TExpQ CompileTypeScope))
-> (Type -> THCompile Type)
-> Type
-> THCompile (TExpQ CompileTypeScope)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type -> THCompile Type
normalizeAndResolve) Type
argTy
            [ConstructorInfo]
_ -> LiftError -> THCompile (TExpQ CompileTypeScope)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError -> THCompile (TExpQ CompileTypeScope))
-> LiftError -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ Text -> LiftError
UserLiftError Text
"Newtypes must have a single constructor with a single argument"
        Set Name
deps <- (Deps -> Set Name)
-> StateT
     Deps (ReaderT (Set Name) (ExceptT LiftError Q)) (Set Name)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Deps -> Set Name
getTyConDeps
        TExpQ CompileType -> THCompile (TExpQ CompileType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileType -> THCompile (TExpQ CompileType))
-> (TExpQ CompileType -> TExpQ CompileType)
-> TExpQ CompileType
-> THCompile (TExpQ CompileType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TExpQ CompileType -> TExpQ CompileType
forall (m :: * -> *) a. Splice m a -> Splice m a
TH.examineSplice (TExpQ CompileType -> THCompile (TExpQ CompileType))
-> TExpQ CompileType -> THCompile (TExpQ CompileType)
forall a b. (a -> b) -> a -> b
$ [||
            let
                argTy' :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                argTy' = unCompileTypeScope $$(TH.liftSplice argTy)
                act :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                act = do
                    maybeDefined <- lookupType () tyName
                    case maybeDefined of
                        Just ty -> pure ty
                        Nothing -> do
                            (_, dtvd) <- mkTyVarDecl tyName typeKind
                            tvds <- traverse (uncurry mkTyVarDecl) tvNamesAndKinds

                            alias <- withTyVars tvds $ mkIterTyLam (fmap snd tvds) <$> argTy'
                            defineType tyName (PLC.Def dtvd alias) deps
                            recordAlias' tyName
                            pure alias
            in CompileType $ runReaderT act mempty
         ||]
    else do
        [TExpQ CompileDeclFun]
constrExprs <- (ConstructorInfo
 -> StateT
      Deps
      (ReaderT (Set Name) (ExceptT LiftError Q))
      (TExpQ CompileDeclFun))
-> [ConstructorInfo]
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     [TExpQ CompileDeclFun]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ConstructorInfo
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
compileConstructorDecl [ConstructorInfo]
cons
        Set Name
deps <- (Deps -> Set Name)
-> StateT
     Deps (ReaderT (Set Name) (ExceptT LiftError Q)) (Set Name)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Deps -> Set Name
getTyConDeps
        TExpQ CompileType -> THCompile (TExpQ CompileType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileType -> THCompile (TExpQ CompileType))
-> (TExpQ CompileType -> TExpQ CompileType)
-> TExpQ CompileType
-> THCompile (TExpQ CompileType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TExpQ CompileType -> TExpQ CompileType
forall (m :: * -> *) a. Splice m a -> Splice m a
TH.examineSplice (TExpQ CompileType -> THCompile (TExpQ CompileType))
-> TExpQ CompileType -> THCompile (TExpQ CompileType)
forall a b. (a -> b) -> a -> b
$ [||
          let
              constrExprs' :: [CompileDeclFun]
              constrExprs' = $$(TH.liftSplice $ tyListE constrExprs)
              act :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
              act = do
                maybeDefined <- lookupType () tyName
                case maybeDefined of
                    Just ty -> pure ty
                    Nothing -> do
                        (_, dtvd) <- mkTyVarDecl tyName typeKind
                        tvds <- traverse (uncurry mkTyVarDecl) tvNamesAndKinds

                        let resultType = mkIterTyApp () (mkTyVar () dtvd) (fmap (mkTyVar () . snd) tvds)
                        matchName <- safeFreshName (T.pack "match_" <> showName tyName)

                        -- See Note [Occurrences of recursive names]
                        let fakeDatatype = Datatype () dtvd [] matchName []

                        defineDatatype' tyName (PLC.Def dtvd fakeDatatype) Set.empty

                        withTyVars tvds $ do
                            -- The TH expressions are in fact all functions that take the result type, so
                            -- we need to apply them
                            let constrActs :: RTCompileScope PLC.DefaultUni fun [VarDecl TyName Name PLC.DefaultUni fun ()]
                                constrActs = sequence $ fmap (\x -> unCompileDeclFun x) constrExprs' <*> [resultType]
                            constrs <- constrActs

                            let datatype = Datatype () dtvd (fmap snd tvds) matchName constrs

                            defineDatatype tyName (PLC.Def dtvd datatype) deps
                        pure $ mkTyVar () dtvd
          in CompileType $ runReaderT act mempty
          ||]

compileConstructorDecl
    :: TH.ConstructorInfo
    -> THCompile (TH.TExpQ CompileDeclFun)
compileConstructorDecl :: ConstructorInfo
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
compileConstructorDecl TH.ConstructorInfo{constructorName :: ConstructorInfo -> Name
TH.constructorName=Name
name, constructorFields :: ConstructorInfo -> [Type]
TH.constructorFields=[Type]
argTys} = do
    [TExpQ CompileTypeScope]
tyExprs <- (Type -> THCompile (TExpQ CompileTypeScope))
-> [Type]
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> THCompile (TExpQ CompileTypeScope)
compileType (Type -> THCompile (TExpQ CompileTypeScope))
-> (Type -> THCompile Type)
-> Type
-> THCompile (TExpQ CompileTypeScope)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type -> THCompile Type
normalizeAndResolve) [Type]
argTys
    TExpQ CompileDeclFun
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileDeclFun
 -> StateT
      Deps
      (ReaderT (Set Name) (ExceptT LiftError Q))
      (TExpQ CompileDeclFun))
-> (TExpQ CompileDeclFun -> TExpQ CompileDeclFun)
-> TExpQ CompileDeclFun
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TExpQ CompileDeclFun -> TExpQ CompileDeclFun
forall (m :: * -> *) a. Splice m a -> Splice m a
TH.examineSplice (TExpQ CompileDeclFun
 -> StateT
      Deps
      (ReaderT (Set Name) (ExceptT LiftError Q))
      (TExpQ CompileDeclFun))
-> TExpQ CompileDeclFun
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
forall a b. (a -> b) -> a -> b
$ [||
         let
             tyExprs' :: forall fun . [RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())]
             tyExprs' = fmap (\x -> unCompileTypeScope x) $$(TH.liftSplice $ tyListE tyExprs)
          -- we won't know the result type until runtime, so take it as an argument
          in CompileDeclFun $ \resultType -> do
              tys' <- sequence tyExprs'
              let constrTy = mkIterTyFun () tys' resultType
              constrName <- safeFreshName $ showName name
              pure $ VarDecl () constrName constrTy
          ||]

makeTypeable :: TH.Type -> TH.Name -> TH.Q [TH.Dec]
makeTypeable :: Type -> Name -> Q [Dec]
makeTypeable Type
uni Name
name = do
    Extension -> Q ()
requireExtension Extension
TH.ScopedTypeVariables

    DatatypeInfo
info <- Name -> Q DatatypeInfo
TH.reifyDatatype Name
name
    (TExpQ CompileType
rhs, Deps
deps) <- THCompile (TExpQ CompileType) -> Q (TExpQ CompileType, Deps)
forall a. THCompile a -> Q (a, Deps)
runTHCompile (THCompile (TExpQ CompileType) -> Q (TExpQ CompileType, Deps))
-> THCompile (TExpQ CompileType) -> Q (TExpQ CompileType, Deps)
forall a b. (a -> b) -> a -> b
$ DatatypeInfo -> THCompile (TExpQ CompileType)
compileTypeRep DatatypeInfo
info

    -- See Note [Closed constraints]
    let constraints :: [Type]
constraints = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isClosedConstraint) ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Type -> Dep -> Type
toConstraint Type
uni (Dep -> Type) -> [Dep] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Deps -> [Dep]
forall a. Set a -> [a]
Set.toList Deps
deps
    -- We need to unwrap the wrapper at the last minute, see Note [Impredicative function universe wrappers]
    let unwrappedRhs :: Q Exp
unwrappedRhs = [| unCompileType |] Q Exp -> Q Exp -> Q Exp
`TH.appE` TExpQ CompileType -> Q Exp
forall a. Q (TExp a) -> Q Exp
TH.unTypeQ TExpQ CompileType
rhs

    Dec
decl <- Name -> [ClauseQ] -> DecQ
TH.funD 'typeRep [[PatQ] -> BodyQ -> [DecQ] -> ClauseQ
TH.clause [PatQ
TH.wildP] (Q Exp -> BodyQ
TH.normalB Q Exp
unwrappedRhs) []]
    [Dec] -> Q [Dec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Maybe Overlap -> [Type] -> Type -> [Dec] -> Dec
TH.InstanceD Maybe Overlap
forall a. Maybe a
Nothing [Type]
constraints (Type -> Type -> Type
typeablePir Type
uni (Name -> Type
TH.ConT Name
name)) [Dec
decl]]

-------
-- Lift
-------

-- | 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 ())

compileLift :: TH.DatatypeInfo -> THCompile [TH.Q TH.Clause]
compileLift :: DatatypeInfo -> THCompile [ClauseQ]
compileLift DatatypeInfo
dt = ((Int, ConstructorInfo)
 -> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ)
-> [(Int, ConstructorInfo)] -> THCompile [ClauseQ]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Int
 -> ConstructorInfo
 -> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ)
-> (Int, ConstructorInfo)
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (DatatypeInfo
-> Int
-> ConstructorInfo
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ
compileConstructorClause DatatypeInfo
dt)) ([Int] -> [ConstructorInfo] -> [(Int, ConstructorInfo)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (DatatypeInfo -> [ConstructorInfo]
sortedCons DatatypeInfo
dt))

compileConstructorClause
    :: TH.DatatypeInfo -> Int -> TH.ConstructorInfo -> THCompile (TH.Q TH.Clause)
compileConstructorClause :: DatatypeInfo
-> Int
-> ConstructorInfo
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ
compileConstructorClause dt :: DatatypeInfo
dt@TH.DatatypeInfo{datatypeName :: DatatypeInfo -> Name
TH.datatypeName=Name
tyName, datatypeVars :: DatatypeInfo -> [TyVarBndr]
TH.datatypeVars=[TyVarBndr]
tvs} Int
index TH.ConstructorInfo{constructorName :: ConstructorInfo -> Name
TH.constructorName=Name
name, constructorFields :: ConstructorInfo -> [Type]
TH.constructorFields=[Type]
argTys} = do
    -- need to be able to lift the argument types
    (Type -> THCompile ()) -> [Type] -> THCompile ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Type -> THCompile ()
addLiftDep [Type]
argTys

    -- We need the actual type parameters for the non-newtype case, and we have to do
    -- it out here, but it will give us redundant constraints in the newtype case,
    -- so we fudge it.
    [TExpQ CompileTypeScope]
tyExprs <- if DatatypeInfo -> Bool
isNewtype DatatypeInfo
dt then [TExpQ CompileTypeScope]
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [] else [TyVarBndr]
-> (TyVarBndr -> THCompile (TExpQ CompileTypeScope))
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [TyVarBndr]
tvs ((TyVarBndr -> THCompile (TExpQ CompileTypeScope))
 -> StateT
      Deps
      (ReaderT (Set Name) (ExceptT LiftError Q))
      [TExpQ CompileTypeScope])
-> (TyVarBndr -> THCompile (TExpQ CompileTypeScope))
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
forall a b. (a -> b) -> a -> b
$ \TyVarBndr
tv -> do
      (Name
n, Kind ()
_) <- TyVarBndr -> THCompile (Name, Kind ())
tvNameAndKind TyVarBndr
tv
      Type -> THCompile (TExpQ CompileTypeScope)
compileType (Name -> Type
TH.VarT Name
n)

    -- Build the patter for the clause definition. All the argument will be called "arg".
    [Name]
patNames <- ReaderT (Set Name) (ExceptT LiftError Q) [Name]
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) [Name]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ReaderT (Set Name) (ExceptT LiftError Q) [Name]
 -> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) [Name])
-> ReaderT (Set Name) (ExceptT LiftError Q) [Name]
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) [Name]
forall a b. (a -> b) -> a -> b
$ ExceptT LiftError Q [Name]
-> ReaderT (Set Name) (ExceptT LiftError Q) [Name]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ExceptT LiftError Q [Name]
 -> ReaderT (Set Name) (ExceptT LiftError Q) [Name])
-> ExceptT LiftError Q [Name]
-> ReaderT (Set Name) (ExceptT LiftError Q) [Name]
forall a b. (a -> b) -> a -> b
$ Q [Name] -> ExceptT LiftError Q [Name]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (Q [Name] -> ExceptT LiftError Q [Name])
-> Q [Name] -> ExceptT LiftError Q [Name]
forall a b. (a -> b) -> a -> b
$ [Type] -> (Type -> Q Name) -> Q [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Type]
argTys ((Type -> Q Name) -> Q [Name]) -> (Type -> Q Name) -> Q [Name]
forall a b. (a -> b) -> a -> b
$ \Type
_ -> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"arg"
    let pat :: PatQ
pat = Name -> [PatQ] -> PatQ
TH.conP Name
name ((Name -> PatQ) -> [Name] -> [PatQ]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> PatQ
TH.varP [Name]
patNames)

    -- `lift arg` for each arg we bind in the pattern. We need the `unsafeTExpCoerce` since this will
    -- necessarily involve types we don't know now: the types of each argument. However, since we
    -- know the type of `lift arg` we can get back into typed land quickly.
    let liftExprs :: [TH.TExpQ (RTCompile PLC.DefaultUni fun (Term TyName Name PLC.DefaultUni fun ()))]
        liftExprs :: [TExpQ
   (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))]
liftExprs = (Name
 -> TExpQ
      (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ())))
-> [Name]
-> [TExpQ
      (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Name
pn -> Q Exp
-> TExpQ
     (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))
forall a. Q Exp -> Q (TExp a)
TH.unsafeTExpCoerce (Q Exp
 -> TExpQ
      (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ())))
-> Q Exp
-> TExpQ
     (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))
forall a b. (a -> b) -> a -> b
$ Name -> Q Exp
TH.varE 'lift Q Exp -> Q Exp -> Q Exp
`TH.appE` Name -> Q Exp
TH.varE Name
pn) [Name]
patNames

    TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
rhsExpr <- if DatatypeInfo -> Bool
isNewtype DatatypeInfo
dt
            then case [TExpQ
   (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))]
forall fun.
[TExpQ
   (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))]
liftExprs of
                    [TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
argExpr] -> TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ
        (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ())))
forall (f :: * -> *) a. Applicative f => a -> f a
pure TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
argExpr
                    [TExpQ
   (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))]
_         -> LiftError
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ
        (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ())))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError
 -> StateT
      Deps
      (ReaderT (Set Name) (ExceptT LiftError Q))
      (TExpQ
         (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))))
-> LiftError
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ
        (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ())))
forall a b. (a -> b) -> a -> b
$ Text -> LiftError
UserLiftError Text
"Newtypes must have a single constructor with a single argument"
            else
                TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ
        (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ())))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ
   (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
 -> StateT
      Deps
      (ReaderT (Set Name) (ExceptT LiftError Q))
      (TExpQ
         (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))))
-> (TExpQ
      (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
    -> TExpQ
         (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ())))
-> TExpQ
     (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ
        (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ())))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
-> TExpQ
     (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
forall (m :: * -> *) a. Splice m a -> Splice m a
TH.examineSplice (TExpQ
   (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
 -> StateT
      Deps
      (ReaderT (Set Name) (ExceptT LiftError Q))
      (TExpQ
         (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))))
-> TExpQ
     (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
-> StateT
     Deps
     (ReaderT (Set Name) (ExceptT LiftError Q))
     (TExpQ
        (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ())))
forall a b. (a -> b) -> a -> b
$ [||
                    -- We bind all the splices with explicit signatures to ensure we
                    -- get type errors as soon as possible, and to aid debugging.
                    let
                        liftExprs' :: forall fun . [RTCompile PLC.DefaultUni fun (Term TyName Name PLC.DefaultUni fun ())]
                        liftExprs' = $$(TH.liftSplice $ tyListE liftExprs)
                        -- We need the `unsafeTExpCoerce` since this will necessarily involve
                        -- types we don't know now: the type which this instance is for (which
                        -- appears in the proxy argument). However, since we know the type of
                        -- `typeRep` we can get back into typed land quickly.
                        trep :: forall fun . RTCompile PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                        trep = $$(TH.unsafeSpliceCoerce [| typeRep (Proxy :: Proxy $(TH.conT tyName)) |])
                    in do
                        -- force creation of datatype
                        _ <- trep

                        -- get the right constructor
                        maybeConstructors <- lookupConstructors () tyName
                        constrs <- case maybeConstructors of
                            Nothing -> Prelude.throw $ LiftMissingDataCons tyName
                            Just cs -> pure cs
                        let constr = constrs !! index

                        lifts :: [Term TyName Name PLC.DefaultUni fun ()] <- sequence liftExprs'
                        -- The 'fun' that is referenced here is the 'fun' that we bind the line above.
                        -- If it was forall-bound instead, 'typeExprs\'' wouldn't type check,
                        -- because 'Type' does not determine 'fun' (unlike 'Term' in 'liftExprs\''
                        -- above).
                        let tyExprs' :: [RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())]
                            tyExprs' = fmap (\x -> unCompileTypeScope x) $$(TH.liftSplice $ tyListE tyExprs)
                        -- The types are compiled in an (empty) local scope.
                        types <- flip runReaderT mempty $ sequence tyExprs'

                        pure $ mkIterApp () (mkIterInst () constr types) lifts
                  ||]
    ClauseQ
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ClauseQ
 -> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ)
-> ClauseQ
-> StateT Deps (ReaderT (Set Name) (ExceptT LiftError Q)) ClauseQ
forall a b. (a -> b) -> a -> b
$ [PatQ] -> BodyQ -> [DecQ] -> ClauseQ
TH.clause [PatQ
pat] (Q Exp -> BodyQ
TH.normalB (Q Exp -> BodyQ) -> Q Exp -> BodyQ
forall a b. (a -> b) -> a -> b
$ TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
-> Q Exp
forall a. Q (TExp a) -> Q Exp
TH.unTypeQ TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
rhsExpr) []

makeLift :: TH.Name -> TH.Q [TH.Dec]
makeLift :: Name -> Q [Dec]
makeLift Name
name = do
    Extension -> Q ()
requireExtension Extension
TH.ScopedTypeVariables

    let uni :: Type
uni = Name -> Type
TH.ConT ''PLC.DefaultUni
    -- we need this too if we're lifting
    [Dec]
typeableDecs <- Type -> Name -> Q [Dec]
makeTypeable Type
uni Name
name
    DatatypeInfo
info <- Name -> Q DatatypeInfo
TH.reifyDatatype Name
name

    let datatypeType :: Type
datatypeType = DatatypeInfo -> Type
TH.datatypeType DatatypeInfo
info

    ([ClauseQ]
clauses, Deps
deps) <- THCompile [ClauseQ] -> Q ([ClauseQ], Deps)
forall a. THCompile a -> Q (a, Deps)
runTHCompile (THCompile [ClauseQ] -> Q ([ClauseQ], Deps))
-> THCompile [ClauseQ] -> Q ([ClauseQ], Deps)
forall a b. (a -> b) -> a -> b
$ DatatypeInfo -> THCompile [ClauseQ]
compileLift DatatypeInfo
info

    {-
    Here we *do* need to add some constraints, because we're going to generate things like
    `instance Lift a => Lift (Maybe a)`. We can't just leave these open because they refer to type variables.

    We *could* put in a Typeable constraint for the type itself. This is somewhat more correct,
    but GHC warns us if we do this because we always also define the instance alongside. So we just
    leave it out.

    We also need to remove any Lift constraints we get for the type we're defining. This can happen if
    we're recursive, since we'll probably end up with constructor arguments of the current type.
    We don't want `instance Lift [a] => Lift [a]`!
    -}
    let prunedDeps :: Deps
prunedDeps = Dep -> Deps -> Deps
forall a. Ord a => a -> Set a -> Set a
Set.delete (Type -> Dep
LiftDep Type
datatypeType) Deps
deps
    -- See Note [Closed constraints]
    let constraints :: [Type]
constraints = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isClosedConstraint) ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Type -> Dep -> Type
toConstraint Type
uni (Dep -> Type) -> [Dep] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Deps -> [Dep]
forall a. Set a -> [a]
Set.toList Deps
prunedDeps

    Dec
decl <- Name -> [ClauseQ] -> DecQ
TH.funD 'lift [ClauseQ]
clauses
    let liftDecs :: [Dec]
liftDecs = [Maybe Overlap -> [Type] -> Type -> [Dec] -> Dec
TH.InstanceD Maybe Overlap
forall a. Maybe a
Nothing [Type]
constraints (Type -> Type -> Type
liftPir Type
uni Type
datatypeType) [Dec
decl]]
    [Dec] -> Q [Dec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [Dec]
typeableDecs [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
liftDecs

-- | In case of exception, it will call `fail` in TemplateHaskell
runTHCompile :: THCompile a -> TH.Q (a, Deps)
runTHCompile :: THCompile a -> Q (a, Deps)
runTHCompile THCompile a
m = do
    Either LiftError (a, Deps)
res <- ExceptT LiftError Q (a, Deps) -> Q (Either LiftError (a, Deps))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT LiftError Q (a, Deps) -> Q (Either LiftError (a, Deps)))
-> (ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
    -> ExceptT LiftError Q (a, Deps))
-> ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
-> Q (Either LiftError (a, Deps))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          (ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
 -> Set Name -> ExceptT LiftError Q (a, Deps))
-> Set Name
-> ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
-> ExceptT LiftError Q (a, Deps)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
-> Set Name -> ExceptT LiftError Q (a, Deps)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Set Name
forall a. Monoid a => a
mempty (ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
 -> Q (Either LiftError (a, Deps)))
-> ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
-> Q (Either LiftError (a, Deps))
forall a b. (a -> b) -> a -> b
$
          (THCompile a
 -> Deps -> ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps))
-> Deps
-> THCompile a
-> ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
forall a b c. (a -> b -> c) -> b -> a -> c
flip THCompile a
-> Deps -> ReaderT (Set Name) (ExceptT LiftError Q) (a, Deps)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Deps
forall a. Monoid a => a
mempty THCompile a
m
    case Either LiftError (a, Deps)
res of
        Left LiftError
a  -> String -> Q (a, Deps)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q (a, Deps)) -> String -> Q (a, Deps)
forall a b. (a -> b) -> a -> b
$ String
"Generating Lift instances: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (LiftError -> Doc Any
forall a ann. Pretty a => a -> Doc ann
PP.pretty LiftError
a)
        Right (a, Deps)
b -> (a, Deps) -> Q (a, Deps)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a, Deps)
b