-- editorconfig-checker-disable-file
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
module PlutusTx.Lift (
    makeLift,
    safeLift,
    safeLiftProgram,
    safeLiftCode,
    lift,
    liftProgram,
    liftProgramDef,
    liftCode,
    typeCheckAgainst,
    typeCode) where

import PlutusTx.Code
import PlutusTx.Lift.Class (makeLift)
import PlutusTx.Lift.Class qualified as Lift
import PlutusTx.Lift.Instances ()

import Data.Bifunctor
import PlutusIR
import PlutusIR qualified as PIR
import PlutusIR.Compiler
import PlutusIR.Compiler.Definitions
import PlutusIR.Error qualified as PIR
import PlutusIR.MkPir qualified as PIR

import PlutusCore qualified as PLC
import PlutusCore.Compiler qualified as PLC
import PlutusCore.Pretty (PrettyConst)
import PlutusCore.Quote
import PlutusCore.StdLib.Data.Function qualified as PLC

import UntypedPlutusCore qualified as UPLC

import Control.Exception
import Control.Lens hiding (lifted)
import Control.Monad.Except hiding (lift)
import Control.Monad.Reader hiding (lift)

import Data.Proxy
import Data.Typeable qualified as GHC
import Prettyprinter

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

type PrettyPrintable uni fun = (Pretty (PLC.SomeTypeIn uni), PLC.Closed uni, uni `PLC.Everywhere` PrettyConst, Pretty fun)

type Throwable uni fun =
    ( Pretty (PLC.SomeTypeIn uni), PLC.GEq uni, PLC.Closed uni, uni `PLC.Everywhere` PrettyConst, GHC.Typeable uni
    , Pretty fun, GHC.Typeable fun
    )

-- | Get a Plutus Core term corresponding to the given value.
safeLift
    :: (Lift.Lift uni a
       , PIR.AsTypeError e (PIR.Term TyName Name uni fun ()) uni fun (Provenance ()), PLC.GEq uni
       , PIR.AsTypeErrorExt e uni (Provenance ())
       , PLC.AsFreeVariableError e
       , AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m
       , PLC.Typecheckable uni fun
       , PrettyPrintable uni fun
       )
    => a -> m (UPLC.Term UPLC.NamedDeBruijn uni fun ())
safeLift :: forall (uni :: * -> *) a e fun (m :: * -> *).
(Lift uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 GEq uni, AsTypeErrorExt e uni (Provenance ()),
 AsFreeVariableError e, AsError e uni fun (Provenance ()),
 MonadError e m, MonadQuote m, Typecheckable uni fun,
 PrettyPrintable uni fun) =>
a -> m (Term NamedDeBruijn uni fun ())
safeLift a
x = do
    Term TyName Name uni fun ()
lifted <- forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) key ann (uni :: * -> *) fun.
(Monad m, Ord key) =>
ann
-> DefT key uni fun ann m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
runDefT () forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) a fun.
Lift uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
Lift.lift a
x
    TypeCheckConfig uni fun
tcConfig <- forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
PLC.getDefTypeCheckConfig forall a b. (a -> b) -> a -> b
$ forall a. a -> Provenance a
Original ()
    -- NOTE:  Disabling simplifier, as it takes a lot of time during runtime
    let ccConfig :: CompilationCtx uni fun a
ccConfig = forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (CompilationOpts a) Int
coMaxSimplifierIterations) Int
0 (forall fun (uni :: * -> *) a.
Default (BuiltinVersion fun) =>
TypeCheckConfig uni fun -> CompilationCtx uni fun a
toDefaultCompilationCtx TypeCheckConfig uni fun
tcConfig)
        ucOpts :: CompilationOpts name a
ucOpts = forall name a. CompilationOpts name a
PLC.defaultCompilationOpts forall a b. a -> (a -> b) -> b
& forall name1 a1 name2 a2.
Iso
  (CompilationOpts name1 a1)
  (CompilationOpts name2 a2)
  (SimplifyOpts name1 a1)
  (SimplifyOpts name2 a2)
PLC.coSimplifyOpts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Lens' (SimplifyOpts name a) Int
UPLC.soMaxSimplifierIterations forall s t a b. ASetter s t a b -> b -> s -> t
.~ Int
0
    PLCTerm uni fun ()
plc <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT forall {a}. CompilationCtx uni fun a
ccConfig forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Term TyName Name uni fun a -> m (PLCTerm uni fun a)
compileTerm Term TyName Name uni fun ()
lifted
    Term Name uni fun (Provenance ())
uplc <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT forall name a. CompilationOpts name a
ucOpts forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) fun (m :: * -> *) name a tyname.
(ToBuiltinMeaning uni fun, MonadQuote m, HasUnique name TermUnique,
 Eq name, MonadReader (CompilationOpts name a) m) =>
Term tyname name uni fun a -> m (Term name uni fun a)
PLC.compileTerm PLCTerm uni fun ()
plc
    Term NamedDeBruijn uni fun (Provenance ())
db <- forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
UPLC.deBruijnTerm Term Name uni fun (Provenance ())
uplc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f a -> f ()
void Term NamedDeBruijn uni fun (Provenance ())
db

-- | Get a Plutus Core program corresponding to the given value.
safeLiftProgram
    :: (Lift.Lift uni a
       , PIR.AsTypeError e (PIR.Term TyName Name uni fun ()) uni fun (Provenance ()),  PLC.GEq uni
       , PIR.AsTypeErrorExt e uni (Provenance ())
       , PLC.AsFreeVariableError e
       , AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m
       , PLC.Typecheckable uni fun
       , PrettyPrintable uni fun
       )
    => a -> m (UPLC.Program UPLC.NamedDeBruijn uni fun ())
safeLiftProgram :: forall (uni :: * -> *) a e fun (m :: * -> *).
(Lift uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 GEq uni, AsTypeErrorExt e uni (Provenance ()),
 AsFreeVariableError e, AsError e uni fun (Provenance ()),
 MonadError e m, MonadQuote m, Typecheckable uni fun,
 PrettyPrintable uni fun) =>
a -> m (Program NamedDeBruijn uni fun ())
safeLiftProgram a
x = forall name (uni :: * -> *) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
UPLC.Program () (forall ann. ann -> Version ann
PLC.defaultVersion ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (uni :: * -> *) a e fun (m :: * -> *).
(Lift uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 GEq uni, AsTypeErrorExt e uni (Provenance ()),
 AsFreeVariableError e, AsError e uni fun (Provenance ()),
 MonadError e m, MonadQuote m, Typecheckable uni fun,
 PrettyPrintable uni fun) =>
a -> m (Term NamedDeBruijn uni fun ())
safeLift a
x

safeLiftCode
    :: (Lift.Lift uni a
       , PIR.AsTypeError e (PIR.Term TyName Name uni fun ()) uni fun (Provenance ()), PLC.GEq uni
       , PIR.AsTypeErrorExt e uni (Provenance ())
       , PLC.AsFreeVariableError e
       , AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m
       , PLC.Typecheckable uni fun
       , PrettyPrintable uni fun
       )
    => a -> m (CompiledCodeIn uni fun a)
safeLiftCode :: forall (uni :: * -> *) a e fun (m :: * -> *).
(Lift uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 GEq uni, AsTypeErrorExt e uni (Provenance ()),
 AsFreeVariableError e, AsError e uni fun (Provenance ()),
 MonadError e m, MonadQuote m, Typecheckable uni fun,
 PrettyPrintable uni fun) =>
a -> m (CompiledCodeIn uni fun a)
safeLiftCode a
x = forall (uni :: * -> *) fun a.
Program NamedDeBruijn uni fun ()
-> Maybe (Program TyName Name uni fun ())
-> CoverageIndex
-> CompiledCodeIn uni fun a
DeserializedCode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (uni :: * -> *) a e fun (m :: * -> *).
(Lift uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 GEq uni, AsTypeErrorExt e uni (Provenance ()),
 AsFreeVariableError e, AsError e uni fun (Provenance ()),
 MonadError e m, MonadQuote m, Typecheckable uni fun,
 PrettyPrintable uni fun) =>
a -> m (Program NamedDeBruijn uni fun ())
safeLiftProgram a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty

unsafely
    :: Throwable uni fun
    => ExceptT (Error uni fun (Provenance ())) Quote a -> a
unsafely :: forall (uni :: * -> *) fun a.
Throwable uni fun =>
ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a -> a
unsafely ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a
ma = forall a. Quote a -> a
runQuote forall a b. (a -> b) -> a -> b
$ do
    Either (Error uni fun (Provenance ())) a
run <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a
ma
    case Either (Error uni fun (Provenance ())) a
run of
        Left Error uni fun (Provenance ())
e  -> forall a e. Exception e => e -> a
throw Error uni fun (Provenance ())
e
        Right a
t -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t

-- | Get a Plutus Core term corresponding to the given value, throwing any errors that occur as exceptions and ignoring fresh names.
lift
    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun)
    => a -> UPLC.Term UPLC.NamedDeBruijn uni fun ()
lift :: forall (uni :: * -> *) a fun.
(Lift uni a, Throwable uni fun, Typecheckable uni fun) =>
a -> Term NamedDeBruijn uni fun ()
lift a
a = forall (uni :: * -> *) fun a.
Throwable uni fun =>
ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a -> a
unsafely forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) a e fun (m :: * -> *).
(Lift uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 GEq uni, AsTypeErrorExt e uni (Provenance ()),
 AsFreeVariableError e, AsError e uni fun (Provenance ()),
 MonadError e m, MonadQuote m, Typecheckable uni fun,
 PrettyPrintable uni fun) =>
a -> m (Term NamedDeBruijn uni fun ())
safeLift a
a

-- | Get a Plutus Core program corresponding to the given value, throwing any errors that occur as exceptions and ignoring fresh names.
liftProgram
    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun)
    => a -> UPLC.Program UPLC.NamedDeBruijn uni fun ()
liftProgram :: forall (uni :: * -> *) a fun.
(Lift uni a, Throwable uni fun, Typecheckable uni fun) =>
a -> Program NamedDeBruijn uni fun ()
liftProgram a
x = forall name (uni :: * -> *) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
UPLC.Program () (forall ann. ann -> Version ann
PLC.defaultVersion ()) forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) a fun.
(Lift uni a, Throwable uni fun, Typecheckable uni fun) =>
a -> Term NamedDeBruijn uni fun ()
lift a
x

-- | Get a Plutus Core program in the default universe corresponding to the given value, throwing any errors that occur as exceptions and ignoring fresh names.
liftProgramDef
    :: Lift.Lift PLC.DefaultUni a
    => a -> UPLC.Program UPLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ()
liftProgramDef :: forall a.
Lift DefaultUni a =>
a -> Program NamedDeBruijn DefaultUni DefaultFun ()
liftProgramDef = forall (uni :: * -> *) a fun.
(Lift uni a, Throwable uni fun, Typecheckable uni fun) =>
a -> Program NamedDeBruijn uni fun ()
liftProgram

-- | Get a Plutus Core program corresponding to the given value as a 'CompiledCodeIn', throwing any errors that occur as exceptions and ignoring fresh names.
liftCode
    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun)
    => a -> CompiledCodeIn uni fun a
liftCode :: forall (uni :: * -> *) a fun.
(Lift uni a, Throwable uni fun, Typecheckable uni fun) =>
a -> CompiledCodeIn uni fun a
liftCode a
x = forall (uni :: * -> *) fun a.
Throwable uni fun =>
ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a -> a
unsafely forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) a e fun (m :: * -> *).
(Lift uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 GEq uni, AsTypeErrorExt e uni (Provenance ()),
 AsFreeVariableError e, AsError e uni fun (Provenance ()),
 MonadError e m, MonadQuote m, Typecheckable uni fun,
 PrettyPrintable uni fun) =>
