{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
module PlutusIR.Transform.Inline.CallSiteInline where
import PlutusCore qualified as PLC
import PlutusCore.Rename (rename)
import PlutusCore.Rename.Internal (Dupable (Dupable))
import PlutusIR.Analysis.Size (Size, termSize)
import PlutusIR.Contexts
import PlutusIR.Core
import PlutusIR.Transform.Inline.Utils
import PlutusIR.Transform.Substitute
applyAndBetaReduce ::
forall tyname name uni fun ann.
(InliningConstraints tyname name uni fun) =>
Term tyname name uni fun ann ->
AppContext tyname name uni fun ann ->
InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
applyAndBetaReduce :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
applyAndBetaReduce Term tyname name uni fun ann
rhs AppContext tyname name uni fun ann
args0 = do
let go ::
Term tyname name uni fun ann ->
AppContext tyname name uni fun ann ->
InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go :: Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
acc AppContext tyname name uni fun ann
args = case (Term tyname name uni fun ann
acc, AppContext tyname name uni fun ann
args) of
(LamAbs ann
_ann name
n Type tyname uni ann
_ty Term tyname name uni fun ann
tm, TermAppContext Term tyname name uni fun ann
arg ann
_ AppContext tyname name uni fun ann
args') -> do
Bool
safe <- name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
safeToBetaReduce name
n Term tyname name uni fun ann
arg Term tyname name uni fun ann
acc
if Bool
safe
then do
Term tyname name uni fun ann
acc' <- do
(name
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Term tyname name uni fun ann)
forall (m :: * -> *) name tyname (uni :: * -> *) fun ann.
Monad m =>
(name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstNamesM
(\name
tmName -> if name
tmName name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
n then Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann))
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Term tyname name uni fun ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
PLC.rename Term tyname name uni fun ann
arg else Maybe (Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing)
Term tyname name uni fun ann
tm
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
acc' AppContext tyname name uni fun ann
args'
else Maybe (Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> (Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (Term tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext Term tyname name uni fun ann
acc AppContext tyname name uni fun ann
args
(TyAbs ann
_ann tyname
n Kind ann
_kd Term tyname name uni fun ann
tm, TypeAppContext Type tyname uni ann
arg ann
_ AppContext tyname name uni fun ann
args') -> do
Term tyname name uni fun ann
acc' <-
(tyname
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Term tyname name uni fun ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann name fun.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstTyNamesM
(\tyname
tyName -> if tyname
tyName tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
n then Type tyname uni ann -> Maybe (Type tyname uni ann)
forall a. a -> Maybe a
Just (Type tyname uni ann -> Maybe (Type tyname uni ann))
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Type tyname uni ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Type tyname uni ann))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Type tyname uni ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.rename Type tyname uni ann
arg else Maybe (Type tyname uni ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Type tyname uni ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Type tyname uni ann)
forall a. Maybe a
Nothing)
Term tyname name uni fun ann
tm
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
acc' AppContext tyname name uni fun ann
args'
(LamAbs{}, TypeAppContext{}) -> Maybe (Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
(TyAbs{}, TermAppContext{}) -> Maybe (Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
(Term tyname name uni fun ann
_, AppContext tyname name uni fun ann
_) -> Maybe (Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun ann)
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> (Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (Term tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext Term tyname name uni fun ann
acc AppContext tyname name uni fun ann
args
safeToBetaReduce ::
name ->
Term tyname name uni fun ann ->
Term tyname name uni fun ann ->
InlineM tyname name uni fun ann Bool
safeToBetaReduce :: name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
safeToBetaReduce = Strictness
-> name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Strictness
-> name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
shouldUnconditionallyInline Strictness
Strict
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
rhs AppContext tyname name uni fun ann
args0
callSiteInline ::
forall tyname name uni fun ann.
(InliningConstraints tyname name uni fun) =>
Size ->
InlineVarInfo tyname name uni fun ann ->
AppContext tyname name uni fun ann ->
InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
callSiteInline :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Size
-> InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
callSiteInline Size
processedTSize = InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
go
where
go :: InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
go InlineVarInfo tyname name uni fun ann
varInfo AppContext tyname name uni fun ann
args = do
let
defAsInlineTerm :: InlineTerm tyname name uni fun ann
defAsInlineTerm = InlineVarInfo tyname name uni fun ann
-> InlineTerm tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
InlineVarInfo tyname name uni fun ann
-> InlineTerm tyname name uni fun ann
varRhs InlineVarInfo tyname name uni fun ann
varInfo
inlineTermToTerm :: InlineTerm tyname name uni fun ann
-> Term tyname name uni fun ann
inlineTermToTerm :: InlineTerm tyname name uni fun ann -> Term tyname name uni fun ann
inlineTermToTerm (Done (Dupable Term tyname name uni fun ann
var)) = Term tyname name uni fun ann
var
headRhs :: Term tyname name uni fun ann
headRhs = InlineTerm tyname name uni fun ann -> Term tyname name uni fun ann
inlineTermToTerm InlineTerm tyname name uni fun ann
defAsInlineTerm
costIsOk :: Bool
costIsOk = Term tyname name uni fun ann -> Bool
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Bool
costIsAcceptable Term tyname name uni fun ann
headRhs
Bool
rhsPure <- Strictness
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Strictness
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
isTermBindingPure (InlineVarInfo tyname name uni fun ann -> Strictness
forall tyname name (uni :: * -> *) fun ann.
InlineVarInfo tyname name uni fun ann -> Strictness
varStrictness InlineVarInfo tyname name uni fun ann
varInfo) Term tyname name uni fun ann
headRhs
if Bool
costIsOk Bool -> Bool -> Bool
&& Bool
rhsPure then do
Term tyname name uni fun ann
renamedRhs <- Term tyname name uni fun ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Term tyname name uni fun ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
rename Term tyname name uni fun ann
headRhs
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
applyAndBetaReduce Term tyname name uni fun ann
renamedRhs AppContext tyname name uni fun ann
args ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
-> (Maybe (Term tyname name uni fun ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann)))
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
forall a b.
ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
-> (a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
b)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Term tyname name uni fun ann
inlined -> do
let
sizeIsOk :: Bool
sizeIsOk = Term tyname name uni fun ann -> Size
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Size
termSize Term tyname name uni fun ann
inlined Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
<= Size
processedTSize
Maybe (Term tyname name uni fun ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann)))
-> Maybe (Term tyname name uni fun ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ if Bool
sizeIsOk then Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just Term tyname name uni fun ann
inlined else Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
Maybe (Term tyname name uni fun ann)
Nothing -> Maybe (Term tyname name uni fun ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
else Maybe (Term tyname name uni fun ann)
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
(Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
(InlineInfo tyname name uni fun ann)
(StateT (InlinerState tyname name uni fun ann) Quote)
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing