-- editorconfig-checker-disable-file
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module PlutusTx.Lift (
    safeLift,
    safeLiftProgram,
    safeLiftCode,
    lift,
    liftProgram,
    liftProgramDef,
    liftCode,
    liftCodeDef,
    typeCheckAgainst,
    typeCode,
    makeTypeable,
    makeLift,
    LiftError(..)
) where

import PlutusTx.Code
import PlutusTx.Lift.Class qualified as Lift
import PlutusTx.Lift.Instances ()
import PlutusTx.Lift.TH (LiftError (..), makeLift, makeTypeable)

import PlutusIR
import PlutusIR qualified as PIR
import PlutusIR.Analysis.Builtins as PIR
import PlutusIR.Compiler
import PlutusIR.Compiler.Definitions
import PlutusIR.Error qualified as PIR
import PlutusIR.MkPir qualified as PIR
import PlutusIR.Transform.RewriteRules as PIR

import PlutusCore qualified as PLC
import PlutusCore.Builtin qualified as PLC
import PlutusCore.Compiler qualified as PLC
import PlutusCore.Pretty
import PlutusCore.Quote
import PlutusCore.StdLib.Data.Function qualified as PLC
import PlutusCore.Version qualified as PLC

import UntypedPlutusCore qualified as UPLC

import Control.Exception
import Control.Lens hiding (lifted)
import Control.Monad (void)
import Control.Monad.Except (ExceptT, MonadError, liftEither, runExceptT)
import Control.Monad.Reader (runReaderT)
import Data.Bifunctor
import Data.Default.Class
import Data.Hashable
import Data.Proxy

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

-- | Get a Plutus Core term corresponding to the given value.
safeLift
    :: forall a e uni fun m
     . (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
       , PrettyUni uni, Pretty fun
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable fun
       )
    => PLC.Version -> a -> m (PIR.Term PLC.TyName PLC.Name uni fun (), UPLC.Term UPLC.NamedDeBruijn uni fun ())
safeLift :: forall a e (uni :: * -> *) 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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> m (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
safeLift Version
v a
x = do
    Term TyName Name uni fun ()
pir <- Quote (Term TyName Name uni fun ())
-> m (Term TyName Name uni fun ())
forall a. Quote a -> m a
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 () (QuoteT Identity) (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 () (QuoteT Identity) (Term TyName Name uni fun ())
 -> Quote (Term TyName Name uni fun ()))
-> DefT
     Name uni fun () (QuoteT Identity) (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ a
-> DefT
     Name uni fun () (QuoteT Identity) (Term TyName Name uni fun ())
forall fun. a -> RTCompile uni fun (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 term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, 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 = TypeCheckConfig uni fun -> CompilationCtx uni fun a
forall (uni :: * -> *) fun a.
(Default (BuiltinsInfo uni fun), Default (CostingPart uni fun),
 Default (RewriteRules uni fun)) =>
TypeCheckConfig uni fun -> CompilationCtx uni fun a
toDefaultCompilationCtx TypeCheckConfig uni fun
tcConfig
          CompilationCtx uni fun a
-> (CompilationCtx uni fun a -> CompilationCtx uni fun a)
-> CompilationCtx uni fun a
forall a b. a -> (a -> b) -> b
& 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 (f :: * -> *).
Functor f =>
(CompilationOpts a -> f (CompilationOpts a))
-> CompilationCtx uni fun a -> f (CompilationCtx uni fun 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 (f :: * -> *).
Functor f =>
(Int -> f Int) -> CompilationOpts a -> f (CompilationOpts a)
coMaxSimplifierIterations) Int
0
          -- This is a bit awkward as it makes the choice not configurable by the user. But it's already
          -- prety annoying passing in the version. We may eventually need to bite the bullet and provide a version
          -- that takes all the compilation options and everything.
          CompilationCtx uni fun a
-> (CompilationCtx uni fun a -> CompilationCtx uni fun a)
-> CompilationCtx uni fun a
forall a b. a -> (a -> b) -> b
& ASetter
  (CompilationCtx uni fun a)
  (CompilationCtx uni fun a)
  DatatypeStyle
  DatatypeStyle
-> DatatypeStyle
-> 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 (f :: * -> *).
Functor f =>
(CompilationOpts a -> f (CompilationOpts a))
-> CompilationCtx uni fun a -> f (CompilationCtx uni fun a)
ccOpts ((CompilationOpts a -> Identity (CompilationOpts a))
 -> CompilationCtx uni fun a -> Identity (CompilationCtx uni fun a))
-> ((DatatypeStyle -> Identity DatatypeStyle)
    -> CompilationOpts a -> Identity (CompilationOpts a))
-> ASetter
     (CompilationCtx uni fun a)
     (CompilationCtx uni fun a)
     DatatypeStyle
     DatatypeStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DatatypeCompilationOpts -> Identity DatatypeCompilationOpts)
-> CompilationOpts a -> Identity (CompilationOpts a)
forall a (f :: * -> *).
Functor f =>
(DatatypeCompilationOpts -> f DatatypeCompilationOpts)
-> CompilationOpts a -> f (CompilationOpts a)
coDatatypes ((DatatypeCompilationOpts -> Identity DatatypeCompilationOpts)
 -> CompilationOpts a -> Identity (CompilationOpts a))
-> ((DatatypeStyle -> Identity DatatypeStyle)
    -> DatatypeCompilationOpts -> Identity DatatypeCompilationOpts)
-> (DatatypeStyle -> Identity DatatypeStyle)
-> CompilationOpts a
-> Identity (CompilationOpts a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DatatypeStyle -> Identity DatatypeStyle)
-> DatatypeCompilationOpts -> Identity DatatypeCompilationOpts
Iso' DatatypeCompilationOpts DatatypeStyle
dcoStyle) (if Version
v Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
>= Version
PLC.plcVersion110 then DatatypeStyle
SumsOfProducts else DatatypeStyle
ScottEncoding)
        ucOpts :: CompilationOpts name2 fun a2
ucOpts = CompilationOpts name2 fun a2
forall fun name a.
Default (BuiltinSemanticsVariant fun) =>
CompilationOpts name fun a
PLC.defaultCompilationOpts
          CompilationOpts name2 fun a2
-> (CompilationOpts name2 fun a2 -> CompilationOpts name2 fun a2)
-> CompilationOpts name2 fun a2
forall a b. a -> (a -> b) -> b
& (SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2))
-> CompilationOpts name2 fun a2
-> Identity (CompilationOpts name2 fun a2)
forall name1 fun a1 name2 a2 (f :: * -> *).
Functor f =>
(SimplifyOpts name1 a1 -> f (SimplifyOpts name2 a2))
-> CompilationOpts name1 fun a1 -> f (CompilationOpts name2 fun a2)
PLC.coSimplifyOpts ((SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2))
 -> CompilationOpts name2 fun a2
 -> Identity (CompilationOpts name2 fun a2))
-> ((Int -> Identity Int)
    -> SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2))
-> (Int -> Identity Int)
-> CompilationOpts name2 fun a2
-> Identity (CompilationOpts name2 fun a2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Identity Int)
-> SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2)
forall name a (f :: * -> *).
Functor f =>
(Int -> f Int) -> SimplifyOpts name a -> f (SimplifyOpts name a)
UPLC.soMaxSimplifierIterations ((Int -> Identity Int)
 -> CompilationOpts name2 fun a2
 -> Identity (CompilationOpts name2 fun a2))
-> Int
-> CompilationOpts name2 fun a2
-> CompilationOpts name2 fun a2
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Int
0
          CompilationOpts name2 fun a2
-> (CompilationOpts name2 fun a2 -> CompilationOpts name2 fun a2)
-> CompilationOpts name2 fun a2
forall a b. a -> (a -> b) -> b
& (SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2))
-> CompilationOpts name2 fun a2
-> Identity (CompilationOpts name2 fun a2)
forall name1 fun a1 name2 a2 (f :: * -> *).
Functor f =>
(SimplifyOpts name1 a1 -> f (SimplifyOpts name2 a2))
-> CompilationOpts name1 fun a1 -> f (CompilationOpts name2 fun a2)
PLC.coSimplifyOpts ((SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2))
 -> CompilationOpts name2 fun a2
 -> Identity (CompilationOpts name2 fun a2))
-> ((Int -> Identity Int)
    -> SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2))