a -> m (CompiledCodeIn uni fun a)
safeLiftCode a
x

{- Note [Checking the type of a term with Typeable]
Checking the type of a term should be simple, right? We can just use 'checkType', easy peasy.

Not so fast - Typeable gives us a PLC type corresponding to a Haskell type, but *inside the PIR Def monad*.
This is because it might have type definitions that it refers to, and we use the standard machinery for that.
We can only discharge the Def monad into a *term*, because of course we have to turn those definitions into
let bindings.

So we don't have access to the type directly, annoyingly. Instead, we can construct a term that typechecks
iff the original term has the given type. We opt for `(\x : <the type> -> x) term`.
-}

-- | Check that PLC term has the given type.
typeCheckAgainst
    :: forall e a uni fun m .
       ( Lift.Typeable uni a
       , PIR.AsTypeError e (PIR.Term TyName Name uni fun ()) uni fun (Provenance ())
       , PIR.AsTypeErrorExt e uni (Provenance ())
       , PIR.AsError e uni fun (Provenance ())
       , MonadError e m, MonadQuote m
       , PLC.GEq uni
       , PLC.Typecheckable uni fun
       , PrettyPrintable uni fun
       )
    => Proxy a
    -> PLC.Term PLC.TyName PLC.Name uni fun ()
    -> m ()
typeCheckAgainst :: forall e a (uni :: * -> *) fun (m :: * -> *).
(Typeable uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 AsTypeErrorExt e uni (Provenance ()),
 AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m,
 GEq uni, Typecheckable uni fun, PrettyPrintable uni fun) =>
Proxy a -> Term TyName Name uni fun () -> m ()
typeCheckAgainst Proxy a
p Term TyName Name uni fun ()
plcTerm = do
    -- See Note [Checking the type of a term with Typeable]
    Term TyName Name uni fun ()
term <- forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
PIR.embed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
PLC.rename Term TyName Name uni fun ()
plcTerm
    -- We need to run Def *before* applying to the term, otherwise we may refer to abstract
    -- types and we won't match up with the term.
    Term TyName Name uni fun ()
idFun <- forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) key ann (uni :: * -> *) fun.
(Monad m, Ord key) =>
ann
-> DefT key uni fun ann m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
runDefT () forall a b. (a -> b) -> a -> b
$ do
        Type TyName uni ()
ty <- forall k (uni :: * -> *) (a :: k) fun.
Typeable uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
Lift.typeRep Proxy a
p
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
PLC.idFun Type TyName uni ()
ty
    let applied :: Term TyName Name uni fun ()
applied = forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name uni fun ()
idFun Term TyName Name uni fun ()
term
    -- Here we use a 'Default' builtin version, because the typechecker needs
    -- to be handed a builtin version (implementation detail).
    -- See Note [Versioned builtins]
    TypeCheckConfig uni fun
tcConfig <- forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
PLC.getDefTypeCheckConfig (forall a. a -> Provenance a
Original ())
    -- The PIR compiler *pointfully* needs a builtin version, but in this instance of only "lifting"
    -- it is safe to default to any builtin version, since the 'Lift'
    -- is impervious to builtins and will not generate code containing builtins.
    -- See Note [Versioned builtins]
    PLCTerm uni fun ()
compiled <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall fun (uni :: * -> *) a.
Default (BuiltinVersion fun) =>
TypeCheckConfig uni fun -> CompilationCtx uni fun a
toDefaultCompilationCtx TypeCheckConfig uni fun
tcConfig) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Term TyName Name uni fun a -> m (PLCTerm uni fun a)
compileTerm Term TyName Name uni fun ()
applied
    -- PLC errors are parameterized over PLC.Terms, whereas PIR errors over PIR.Terms and as such, these prism errors cannot be unified.
    -- We instead run the ExceptT, collect any PLC error and explicitly lift into a PIR error by wrapping with PIR._PLCError
    Either (Error uni fun (Provenance ())) ()
