{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

{-| An inlining pass.

This pass is essentially a copy of the PIR inliner, and should be KEPT IN SYNC
with it. It's hard to do this with true abstraction, so we just have to keep
two copies reasonably similar.

However, there are some differences. In the interests of making it easier
to keep things in sync, these are explicitly listed in
Note [Differences from PIR inliner]. If you add another difference,
please note it there! Obviously fewer differences is better.

See Note [The problem of inlining destructors] for why this pass exists. -}
module UntypedPlutusCore.Transform.Inline
  ( inline
  , InlineHints (..)

    -- * Exported for testing
  , InlineM
  , S (..)
  , Decoration (..)
  , Ann
  , InlineInfo (..)
  , Subst (..)
  , TermEnv (..)
  , isFirstVarBeforeEffects
  , isStrictIn
  , effectSafe
  ) where

import Control.Lens (Lens', forMOf, makeLenses, view, (%~), (&), (^.), _1)
import Control.Monad.Extra (ifM, (&&^), (||^))
import Control.Monad.Reader (ReaderT (runReaderT))
import Control.Monad.State (StateT, evalStateT, gets, modify')
import Data.Bifunctor (first)
import Data.Vector qualified as V
import PlutusCore qualified as PLC
import PlutusCore.Annotation (Inline (AlwaysInline, SafeToInline), InlineHints (..))
import PlutusCore.Builtin (ToBuiltinMeaning (BuiltinSemanticsVariant))
import PlutusCore.Builtin qualified as PLC
import PlutusCore.MkPlc (mkIterApp)
import PlutusCore.Name.Unique (HasUnique, TermUnique (..), Unique (..))
import PlutusCore.Name.UniqueMap qualified as UMap
import PlutusCore.Quote (MonadQuote (..), Quote)
import PlutusCore.Rename (Dupable, dupable, liftDupable)
import PlutusPrelude (Generic)
import UntypedPlutusCore.Analysis.Usages qualified as Usages
import UntypedPlutusCore.AstSize (AstSize, termAstSize)
import UntypedPlutusCore.Core qualified as UPLC
import UntypedPlutusCore.Core.Plated (termSubterms)
import UntypedPlutusCore.Core.Type (Term (..), modifyTermAnn, termAnn)
import UntypedPlutusCore.MkUPlc (Def (..), UTermDef, UVarDecl (..))
import UntypedPlutusCore.Purity
  ( EvalTerm (EvalTerm, Unknown)
  , Purity (MaybeImpure, Pure)
  , isPure
  , termEvaluationOrder
  , unEvalOrder
  )
import UntypedPlutusCore.Rename ()
import UntypedPlutusCore.Subst (termSubstNamesM)
import UntypedPlutusCore.Transform.Certify.Hints qualified as CertifierHints
import UntypedPlutusCore.Transform.Simplifier
  ( SimplifierStage (Inline)
  , SimplifierT
  , recordSimplificationWithHints
  )

{- Note [Differences from PIR inliner]
See the module comment for explanation for why this exists and is similar to
the PIR inliner.

1. No types (obviously).
2. No strictness information (we only have lambda arguments, which are always
   strict).
3. Handling of multiple beta-reductions in one go, this is handled in PIR by a
   dedicated pass.
4. Simplistic purity analysis, in particular we don't try to be clever about
   builtins (should mostly be handled in PIR).
-}

-- | Substitution range, 'SubstRng' in the paper.
newtype InlineTerm name uni fun a = Done (Dupable (Term name uni fun a))

{-| Term substitution, 'Subst' in the paper.
A map of unprocessed variable and its substitution range. -}
newtype TermEnv name uni fun a = TermEnv
  {forall name (uni :: * -> *) fun a.
TermEnv name uni fun a
-> UniqueMap TermUnique (InlineTerm name uni fun a)
_unTermEnv :: PLC.UniqueMap TermUnique (InlineTerm name uni fun a)}
  deriving newtype (NonEmpty (TermEnv name uni fun a) -> TermEnv name uni fun a
TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
(TermEnv name uni fun a
 -> TermEnv name uni fun a -> TermEnv name uni fun a)
-> (NonEmpty (TermEnv name uni fun a) -> TermEnv name uni fun a)
-> (forall b.
    Integral b =>
    b -> TermEnv name uni fun a -> TermEnv name uni fun a)
-> Semigroup (TermEnv name uni fun a)
forall b.
Integral b =>
b -> TermEnv name uni fun a -> TermEnv name uni fun a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall name (uni :: * -> *) fun a.
NonEmpty (TermEnv name uni fun a) -> TermEnv name uni fun a
forall name (uni :: * -> *) fun a.
TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
forall name (uni :: * -> *) fun a b.
Integral b =>
b -> TermEnv name uni fun a -> TermEnv name uni fun a
$c<> :: forall name (uni :: * -> *) fun a.
TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
<> :: TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
$csconcat :: forall name (uni :: * -> *) fun a.
NonEmpty (TermEnv name uni fun a) -> TermEnv name uni fun a
sconcat :: NonEmpty (TermEnv name uni fun a) -> TermEnv name uni fun a
$cstimes :: forall name (uni :: * -> *) fun a b.
Integral b =>
b -> TermEnv name uni fun a -> TermEnv name uni fun a
stimes :: forall b.
Integral b =>
b -> TermEnv name uni fun a -> TermEnv name uni fun a
Semigroup, Semigroup (TermEnv name uni fun a)
TermEnv name uni fun a
Semigroup (TermEnv name uni fun a) =>
TermEnv name uni fun a
-> (TermEnv name uni fun a
    -> TermEnv name uni fun a -> TermEnv name uni fun a)
-> ([TermEnv name uni fun a] -> TermEnv name uni fun a)
-> Monoid (TermEnv name uni fun a)
[TermEnv name uni fun a] -> TermEnv name uni fun a
TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall name (uni :: * -> *) fun a.
Semigroup (TermEnv name uni fun a)
forall name (uni :: * -> *) fun a. TermEnv name uni fun a
forall name (uni :: * -> *) fun a.
[TermEnv name uni fun a] -> TermEnv name uni fun a
forall name (uni :: * -> *) fun a.
TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
$cmempty :: forall name (uni :: * -> *) fun a. TermEnv name uni fun a
mempty :: TermEnv name uni fun a
$cmappend :: forall name (uni :: * -> *) fun a.
TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
mappend :: TermEnv name uni fun a
-> TermEnv name uni fun a -> TermEnv name uni fun a
$cmconcat :: forall name (uni :: * -> *) fun a.
[TermEnv name uni fun a] -> TermEnv name uni fun a
mconcat :: [TermEnv name uni fun a] -> TermEnv name uni fun a
Monoid)

{-| Wrapper of term substitution so that it's similar to the PIR inliner.
See Note [Differences from PIR inliner] 1 -}
newtype Subst name uni fun a = Subst {forall name (uni :: * -> *) fun a.
Subst name uni fun a -> TermEnv name uni fun a
_termEnv :: TermEnv name uni fun a}
  deriving stock ((forall x. Subst name uni fun a -> Rep (Subst name uni fun a) x)
-> (forall x. Rep (Subst name uni fun a) x -> Subst name uni fun a)
-> Generic (Subst name uni fun a)
forall x. Rep (Subst name uni fun a) x -> Subst name uni fun a
forall x. Subst name uni fun a -> Rep (Subst name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall name (uni :: * -> *) fun a x.
Rep (Subst name uni fun a) x -> Subst name uni fun a
forall name (uni :: * -> *) fun a x.
Subst name uni fun a -> Rep (Subst name uni fun a) x
$cfrom :: forall name (uni :: * -> *) fun a x.
Subst name uni fun a -> Rep (Subst name uni fun a) x
from :: forall x. Subst name uni fun a -> Rep (Subst name uni fun a) x
$cto :: forall name (uni :: * -> *) fun a x.
Rep (Subst name uni fun a) x -> Subst name uni fun a
to :: forall x. Rep (Subst name uni fun a) x -> Subst name uni fun a
Generic)
  deriving newtype (NonEmpty (Subst name uni fun a) -> Subst name uni fun a
Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
(Subst name uni fun a
 -> Subst name uni fun a -> Subst name uni fun a)
-> (NonEmpty (Subst name uni fun a) -> Subst name uni fun a)
-> (forall b.
    Integral b =>
    b -> Subst name uni fun a -> Subst name uni fun a)
-> Semigroup (Subst name uni fun a)
forall b.
Integral b =>
b -> Subst name uni fun a -> Subst name uni fun a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall name (uni :: * -> *) fun a.
NonEmpty (Subst name uni fun a) -> Subst name uni fun a
forall name (uni :: * -> *) fun a.
Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
forall name (uni :: * -> *) fun a b.
Integral b =>
b -> Subst name uni fun a -> Subst name uni fun a
$c<> :: forall name (uni :: * -> *) fun a.
Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
<> :: Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
$csconcat :: forall name (uni :: * -> *) fun a.
NonEmpty (Subst name uni fun a) -> Subst name uni fun a
sconcat :: NonEmpty (Subst name uni fun a) -> Subst name uni fun a
$cstimes :: forall name (uni :: * -> *) fun a b.
Integral b =>
b -> Subst name uni fun a -> Subst name uni fun a
stimes :: forall b.
Integral b =>
b -> Subst name uni fun a -> Subst name uni fun a
Semigroup, Semigroup (Subst name uni fun a)
Subst name uni fun a
Semigroup (Subst name uni fun a) =>
Subst name uni fun a
-> (Subst name uni fun a
    -> Subst name uni fun a -> Subst name uni fun a)
-> ([Subst name uni fun a] -> Subst name uni fun a)
-> Monoid (Subst name uni fun a)
[Subst name uni fun a] -> Subst name uni fun a
Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall name (uni :: * -> *) fun a. Semigroup (Subst name uni fun a)
forall name (uni :: * -> *) fun a. Subst name uni fun a
forall name (uni :: * -> *) fun a.
[Subst name uni fun a] -> Subst name uni fun a
forall name (uni :: * -> *) fun a.
Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
$cmempty :: forall name (uni :: * -> *) fun a. Subst name uni fun a
mempty :: Subst name uni fun a
$cmappend :: forall name (uni :: * -> *) fun a.
Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
mappend :: Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
$cmconcat :: forall name (uni :: * -> *) fun a.
[Subst name uni fun a] -> Subst name uni fun a
mconcat :: [Subst name uni fun a] -> Subst name uni fun a
Monoid)

makeLenses ''TermEnv
makeLenses ''Subst

data VarInfo name uni fun ann = VarInfo
  { forall name (uni :: * -> *) fun ann.
VarInfo name uni fun ann -> [(name, ann)]
_varBinders :: [(name, ann)]
  -- ^ Lambda binders in the RHS (definition) of the variable.
  , forall name (uni :: * -> *) fun ann.
VarInfo name uni fun ann -> Term name uni fun ann
_varRhs :: Term name uni fun ann
  -- ^ The RHS (definition) of the variable.
  , forall name (uni :: * -> *) fun ann.
VarInfo name uni fun ann -> InlineTerm name uni fun ann
_varRhsBody :: InlineTerm name uni fun ann
  {-^ The body of the RHS of the variable (i.e., RHS minus the binders).
  Using 'InlineTerm' here to ensure the body is renamed when inlined. -}
  }

makeLenses ''VarInfo

-- | UPLC inliner state
data S name uni fun a = S
  { forall name (uni :: * -> *) fun a.
S name uni fun a -> Subst name uni fun a
_subst :: Subst name uni fun a
  , forall name (uni :: * -> *) fun a.
S name uni fun a -> UniqueMap TermUnique (VarInfo name uni fun a)
_vars :: PLC.UniqueMap TermUnique (VarInfo name uni fun a)
  }

makeLenses ''S

instance Semigroup (S name uni fun a) where
  S Subst name uni fun a
a1 UniqueMap TermUnique (VarInfo name uni fun a)
b1 <> :: S name uni fun a -> S name uni fun a -> S name uni fun a
<> S Subst name uni fun a
a2 UniqueMap TermUnique (VarInfo name uni fun a)
b2 = Subst name uni fun a
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> S name uni fun a
forall name (uni :: * -> *) fun a.
Subst name uni fun a
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> S name uni fun a
S (Subst name uni fun a
a1 Subst name uni fun a
-> Subst name uni fun a -> Subst name uni fun a
forall a. Semigroup a => a -> a -> a
<> Subst name uni fun a
a2) (UniqueMap TermUnique (VarInfo name uni fun a)
b1 UniqueMap TermUnique (VarInfo name uni fun a)
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> UniqueMap TermUnique (VarInfo name uni fun a)
forall a. Semigroup a => a -> a -> a
<> UniqueMap TermUnique (VarInfo name uni fun a)
b2)

instance Monoid (S name uni fun a) where
  mempty :: S name uni fun a
mempty = Subst name uni fun a
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> S name uni fun a
forall name (uni :: * -> *) fun a.
Subst name uni fun a
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> S name uni fun a
S Subst name uni fun a
forall a. Monoid a => a
mempty UniqueMap TermUnique (VarInfo name uni fun a)
forall a. Monoid a => a
mempty

type ExternalConstraints name uni fun m =
  ( HasUnique name TermUnique
  , Eq name
  , PLC.ToBuiltinMeaning uni fun
  , MonadQuote m
  )

type InliningConstraints name uni fun =
  ( HasUnique name TermUnique
  , Eq name
  , PLC.ToBuiltinMeaning uni fun
  )

-- See Note [Differences from PIR inliner] 2
data InlineInfo name fun a = InlineInfo
  { forall name fun a. InlineInfo name fun a -> Usages
_iiUsages :: Usages.Usages
  , forall name fun a. InlineInfo name fun a -> InlineHints name a
_iiHints :: InlineHints name a
  , forall name fun a.
InlineInfo name fun a -> BuiltinSemanticsVariant fun
_iiBuiltinSemanticsVariant :: PLC.BuiltinSemanticsVariant fun
  , forall name fun a. InlineInfo name fun a -> Bool
_iiInlineConstants :: Bool
  , forall name fun a. InlineInfo name fun a -> AstSize
_iiInlineCallsiteGrowth :: AstSize
  , forall name fun a. InlineInfo name fun a -> Bool
_iiPreserveLogging :: Bool
  }

makeLenses ''InlineInfo

-- Using a concrete monad makes a very large difference to the performance
-- of this module (determined from profiling)

-- | The monad the inliner runs in.
type InlineM name uni fun a =
  ReaderT (InlineInfo name fun a) (StateT (S name uni fun (Ann a)) Quote)

-- | Look up the unprocessed variable in the substitution.
lookupTerm
  :: HasUnique name TermUnique
  => name
  -> S name uni fun a
  -> Maybe (InlineTerm name uni fun a)
lookupTerm :: forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name -> S name uni fun a -> Maybe (InlineTerm name uni fun a)
lookupTerm name
n S name uni fun a
s = name
-> UniqueMap TermUnique (InlineTerm name uni fun a)
-> Maybe (InlineTerm name uni fun a)
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
UMap.lookupName name
n (UniqueMap TermUnique (InlineTerm name uni fun a)
 -> Maybe (InlineTerm name uni fun a))
-> UniqueMap TermUnique (InlineTerm name uni fun a)
-> Maybe (InlineTerm name uni fun a)
forall a b. (a -> b) -> a -> b
$ S name uni fun a
s S name uni fun a
-> Getting
     (UniqueMap TermUnique (InlineTerm name uni fun a))
     (S name uni fun a)
     (UniqueMap TermUnique (InlineTerm name uni fun a))
-> UniqueMap TermUnique (InlineTerm name uni fun a)
forall s a. s -> Getting a s a -> a
^. (Subst name uni fun a
 -> Const
      (UniqueMap TermUnique (InlineTerm name uni fun a))
      (Subst name uni fun a))
-> S name uni fun a
-> Const
     (UniqueMap TermUnique (InlineTerm name uni fun a))
     (S name uni fun a)
forall name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Subst name uni fun a -> f (Subst name uni fun a))
-> S name uni fun a -> f (S name uni fun a)
subst ((Subst name uni fun a
  -> Const
       (UniqueMap TermUnique (InlineTerm name uni fun a))
       (Subst name uni fun a))
 -> S name uni fun a
 -> Const
      (UniqueMap TermUnique (InlineTerm name uni fun a))
      (S name uni fun a))
-> ((UniqueMap TermUnique (InlineTerm name uni fun a)
     -> Const
          (UniqueMap TermUnique (InlineTerm name uni fun a))
          (UniqueMap TermUnique (InlineTerm name uni fun a)))
    -> Subst name uni fun a
    -> Const
         (UniqueMap TermUnique (InlineTerm name uni fun a))
         (Subst name uni fun a))
-> Getting
     (UniqueMap TermUnique (InlineTerm name uni fun a))
     (S name uni fun a)
     (UniqueMap TermUnique (InlineTerm name uni fun a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermEnv name uni fun a
 -> Const
      (UniqueMap TermUnique (InlineTerm name uni fun a))
      (TermEnv name uni fun a))
-> Subst name uni fun a
-> Const
     (UniqueMap TermUnique (InlineTerm name uni fun a))
     (Subst name uni fun a)
forall name (uni :: * -> *) fun a name (uni :: * -> *) fun a
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (TermEnv name uni fun a) (f (TermEnv name uni fun a))
-> p (Subst name uni fun a) (f (Subst name uni fun a))
termEnv ((TermEnv name uni fun a
  -> Const
       (UniqueMap TermUnique (InlineTerm name uni fun a))
       (TermEnv name uni fun a))
 -> Subst name uni fun a
 -> Const
      (UniqueMap TermUnique (InlineTerm name uni fun a))
      (Subst name uni fun a))
-> ((UniqueMap TermUnique (InlineTerm name uni fun a)
     -> Const
          (UniqueMap TermUnique (InlineTerm name uni fun a))
          (UniqueMap TermUnique (InlineTerm name uni fun a)))
    -> TermEnv name uni fun a
    -> Const
         (UniqueMap TermUnique (InlineTerm name uni fun a))
         (TermEnv name uni fun a))
-> (UniqueMap TermUnique (InlineTerm name uni fun a)
    -> Const
         (UniqueMap TermUnique (InlineTerm name uni fun a))
         (UniqueMap TermUnique (InlineTerm name uni fun a)))
-> Subst name uni fun a
-> Const
     (UniqueMap TermUnique (InlineTerm name uni fun a))
     (Subst name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueMap TermUnique (InlineTerm name uni fun a)
 -> Const
      (UniqueMap TermUnique (InlineTerm name uni fun a))
      (UniqueMap TermUnique (InlineTerm name uni fun a)))
-> TermEnv name uni fun a
-> Const
     (UniqueMap TermUnique (InlineTerm name uni fun a))
     (TermEnv name uni fun a)
forall name (uni :: * -> *) fun a name (uni :: * -> *) fun a
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (UniqueMap TermUnique (InlineTerm name uni fun a))
  (f (UniqueMap TermUnique (InlineTerm name uni fun a)))
-> p (TermEnv name uni fun a) (f (TermEnv name uni fun a))
unTermEnv

-- | Insert the unprocessed variable into the substitution.
extendTerm
  :: HasUnique name TermUnique
  => name
  -- ^ The name of the variable.
  -> InlineTerm name uni fun a
  -- ^ The substitution range.
  -> S name uni fun a
  -- ^ The substitution.
  -> S name uni fun a
extendTerm :: forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name
-> InlineTerm name uni fun a
-> S name uni fun a
-> S name uni fun a
extendTerm name
n InlineTerm name uni fun a
clos S name uni fun a
s =
  S name uni fun a
s S name uni fun a
-> (S name uni fun a -> S name uni fun a) -> S name uni fun a
forall a b. a -> (a -> b) -> b
& (Subst name uni fun a -> Identity (Subst name uni fun a))
-> S name uni fun a -> Identity (S name uni fun a)
forall name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Subst name uni fun a -> f (Subst name uni fun a))
-> S name uni fun a -> f (S name uni fun a)
subst ((Subst name uni fun a -> Identity (Subst name uni fun a))
 -> S name uni fun a -> Identity (S name uni fun a))
-> ((UniqueMap TermUnique (InlineTerm name uni fun a)
     -> Identity (UniqueMap TermUnique (InlineTerm name uni fun a)))
    -> Subst name uni fun a -> Identity (Subst name uni fun a))
-> (UniqueMap TermUnique (InlineTerm name uni fun a)
    -> Identity (UniqueMap TermUnique (InlineTerm name uni fun a)))
-> S name uni fun a
-> Identity (S name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermEnv name uni fun a -> Identity (TermEnv name uni fun a))
-> Subst name uni fun a -> Identity (Subst name uni fun a)
forall name (uni :: * -> *) fun a name (uni :: * -> *) fun a
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (TermEnv name uni fun a) (f (TermEnv name uni fun a))
-> p (Subst name uni fun a) (f (Subst name uni fun a))
termEnv ((TermEnv name uni fun a -> Identity (TermEnv name uni fun a))
 -> Subst name uni fun a -> Identity (Subst name uni fun a))
-> ((UniqueMap TermUnique (InlineTerm name uni fun a)
     -> Identity (UniqueMap TermUnique (InlineTerm name uni fun a)))
    -> TermEnv name uni fun a -> Identity (TermEnv name uni fun a))
-> (UniqueMap TermUnique (InlineTerm name uni fun a)
    -> Identity (UniqueMap TermUnique (InlineTerm name uni fun a)))
-> Subst name uni fun a
-> Identity (Subst name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueMap TermUnique (InlineTerm name uni fun a)
 -> Identity (UniqueMap TermUnique (InlineTerm name uni fun a)))
-> TermEnv name uni fun a -> Identity (TermEnv name uni fun a)
forall name (uni :: * -> *) fun a name (uni :: * -> *) fun a
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (UniqueMap TermUnique (InlineTerm name uni fun a))
  (f (UniqueMap TermUnique (InlineTerm name uni fun a)))
-> p (TermEnv name uni fun a) (f (TermEnv name uni fun a))
unTermEnv ((UniqueMap TermUnique (InlineTerm name uni fun a)
  -> Identity (UniqueMap TermUnique (InlineTerm name uni fun a)))
 -> S name uni fun a -> Identity (S name uni fun a))
-> (UniqueMap TermUnique (InlineTerm name uni fun a)
    -> UniqueMap TermUnique (InlineTerm name uni fun a))
-> S name uni fun a
-> S name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ name
-> InlineTerm name uni fun a
-> UniqueMap TermUnique (InlineTerm name uni fun a)
-> UniqueMap TermUnique (InlineTerm name uni fun a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName name
n InlineTerm name uni fun a
clos

lookupVarInfo
  :: HasUnique name TermUnique
  => name
  -> S name uni fun a
  -> Maybe (VarInfo name uni fun a)
lookupVarInfo :: forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name -> S name uni fun a -> Maybe (VarInfo name uni fun a)
lookupVarInfo name
n S name uni fun a
s = name
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> Maybe (VarInfo name uni fun a)
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
UMap.lookupName name
n (UniqueMap TermUnique (VarInfo name uni fun a)
 -> Maybe (VarInfo name uni fun a))
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> Maybe (VarInfo name uni fun a)
forall a b. (a -> b) -> a -> b
$ S name uni fun a
s S name uni fun a
-> Getting
     (UniqueMap TermUnique (VarInfo name uni fun a))
     (S name uni fun a)
     (UniqueMap TermUnique (VarInfo name uni fun a))
-> UniqueMap TermUnique (VarInfo name uni fun a)
forall s a. s -> Getting a s a -> a
^. Getting
  (UniqueMap TermUnique (VarInfo name uni fun a))
  (S name uni fun a)
  (UniqueMap TermUnique (VarInfo name uni fun a))
forall name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(UniqueMap TermUnique (VarInfo name uni fun a)
 -> f (UniqueMap TermUnique (VarInfo name uni fun a)))
-> S name uni fun a -> f (S name uni fun a)
vars

extendVarInfo
  :: HasUnique name TermUnique
  => name
  -> VarInfo name uni fun a
  -> S name uni fun a
  -> S name uni fun a
extendVarInfo :: forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name
-> VarInfo name uni fun a -> S name uni fun a -> S name uni fun a
extendVarInfo name
n VarInfo name uni fun a
info S name uni fun a
s = S name uni fun a
s S name uni fun a
-> (S name uni fun a -> S name uni fun a) -> S name uni fun a
forall a b. a -> (a -> b) -> b
& (UniqueMap TermUnique (VarInfo name uni fun a)
 -> Identity (UniqueMap TermUnique (VarInfo name uni fun a)))
-> S name uni fun a -> Identity (S name uni fun a)
forall name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(UniqueMap TermUnique (VarInfo name uni fun a)
 -> f (UniqueMap TermUnique (VarInfo name uni fun a)))
-> S name uni fun a -> f (S name uni fun a)
vars ((UniqueMap TermUnique (VarInfo name uni fun a)
  -> Identity (UniqueMap TermUnique (VarInfo name uni fun a)))
 -> S name uni fun a -> Identity (S name uni fun a))
-> (UniqueMap TermUnique (VarInfo name uni fun a)
    -> UniqueMap TermUnique (VarInfo name uni fun a))
-> S name uni fun a
-> S name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ name
-> VarInfo name uni fun a
-> UniqueMap TermUnique (VarInfo name uni fun a)
-> UniqueMap TermUnique (VarInfo name uni fun a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName name
n VarInfo name uni fun a
info

{-| Inline simple bindings. Relies on global uniqueness, and preserves it.
See Note [Inlining and global uniqueness] -}
inline
  :: forall name uni fun m a
   . ExternalConstraints name uni fun m
  => AstSize
  -- ^ inline threshold
  -> Bool
  -- ^ inline constants
  -> Bool
  -- ^ preserve logging
  -> InlineHints name a
  -> PLC.BuiltinSemanticsVariant fun
  -> Term name uni fun a
  -> SimplifierT name uni fun a m (Term name uni fun a)
inline :: forall name (uni :: * -> *) fun (m :: * -> *) a.
ExternalConstraints name uni fun m =>
AstSize
-> Bool
-> Bool
-> InlineHints name a
-> BuiltinSemanticsVariant fun
-> Term name uni fun a
-> SimplifierT name uni fun a m (Term name uni fun a)
inline
  AstSize
callsiteGrowth
  Bool
inlineConstants
  Bool
preserveLogging
  InlineHints name a
hints
  BuiltinSemanticsVariant fun
builtinSemanticsVariant
  Term name uni fun a
t = do
    Term name uni fun (Ann a)
decoratedResult <-
      Quote (Term name uni fun (Ann a))
-> SimplifierT name uni fun a m (Term name uni fun (Ann a))
forall a. Quote a -> SimplifierT name uni fun a m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Term name uni fun (Ann a))
 -> SimplifierT name uni fun a m (Term name uni fun (Ann a)))
-> Quote (Term name uni fun (Ann a))
-> SimplifierT name uni fun a m (Term name uni fun (Ann a))
forall a b. (a -> b) -> a -> b
$
        (StateT
   (S name uni fun (Ann a))
   (QuoteT Identity)
   (Term name uni fun (Ann a))
 -> S name uni fun (Ann a) -> Quote (Term name uni fun (Ann a)))
-> S name uni fun (Ann a)
-> StateT
     (S name uni fun (Ann a))
     (QuoteT Identity)
     (Term name uni fun (Ann a))
-> Quote (Term name uni fun (Ann a))
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  (S name uni fun (Ann a))
  (QuoteT Identity)
  (Term name uni fun (Ann a))
-> S name uni fun (Ann a) -> Quote (Term name uni fun (Ann a))
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT S name uni fun (Ann a)
forall a. Monoid a => a
mempty (StateT
   (S name uni fun (Ann a))
   (QuoteT Identity)
   (Term name uni fun (Ann a))
 -> Quote (Term name uni fun (Ann a)))
-> StateT
     (S name uni fun (Ann a))
     (QuoteT Identity)
     (Term name uni fun (Ann a))
-> Quote (Term name uni fun (Ann a))
forall a b. (a -> b) -> a -> b
$
          ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  (Term name uni fun (Ann a))
-> InlineInfo name fun a
-> StateT
     (S name uni fun (Ann a))
     (QuoteT Identity)
     (Term name uni fun (Ann a))
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT
            (Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
processTerm (a -> Ann a
forall a. a -> Ann a
emptyDecoration (a -> Ann a) -> Term name uni fun a -> Term name uni fun (Ann a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun a
t))
            InlineInfo
              { _iiUsages :: Usages
_iiUsages = Term name uni fun a -> Usages
forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
Term name uni fun a -> Usages
Usages.termUsages Term name uni fun a
t
              , _iiHints :: InlineHints name a
_iiHints = InlineHints name a
hints
              , _iiBuiltinSemanticsVariant :: BuiltinSemanticsVariant fun
_iiBuiltinSemanticsVariant = BuiltinSemanticsVariant fun
builtinSemanticsVariant
              , _iiInlineConstants :: Bool
_iiInlineConstants = Bool
inlineConstants
              , _iiInlineCallsiteGrowth :: AstSize
_iiInlineCallsiteGrowth = AstSize
callsiteGrowth
              , _iiPreserveLogging :: Bool
_iiPreserveLogging = Bool
preserveLogging
              }
    let result :: Term name uni fun a
result = Ann a -> a
forall a b. (a, b) -> b
snd (Ann a -> a) -> Term name uni fun (Ann a) -> Term name uni fun a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun (Ann a)
decoratedResult
    Hints
-> Term name uni fun a
-> SimplifierStage
-> Term name uni fun a
-> SimplifierT name uni fun a m ()
forall (m :: * -> *) name (uni :: * -> *) fun a.
Monad m =>
Hints
-> Term name uni fun a
-> SimplifierStage
-> Term name uni fun a
-> SimplifierT name uni fun a m ()
recordSimplificationWithHints (Inline -> Hints
CertifierHints.Inline (Term name uni fun (Ann a) -> Inline
forall name (uni :: * -> *) fun a.
Term name uni fun (Ann a) -> Inline
mkHints Term name uni fun (Ann a)
decoratedResult)) Term name uni fun a
t SimplifierStage
Inline Term name uni fun a
result
    Term name uni fun a
-> SimplifierT name uni fun a m (Term name uni fun a)
forall a. a -> SimplifierT name uni fun a m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term name uni fun a
result

-- See Note [Differences from PIR inliner] 3

{-| Extract the list of applications from a term,
a bit like a "multi-beta" reduction.

Some examples will help (annotations are omitted):
[(\x . t) a] -> Just ([(x, a)], t)

[[[(\x . (\y . (\z . t))) a] b] c] -> Just ([(x, a), (y, b), (z, c)]) t)

[[(\x . t) a] b] -> Nothing -}
extractApps
  :: Term name uni fun a
  -> Maybe ([(UTermDef name uni fun a, a)], Term name uni fun a)
extractApps :: forall name (uni :: * -> *) fun a.
Term name uni fun a
-> Maybe ([(UTermDef name uni fun a, a)], Term name uni fun a)
extractApps = [(Term name uni fun a, a)]
-> Term name uni fun a
-> Maybe
     ([(Def (UVarDecl name a) (Term name uni fun a), a)],
      Term name uni fun a)
forall {name} {uni :: * -> *} {fun} {ann}.
[(Term name uni fun ann, ann)]
-> Term name uni fun ann
-> Maybe
     ([(Def (UVarDecl name ann) (Term name uni fun ann), ann)],
      Term name uni fun ann)
go []
  where
    go :: [(Term name uni fun ann, ann)]
-> Term name uni fun ann
-> Maybe
     ([(Def (UVarDecl name ann) (Term name uni fun ann), ann)],
      Term name uni fun ann)
go [(Term name uni fun ann, ann)]
argStack (Apply ann
aa Term name uni fun ann
f Term name uni fun ann
arg) = [(Term name uni fun ann, ann)]
-> Term name uni fun ann
-> Maybe
     ([(Def (UVarDecl name ann) (Term name uni fun ann), ann)],
      Term name uni fun ann)
go ((Term name uni fun ann
arg, ann
aa) (Term name uni fun ann, ann)
-> [(Term name uni fun ann, ann)] -> [(Term name uni fun ann, ann)]
forall a. a -> [a] -> [a]
: [(Term name uni fun ann, ann)]
argStack) Term name uni fun ann
f
    go [(Term name uni fun ann, ann)]
argStack Term name uni fun ann
t = [(Term name uni fun ann, ann)]
-> [(Def (UVarDecl name ann) (Term name uni fun ann), ann)]
-> Term name uni fun ann
-> Maybe
     ([(Def (UVarDecl name ann) (Term name uni fun ann), ann)],
      Term name uni fun ann)
forall {val} {b} {name} {ann} {uni :: * -> *} {fun}.
[(val, b)]
-> [(Def (UVarDecl name ann) val, b)]
-> Term name uni fun ann
-> Maybe
     ([(Def (UVarDecl name ann) val, b)], Term name uni fun ann)
matchArgs [(Term name uni fun ann, ann)]
argStack [] Term name uni fun ann
t
    matchArgs :: [(val, b)]
-> [(Def (UVarDecl name ann) val, b)]
-> Term name uni fun ann
-> Maybe
     ([(Def (UVarDecl name ann) val, b)], Term name uni fun ann)
matchArgs ((val
arg, b
aa) : [(val, b)]
rest) [(Def (UVarDecl name ann) val, b)]
acc (LamAbs ann
a name
n Term name uni fun ann
body) =
      [(val, b)]
-> [(Def (UVarDecl name ann) val, b)]
-> Term name uni fun ann
-> Maybe
     ([(Def (UVarDecl name ann) val, b)], Term name uni fun ann)
matchArgs [(val, b)]
rest ((UVarDecl name ann -> val -> Def (UVarDecl name ann) val
forall var val. var -> val -> Def var val
Def (ann -> name -> UVarDecl name ann
forall name ann. ann -> name -> UVarDecl name ann
UVarDecl ann
a name
n) val
arg, b
aa) (Def (UVarDecl name ann) val, b)
-> [(Def (UVarDecl name ann) val, b)]
-> [(Def (UVarDecl name ann) val, b)]
forall a. a -> [a] -> [a]
: [(Def (UVarDecl name ann) val, b)]
acc) Term name uni fun ann
body
    matchArgs [] [(Def (UVarDecl name ann) val, b)]
acc Term name uni fun ann
t =
      if [(Def (UVarDecl name ann) val, b)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Def (UVarDecl name ann) val, b)]
acc then Maybe ([(Def (UVarDecl name ann) val, b)], Term name uni fun ann)
forall a. Maybe a
Nothing else ([(Def (UVarDecl name ann) val, b)], Term name uni fun ann)
-> Maybe
     ([(Def (UVarDecl name ann) val, b)], Term name uni fun ann)
forall a. a -> Maybe a
Just ([(Def (UVarDecl name ann) val, b)]
-> [(Def (UVarDecl name ann) val, b)]
forall a. [a] -> [a]
reverse [(Def (UVarDecl name ann) val, b)]
acc, Term name uni fun ann
t)
    matchArgs ((val, b)
_ : [(val, b)]
_) [(Def (UVarDecl name ann) val, b)]
_ Term name uni fun ann
_ = Maybe ([(Def (UVarDecl name ann) val, b)], Term name uni fun ann)
forall a. Maybe a
Nothing

-- | The inverse of 'extractApps'.
restoreApps
  :: [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
  -> Term name uni fun (Ann a)
  -> Term name uni fun (Ann a)
restoreApps :: forall a name (uni :: * -> *) fun.
[(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
restoreApps [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
defs Term name uni fun (Ann a)
t = [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a)
-> [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a)
forall {name} {uni :: * -> *} {fun} {a} {a}.
[(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a)
-> [(Either
       (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
     Ann a)]
-> Term name uni fun (Ann a)
makeLams [] Term name uni fun (Ann a)
t ([(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
-> [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
forall a. [a] -> [a]
reverse [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
defs)
  where
    -- `aa` is the annotation on the Apply node, and `al` is the annotation
    -- on the LamAbs node.
    makeLams :: [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a)
-> [(Either
       (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
     Ann a)]
-> Term name uni fun (Ann a)
makeLams [(Maybe (Term name uni fun (Ann a)), Ann a)]
args Term name uni fun (Ann a)
acc ((Left Ann a
al, Ann a
aa) : [(Either
    (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
  Ann a)]
rest) =
      -- `Left` means the binding is dropped, so `acc` should be decorated with `al`
      -- plus `DLamDrop`.
      -- This corresponds to Note [Inliner's Certifier Hints], #3.
      [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a)
-> [(Either
       (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
     Ann a)]
-> Term name uni fun (Ann a)
makeLams ((Maybe (Term name uni fun (Ann a))
forall a. Maybe a
Nothing, Ann a
aa) (Maybe (Term name uni fun (Ann a)), Ann a)
-> [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> [(Maybe (Term name uni fun (Ann a)), Ann a)]
forall a. a -> [a] -> [a]
: [(Maybe (Term name uni fun (Ann a)), Ann a)]
args) ([Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith (Ann a
al Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++ [Decoration
DLamDrop]) Term name uni fun (Ann a)
acc) [(Either
    (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
  Ann a)]
rest
    makeLams [(Maybe (Term name uni fun (Ann a)), Ann a)]
args Term name uni fun (Ann a)
acc ((Right (Def (UVarDecl Ann a
al name
n) Term name uni fun (Ann a)
rhs), Ann a
aa) : [(Either
    (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
  Ann a)]
rest) =
      [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a)
-> [(Either
       (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
     Ann a)]
-> Term name uni fun (Ann a)
makeLams ((Term name uni fun (Ann a) -> Maybe (Term name uni fun (Ann a))
forall a. a -> Maybe a
Just Term name uni fun (Ann a)
rhs, Ann a
aa) (Maybe (Term name uni fun (Ann a)), Ann a)
-> [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> [(Maybe (Term name uni fun (Ann a)), Ann a)]
forall a. a -> [a] -> [a]
: [(Maybe (Term name uni fun (Ann a)), Ann a)]
args) (Ann a
-> name -> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs Ann a
al name
n Term name uni fun (Ann a)
acc) [(Either
    (Ann a) (Def (UVarDecl name (Ann a)) (Term name uni fun (Ann a))),
  Ann a)]
rest
    makeLams [(Maybe (Term name uni fun (Ann a)), Ann a)]
args Term name uni fun (Ann a)
acc [] =
      [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall {name} {uni :: * -> *} {fun} {a}.
[(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
makeApps [(Maybe (Term name uni fun (Ann a)), Ann a)]
args Term name uni fun (Ann a)
acc

    makeApps :: [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
makeApps ((Maybe (Term name uni fun (Ann a))
Nothing, Ann a
aa) : [(Maybe (Term name uni fun (Ann a)), Ann a)]
args) Term name uni fun (Ann a)
acc =
      -- `Nothing` means the binding is dropped, so we decorate `acc with `aa` plus `DDrop`.
      -- This corresponds to Note [Inliner's Certifier Hints], #2.
      [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
makeApps [(Maybe (Term name uni fun (Ann a)), Ann a)]
args ([Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith (Ann a
aa Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++ [Decoration
DDrop]) Term name uni fun (Ann a)
acc)
    makeApps ((Just Term name uni fun (Ann a)
arg, Ann a
aa) : [(Maybe (Term name uni fun (Ann a)), Ann a)]
args) Term name uni fun (Ann a)
acc =
      [(Maybe (Term name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
makeApps [(Maybe (Term name uni fun (Ann a)), Ann a)]
args (Ann a
-> Term name uni fun (Ann a)
-> Term name uni fun (Ann a)
-> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply Ann a
aa Term name uni fun (Ann a)
acc Term name uni fun (Ann a)
arg)
    makeApps [] Term name uni fun (Ann a)
acc = Term name uni fun (Ann a)
acc

-- | Run the inliner on a `UntypedPlutusCore.Core.Type.Term`.
processTerm
  :: forall name uni fun a
   . InliningConstraints name uni fun
  => Term name uni fun (Ann a)
  -> InlineM name uni fun a (Term name uni fun (Ann a))
processTerm :: forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
processTerm = Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
handleTerm
  where
    handleTerm
      :: Term name uni fun (Ann a)
      -> InlineM name uni fun a (Term name uni fun (Ann a))
    handleTerm :: Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
handleTerm = \case
      v :: Term name uni fun (Ann a)
v@(Var Ann a
a name
n) ->
        Term name uni fun (Ann a)
-> (Term name uni fun (Ann a) -> Term name uni fun (Ann a))
-> Maybe (Term name uni fun (Ann a))
-> Term name uni fun (Ann a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
          Term name uni fun (Ann a)
v
          -- See Note [Inliner's Certifier Hints], #1
          ([Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith (Ann a
a Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations) (Term name uni fun (Ann a) -> Term name uni fun (Ann a))
-> (Term name uni fun (Ann a) -> Term name uni fun (Ann a))
-> Term name uni fun (Ann a)
-> Term name uni fun (Ann a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith [Decoration
DExpand])
          (Maybe (Term name uni fun (Ann a)) -> Term name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe (Term name uni fun (Ann a)))
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe (Term name uni fun (Ann a)))
substName name
n
      -- See Note [Differences from PIR inliner] 3
      (Term name uni fun (Ann a)
-> Maybe
     ([(UTermDef name uni fun (Ann a), Ann a)],
      Term name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
Term name uni fun a
-> Maybe ([(UTermDef name uni fun a, a)], Term name uni fun a)
extractApps -> Just ([(UTermDef name uni fun (Ann a), Ann a)]
bs, Term name uni fun (Ann a)
t)) -> do
        [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
ebs <- ((UTermDef name uni fun (Ann a), Ann a)
 -> ReaderT
      (InlineInfo name fun a)
      (StateT (S name uni fun (Ann a)) (QuoteT Identity))
      (Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a))
-> [(UTermDef name uni fun (Ann a), Ann a)]
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Term name uni fun (Ann a)
-> (UTermDef name uni fun (Ann a), Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> (UTermDef name uni fun (Ann a), Ann a)
-> InlineM
     name
     uni
     fun
     a
     (Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)
processSingleBinding Term name uni fun (Ann a)
t) [(UTermDef name uni fun (Ann a), Ann a)]
bs
        Term name uni fun (Ann a)
t' <- Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
processTerm Term name uni fun (Ann a)
t
        Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term name uni fun (Ann a)
 -> InlineM name uni fun a (Term name uni fun (Ann a)))
-> Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall a b. (a -> b) -> a -> b
$ [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall a name (uni :: * -> *) fun.
[(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
restoreApps [(Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)]
ebs Term name uni fun (Ann a)
t'
      Term name uni fun (Ann a)
t -> Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
inlineSaturatedApp (Term name uni fun (Ann a)
 -> InlineM name uni fun a (Term name uni fun (Ann a)))
-> InlineM name uni fun a (Term name uni fun (Ann a))
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo name fun a)
        (StateT (S name uni fun (Ann a)) (QuoteT Identity))))
  (Term name uni fun (Ann a))
  (Term name uni fun (Ann a))
  (Term name uni fun (Ann a))
  (Term name uni fun (Ann a))
-> Term name uni fun (Ann a)
-> (Term name uni fun (Ann a)
    -> InlineM name uni fun a (Term name uni fun (Ann a)))
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall (m :: * -> *) s t a b.
LensLike (WrappedMonad m) s t a b -> s -> (a -> m b) -> m t
forMOf LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo name fun a)
        (StateT (S name uni fun (Ann a)) (QuoteT Identity))))
  (Term name uni fun (Ann a))
  (Term name uni fun (Ann a))
  (Term name uni fun (Ann a))
  (Term name uni fun (Ann a))
forall name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Term name uni fun ann -> f (Term name uni fun ann))
-> Term name uni fun ann -> f (Term name uni fun ann)
termSubterms Term name uni fun (Ann a)
t Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
processTerm

    -- See Note [Renaming strategy]
    substName :: name -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
    substName :: name
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe (Term name uni fun (Ann a)))
substName name
name = (S name uni fun (Ann a) -> Maybe (InlineTerm name uni fun (Ann a)))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe (InlineTerm name uni fun (Ann a)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (name
-> S name uni fun (Ann a)
-> Maybe (InlineTerm name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name -> S name uni fun a -> Maybe (InlineTerm name uni fun a)
lookupTerm name
name) ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  (Maybe (InlineTerm name uni fun (Ann a)))
-> (Maybe (InlineTerm name uni fun (Ann a))
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         (Maybe (Term name uni fun (Ann a))))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe (Term name uni fun (Ann a)))
forall a b.
ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  a
-> (a
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         b)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (InlineTerm name uni fun (Ann a)
 -> InlineM name uni fun a (Term name uni fun (Ann a)))
-> Maybe (InlineTerm name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe (Term name uni fun (Ann a)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse InlineTerm name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
renameTerm

    -- See Note [Inlining approach and 'Secrets of the GHC Inliner']
    renameTerm
      :: InlineTerm name uni fun (Ann a)
      -> InlineM name uni fun a (Term name uni fun (Ann a))
    renameTerm :: InlineTerm name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
renameTerm = \case
      -- Already processed term, just rename and put it in, don't do any
      -- further optimization here.
      Done Dupable (Term name uni fun (Ann a))
t -> Dupable (Term name uni fun (Ann a))
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Term name uni fun (Ann a))
t

processSingleBinding
  :: InliningConstraints name uni fun
  => Term name uni fun (Ann a)
  -> (UTermDef name uni fun (Ann a), Ann a)
  -> InlineM name uni fun a (Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)
processSingleBinding :: forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> (UTermDef name uni fun (Ann a), Ann a)
-> InlineM
     name
     uni
     fun
     a
     (Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)
processSingleBinding Term name uni fun (Ann a)
body (Def vd :: UVarDecl name (Ann a)
vd@(UVarDecl Ann a
a name
n) Term name uni fun (Ann a)
rhs0, Ann a
aa) =
  (,Ann a
aa) (Either (Ann a) (UTermDef name uni fun (Ann a))
 -> (Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)), Ann a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    Term name uni fun (Ann a)
-> a
-> name
-> Term name uni fun (Ann a)
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> a
-> name
-> Term name uni fun (Ann a)
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
maybeAddSubst Term name uni fun (Ann a)
body (Ann a -> a
forall a b. (a, b) -> b
snd Ann a
a) name
n Term name uni fun (Ann a)
rhs0 InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
-> (Maybe (Term name uni fun (Ann a))
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         (Either (Ann a) (UTermDef name uni fun (Ann a))))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)))
forall a b.
ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  a
-> (a
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         b)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Term name uni fun (Ann a)
rhs -> do
        let ([(name, Ann a)]
binders, Term name uni fun (Ann a)
rhsBody) = Term name uni fun (Ann a)
-> ([(name, Ann a)], Term name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
Term name uni fun a -> ([(name, a)], Term name uni fun a)
UPLC.splitParams Term name uni fun (Ann a)
rhs
        (S name uni fun (Ann a) -> S name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((S name uni fun (Ann a) -> S name uni fun (Ann a))
 -> ReaderT
      (InlineInfo name fun a)
      (StateT (S name uni fun (Ann a)) (QuoteT Identity))
      ())
-> (VarInfo name uni fun (Ann a)
    -> S name uni fun (Ann a) -> S name uni fun (Ann a))
-> VarInfo name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name
-> VarInfo name uni fun (Ann a)
-> S name uni fun (Ann a)
-> S name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name
-> VarInfo name uni fun a -> S name uni fun a -> S name uni fun a
extendVarInfo name
n (VarInfo name uni fun (Ann a)
 -> ReaderT
      (InlineInfo name fun a)
      (StateT (S name uni fun (Ann a)) (QuoteT Identity))
      ())
-> VarInfo name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     ()
forall a b. (a -> b) -> a -> b
$
          VarInfo
            { _varBinders :: [(name, Ann a)]
_varBinders = [(name, Ann a)]
binders
            , _varRhs :: Term name uni fun (Ann a)
_varRhs = Term name uni fun (Ann a)
rhs
            , _varRhsBody :: InlineTerm name uni fun (Ann a)
_varRhsBody = Dupable (Term name uni fun (Ann a))
-> InlineTerm name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
Dupable (Term name uni fun a) -> InlineTerm name uni fun a
Done (Term name uni fun (Ann a) -> Dupable (Term name uni fun (Ann a))
forall a. a -> Dupable a
dupable Term name uni fun (Ann a)
rhsBody)
            }
        Either (Ann a) (UTermDef name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Ann a) (UTermDef name uni fun (Ann a))
 -> ReaderT
      (InlineInfo name fun a)
      (StateT (S name uni fun (Ann a)) (QuoteT Identity))
      (Either (Ann a) (UTermDef name uni fun (Ann a))))
-> (UTermDef name uni fun (Ann a)
    -> Either (Ann a) (UTermDef name uni fun (Ann a)))
-> UTermDef name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTermDef name uni fun (Ann a)
-> Either (Ann a) (UTermDef name uni fun (Ann a))
forall a b. b -> Either a b
Right (UTermDef name uni fun (Ann a)
 -> ReaderT
      (InlineInfo name fun a)
      (StateT (S name uni fun (Ann a)) (QuoteT Identity))
      (Either (Ann a) (UTermDef name uni fun (Ann a))))
-> UTermDef name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)))
forall a b. (a -> b) -> a -> b
$ UVarDecl name (Ann a)
-> Term name uni fun (Ann a) -> UTermDef name uni fun (Ann a)
forall var val. var -> val -> Def var val
Def UVarDecl name (Ann a)
vd Term name uni fun (Ann a)
rhs
      Maybe (Term name uni fun (Ann a))
Nothing -> Either (Ann a) (UTermDef name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Either (Ann a) (UTermDef name uni fun (Ann a)))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ann a -> Either (Ann a) (UTermDef name uni fun (Ann a))
forall a b. a -> Either a b
Left Ann a
a)

{-| Check against the heuristics we have for inlining and either inline
the term binding or not. The arguments to this function are the fields of the
'TermBinding' being processed.
Nothing means that we are inlining the term:
  * we have extended the substitution, and
  * we are removing the binding (hence we return Nothing). -}
maybeAddSubst
  :: forall name uni fun a
   . InliningConstraints name uni fun
  => Term name uni fun (Ann a)
  -> a
  -> name
  -> Term name uni fun (Ann a)
  -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
maybeAddSubst :: forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> a
-> name
-> Term name uni fun (Ann a)
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
maybeAddSubst Term name uni fun (Ann a)
body a
a name
n Term name uni fun (Ann a)
rhs0 = do
  Term name uni fun (Ann a)
rhs <- Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
processTerm Term name uni fun (Ann a)
rhs0

  -- Check whether we've been told specifically to inline this
  InlineHints name a
hints <- Getting
  (InlineHints name a) (InlineInfo name fun a) (InlineHints name a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (InlineHints name a)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (InlineHints name a) (InlineInfo name fun a) (InlineHints name a)
forall name fun a name a (f :: * -> *).
Functor f =>
(InlineHints name a -> f (InlineHints name a))
-> InlineInfo name fun a -> f (InlineInfo name fun a)
iiHints
  case InlineHints name a -> a -> name -> Inline
forall name a. InlineHints name a -> a -> name -> Inline
shouldInline InlineHints name a
hints a
a name
n of
    Inline
AlwaysInline ->
      -- if we've been told specifically, then do it right away
      InlineTerm name uni fun (Ann a)
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall b.
InlineTerm name uni fun (Ann a) -> InlineM name uni fun a (Maybe b)
extendAndDrop (Dupable (Term name uni fun (Ann a))
-> InlineTerm name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
Dupable (Term name uni fun a) -> InlineTerm name uni fun a
Done (Dupable (Term name uni fun (Ann a))
 -> InlineTerm name uni fun (Ann a))
-> Dupable (Term name uni fun (Ann a))
-> InlineTerm name uni fun (Ann a)
forall a b. (a -> b) -> a -> b
$ Term name uni fun (Ann a) -> Dupable (Term name uni fun (Ann a))
forall a. a -> Dupable a
dupable Term name uni fun (Ann a)
rhs)
    Inline
hint ->
      let safeToInline :: Bool
safeToInline = Inline
hint Inline -> Inline -> Bool
forall a. Eq a => a -> a -> Bool
== Inline
SafeToInline
       in ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  Bool
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM
            (Bool
-> name
-> Term name uni fun (Ann a)
-> Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     Bool
forall name (uni :: * -> *) fun a b c.
InliningConstraints name uni fun =>
Bool
-> name
-> Term name uni fun a
-> Term name uni fun b
-> InlineM name uni fun c Bool
shouldUnconditionallyInline Bool
safeToInline name
n Term name uni fun (Ann a)
rhs Term name uni fun (Ann a)
body)
            (InlineTerm name uni fun (Ann a)
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall b.
InlineTerm name uni fun (Ann a) -> InlineM name uni fun a (Maybe b)
extendAndDrop (Dupable (Term name uni fun (Ann a))
-> InlineTerm name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
Dupable (Term name uni fun a) -> InlineTerm name uni fun a
Done (Dupable (Term name uni fun (Ann a))
 -> InlineTerm name uni fun (Ann a))
-> Dupable (Term name uni fun (Ann a))
-> InlineTerm name uni fun (Ann a)
forall a b. (a -> b) -> a -> b
$ Term name uni fun (Ann a) -> Dupable (Term name uni fun (Ann a))
forall a. a -> Dupable a
dupable Term name uni fun (Ann a)
rhs))
            (Maybe (Term name uni fun (Ann a))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term name uni fun (Ann a))
 -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a))))
-> Maybe (Term name uni fun (Ann a))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall a b. (a -> b) -> a -> b
$ Term name uni fun (Ann a) -> Maybe (Term name uni fun (Ann a))
forall a. a -> Maybe a
Just Term name uni fun (Ann a)
rhs)
  where
    extendAndDrop
      :: forall b
       . InlineTerm name uni fun (Ann a)
      -> InlineM name uni fun a (Maybe b)
    extendAndDrop :: forall b.
InlineTerm name uni fun (Ann a) -> InlineM name uni fun a (Maybe b)
extendAndDrop InlineTerm name uni fun (Ann a)
t = (S name uni fun (Ann a) -> S name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (name
-> InlineTerm name uni fun (Ann a)
-> S name uni fun (Ann a)
-> S name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name
-> InlineTerm name uni fun a
-> S name uni fun a
-> S name uni fun a
extendTerm name
n InlineTerm name uni fun (Ann a)
t) ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  ()
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe b)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe b)
forall a b.
ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     b
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe b
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe b)
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe b
forall a. Maybe a
Nothing

shouldUnconditionallyInline
  :: InliningConstraints name uni fun
  => Bool
  {-^ Whether we know that the binding is safe to inline.
  If so, bypass the purity check. -}
  -> name
  -> Term name uni fun a
  -> Term name uni fun b
  -> InlineM name uni fun c Bool
shouldUnconditionallyInline :: forall name (uni :: * -> *) fun a b c.
InliningConstraints name uni fun =>
Bool
-> name
-> Term name uni fun a
-> Term name uni fun b
-> InlineM name uni fun c Bool
shouldUnconditionallyInline Bool
safe name
n Term name uni fun a
rhs Term name uni fun b
body = do
  Bool
isTermPure <- Term name uni fun a -> InlineM name uni fun c Bool
forall (uni :: * -> *) fun name a b.
ToBuiltinMeaning uni fun =>
Term name uni fun a -> InlineM name uni fun b Bool
checkPurity Term name uni fun a
rhs
  Bool
inlineConstants <- Getting Bool (InlineInfo name fun c) Bool
-> InlineM name uni fun c Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool (InlineInfo name fun c) Bool
forall name fun a (f :: * -> *).
Functor f =>
(Bool -> f Bool)
-> InlineInfo name fun a -> f (InlineInfo name fun a)
iiInlineConstants
  Bool -> InlineM name uni fun c Bool
preUnconditional Bool
isTermPure InlineM name uni fun c Bool
-> InlineM name uni fun c Bool -> InlineM name uni fun c Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
||^ Bool -> Bool -> InlineM name uni fun c Bool
postUnconditional Bool
inlineConstants Bool
isTermPure
  where
    -- similar to the paper, preUnconditional inlining checks that the binder
    -- is 'OnceSafe'.  I.e., it's used at most once AND it neither duplicate code
    -- or work. While we don't check for lambda etc like in the paper,
    -- 'effectSafe' ensures that it isn't doing any substantial work.
    -- We actually also inline 'Dead' binders (i.e., remove dead code) here.
    preUnconditional :: Bool -> InlineM name uni fun c Bool
preUnconditional Bool
isTermPure =
      name -> InlineM name uni fun c Bool
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
name -> InlineM name uni fun a Bool
nameUsedAtMostOnce name
n InlineM name uni fun c Bool
-> InlineM name uni fun c Bool -> InlineM name uni fun c Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
&&^ (Bool -> InlineM name uni fun c Bool
forall a.
a
-> ReaderT
     (InlineInfo name fun c)
     (StateT (S name uni fun (Ann c)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
safe InlineM name uni fun c Bool
-> InlineM name uni fun c Bool -> InlineM name uni fun c Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
||^ Term name uni fun b -> name -> Bool -> InlineM name uni fun c Bool
forall name (uni :: * -> *) fun a b.
InliningConstraints name uni fun =>
Term name uni fun a -> name -> Bool -> InlineM name uni fun b Bool
effectSafe Term name uni fun b
body name
n Bool
isTermPure)
    -- See Note [Inlining approach and 'Secrets of the GHC Inliner'] and
    -- [Inlining and purity]. This is the case where we don't know that the number
    -- of occurrences is exactly one, so there's no point checking if the term is
    -- immediately evaluated.
    postUnconditional :: Bool -> Bool -> InlineM name uni fun c Bool
postUnconditional Bool
inlineConstants Bool
isTermPure =
      Bool -> InlineM name uni fun c Bool
forall a.
a
-> ReaderT
     (InlineInfo name fun c)
     (StateT (S name uni fun (Ann c)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
safe Bool -> Bool -> Bool
|| Bool
isTermPure) InlineM name uni fun c Bool
-> InlineM name uni fun c Bool -> InlineM name uni fun c Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
&&^ Bool -> Term name uni fun a -> InlineM name uni fun c Bool
forall name (uni :: * -> *) fun a b.
Bool -> Term name uni fun a -> InlineM name uni fun b Bool
acceptable Bool
inlineConstants Term name uni fun a
rhs

-- | Check if term is pure. See Note [Inlining and purity]
checkPurity
  :: PLC.ToBuiltinMeaning uni fun
  => Term name uni fun a
  -> InlineM name uni fun b Bool
checkPurity :: forall (uni :: * -> *) fun name a b.
ToBuiltinMeaning uni fun =>
Term name uni fun a -> InlineM name uni fun b Bool
checkPurity Term name uni fun a
t = do
  BuiltinSemanticsVariant fun
builtinSemanticsVariant <- Getting
  (BuiltinSemanticsVariant fun)
  (InlineInfo name fun b)
  (BuiltinSemanticsVariant fun)
-> ReaderT
     (InlineInfo name fun b)
     (StateT (S name uni fun (Ann b)) (QuoteT Identity))
     (BuiltinSemanticsVariant fun)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (BuiltinSemanticsVariant fun)
  (InlineInfo name fun b)
  (BuiltinSemanticsVariant fun)
forall name fun a fun (f :: * -> *).
Functor f =>
(BuiltinSemanticsVariant fun -> f (BuiltinSemanticsVariant fun))
-> InlineInfo name fun a -> f (InlineInfo name fun a)
iiBuiltinSemanticsVariant
  Bool -> InlineM name uni fun b Bool
forall a.
a
-> ReaderT
     (InlineInfo name fun b)
     (StateT (S name uni fun (Ann b)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> InlineM name uni fun b Bool)
-> Bool -> InlineM name uni fun b Bool
forall a b. (a -> b) -> a -> b
$ BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant fun
builtinSemanticsVariant Term name uni fun a
t

nameUsedAtMostOnce
  :: forall name uni fun a
   . InliningConstraints name uni fun
  => name
  -> InlineM name uni fun a Bool
nameUsedAtMostOnce :: forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
name -> InlineM name uni fun a Bool
nameUsedAtMostOnce name
n = do
  Usages
usgs <- Getting Usages (InlineInfo name fun a) Usages
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     Usages
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Usages (InlineInfo name fun a) Usages
forall name fun a (f :: * -> *).
Functor f =>
(Usages -> f Usages)
-> InlineInfo name fun a -> f (InlineInfo name fun a)
iiUsages
  -- 'inlining' terms used 0 times is a cheap way to remove dead code
  -- while we're here
  Bool -> InlineM name uni fun a Bool
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> InlineM name uni fun a Bool)
-> Bool -> InlineM name uni fun a Bool
forall a b. (a -> b) -> a -> b
$ name -> Usages -> Int
forall n unique. HasUnique n unique => n -> Usages -> Int
Usages.getUsageCount name
n Usages
usgs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1

isFirstVarBeforeEffects
  :: forall name uni fun ann
   . InliningConstraints name uni fun
  => BuiltinSemanticsVariant fun
  -> name
  -> Term name uni fun ann
  -> Bool
isFirstVarBeforeEffects :: forall name (uni :: * -> *) fun ann.
InliningConstraints name uni fun =>
BuiltinSemanticsVariant fun
-> name -> Term name uni fun ann -> Bool
isFirstVarBeforeEffects BuiltinSemanticsVariant fun
builtinSemanticsVariant name
n Term name uni fun ann
t =
  -- This can in the worst case traverse a lot of the term, which could lead to
  -- us doing ~quadratic work as we process the program. However in practice
  -- most terms have a relatively short evaluation order before we hit Unknown,
  -- so it's not too bad.
  [EvalTerm name uni fun ann] -> Bool
go (EvalOrder name uni fun ann -> [EvalTerm name uni fun ann]
forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a -> [EvalTerm name uni fun a]
unEvalOrder (BuiltinSemanticsVariant fun
-> Term name uni fun ann -> EvalOrder name uni fun ann
forall name (uni :: * -> *) fun a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun
-> Term name uni fun a -> EvalOrder name uni fun a
termEvaluationOrder BuiltinSemanticsVariant fun
builtinSemanticsVariant Term name uni fun ann
t))
  where
    -- Found the variable we're looking for!
    go :: [EvalTerm name uni fun ann] -> Bool
go ((EvalTerm Purity
_ WorkFreedom
_ (Var ann
_ name
n')) : [EvalTerm name uni fun ann]
_) | name
n name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
n' = Bool
True
    -- Found a pure term, ignore it and continue
    go ((EvalTerm Purity
Pure WorkFreedom
_ Term name uni fun ann
_) : [EvalTerm name uni fun ann]
rest) = [EvalTerm name uni fun ann] -> Bool
go [EvalTerm name uni fun ann]
rest
    -- Found a possibly impure term, our variable is definitely not first
    go ((EvalTerm Purity
MaybeImpure WorkFreedom
_ Term name uni fun ann
_) : [EvalTerm name uni fun ann]
_) = Bool
False
    -- Don't know, be conservative
    go (EvalTerm name uni fun ann
Unknown : [EvalTerm name uni fun ann]
_) = Bool
False
    go [] = Bool
False

{-| Check if the given name is strict in the given term.
  This means that at least one occurrence of the name is found outside of the following:
  * 'delay' term
  * lambda body
  * case branch -}
isStrictIn
  :: forall name uni fun a
   . Eq name
  => name
  -> Term name uni fun a
  -> Bool
isStrictIn :: forall name (uni :: * -> *) fun a.
Eq name =>
name -> Term name uni fun a -> Bool
isStrictIn name
name = Term name uni fun a -> Bool
go
  where
    go :: Term name uni fun a -> Bool
    go :: Term name uni fun a -> Bool
go = \case
      Var a
_ann name
name' -> name
name name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
name'
      LamAbs a
_ann name
_paramName Term name uni fun a
_body -> Bool
False
      Apply a
_ann Term name uni fun a
t1 Term name uni fun a
t2 -> Term name uni fun a -> Bool
go Term name uni fun a
t1 Bool -> Bool -> Bool
|| Term name uni fun a -> Bool
go Term name uni fun a
t2
      Force a
_ann Term name uni fun a
t -> Term name uni fun a -> Bool
go Term name uni fun a
t
      Delay a
_ann Term name uni fun a
_term -> Bool
False
      Constant {} -> Bool
False
      Builtin {} -> Bool
False
      Error {} -> Bool
False
      Constr a
_ann Word64
_idx [Term name uni fun a]
terms -> (Term name uni fun a -> Bool) -> [Term name uni fun a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Term name uni fun a -> Bool
go [Term name uni fun a]
terms
      Case a
_ann Term name uni fun a
scrut Vector (Term name uni fun a)
_branches -> Term name uni fun a -> Bool
go Term name uni fun a
scrut

effectSafe
  :: forall name uni fun a b
   . InliningConstraints name uni fun
  => Term name uni fun a
  -> name
  -> Bool
  -- ^ is it pure? See Note [Inlining and purity]
  -> InlineM name uni fun b Bool
effectSafe :: forall name (uni :: * -> *) fun a b.
InliningConstraints name uni fun =>
Term name uni fun a -> name -> Bool -> InlineM name uni fun b Bool
effectSafe Term name uni fun a
body name
n Bool
termIsPure = do
  Bool
preserveLogging <- Getting Bool (InlineInfo name fun b) Bool
-> InlineM name uni fun b Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool (InlineInfo name fun b) Bool
forall name fun a (f :: * -> *).
Functor f =>
(Bool -> f Bool)
-> InlineInfo name fun a -> f (InlineInfo name fun a)
iiPreserveLogging
  BuiltinSemanticsVariant fun
builtinSemantics <- Getting
  (BuiltinSemanticsVariant fun)
  (InlineInfo name fun b)
  (BuiltinSemanticsVariant fun)
-> ReaderT
     (InlineInfo name fun b)
     (StateT (S name uni fun (Ann b)) (QuoteT Identity))
     (BuiltinSemanticsVariant fun)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (BuiltinSemanticsVariant fun)
  (InlineInfo name fun b)
  (BuiltinSemanticsVariant fun)
forall name fun a fun (f :: * -> *).
Functor f =>
(BuiltinSemanticsVariant fun -> f (BuiltinSemanticsVariant fun))
-> InlineInfo name fun a -> f (InlineInfo name fun a)
iiBuiltinSemanticsVariant
  Bool -> InlineM name uni fun b Bool
forall a.
a
-> ReaderT
     (InlineInfo name fun b)
     (StateT (S name uni fun (Ann b)) (QuoteT Identity))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> InlineM name uni fun b Bool)
-> Bool -> InlineM name uni fun b Bool
forall a b. (a -> b) -> a -> b
$
    Bool
termIsPure
      Bool -> Bool -> Bool
|| BuiltinSemanticsVariant fun -> name -> Term name uni fun a -> Bool
forall name (uni :: * -> *) fun ann.
InliningConstraints name uni fun =>
BuiltinSemanticsVariant fun
-> name -> Term name uni fun ann -> Bool
isFirstVarBeforeEffects BuiltinSemanticsVariant fun
builtinSemantics name
n Term name uni fun a
body
      Bool -> Bool -> Bool
|| (Bool -> Bool
not Bool
preserveLogging Bool -> Bool -> Bool
&& name -> Term name uni fun a -> Bool
forall name (uni :: * -> *) fun a.
Eq name =>
name -> Term name uni fun a -> Bool
isStrictIn name
n Term name uni fun a
body)

{-| Should we inline? Should only inline things that won't duplicate work
or code.  See Note [Inlining approach and 'Secrets of the GHC Inliner'] -}
acceptable
  :: Bool
  -- ^ inline constants
  -> Term name uni fun a
  -> InlineM name uni fun b Bool
acceptable :: forall name (uni :: * -> *) fun a b.
Bool -> Term name uni fun a -> InlineM name uni fun b Bool
acceptable Bool
inlineConstants Term name uni fun a
t =
  -- See Note [Inlining criteria]
  Bool
-> ReaderT
     (InlineInfo name fun b)
     (StateT (S name uni fun (Ann b)) (QuoteT Identity))
     Bool
forall a.
a
-> ReaderT
     (InlineInfo name fun b)
     (StateT (S name uni fun (Ann b)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> ReaderT
      (InlineInfo name fun b)
      (StateT (S name uni fun (Ann b)) (QuoteT Identity))
      Bool)
-> Bool
-> ReaderT
     (InlineInfo name fun b)
     (StateT (S name uni fun (Ann b)) (QuoteT Identity))
     Bool
forall a b. (a -> b) -> a -> b
$ Term name uni fun a -> Bool
forall name (uni :: * -> *) fun a. Term name uni fun a -> Bool
costIsAcceptable Term name uni fun a
t Bool -> Bool -> Bool
&& Bool -> Term name uni fun a -> Bool
forall name (uni :: * -> *) fun a.
Bool -> Term name uni fun a -> Bool
sizeIsAcceptable Bool
inlineConstants Term name uni fun a
t

{-| Is the cost increase (in terms of evaluation work) of inlining a variable
whose RHS is the given term acceptable? -}
costIsAcceptable :: Term name uni fun a -> Bool
costIsAcceptable :: forall name (uni :: * -> *) fun a. Term name uni fun a -> Bool
costIsAcceptable = \case
  Builtin {} -> Bool
True
  Var {} -> Bool
True
  Constant {} -> Bool
True
  Error {} -> Bool
True
  -- This will mean that we create closures at each use site instead of
  -- once, but that's a very low cost which we're okay rounding to 0.
  LamAbs {} -> Bool
True
  Apply {} -> Bool
False
  -- Inlining constructors of size 1 or 0 seems okay, but does result in doing
  -- the work for the elements at each use site.
  Constr a
_ Word64
_ [Term name uni fun a]
es ->
    case [Term name uni fun a]
es of
      [] -> Bool
True
      [Term name uni fun a
e] -> Term name uni fun a -> Bool
forall name (uni :: * -> *) fun a. Term name uni fun a -> Bool
costIsAcceptable Term name uni fun a
e
      [Term name uni fun a]
_ -> Bool
False
  -- Inlining a case means redoing the match at each use site
  Case {} -> Bool
False
  Force {} -> Bool
False
  Delay {} -> Bool
True

{-| Is the size increase (in the AST) of inlining a variable whose RHS is
the given term acceptable? -}
sizeIsAcceptable
  :: Bool
  -- ^ inline constants
  -> Term name uni fun a
  -> Bool
sizeIsAcceptable :: forall name (uni :: * -> *) fun a.
Bool -> Term name uni fun a -> Bool
sizeIsAcceptable Bool
inlineConstants = \case
  Builtin {} -> Bool
True
  Var {} -> Bool
True
  Error {} -> Bool
True
  -- See Note [Differences from PIR inliner] 4
  LamAbs {} -> Bool
False
  -- Inlining constructors of size 1 or 0 seems okay
  Constr a
_ Word64
_ [Term name uni fun a]
es -> case [Term name uni fun a]
es of
    [] -> Bool
True
    [Term name uni fun a
e] -> Bool -> Term name uni fun a -> Bool
forall name (uni :: * -> *) fun a.
Bool -> Term name uni fun a -> Bool
sizeIsAcceptable Bool
inlineConstants Term name uni fun a
e
    [Term name uni fun a]
_ -> Bool
False
  -- Cases are pretty big, due to the case branches
  Case {} -> Bool
False
  -- Inlining constants is deemed acceptable if the 'inlineConstants'
  -- flag is turned on, see Note [Inlining constants].
  Constant {} -> Bool
inlineConstants
  Apply {} -> Bool
False
  Force a
_ Term name uni fun a
t -> Bool -> Term name uni fun a -> Bool
forall name (uni :: * -> *) fun a.
Bool -> Term name uni fun a -> Bool
sizeIsAcceptable Bool
inlineConstants Term name uni fun a
t
  Delay a
_ Term name uni fun a
t -> Bool -> Term name uni fun a -> Bool
forall name (uni :: * -> *) fun a.
Bool -> Term name uni fun a -> Bool
sizeIsAcceptable Bool
inlineConstants Term name uni fun a
t

-- | Fully apply and beta reduce.
fullyApplyAndBetaReduce
  :: forall name uni fun a
   . InliningConstraints name uni fun
  => Ann a
  -- ^ Annotation on the variable to be replaced
  -> VarInfo name uni fun (Ann a)
  -> [(Ann a, Term name uni fun (Ann a))]
  -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
fullyApplyAndBetaReduce :: forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Ann a
-> VarInfo name uni fun (Ann a)
-> [(Ann a, Term name uni fun (Ann a))]
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
fullyApplyAndBetaReduce Ann a
av VarInfo name uni fun (Ann a)
info [(Ann a, Term name uni fun (Ann a))]
args0 = do
  Term name uni fun (Ann a)
rhsBody <-
    -- Since we would like to fully apply here, we add decorations to
    -- `rhsBody` in the following order:
    --
    --   * decorations on the outermost Apply node, plus DDrop
    --   * decorations on the next Apply node, plus DDrop
    --   * ...
    --   * decorations on the innermost Apply node, plus DDrop
    --   * `av` plus DExpand.
    --   * decorations on the first LamAbs, plus DLamDrop
    --   * decorations on the second LamAbs, plus DLamDrop
    --   * ...
    --   * decorations on the last LamAbs, plus DLamDrop
    --
    -- See Note [Inliner's Certifier Hints].
    [Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith
      ( ((Ann a, Term name uni fun (Ann a)) -> [Decoration])
-> [(Ann a, Term name uni fun (Ann a))] -> [Decoration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Ann a
annApply, Term name uni fun (Ann a)
_arg) -> Ann a
annApply Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++ [Decoration
DDrop]) ([(Ann a, Term name uni fun (Ann a))]
-> [(Ann a, Term name uni fun (Ann a))]
forall a. [a] -> [a]
reverse [(Ann a, Term name uni fun (Ann a))]
args0)
          [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++ Ann a
av Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations
          [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++ [Decoration
DExpand]
          [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++ ((name, Ann a) -> [Decoration]) -> [(name, Ann a)] -> [Decoration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(name
_name, Ann a
annLam) -> Ann a
annLam Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++ [Decoration
DLamDrop]) (VarInfo name uni fun (Ann a)
info VarInfo name uni fun (Ann a)
-> Getting
     [(name, Ann a)] (VarInfo name uni fun (Ann a)) [(name, Ann a)]
-> [(name, Ann a)]
forall s a. s -> Getting a s a -> a
^. Getting
  [(name, Ann a)] (VarInfo name uni fun (Ann a)) [(name, Ann a)]
forall name (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
([(name, ann)] -> f [(name, ann)])
-> VarInfo name uni fun ann -> f (VarInfo name uni fun ann)
varBinders)
      )
      (Term name uni fun (Ann a) -> Term name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dupable (Term name uni fun (Ann a))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable (let Done Dupable (Term name uni fun (Ann a))
rhsBody = VarInfo name uni fun (Ann a)
info VarInfo name uni fun (Ann a)
-> Getting
     (InlineTerm name uni fun (Ann a))
     (VarInfo name uni fun (Ann a))
     (InlineTerm name uni fun (Ann a))
-> InlineTerm name uni fun (Ann a)
forall s a. s -> Getting a s a -> a
^. Getting
  (InlineTerm name uni fun (Ann a))
  (VarInfo name uni fun (Ann a))
  (InlineTerm name uni fun (Ann a))
forall name (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(InlineTerm name uni fun ann -> f (InlineTerm name uni fun ann))
-> VarInfo name uni fun ann -> f (VarInfo name uni fun ann)
varRhsBody in Dupable (Term name uni fun (Ann a))
rhsBody)
  let go
        :: Term name uni fun (Ann a)
        -> [(name, Ann a)]
        -> [(Ann a, Term name uni fun (Ann a))]
        -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
      go :: Term name uni fun (Ann a)
-> [(name, Ann a)]
-> [(Ann a, Term name uni fun (Ann a))]
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
go Term name uni fun (Ann a)
acc [(name, Ann a)]
bs [(Ann a, Term name uni fun (Ann a))]
args = case ([(name, Ann a)]
bs, [(Ann a, Term name uni fun (Ann a))]
args) of
        ([], [(Ann a, Term name uni fun (Ann a))]
_) -> Maybe (Term name uni fun (Ann a))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term name uni fun (Ann a))
 -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a))))
-> (Term name uni fun (Ann a) -> Maybe (Term name uni fun (Ann a)))
-> Term name uni fun (Ann a)
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term name uni fun (Ann a) -> Maybe (Term name uni fun (Ann a))
forall a. a -> Maybe a
Just (Term name uni fun (Ann a)
 -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a))))
-> Term name uni fun (Ann a)
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall a b. (a -> b) -> a -> b
$ Term name uni fun (Ann a)
-> [(Ann a, Term name uni fun (Ann a))]
-> Term name uni fun (Ann a)
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp Term name uni fun (Ann a)
acc [(Ann a, Term name uni fun (Ann a))]
args
        ((name
param, Ann a
_annLam) : [(name, Ann a)]
params, (Ann a
_annArg, Term name uni fun (Ann a)
arg) : [(Ann a, Term name uni fun (Ann a))]
args') -> do
          Bool
safe <- name -> Term name uni fun (Ann a) -> InlineM name uni fun a Bool
safeToBetaReduce name
param Term name uni fun (Ann a)
arg
          if Bool
safe
            then do
              Term name uni fun (Ann a)
acc' <-
                (name
 -> Ann a
 -> InlineM name uni fun a (Maybe (Term name uni fun (Ann a))))
-> Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall (m :: * -> *) name ann (uni :: * -> *) fun.
Monad m =>
(name -> ann -> m (Maybe (Term name uni fun ann)))
-> Term name uni fun ann -> m (Term name uni fun ann)
termSubstNamesM
                  ( \name
n Ann a
a ->
                      if name
n name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
param
                        then
                          Term name uni fun (Ann a) -> Maybe (Term name uni fun (Ann a))
forall a. a -> Maybe a
Just
                            -- See Note [Inliner's Certifier Hints], #1
                            (Term name uni fun (Ann a) -> Maybe (Term name uni fun (Ann a)))
-> (Term name uni fun (Ann a) -> Term name uni fun (Ann a))
-> Term name uni fun (Ann a)
-> Maybe (Term name uni fun (Ann a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith (Ann a
a Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations)
                            (Term name uni fun (Ann a) -> Term name uni fun (Ann a))
-> (Term name uni fun (Ann a) -> Term name uni fun (Ann a))
-> Term name uni fun (Ann a)
-> Term name uni fun (Ann a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith [Decoration
DExpand]
                            (Term name uni fun (Ann a) -> Maybe (Term name uni fun (Ann a)))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term name uni fun (Ann a) -> m (Term name uni fun (Ann a))
PLC.rename Term name uni fun (Ann a)
arg
                        else Maybe (Term name uni fun (Ann a))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term name uni fun (Ann a))
forall a. Maybe a
Nothing
                  )
                  Term name uni fun (Ann a)
acc
              Term name uni fun (Ann a)
-> [(name, Ann a)]
-> [(Ann a, Term name uni fun (Ann a))]
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
go Term name uni fun (Ann a)
acc' [(name, Ann a)]
params [(Ann a, Term name uni fun (Ann a))]
args'
            else Maybe (Term name uni fun (Ann a))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term name uni fun (Ann a))
forall a. Maybe a
Nothing
        ([(name, Ann a)], [(Ann a, Term name uni fun (Ann a))])
_ -> Maybe (Term name uni fun (Ann a))
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term name uni fun (Ann a))
forall a. Maybe a
Nothing

      -- Is it safe to turn `(\a -> body) arg` into `body [a := arg]`?
      -- The criteria is the same as the criteria for unconditionally
      -- inlining `a`, since inlining is the same as beta reduction.
      safeToBetaReduce
        :: name
        -> Term name uni fun (Ann a)
        -> InlineM name uni fun a Bool
      safeToBetaReduce :: name -> Term name uni fun (Ann a) -> InlineM name uni fun a Bool
safeToBetaReduce name
a Term name uni fun (Ann a)
arg = Bool
-> name
-> Term name uni fun (Ann a)
-> Term name uni fun (Ann a)
-> InlineM name uni fun a Bool
forall name (uni :: * -> *) fun a b c.
InliningConstraints name uni fun =>
Bool
-> name
-> Term name uni fun a
-> Term name uni fun b
-> InlineM name uni fun c Bool
shouldUnconditionallyInline Bool
False name
a Term name uni fun (Ann a)
arg Term name uni fun (Ann a)
rhsBody
  Term name uni fun (Ann a)
-> [(name, Ann a)]
-> [(Ann a, Term name uni fun (Ann a))]
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
go Term name uni fun (Ann a)
rhsBody (VarInfo name uni fun (Ann a)
info VarInfo name uni fun (Ann a)
-> Getting
     [(name, Ann a)] (VarInfo name uni fun (Ann a)) [(name, Ann a)]
-> [(name, Ann a)]
forall s a. s -> Getting a s a -> a
^. Getting
  [(name, Ann a)] (VarInfo name uni fun (Ann a)) [(name, Ann a)]
forall name (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
([(name, ann)] -> f [(name, ann)])
-> VarInfo name uni fun ann -> f (VarInfo name uni fun ann)
varBinders) [(Ann a, Term name uni fun (Ann a))]
args0

{-| This works in the same way as
'PlutusIR.Transform.Inline.CallSiteInline.inlineSaturatedApp'.
See Note [Inlining and beta reduction of functions]. -}
inlineSaturatedApp
  :: forall name uni fun a
   . InliningConstraints name uni fun
  => Term name uni fun (Ann a)
  -> InlineM name uni fun a (Term name uni fun (Ann a))
inlineSaturatedApp :: forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Term name uni fun (Ann a)
-> InlineM name uni fun a (Term name uni fun (Ann a))
inlineSaturatedApp Term name uni fun (Ann a)
t
  | (Var Ann a
av name
name, [(Ann a, Term name uni fun (Ann a))]
args) <- Term name uni fun (Ann a)
-> (Term name uni fun (Ann a),
    [(Ann a, Term name uni fun (Ann a))])
forall name (uni :: * -> *) fun a.
Term name uni fun a
-> (Term name uni fun a, [(a, Term name uni fun a)])
UPLC.splitApplication Term name uni fun (Ann a)
t =
      (S name uni fun (Ann a) -> Maybe (VarInfo name uni fun (Ann a)))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Maybe (VarInfo name uni fun (Ann a)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (name
-> S name uni fun (Ann a) -> Maybe (VarInfo name uni fun (Ann a))
forall name (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name -> S name uni fun a -> Maybe (VarInfo name uni fun a)
lookupVarInfo name
name) ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  (Maybe (VarInfo name uni fun (Ann a)))
-> (Maybe (VarInfo name uni fun (Ann a))
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         (Term name uni fun (Ann a)))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a b.
ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  a
-> (a
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         b)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe (VarInfo name uni fun (Ann a))
Nothing -> Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term name uni fun (Ann a)
t
        Just VarInfo name uni fun (Ann a)
varInfo ->
          Ann a
-> VarInfo name uni fun (Ann a)
-> [(Ann a, Term name uni fun (Ann a))]
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
forall name (uni :: * -> *) fun a.
InliningConstraints name uni fun =>
Ann a
-> VarInfo name uni fun (Ann a)
-> [(Ann a, Term name uni fun (Ann a))]
-> InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
fullyApplyAndBetaReduce Ann a
av VarInfo name uni fun (Ann a)
varInfo [(Ann a, Term name uni fun (Ann a))]
args InlineM name uni fun a (Maybe (Term name uni fun (Ann a)))
-> (Maybe (Term name uni fun (Ann a))
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         (Term name uni fun (Ann a)))
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a b.
ReaderT
  (InlineInfo name fun a)
  (StateT (S name uni fun (Ann a)) (QuoteT Identity))
  a
-> (a
    -> ReaderT
         (InlineInfo name fun a)
         (StateT (S name uni fun (Ann a)) (QuoteT Identity))
         b)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Maybe (Term name uni fun (Ann a))
Nothing -> Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term name uni fun (Ann a)
t
            Just Term name uni fun (Ann a)
fullyApplied -> do
              AstSize
thresh <- Getting AstSize (InlineInfo name fun a) AstSize
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     AstSize
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting AstSize (InlineInfo name fun a) AstSize
forall name fun a (f :: * -> *).
Functor f =>
(AstSize -> f AstSize)
-> InlineInfo name fun a -> f (InlineInfo name fun a)
iiInlineCallsiteGrowth
              let
                -- Inline only if the size is no bigger than
                -- not inlining plus threshold.
                sizeIsOk :: Bool
sizeIsOk =
                  Term name uni fun (Ann a) -> AstSize
forall name (uni :: * -> *) fun ann.
Term name uni fun ann -> AstSize
termAstSize Term name uni fun (Ann a)
fullyApplied AstSize -> AstSize -> Bool
forall a. Ord a => a -> a -> Bool
<= Term name uni fun (Ann a) -> AstSize
forall name (uni :: * -> *) fun ann.
Term name uni fun ann -> AstSize
termAstSize Term name uni fun (Ann a)
t AstSize -> AstSize -> AstSize
forall a. Num a => a -> a -> a
+ AstSize -> AstSize -> AstSize
forall a. Ord a => a -> a -> a
max AstSize
0 AstSize
thresh
                rhs :: Term name uni fun (Ann a)
rhs = VarInfo name uni fun (Ann a)
varInfo VarInfo name uni fun (Ann a)
-> Getting
     (Term name uni fun (Ann a))
     (VarInfo name uni fun (Ann a))
     (Term name uni fun (Ann a))
-> Term name uni fun (Ann a)
forall s a. s -> Getting a s a -> a
^. Getting
  (Term name uni fun (Ann a))
  (VarInfo name uni fun (Ann a))
  (Term name uni fun (Ann a))
forall name (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(Term name uni fun ann -> f (Term name uni fun ann))
-> VarInfo name uni fun ann -> f (VarInfo name uni fun ann)
varRhs
                -- Cost is always OK if the RHS is a LamAbs,
                -- but may not be otherwise.
                costIsOk :: Bool
costIsOk = Term name uni fun (Ann a) -> Bool
forall name (uni :: * -> *) fun a. Term name uni fun a -> Bool
costIsAcceptable Term name uni fun (Ann a)
rhs
              -- The RHS is always pure if it is a LamAbs,
              -- but may not be otherwise.
              Bool
rhsPure <- Term name uni fun (Ann a) -> InlineM name uni fun a Bool
forall (uni :: * -> *) fun name a b.
ToBuiltinMeaning uni fun =>
Term name uni fun a -> InlineM name uni fun b Bool
checkPurity Term name uni fun (Ann a)
rhs
              Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term name uni fun (Ann a)
 -> ReaderT
      (InlineInfo name fun a)
      (StateT (S name uni fun (Ann a)) (QuoteT Identity))
      (Term name uni fun (Ann a)))
-> Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a b. (a -> b) -> a -> b
$
                if Bool
sizeIsOk Bool -> Bool -> Bool
&& Bool
costIsOk Bool -> Bool -> Bool
&& Bool
rhsPure
                  then Term name uni fun (Ann a)
fullyApplied
                  else Term name uni fun (Ann a)
t
  | Bool
otherwise = Term name uni fun (Ann a)
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     (Term name uni fun (Ann a))
forall a.
a
-> ReaderT
     (InlineInfo name fun a)
     (StateT (S name uni fun (Ann a)) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term name uni fun (Ann a)
t

-------------------------------------------------------------------------------
-- The following are types and functions for producing certifier hints.
-- See Note [Inliner's Certifier Hints] for an overview.
-------------------------------------------------------------------------------

-- | An enclosing Drop, LamDrop or Expand layer
data Decoration = DDrop | DLamDrop | DExpand

type Ann a = ([Decoration], a)

emptyDecoration :: a -> Ann a
emptyDecoration :: forall a. a -> Ann a
emptyDecoration = ([Decoration]
forall a. Monoid a => a
mempty,)
{-# INLINE emptyDecoration #-}

decorations :: Lens' (Ann a) [Decoration]
decorations :: forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations = ([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
forall s t a b. Field1 s t a b => Lens s t a b
Lens (Ann a) (Ann a) [Decoration] [Decoration]
_1
{-# INLINE decorations #-}

-- | Prepend the given decorations
decorateWith :: [Decoration] -> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith :: forall name (uni :: * -> *) fun a.
[Decoration]
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
decorateWith [Decoration]
ds = (Ann a -> Ann a)
-> Term name uni fun (Ann a) -> Term name uni fun (Ann a)
forall ann name (uni :: * -> *) fun.
(ann -> ann) -> Term name uni fun ann -> Term name uni fun ann
modifyTermAnn (([Decoration] -> [Decoration]) -> Ann a -> Ann a
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([Decoration]
ds [Decoration] -> [Decoration] -> [Decoration]
forall a. [a] -> [a] -> [a]
++))
{-# INLINE decorateWith #-}

-- | Fold a decorated term into certifier hints.
mkHints :: Term name uni fun (Ann a) -> CertifierHints.Inline
mkHints :: forall name (uni :: * -> *) fun a.
Term name uni fun (Ann a) -> Inline
mkHints = Term name uni fun (Ann a) -> Inline
forall name (uni :: * -> *) fun a.
Term name uni fun (Ann a) -> Inline
go
  where
    go :: Term name uni fun (Ann a) -> Inline
go Term name uni fun (Ann a)
t = Inline -> [Decoration] -> Inline
decorate Inline
hints [Decoration]
ds
      where
        decorate :: CertifierHints.Inline -> [Decoration] -> CertifierHints.Inline
        decorate :: Inline -> [Decoration] -> Inline
decorate = (Decoration -> Inline -> Inline)
-> Inline -> [Decoration] -> Inline
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Decoration -> Inline -> Inline)
 -> Inline -> [Decoration] -> Inline)
-> (Decoration -> Inline -> Inline)
-> Inline
-> [Decoration]
-> Inline
forall a b. (a -> b) -> a -> b
$ \Decoration
d Inline
h -> case Decoration
d of
          Decoration
DDrop -> Inline -> Inline
CertifierHints.InlDrop Inline
h
          Decoration
DLamDrop -> Inline -> Inline
CertifierHints.InlLamDrop Inline
h
          Decoration
DExpand -> Inline -> Inline
CertifierHints.InlExpand Inline
h

        ds :: [Decoration]
ds = Term name uni fun (Ann a) -> Ann a
forall name (uni :: * -> *) fun ann. Term name uni fun ann -> ann
termAnn Term name uni fun (Ann a)
t Ann a -> Getting [Decoration] (Ann a) [Decoration] -> [Decoration]
forall s a. s -> Getting a s a -> a
^. Getting [Decoration] (Ann a) [Decoration]
forall a (f :: * -> *).
Functor f =>
([Decoration] -> f [Decoration]) -> Ann a -> f (Ann a)
decorations

        hints :: Inline
hints = case Term name uni fun (Ann a)
t of
          Var {} -> Inline
CertifierHints.InlVar
          LamAbs Ann a
_ name
_ Term name uni fun (Ann a)
body -> Inline -> Inline
CertifierHints.InlLam (Term name uni fun (Ann a) -> Inline
go Term name uni fun (Ann a)
body)
          Apply Ann a
_ Term name uni fun (Ann a)
fun Term name uni fun (Ann a)
arg -> Inline -> Inline -> Inline
CertifierHints.InlApply (Term name uni fun (Ann a) -> Inline
go Term name uni fun (Ann a)
fun) (Term name uni fun (Ann a) -> Inline
go Term name uni fun (Ann a)
arg)
          Force Ann a
_ Term name uni fun (Ann a)
body -> Inline -> Inline
CertifierHints.InlForce (Term name uni fun (Ann a) -> Inline
go Term name uni fun (Ann a)
body)
          Delay Ann a
_ Term name uni fun (Ann a)
body -> Inline -> Inline
CertifierHints.InlDelay (Term name uni fun (Ann a) -> Inline
go Term name uni fun (Ann a)
body)
          Constant {} -> Inline
CertifierHints.InlCon
          Builtin {} -> Inline
CertifierHints.InlBuiltin
          Error {} -> Inline
CertifierHints.InlError
          Constr Ann a
_ Word64
_ [Term name uni fun (Ann a)]
args -> [Inline] -> Inline
CertifierHints.InlConstr (Term name uni fun (Ann a) -> Inline
go (Term name uni fun (Ann a) -> Inline)
-> [Term name uni fun (Ann a)] -> [Inline]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term name uni fun (Ann a)]
args)
          Case Ann a
_ Term name uni fun (Ann a)
scrut Vector (Term name uni fun (Ann a))
alts -> Inline -> [Inline] -> Inline
CertifierHints.InlCase (Term name uni fun (Ann a) -> Inline
go Term name uni fun (Ann a)
scrut) (Term name uni fun (Ann a) -> Inline
go (Term name uni fun (Ann a) -> Inline)
-> [Term name uni fun (Ann a)] -> [Inline]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Term name uni fun (Ann a)) -> [Term name uni fun (Ann a)]
forall a. Vector a -> [a]
V.toList Vector (Term name uni fun (Ann a))
alts)

{- Note [Inliner's Certifier Hints]

To certify the inliner, the certifier requires the inliner to emit hints that record
where inlining operations occur. These hints are represented by the `Inline` data type
defined in `UntypedPlutusCore.Transform.Certify.Hints`.

Given a pre-term and a post-term, the expected hints can be defined by viewing the
inliner as a process that repeatedly performs one of the following two operations:

1. Substituting a term for a variable
2. Dropping a dead binding

Certifier hints are then defined constructively according to the following procedure.
In the end, the final hints mirror the post-term structure, except that each node may be
decorated with an arbitrary number of `InlExpand`, `InlDrop` and `InlLamDrop` layers,
reflecting the inlining operations that the inliner has performed.

- Initially the hints mirror the pre-term structure, using constructors of `Inline`
  except `InlExpand`, `InlDrop` and `InlLamDrop`. Excluding these three constructors,
  there is a 1-1 correspondence between hints constructors and AST constructors.

- Suppose the inliner performs operation 1, substituting term `N` for variable `v`.
  Before the substitution, we have

    hints(v) = decorations(InlVar)

  where `decorations` denotes an arbitrary number of enclosing `InlExpand`, `InlDrop` or
  `InlLamDrop` layers. After the substitution, the hints at this location should become

    decorations(InlExpand hints(N))                          (#1)

  In other words, `InlVar` is replaced by `hints(N)` wrapped in an additional `InlExpand`.

- Suppose the inliner performs operation 2, turning `(\x‾ₙ y. M) X‾ₙ Y` into `(\x‾ₙ. M) X‾ₙ`,
  where `x‾ₙ` and `X‾ₙ` denote sequences `x₁ x₂ ... xₙ` and `X₁ X₂ ... Xₙ` with `n >= 0`.
  Before this, we have

    hints((\x‾ₙ y. M) X‾ₙ Y) = decorations₁(InlApply (hints((\x‾ₙ y. M) X‾ₙ)) (hints(Y)))
    hints(\y. M) = decorations₂(InlLam hints(M))

  Afterwards, the hints for `(\x‾ₙ. M) X‾ₙ` should become

    decorations₁(InlDrop (hints((\x‾ₙ y. M) X‾ₙ)))           (#2)

  That is, it is decorated with `decorations₁` plus `InlDrop`.
  The hints for `M` should become

    decorations₂(InlLamDrop (hints(M)))                      (#3)

  That is, it is decorated with `decorations₂`, plus `InlLamDrop`. Note that when `n = 0`,
  `(\x‾ₙ y. M) X‾ₙ` becomes `M`, and therefore, `hints(M)` should be decorated with
  `decorations₁` plus `InlDrop` plus `InlLamDrop` plus `decorations₂`.

Refer to the golden tests for examples of hints (look for files ending with
`.golden.certifier-hints`).

Implementing this is quite fiddly, but is still easier than it sounds from the above
description. Observe that at any point during inlining, the hints structure mirrors
the structure of the current term, except for the decorations. Therefore all we need
is to store the decorations of each node in its `ann`. When inlining is done, we can
construct the hints structure using these decorations.
-}