-> (Int -> Identity Int)
-> CompilationOpts name2 fun a2
-> Identity (CompilationOpts name2 fun a2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Identity Int)
-> SimplifyOpts name2 a2 -> Identity (SimplifyOpts name2 a2)
forall name a (f :: * -> *).
Functor f =>
(Int -> f Int) -> SimplifyOpts name a -> f (SimplifyOpts name a)
UPLC.soMaxCseIterations ((Int -> Identity Int)
 -> CompilationOpts name2 fun a2
 -> Identity (CompilationOpts name2 fun a2))
-> Int
-> CompilationOpts name2 fun a2
-> CompilationOpts name2 fun a2
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Int
0
    PLCProgram uni fun ()
plc <- (ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
 -> CompilationCtx uni fun () -> m (PLCProgram uni fun ()))
-> CompilationCtx uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
-> m (PLCProgram uni fun ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
-> CompilationCtx uni fun () -> m (PLCProgram 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 (PLCProgram uni fun ())
 -> m (PLCProgram uni fun ()))
-> ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
-> m (PLCProgram uni fun ())
forall a b. (a -> b) -> a -> b
$ Program TyName Name uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Program TyName Name uni fun a -> m (PLCProgram uni fun a)
compileProgram (()
-> Version
-> Term TyName Name uni fun ()
-> Program TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program () Version
v Term TyName Name uni fun ()
pir)
    Program Name uni fun (Provenance ())
uplc <- (ReaderT
   (CompilationOpts Name fun (Provenance ()))
   m
   (Program Name uni fun (Provenance ()))
 -> CompilationOpts Name fun (Provenance ())
 -> m (Program Name uni fun (Provenance ())))
-> CompilationOpts Name fun (Provenance ())
-> ReaderT
     (CompilationOpts Name fun (Provenance ()))
     m
     (Program Name uni fun (Provenance ()))
-> m (Program Name uni fun (Provenance ()))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (CompilationOpts Name fun (Provenance ()))
  m
  (Program Name uni fun (Provenance ()))
-> CompilationOpts Name fun (Provenance ())
-> m (Program Name uni fun (Provenance ()))
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CompilationOpts Name fun (Provenance ())
forall {name2} {a2}. CompilationOpts name2 fun a2
ucOpts (ReaderT
   (CompilationOpts Name fun (Provenance ()))
   m
   (Program Name uni fun (Provenance ()))
 -> m (Program Name uni fun (Provenance ())))
-> ReaderT
     (CompilationOpts Name fun (Provenance ()))
     m
     (Program Name uni fun (Provenance ()))
-> m (Program Name uni fun (Provenance ()))
forall a b. (a -> b) -> a -> b
$ PLCProgram uni fun ()
-> ReaderT
     (CompilationOpts Name fun (Provenance ()))
     m
     (Program Name uni fun (Provenance ()))
forall (m :: * -> *) (uni :: * -> *) fun name a tyname.
(Compiling m uni fun name a,
 MonadReader (CompilationOpts name fun a) m) =>
Program tyname name uni fun a -> m (Program name uni fun a)
PLC.compileProgram PLCProgram uni fun ()
plc
    UPLC.Program Provenance ()
_ Version
_ Term NamedDeBruijn uni fun (Provenance ())
db <- LensLike
  m
  (Program Name uni fun (Provenance ()))
  (Program NamedDeBruijn uni fun (Provenance ()))
  (Term Name uni fun (Provenance ()))
  (Term NamedDeBruijn uni fun (Provenance ()))
-> LensLike
     m
     (Program Name uni fun (Provenance ()))
     (Program NamedDeBruijn uni fun (Provenance ()))
     (Term Name uni fun (Provenance ()))
     (Term NamedDeBruijn uni fun (Provenance ()))
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 (Provenance ()))
  (Program NamedDeBruijn uni fun (Provenance ()))
  (Term Name uni fun (Provenance ()))
  (Term NamedDeBruijn uni fun (Provenance ()))
forall name1 (uni1 :: * -> *) fun1 ann name2 (uni2 :: * -> *) fun2
       (f :: * -> *).
