{-# 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.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 = ( PLC.GShow uni, PLC.Closed uni, uni `PLC.Everywhere` PrettyConst, Pretty fun)

type Throwable uni fun =
    ( PLC.GShow 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 :: a -> m (Term NamedDeBruijn uni fun ())
safeLift a
x = do
    Term TyName Name uni fun ()
lifted <- Quote (Term TyName Name uni fun ())
-> m (Term TyName Name uni fun ())
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Term TyName Name uni fun ())
 -> m (Term TyName Name uni fun ()))
-> Quote (Term TyName Name uni fun ())
-> m (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ ()
-> DefT Name uni fun () Quote (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
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 () (DefT Name uni fun () Quote (Term TyName Name uni fun ())
 -> Quote (Term TyName Name uni fun ()))
-> DefT Name uni fun () Quote (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ a -> DefT Name uni fun () Quote (Term TyName Name uni fun ())
forall (uni :: * -> *) a fun.
Lift uni a =>
a -> RTCompile uni fun (Term TyName Name uni fun ())
Lift.lift a
x
    TypeCheckConfig uni fun
tcConfig <- Provenance () -> m (TypeCheckConfig uni fun)
forall err (m :: * -> *) term (uni :: * -> *) fun ann.
(MonadError err m, AsTypeError err term uni fun ann,
 Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
PLC.getDefTypeCheckConfig (Provenance () -> m (TypeCheckConfig uni fun))
-> Provenance () -> m (TypeCheckConfig uni fun)
forall a b. (a -> b) -> a -> b
$ () -> Provenance ()
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 = ASetter
  (CompilationCtx uni fun a) (CompilationCtx uni fun a) Int Int
-> Int -> CompilationCtx uni fun a -> CompilationCtx uni fun a
forall s t a b. ASetter s t a b -> b -> s -> t
set ((CompilationOpts a -> Identity (CompilationOpts a))
-> CompilationCtx uni fun a -> Identity (CompilationCtx uni fun a)
forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts ((CompilationOpts a -> Identity (CompilationOpts a))
 -> CompilationCtx uni fun a -> Identity (CompilationCtx uni fun a))
-> ((Int -> Identity Int)
    -> CompilationOpts a -> Identity (CompilationOpts a))
-> ASetter
     (CompilationCtx uni fun a) (CompilationCtx uni fun a) Int Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Identity Int)
-> CompilationOpts a -> Identity (CompilationOpts a)
forall a. Lens' (CompilationOpts a) Int
coMaxSimplifierIterations) Int
0 (TypeCheckConfig uni fun -> CompilationCtx uni fun a
forall (uni :: * -> *) fun a.
TypeCheckConfig uni fun -> CompilationCtx uni fun a
toDefaultCompilationCtx TypeCheckConfig uni fun
tcConfig)
        usOpts :: SimplifyOpts a
usOpts = ASetter (SimplifyOpts a) (SimplifyOpts a) Int Int
-> Int -> SimplifyOpts a -> SimplifyOpts a
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (SimplifyOpts a) (SimplifyOpts a) Int Int
forall a. Lens' (SimplifyOpts a) Int
UPLC.soMaxSimplifierIterations Int
0 SimplifyOpts a
forall a. SimplifyOpts a
UPLC.defaultSimplifyOpts
    PLCTerm uni fun ()
compiled <- (ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
 -> CompilationCtx uni fun () -> m (PLCTerm uni fun ()))
-> CompilationCtx uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
-> m (PLCTerm uni fun ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
-> CompilationCtx uni fun () -> m (PLCTerm uni fun ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CompilationCtx uni fun ()
forall a. CompilationCtx uni fun a
ccConfig (ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
 -> m (PLCTerm uni fun ()))
-> ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
-> m (PLCTerm uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
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
    let erased :: Term Name uni fun (Provenance ())
erased = PLCTerm uni fun () -> Term Name uni fun (Provenance ())
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
UPLC.erase PLCTerm uni fun ()
compiled
    Term NamedDeBruijn uni fun (Provenance ())
db <- Term Name uni fun (Provenance ())
-> m (Term NamedDeBruijn uni fun (Provenance ()))
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 ())
 -> m (Term NamedDeBruijn uni fun (Provenance ())))
-> m (Term Name uni fun (Provenance ()))
-> m (Term NamedDeBruijn uni fun (Provenance ()))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SimplifyOpts (Provenance ())
-> Term Name uni fun (Provenance ())
-> m (Term Name uni fun (Provenance ()))
forall (uni :: * -> *) fun (m :: * -> *) a.
(ToBuiltinMeaning uni fun, MonadQuote m) =>
SimplifyOpts a -> Term Name uni fun a -> m (Term Name uni fun a)
UPLC.simplifyTerm SimplifyOpts (Provenance ())
forall a. SimplifyOpts a
usOpts Term Name uni fun (Provenance ())
erased
    Term NamedDeBruijn uni fun () -> m (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedDeBruijn uni fun ()
 -> m (Term NamedDeBruijn uni fun ()))
-> Term NamedDeBruijn uni fun ()
-> m (Term NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ Term NamedDeBruijn uni fun (Provenance ())
-> Term NamedDeBruijn uni fun ()
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 :: a -> m (Program NamedDeBruijn uni fun ())
safeLiftProgram a
x = ()
-> Version ()
-> Term NamedDeBruijn uni fun ()
-> Program NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
UPLC.Program () (() -> Version ()
forall ann. ann -> Version ann
PLC.defaultVersion ()) (Term NamedDeBruijn uni fun () -> Program NamedDeBruijn uni fun ())
-> m (Term NamedDeBruijn uni fun ())
-> m (Program NamedDeBruijn uni fun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (Term NamedDeBruijn uni fun ())
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 :: a -> m (CompiledCodeIn uni fun a)
safeLiftCode a
x = Program NamedDeBruijn uni fun ()
-> Maybe (Program TyName Name uni fun ())
-> CoverageIndex
-> CompiledCodeIn uni fun a
forall (uni :: * -> *) fun a.
Program NamedDeBruijn uni fun ()
-> Maybe (Program TyName Name uni fun ())
-> CoverageIndex
-> CompiledCodeIn uni fun a
DeserializedCode (Program NamedDeBruijn uni fun ()
 -> Maybe (Program TyName Name uni fun ())
 -> CoverageIndex
 -> CompiledCodeIn uni fun a)
-> m (Program NamedDeBruijn uni fun ())
-> m (Maybe (Program TyName Name uni fun ())
      -> CoverageIndex -> CompiledCodeIn uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (Program NamedDeBruijn uni fun ())
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 m (Maybe (Program TyName Name uni fun ())
   -> CoverageIndex -> CompiledCodeIn uni fun a)
-> m (Maybe (Program TyName Name uni fun ()))
-> m (CoverageIndex -> CompiledCodeIn uni fun a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (Program TyName Name uni fun ())
-> m (Maybe (Program TyName Name uni fun ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Program TyName Name uni fun ())
forall a. Maybe a
Nothing m (CoverageIndex -> CompiledCodeIn uni fun a)
-> m CoverageIndex -> m (CompiledCodeIn uni fun a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoverageIndex -> m CoverageIndex
forall (f :: * -> *) a. Applicative f => a -> f a
pure CoverageIndex
forall a. Monoid a => a
mempty

unsafely
    :: Throwable uni fun
    => ExceptT (Error uni fun (Provenance ())) Quote a -> a
unsafely :: ExceptT (Error uni fun (Provenance ())) Quote a -> a
unsafely ExceptT (Error uni fun (Provenance ())) Quote a
ma = Quote a -> a
forall a. Quote a -> a
runQuote (Quote a -> a) -> Quote a -> a
forall a b. (a -> b) -> a -> b
$ do
    Either (Error uni fun (Provenance ())) a
run <- ExceptT (Error uni fun (Provenance ())) Quote a
-> Quote (Either (Error uni fun (Provenance ())) a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT (Error uni fun (Provenance ())) Quote a
ma
    case Either (Error uni fun (Provenance ())) a
run of
        Left Error uni fun (Provenance ())
e  -> Error uni fun (Provenance ()) -> Quote a
forall a e. Exception e => e -> a
throw Error uni fun (Provenance ())
e
        Right a
t -> a -> Quote a
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 :: a -> Term NamedDeBruijn uni fun ()
lift a
a = ExceptT
  (Error uni fun (Provenance ()))
  Quote
  (Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun a.
Throwable uni fun =>
ExceptT (Error uni fun (Provenance ())) Quote a -> a
unsafely (ExceptT
   (Error uni fun (Provenance ()))
   Quote
   (Term NamedDeBruijn uni fun ())
 -> Term NamedDeBruijn uni fun ())
-> ExceptT
     (Error uni fun (Provenance ()))
     Quote
     (Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ a
-> ExceptT
     (Error uni fun (Provenance ()))
     Quote
     (Term NamedDeBruijn uni fun ())
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 :: a -> Program NamedDeBruijn uni fun ()
liftProgram a
x = ()
-> Version ()
-> Term NamedDeBruijn uni fun ()
-> Program NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
UPLC.Program () (() -> Version ()
forall ann. ann -> Version ann
PLC.defaultVersion ()) (Term NamedDeBruijn uni fun () -> Program NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun ()
-> Program NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ a -> Term NamedDeBruijn uni fun ()
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 :: a -> Program NamedDeBruijn DefaultUni DefaultFun ()
liftProgramDef = a -> Program NamedDeBruijn DefaultUni DefaultFun ()
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 :: a -> CompiledCodeIn uni fun a
liftCode a
x = ExceptT
  (Error uni fun (Provenance ())) Quote (CompiledCodeIn uni fun a)
-> CompiledCodeIn uni fun a
forall (uni :: * -> *) fun a.
Throwable uni fun =>
ExceptT (Error uni fun (Provenance ())) Quote a -> a
unsafely (ExceptT
   (Error uni fun (Provenance ())) Quote (CompiledCodeIn uni fun a)
 -> CompiledCodeIn uni fun a)
-> ExceptT
     (Error uni fun (Provenance ())) Quote (CompiledCodeIn uni fun a)
-> CompiledCodeIn uni fun a
forall a b. (a -> b) -> a -> b
$ a
-> ExceptT
     (Error uni fun (Provenance ())) Quote (CompiledCodeIn uni fun a)
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 :: 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 <- Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
PIR.embed (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> m (Term TyName Name uni fun ())
-> m (Term TyName Name uni fun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
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 <- Quote (Term TyName Name uni fun ())
-> m (Term TyName Name uni fun ())
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Term TyName Name uni fun ())
 -> m (Term TyName Name uni fun ()))
-> Quote (Term TyName Name uni fun ())
-> m (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ ()
-> DefT Name uni fun () Quote (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
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 () (DefT Name uni fun () Quote (Term TyName Name uni fun ())
 -> Quote (Term TyName Name uni fun ()))
-> DefT Name uni fun () Quote (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ do
        Type TyName uni ()
ty <- 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 ())
Lift.typeRep Proxy a
p
        Term TyName Name uni fun ()
-> DefT Name uni fun () Quote (Term TyName Name uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ()
 -> DefT Name uni fun () Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> DefT Name uni fun () Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name uni fun ()
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 = ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
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
    TypeCheckConfig uni fun
tcConfig <- Provenance () -> m (TypeCheckConfig uni fun)
forall err (m :: * -> *) term (uni :: * -> *) fun ann.
(MonadError err m, AsTypeError err term uni fun ann,
 Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
PLC.getDefTypeCheckConfig (() -> Provenance ()
forall a. a -> Provenance a
Original ())
    PLCTerm uni fun ()
compiled <- (ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
 -> CompilationCtx uni fun () -> m (PLCTerm uni fun ()))
-> CompilationCtx uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
-> m (PLCTerm uni fun ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
-> CompilationCtx uni fun () -> m (PLCTerm uni fun ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (TypeCheckConfig uni fun -> CompilationCtx uni fun ()
forall (uni :: * -> *) fun a.
TypeCheckConfig uni fun -> CompilationCtx uni fun a
toDefaultCompilationCtx TypeCheckConfig uni fun
tcConfig) (ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
 -> m (PLCTerm uni fun ()))
-> ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
-> m (PLCTerm uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCTerm uni fun ())
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 <- ExceptT (Error uni fun (Provenance ())) m ()
-> m (Either (Error uni fun (Provenance ())) ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT (Error uni fun (Provenance ())) m ()
 -> m (Either (Error uni fun (Provenance ())) ()))
-> ExceptT (Error uni fun (Provenance ())) m ()
-> m (Either (Error uni fun (Provenance ())) ())
forall a b. (a -> b) -> a -> b
$ ExceptT
  (Error uni fun (Provenance ())) m (Normalized (Type TyName uni ()))
-> ExceptT (Error uni fun (Provenance ())) m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ExceptT
   (Error uni fun (Provenance ())) m (Normalized (Type TyName uni ()))
 -> ExceptT (Error uni fun (Provenance ())) m ())
-> ExceptT
     (Error uni fun (Provenance ())) m (Normalized (Type TyName uni ()))
-> ExceptT (Error uni fun (Provenance ())) m ()
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig uni fun
-> PLCTerm uni fun ()
-> ExceptT
     (Error uni fun (Provenance ())) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
(MonadError err m, MonadQuote m,
 AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, GEq uni, Ix fun) =>
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 = (Error uni fun (Provenance ()) -> e)
-> Either (Error uni fun (Provenance ())) () -> Either e ()
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Getting e (Error uni fun (Provenance ())) e
-> Error uni fun (Provenance ()) -> e
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (AReview e (Error uni fun (Provenance ()))
-> Getter (Error uni fun (Provenance ())) e
forall t b. AReview t b -> Getter b t
re AReview e (Error uni fun (Provenance ()))
forall r (uni :: * -> *) fun a.
AsError r uni fun a =>
Prism' r (Error uni fun a)
PIR._PLCError)) Either (Error uni fun (Provenance ())) ()
plcConcrete
    Either e () -> m ()
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 :: 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
    ()
_ <- Proxy a -> Term TyName Name uni fun () -> m ()
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
    let erased :: Program Name uni fun ()
erased = Program TyName Name uni fun () -> Program Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
Program tyname name uni fun ann -> Program name uni fun ann
UPLC.eraseProgram Program TyName Name uni fun ()
prog
    Program NamedDeBruijn uni fun ()
db <-  LensLike
  m
  (Program Name uni fun ())
  (Program NamedDeBruijn uni fun ())
  (Term Name uni fun ())
  (Term NamedDeBruijn uni fun ())
-> LensLike
     m
     (Program Name uni fun ())
     (Program NamedDeBruijn uni fun ())
     (Term Name uni fun ())
     (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike
  m
  (Program Name uni fun ())
  (Program NamedDeBruijn uni fun ())
  (Term Name uni fun ())
  (Term NamedDeBruijn uni fun ())
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 (\Term Name uni fun ()
t -> Term Name uni fun () -> m (Term NamedDeBruijn uni fun ())
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 () -> m (Term NamedDeBruijn uni fun ()))
-> m (Term Name uni fun ()) -> m (Term NamedDeBruijn uni fun ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SimplifyOpts () -> Term Name uni fun () -> m (Term Name uni fun ())
forall (uni :: * -> *) fun (m :: * -> *) a.
(ToBuiltinMeaning uni fun, MonadQuote m) =>
SimplifyOpts a -> Term Name uni fun a -> m (Term Name uni fun a)
UPLC.simplifyTerm SimplifyOpts ()
forall a. SimplifyOpts a
UPLC.defaultSimplifyOpts Term Name uni fun ()
t) Program Name uni fun ()
erased
    CompiledCodeIn uni fun a -> m (CompiledCodeIn uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CompiledCodeIn uni fun a -> m (CompiledCodeIn uni fun a))
-> CompiledCodeIn uni fun a -> m (CompiledCodeIn uni fun a)
forall a b. (a -> b) -> a -> b
$ Program NamedDeBruijn uni fun ()
-> Maybe (Program TyName Name uni fun ())
-> CoverageIndex
-> CompiledCodeIn uni fun a
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 Maybe (Program TyName Name uni fun ())
forall a. Maybe a
Nothing CoverageIndex
forall a. Monoid a => a
mempty