plcConcrete <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
PLC.inferType TypeCheckConfig uni fun
tcConfig PLCTerm uni fun ()
compiled
    -- note: e is a scoped tyvar acting here AsError e uni (Provenance ())
    let plcPrismatic :: Either e ()
plcPrismatic = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (forall t b. AReview t b -> Getter b t
re forall r (uni :: * -> *) fun a.
AsError r uni fun a =>
Prism' r (Error uni fun a)
PIR._PLCError)) Either (Error uni fun (Provenance ())) ()
plcConcrete
    forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither Either e ()
plcPrismatic -- embed prismatic-either to a monaderror

-- | Try to interpret a PLC program as a 'CompiledCodeIn' of the given type. Returns successfully iff the program has the right type.
typeCode
    :: forall e a uni fun m .
       ( Lift.Typeable uni a
       , PIR.AsTypeError e (PIR.Term TyName Name uni fun ()) uni fun (Provenance ())
       , PIR.AsTypeErrorExt e uni (Provenance ())
       , PLC.AsFreeVariableError e
       , PIR.AsError e uni fun (Provenance ())
       , MonadError e m, MonadQuote m
       , PLC.GEq uni
       , PLC.Typecheckable uni fun
       , PrettyPrintable uni fun
       )
    => Proxy a
    -> PLC.Program PLC.TyName PLC.Name uni fun ()
    -> m (CompiledCodeIn uni fun a)
typeCode :: forall e a (uni :: * -> *) fun (m :: * -> *).
(Typeable uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 AsTypeErrorExt e uni (Provenance ()), AsFreeVariableError e,
 AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m,
 GEq uni, Typecheckable uni fun, PrettyPrintable uni fun) =>
Proxy a
-> Program TyName Name uni fun () -> m (CompiledCodeIn uni fun a)
typeCode Proxy a
p prog :: Program TyName Name uni fun ()
prog@(PLC.Program ()
_ Version ()
_ Term TyName Name uni fun ()
term) = do
    ()
_ <- forall e a (uni :: * -> *) fun (m :: * -> *).
(Typeable uni a,
 AsTypeError
   e (Term TyName Name uni fun ()) uni fun (Provenance ()),
 AsTypeErrorExt e uni (Provenance ()),
 AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m,
 GEq uni, Typecheckable uni fun, PrettyPrintable uni fun) =>
Proxy a -> Term TyName Name uni fun () -> m ()
typeCheckAgainst Proxy a
p Term TyName Name uni fun ()
term
    Program Name uni fun ()
compiled <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT forall name a. CompilationOpts name a
PLC.defaultCompilationOpts forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) fun (m :: * -> *) name a tyname.
(ToBuiltinMeaning uni fun, MonadQuote m, HasUnique name TermUnique,
 Eq name, MonadReader (CompilationOpts name a) m) =>
Program tyname name uni fun a -> m (Program name uni fun a)
PLC.compileProgram Program TyName Name uni fun ()
prog
    Program NamedDeBruijn uni fun ()
db <- forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf forall name1 (uni1 :: * -> *) fun1 ann name2 (uni2 :: * -> *) fun2.
Lens
  (Program name1 uni1 fun1 ann)
  (Program name2 uni2 fun2 ann)
  (Term name1 uni1 fun1 ann)
  (Term name2 uni2 fun2 ann)
UPLC.progTerm forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
UPLC.deBruijnTerm Program Name uni fun ()
compiled
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) fun a.
Program NamedDeBruijn uni fun ()
-> Maybe (Program TyName Name uni fun ())
-> CoverageIndex
-> CompiledCodeIn uni fun a
DeserializedCode Program NamedDeBruijn uni fun ()
db forall a. Maybe a
Nothing forall a. Monoid a => a
mempty