Functor f =>
(Term name1 uni1 fun1 ann -> f (Term name2 uni2 fun2 ann))
-> Program name1 uni1 fun1 ann -> f (Program name2 uni2 fun2 ann)
UPLC.progTerm 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 Program Name uni fun (Provenance ())
uplc
    (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
-> m (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ()
pir, 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
       , PrettyUni uni, Pretty fun
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable fun
       )
    => PLC.Version -> a -> m (PIR.Program PLC.TyName PLC.Name uni fun (), 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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> m (Program TyName Name uni fun (),
      Program NamedDeBruijn uni fun ())
safeLiftProgram Version
v a
x = (Term TyName Name uni fun () -> Program TyName Name uni fun ())
-> (Term NamedDeBruijn uni fun ()
    -> Program NamedDeBruijn uni fun ())
-> (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
-> (Program TyName Name uni fun (),
    Program NamedDeBruijn uni fun ())
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (()
-> Version
-> Term TyName Name uni fun ()
-> Program TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
PIR.Program () Version
v) (()
-> Version
-> Term NamedDeBruijn uni fun ()
-> Program NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Version -> Term name uni fun ann -> Program name uni fun ann
UPLC.Program () Version
v) ((Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
 -> (Program TyName Name uni fun (),
     Program NamedDeBruijn uni fun ()))
-> m (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
-> m (Program TyName Name uni fun (),
      Program NamedDeBruijn uni fun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Version
-> a
-> m (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
forall a e (uni :: * -> *) 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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> m (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
safeLift Version
v 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
       , PrettyUni uni, Pretty fun
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable fun
       )
    => PLC.Version -> 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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version -> a -> m (CompiledCodeIn uni fun a)
safeLiftCode Version
v =
    ((Program TyName Name uni fun (), Program NamedDeBruijn uni fun ())
 -> CompiledCodeIn uni fun a)
-> m (Program TyName Name uni fun (),
      Program NamedDeBruijn uni fun ())
-> m (CompiledCodeIn uni fun a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
        ( \(Program TyName Name uni fun ()
pir, Program NamedDeBruijn uni fun ()
uplc) ->
            Program NamedDeBruijn uni fun SrcSpans
-> Maybe (Program TyName Name uni fun SrcSpans)
-> CoverageIndex
-> CompiledCodeIn uni fun a
forall (uni :: * -> *) fun a.
Program NamedDeBruijn uni fun SrcSpans
-> Maybe (Program TyName Name uni fun SrcSpans)
-> CoverageIndex
-> CompiledCodeIn uni fun a
DeserializedCode (SrcSpans
forall a. Monoid a => a
mempty SrcSpans
-> Program NamedDeBruijn uni fun ()
-> Program NamedDeBruijn uni fun SrcSpans
forall a b.
a
-> Program NamedDeBruijn uni fun b
-> Program NamedDeBruijn uni fun a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Program NamedDeBruijn uni fun ()
uplc) (Program TyName Name uni fun SrcSpans
-> Maybe (Program TyName Name uni fun SrcSpans)
forall a. a -> Maybe a
Just (SrcSpans
forall a. Monoid a => a
mempty SrcSpans
-> Program TyName Name uni fun ()
-> Program TyName Name uni fun SrcSpans
forall a b.
a -> Program TyName Name uni fun b -> Program TyName Name uni fun a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Program TyName Name uni fun ()
pir)) CoverageIndex
forall a. Monoid a => a
mempty
        )
        (m (Program TyName Name uni fun (),
    Program NamedDeBruijn uni fun ())
 -> m (CompiledCodeIn uni fun a))
-> (a
    -> m (Program TyName Name uni fun (),
          Program NamedDeBruijn uni fun ()))
-> a
-> m (CompiledCodeIn uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Version
-> a
-> m (Program TyName Name uni fun (),
      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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> m (Program TyName Name uni fun (),
      Program NamedDeBruijn uni fun ())
safeLiftProgram Version
v

unsafely
    :: ThrowableBuiltins uni fun
    => ExceptT (Error uni fun (Provenance ())) Quote a -> a
unsafely :: forall (uni :: * -> *) fun a.
ThrowableBuiltins uni fun =>
ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a -> a
unsafely ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) 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 ())) (QuoteT Identity) a
-> QuoteT Identity (Either (Error uni fun (Provenance ())) a)
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  -> 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 a. a -> QuoteT Identity 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, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun, PLC.GEq uni
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable fun
       )
    => PLC.Version -> a -> (PIR.Term PLC.TyName PLC.Name uni fun (), UPLC.Term UPLC.NamedDeBruijn uni fun ())
lift :: forall (uni :: * -> *) a fun.
(Lift uni a, ThrowableBuiltins uni fun, Typecheckable uni fun,
 GEq uni, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
lift Version
v a
a = ExceptT
  (Error uni fun (Provenance ()))
  (QuoteT Identity)
  (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
-> (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun a.
ThrowableBuiltins uni fun =>
ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a -> a
unsafely (ExceptT
   (Error uni fun (Provenance ()))
   (QuoteT Identity)
   (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
 -> (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ()))
-> ExceptT
     (Error uni fun (Provenance ()))
     (QuoteT Identity)
     (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
-> (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ Version
-> a
-> ExceptT
     (Error uni fun (Provenance ()))
     (QuoteT Identity)
     (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
forall a e (uni :: * -> *) 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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> m (Term TyName Name uni fun (), Term NamedDeBruijn uni fun ())
safeLift Version
v 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, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun, PLC.GEq uni
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable fun
       )
    => PLC.Version -> a -> (PIR.Program PLC.TyName PLC.Name uni fun (), UPLC.Program UPLC.NamedDeBruijn uni fun ())
liftProgram :: forall (uni :: * -> *) a fun.
(Lift uni a, ThrowableBuiltins uni fun, Typecheckable uni fun,
 GEq uni, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> (Program TyName Name uni fun (),
    Program NamedDeBruijn uni fun ())
liftProgram Version
v a
x = ExceptT
  (Error uni fun (Provenance ()))
  (QuoteT Identity)
  (Program TyName Name uni fun (), Program NamedDeBruijn uni fun ())
-> (Program TyName Name uni fun (),
    Program NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun a.
ThrowableBuiltins uni fun =>
ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a -> a
unsafely (ExceptT
   (Error uni fun (Provenance ()))
   (QuoteT Identity)
   (Program TyName Name uni fun (), Program NamedDeBruijn uni fun ())
 -> (Program TyName Name uni fun (),
     Program NamedDeBruijn uni fun ()))
-> ExceptT
     (Error uni fun (Provenance ()))
     (QuoteT Identity)
     (Program TyName Name uni fun (), Program NamedDeBruijn uni fun ())
-> (Program TyName Name uni fun (),
    Program NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ Version
-> a
-> ExceptT
     (Error uni fun (Provenance ()))
     (QuoteT Identity)
     (Program TyName Name uni fun (), 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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> m (Program TyName Name uni fun (),
      Program NamedDeBruijn uni fun ())
safeLiftProgram Version
v a
x

-- | Get a Plutus Core program in the default universe with the default version, corresponding to the given value, throwing any errors that occur as exceptions and ignoring fresh names.
liftProgramDef
    :: Lift.Lift PLC.DefaultUni a
    => a -> (PIR.Program PLC.TyName PLC.Name PLC.DefaultUni PLC.DefaultFun (), UPLC.Program UPLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ())
liftProgramDef :: forall a.
Lift DefaultUni a =>
a
-> (Program TyName Name DefaultUni DefaultFun (),
    Program NamedDeBruijn DefaultUni DefaultFun ())
liftProgramDef = Version
-> a
-> (Program TyName Name DefaultUni DefaultFun (),
    Program NamedDeBruijn DefaultUni DefaultFun ())
forall (uni :: * -> *) a fun.
(Lift uni a, ThrowableBuiltins uni fun, Typecheckable uni fun,
 GEq uni, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version
-> a
-> (Program TyName Name uni fun (),
    Program NamedDeBruijn uni fun ())
liftProgram Version
PLC.latestVersion

-- | 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, PLC.GEq uni, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable fun
       )
    => PLC.Version -> a -> CompiledCodeIn uni fun a
liftCode :: forall (uni :: * -> *) a fun.
(Lift uni a, GEq uni, ThrowableBuiltins uni fun,
 Typecheckable uni fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version -> a -> CompiledCodeIn uni fun a
liftCode Version
v a
x = ExceptT
  (Error uni fun (Provenance ()))
  (QuoteT Identity)
  (CompiledCodeIn uni fun a)
-> CompiledCodeIn uni fun a
forall (uni :: * -> *) fun a.
ThrowableBuiltins uni fun =>
ExceptT (Error uni fun (Provenance ())) (QuoteT Identity) a -> a
unsafely (ExceptT
   (Error uni fun (Provenance ()))
   (QuoteT Identity)
   (CompiledCodeIn uni fun a)
 -> CompiledCodeIn uni fun a)
-> ExceptT
     (Error uni fun (Provenance ()))
     (QuoteT Identity)
     (CompiledCodeIn uni fun a)
-> CompiledCodeIn uni fun a
forall a b. (a -> b) -> a -> b
$ Version
-> a
-> ExceptT
     (Error uni fun (Provenance ()))
     (QuoteT Identity)
     (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, PrettyUni uni,
 Pretty fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version -> a -> m (CompiledCodeIn uni fun a)
safeLiftCode Version
v a
x

-- | Get a Plutus Core program with the default version, corresponding to the given value as a 'CompiledCodeIn', throwing any errors that occur as exceptions and ignoring fresh names.
liftCodeDef
    :: ( Lift.Lift uni a, PLC.GEq uni, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable fun
       )
    => a -> CompiledCodeIn uni fun a
liftCodeDef :: forall (uni :: * -> *) a fun.
(Lift uni a, GEq uni, ThrowableBuiltins uni fun,
 Typecheckable uni fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
a -> CompiledCodeIn uni fun a
liftCodeDef = Version -> a -> CompiledCodeIn uni fun a
forall (uni :: * -> *) a fun.
(Lift uni a, GEq uni, ThrowableBuiltins uni fun,
 Typecheckable uni fun, Default (CostingPart uni fun),
 Default (BuiltinsInfo uni fun), Default (RewriteRules uni fun),
 Hashable fun) =>
Version -> a -> CompiledCodeIn uni fun a
liftCode Version
PLC.latestVersion

{- 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
       , PrettyUni uni, Pretty fun
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       )
    => Proxy a
    -> PLC.Program 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, PrettyUni uni, Pretty fun,
 Default (CostingPart uni fun), Default (BuiltinsInfo uni fun),
 Default (RewriteRules uni fun)) =>
Proxy a -> Program TyName Name uni fun () -> m ()
typeCheckAgainst Proxy a
p (PLC.Program ()
_ Version
v 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.embedTerm (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
forall (m :: * -> *).
MonadQuote m =>
Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
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 a. Quote a -> m a
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 () (QuoteT Identity) (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 () (QuoteT Identity) (Term TyName Name uni fun ())
 -> Quote (Term TyName Name uni fun ()))
-> DefT
     Name uni fun () (QuoteT Identity) (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 fun. Proxy a -> RTCompile uni fun (Type TyName uni ())
forall k (uni :: * -> *) (a :: k) fun.
Typeable uni a =>
Proxy a -> RTCompile uni fun (Type TyName uni ())
Lift.typeRep Proxy a
p
        Term TyName Name uni fun ()
-> DefT
     Name uni fun () (QuoteT Identity) (Term TyName Name uni fun ())
forall a. a -> DefT Name uni fun () (QuoteT Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ()
 -> DefT
      Name uni fun () (QuoteT Identity) (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> DefT
     Name uni fun () (QuoteT Identity) (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
    -- Here we use a 'Default' builtin semantics variant, because the
    -- typechecker needs to be handed a builtin semantics variant (implementation detail).
    -- See Note [Builtin semantics variants]
    TypeCheckConfig uni fun
tcConfig <- Provenance () -> m (TypeCheckConfig uni fun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
PLC.getDefTypeCheckConfig (() -> Provenance ()
forall a. a -> Provenance a
Original ())
    -- The PIR compiler *pointfully* needs a builtin semantics variant, but in
    -- this instance of only "lifting" it is safe to default to any builtin
    -- semantics variant, since the 'Lift' is impervious to builtins and will
    -- not generate code containing builtins.  See Note [Builtin semantics variants]
    PLCProgram uni fun ()
compiled <- (ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
 -> CompilationCtx uni fun () -> m (PLCProgram uni fun ()))
-> CompilationCtx uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
-> m (PLCProgram uni fun ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
-> CompilationCtx uni fun () -> m (PLCProgram uni fun ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (TypeCheckConfig uni fun -> CompilationCtx uni fun ()
forall (uni :: * -> *) fun a.
(Default (BuiltinsInfo uni fun), Default (CostingPart uni fun),
 Default (RewriteRules uni fun)) =>
TypeCheckConfig uni fun -> CompilationCtx uni fun a
toDefaultCompilationCtx TypeCheckConfig uni fun
tcConfig) (ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
 -> m (PLCProgram uni fun ()))
-> ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
-> m (PLCProgram uni fun ())
forall a b. (a -> b) -> a -> b
$ Program TyName Name uni fun ()
-> ReaderT (CompilationCtx uni fun ()) m (PLCProgram uni fun ())
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Program TyName Name uni fun a -> m (PLCProgram uni fun a)
compileProgram (()
-> Version
-> Term TyName Name uni fun ()
-> Program TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program () Version
v 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
-> PLCProgram uni fun ()
-> ExceptT
     (Error uni fun (Provenance ())) m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> Program TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
PLC.inferTypeOfProgram TypeCheckConfig uni fun
tcConfig PLCProgram 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 a b c. (a -> b) -> Either a c -> Either b c
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)
Prism' e (Error uni fun (Provenance ()))
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
       , PrettyUni uni, Pretty fun
       , Default (PLC.CostingPart uni fun)
       , Default (PIR.BuiltinsInfo uni fun)
       , Default (PIR.RewriteRules uni fun)
       , Hashable 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, PrettyUni uni, Pretty fun,
 Default (CostingPart uni fun), Default (BuiltinsInfo uni fun),
 Default (RewriteRules uni fun), Hashable fun) =>
Proxy a
-> Program TyName Name uni fun () -> m (CompiledCodeIn uni fun a)
typeCode Proxy a
p Program TyName Name uni fun ()
prog = do
    ()
_ <- Proxy a -> Program 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, PrettyUni uni, Pretty fun,
 Default (CostingPart uni fun), Default (BuiltinsInfo uni fun),
 Default (RewriteRules uni fun)) =>
Proxy a -> Program TyName Name uni fun () -> m ()
typeCheckAgainst Proxy a
p Program TyName Name uni fun ()
prog
    Program Name uni fun ()
compiled <-
        (ReaderT (CompilationOpts Name fun ()) m (Program Name uni fun ())
 -> CompilationOpts Name fun () -> m (Program Name uni fun ()))
-> CompilationOpts Name fun ()
-> ReaderT
     (CompilationOpts Name fun ()) m (Program Name uni fun ())
-> m (Program Name uni fun ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (CompilationOpts Name fun ()) m (Program Name uni fun ())
-> CompilationOpts Name fun () -> m (Program Name uni fun ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CompilationOpts Name fun ()
forall fun name a.
Default (BuiltinSemanticsVariant fun) =>
CompilationOpts name fun a
PLC.defaultCompilationOpts
        (ReaderT (CompilationOpts Name fun ()) m (Program Name uni fun ())
 -> m (Program Name uni fun ()))
-> ReaderT
     (CompilationOpts Name fun ()) m (Program Name uni fun ())
-> m (Program Name uni fun ())
forall a b. (a -> b) -> a -> b
$ Program TyName Name uni fun ()
-> ReaderT
     (CompilationOpts Name fun ()) m (Program Name uni fun ())
forall (m :: * -> *) (uni :: * -> *) fun name a tyname.
(Compiling m uni fun name a,
 MonadReader (CompilationOpts name fun 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 <- 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
       (f :: * -> *).
Functor f =>
(Term name1 uni1 fun1 ann -> f (Term name2 uni2 fun2 ann))
-> Program name1 uni1 fun1 ann -> f (Program name2 uni2 fun2 ann)
UPLC.progTerm 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 Program Name uni fun ()
compiled
    CompiledCodeIn uni fun a -> m (CompiledCodeIn uni fun a)
forall a. a -> m 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 SrcSpans
-> Maybe (Program TyName Name uni fun SrcSpans)
-> CoverageIndex
-> CompiledCodeIn uni fun a
forall (uni :: * -> *) fun a.
Program NamedDeBruijn uni fun SrcSpans
-> Maybe (Program TyName Name uni fun SrcSpans)
-> CoverageIndex
-> CompiledCodeIn uni fun a
DeserializedCode (SrcSpans
forall a. Monoid a => a
mempty SrcSpans
-> Program NamedDeBruijn uni fun ()
-> Program NamedDeBruijn uni fun SrcSpans
forall a b.
a
-> Program NamedDeBruijn uni fun b
-> Program NamedDeBruijn uni fun a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Program NamedDeBruijn uni fun ()
db) Maybe (Program TyName Name uni fun SrcSpans)
forall a. Maybe a
Nothing CoverageIndex
forall a. Monoid a => a
mempty