{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE TypeFamilies     #-}

{- | An inlining pass of *non-recursive* bindings. It includes
(1) unconditional inlining: similar to `PreInlineUnconditionally` and `PostInlineUnconditionally`
in the paper 'Secrets of the GHC Inliner'.
(2) call site inlining of fully applied functions. See `Inline.CallSiteInline.hs`
-}

module PlutusIR.Transform.Inline.Inline (inline, inlinePass, inlinePassSC, InlineHints (..)) where
import PlutusCore qualified as PLC
import PlutusCore.Annotation
import PlutusCore.Name.Unique
import PlutusCore.Quote
import PlutusCore.Rename (dupable)
import PlutusIR
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.Size (termSize)
import PlutusIR.Analysis.Usages qualified as Usages
import PlutusIR.Analysis.VarInfo qualified as VarInfo
import PlutusIR.Contexts (AppContext (..), fillAppContext, splitApplication)
import PlutusIR.MkPir (mkLet)
import PlutusIR.Pass
import PlutusIR.Transform.Inline.CallSiteInline (callSiteInline)
import PlutusIR.Transform.Inline.Utils
import PlutusIR.Transform.Rename ()
import PlutusIR.TypeCheck qualified as TC
import PlutusPrelude

import Control.Lens (forMOf, traverseOf)
import Control.Monad.Extra
import Control.Monad.Reader (runReaderT)
import Control.Monad.State (evalStateT, modify')
import Control.Monad.State.Class (gets)
import Data.Maybe

{- Note [Inlining approach and 'Secrets of the GHC Inliner']
The approach we take is more-or-less exactly taken from 'Secrets of the GHC Inliner'.

Overall, the cause of differences is that we are largely trying to just clean up some
basic issues, not do serious optimization. In many cases we've already run the GHC simplifier
on our input!

We differ from the paper a few ways, mostly leaving things out:

Functionality
------------

Inlining recursive bindings: not worth it, complicated.

Context-based inlining: Not needed atm.

Also, GHC implements many different optimization in a single simplifier pass.
The paper focusses on inlining, but does so in the context of GHC's monolithic simplifier, which
includes beta reduction and deadcode elimination.
We have opted to have more, single-purpose passes. See e.g. `Deadcode.hs` and `Beta.hs` for other
passes.

Implementation
--------------

In-scope set: we don't bother keeping it atm.

Suspended substitutions ('SuspEx') for values: we don't need it, because we simplify the RHS before
preInlineUnconditional. For GHC, they can do more simplification in context, but they only want to
process the binding RHS once, so delaying it until the call site is better
if it's a single-occurrence term. But in our case it's fine to leave any improved in-context
simplification to later passes, so we don't need this complication.

Optimization after substituting in DoneExprs: we can't make different inlining decisions
contextually, so there's no point doing this.
-}

{- Note [The problem of inlining destructors]
Destructors are *perfect* candidates for inlining:

1. They are *always* called fully-saturated, because they are created from pattern matches,
which always provide all the arguments.
2. They will reduce well after being inlined, since their bodies consist of just one argument
applied to the others.

Unfortunately, we can't inline them even after we've compiled datatypes, because compiled datatypes
look like this (see Note [Abstract data types]). Here's an example with Maybe:

(/\Maybe :: * -> * .
  \Nothing :: forall a . Maybe a  .
  \Just :: forall a . a -> Maybe .
  \match_Maybe : forall r . Maybe a -> r -> (a -> r) -> r .
    <user term>
)
-- defn of Maybe
{ \ a . forall r . r -> (a -> r) -> r }
-- defn of Nothing
(/\ a . /\ r . \(nothing_case :: r) . \(just_case :: a -> r) . nothing_case)
-- defn of Just
(/\ a . \(x : a) . /\ r . \(nothing_case :: r) . \(just_case :: a -> r) . just_case x)
-- defn of match_Maybe
(/\ a . \(dt : forall r . r -> (a -> r) -> r) . dt)

The definitions of the constructors/destructor don't look like let-bindings because there
is a type abstraction in between the lambdas and their arguments! And this abstraction
is important: the bodies of the constructors/destructor only typecheck if they are
*outside* the type abstraction, because they fundamentally rely on knowing what the
type actually *is* in order to be able to construct/destruct it. e.g. for a Scott-encoded
type we actually need to know that the datatype is encoded as a matching function,
not just an abstract type. So we can't just put the definitions of the
constructors/destructor inside the type abstraction.

We *could* inline the datatype definition. That would get rid of the type abstraction,
letting us inline the constructors/destructor (by effectively making the datatype not
abstract inside the body). But this way lies madness: doing that consistently would
mean inlining the definitions of *all* datatypes, which would enormously (exponentially!)
bloat the types inside, making the typechecker (and everything else that processes the
AST) incredibly slow.

So it seems that we're stuck. We can't inline destructors in PIR.

But we *can* do it in UPLC! No types, so no problem. The type abstraction/instantiation will
turn into a delay/force pair and get simplified away, and then we have something that we can
inline. This is essentially the reason for the existence of the UPLC inlining pass.

Note that much the same reasoning applies to constructors also. The main difference
is that they might not be applied saturated, so it's not _always_ clear that we want to
inline them. But at least in UPLC we _can_ inline them.
-}

{- Note [Inlining and global uniqueness]
Inlining relies on global uniqueness for two reasons:
1. We track various things in big maps keyed by unique. This is tricky without global
uniqueness, but very straightforward with it: since names are globally unique, we can
just use them as map keys and not worry about things.
2. You need global uniqueness to be able to do substitution without worrying about
avoiding variable capture.

Inlining things can break global uniqueness, because it can duplicate terms, and those
terms can have binders in them.

There are two ways to approach this:
1. Try to maintain global uniqueness
2. Carefully track which terms have been potentially duplicated, and make sure you never
do anything unsafe with them.

We could probably do 2, but it is tricky and requires subtle argumentation to establish
its safety.  On the other hand, it is actually very easy to do 1: just rename terms
when we substitute them in! This is much more obviously correct since it maintains the
global uniqueness invariant. The only cost is that we won't have any pre-computed
information about the fresh variables (e.g. usage counts), since we compute all that
up-front. But this can only bit us if we process the renamed terms (which we currently
don't), and the effect would only be slightly worse optimization.

Renaming everything is a bit overkill, it corresponds to 'The sledgehammer' in 'Secrets'.
But we don't really care about the costs listed there: it's easy for us to get a name
supply, and the performance cost does not currently seem relevant. So it's fine.
-}

inlinePassSC
    :: forall uni fun ann m
    . (PLC.Typecheckable uni fun, PLC.GEq uni, Ord ann, ExternalConstraints TyName Name uni fun m)
    => Bool
    -- ^ should we inline constants?
    -> TC.PirTCConfig uni fun
    -> InlineHints Name ann
    -> BuiltinsInfo uni fun
    -> Pass m TyName Name uni fun ann
inlinePassSC :: forall (uni :: * -> *) fun ann (m :: * -> *).
(Typecheckable uni fun, GEq uni, Ord ann,
 ExternalConstraints TyName Name uni fun m) =>
Bool
-> PirTCConfig uni fun
-> InlineHints Name ann
-> BuiltinsInfo uni fun
-> Pass m TyName Name uni fun ann
inlinePassSC Bool
ic PirTCConfig uni fun
tcconfig InlineHints Name ann
hints BuiltinsInfo uni fun
binfo =
    Pass m TyName Name uni fun ann
forall name tyname (m :: * -> *) a (uni :: * -> *) fun.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 MonadQuote m, Ord a) =>
Pass m tyname name uni fun a
renamePass Pass m TyName Name uni fun ann
-> Pass m TyName Name uni fun ann -> Pass m TyName Name uni fun ann
forall a. Semigroup a => a -> a -> a
<> Bool
-> PirTCConfig uni fun
-> InlineHints Name ann
-> BuiltinsInfo uni fun
-> Pass m TyName Name uni fun ann
forall (uni :: * -> *) fun ann (m :: * -> *).
(Typecheckable uni fun, GEq uni, Ord ann,
 ExternalConstraints TyName Name uni fun m) =>
Bool
-> PirTCConfig uni fun
-> InlineHints Name ann
-> BuiltinsInfo uni fun
-> Pass m TyName Name uni fun ann
inlinePass Bool
ic PirTCConfig uni fun
tcconfig InlineHints Name ann
hints BuiltinsInfo uni fun
binfo

inlinePass
    :: forall uni fun ann m
    . (PLC.Typecheckable uni fun, PLC.GEq uni, Ord ann, ExternalConstraints TyName Name uni fun m)
    => Bool
    -- ^ should we inline constants?
    -> TC.PirTCConfig uni fun
    -> InlineHints Name ann
    -> BuiltinsInfo uni fun
    -> Pass m TyName Name uni fun ann
inlinePass :: forall (uni :: * -> *) fun ann (m :: * -> *).
(Typecheckable uni fun, GEq uni, Ord ann,
 ExternalConstraints TyName Name uni fun m) =>
Bool
-> PirTCConfig uni fun
-> InlineHints Name ann
-> BuiltinsInfo uni fun
-> Pass m TyName Name uni fun ann
inlinePass Bool
ic PirTCConfig uni fun
tcconfig InlineHints Name ann
hints BuiltinsInfo uni fun
binfo =
  String
-> Pass m TyName Name uni fun ann -> Pass m TyName Name uni fun ann
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
"inline" (Pass m TyName Name uni fun ann -> Pass m TyName Name uni fun ann)
-> Pass m TyName Name uni fun ann -> Pass m TyName Name uni fun ann
forall a b. (a -> b) -> a -> b
$
    (Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann))
-> [Condition TyName Name uni fun ann]
-> [BiCondition TyName Name uni fun ann]
-> Pass m TyName Name uni fun ann
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
Pass
      (Bool
-> InlineHints Name ann
-> BuiltinsInfo uni fun
-> Term TyName Name uni fun ann
-> m (Term TyName Name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (m :: * -> *).
ExternalConstraints tyname name uni fun m =>
Bool
-> InlineHints name ann
-> BuiltinsInfo uni fun
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
inline Bool
ic InlineHints Name ann
hints BuiltinsInfo uni fun
binfo )
      [Condition TyName Name uni fun ann
forall tyname name a (uni :: * -> *) fun.
(HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a) =>
Condition tyname name uni fun a
GloballyUniqueNames, PirTCConfig uni fun -> Condition TyName Name uni fun ann
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcconfig]
      [Condition TyName Name uni fun ann
-> BiCondition TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun a.
Condition tyname name uni fun a
-> BiCondition tyname name uni fun a
ConstCondition Condition TyName Name uni fun ann
forall tyname name a (uni :: * -> *) fun.
(HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a) =>
Condition tyname name uni fun a
GloballyUniqueNames, Condition TyName Name uni fun ann
-> BiCondition TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun a.
Condition tyname name uni fun a
-> BiCondition tyname name uni fun a
ConstCondition (PirTCConfig uni fun -> Condition TyName Name uni fun ann
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcconfig)]

-- | Inline non-recursive bindings. Relies on global uniqueness, and preserves it.
-- See Note [Inlining and global uniqueness]
inline
    :: forall tyname name uni fun ann m
    . ExternalConstraints tyname name uni fun m
    => Bool
    -- ^ should we inline constants?
    -> InlineHints name ann
    -> BuiltinsInfo uni fun
    -> Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann)
inline :: forall tyname name (uni :: * -> *) fun ann (m :: * -> *).
ExternalConstraints tyname name uni fun m =>
Bool
-> InlineHints name ann
-> BuiltinsInfo uni fun
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
inline Bool
ic InlineHints name ann
hints BuiltinsInfo uni fun
binfo Term tyname name uni fun ann
t = let
        inlineInfo :: InlineInfo tyname name uni fun ann
        inlineInfo :: InlineInfo tyname name uni fun ann
inlineInfo = VarsInfo tyname name uni ann
-> Usages
-> InlineHints name ann
-> BuiltinsInfo uni fun
-> Bool
-> InlineInfo tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
VarsInfo tyname name uni ann
-> Usages
-> InlineHints name ann
-> BuiltinsInfo uni fun
-> Bool
-> InlineInfo tyname name uni fun ann
InlineInfo VarsInfo tyname name uni ann
vinfo Usages
usgs InlineHints name ann
hints BuiltinsInfo uni fun
binfo Bool
ic
        vinfo :: VarsInfo tyname name uni ann
vinfo = Term tyname name uni fun ann -> VarsInfo tyname name uni ann
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
VarInfo.termVarInfo Term tyname name uni fun ann
t
        usgs :: Usages.Usages
        usgs :: Usages
usgs = Term tyname name uni fun ann -> Usages
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> Usages
Usages.termUsages Term tyname name uni fun ann
t
    in Quote (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Term tyname name uni fun ann)
 -> m (Term tyname name uni fun ann))
-> Quote (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ (StateT
   (InlinerState tyname name uni fun ann)
   (QuoteT Identity)
   (Term tyname name uni fun ann)
 -> InlinerState tyname name uni fun ann
 -> Quote (Term tyname name uni fun ann))
-> InlinerState tyname name uni fun ann
-> StateT
     (InlinerState tyname name uni fun ann)
     (QuoteT Identity)
     (Term tyname name uni fun ann)
-> Quote (Term tyname name uni fun ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  (InlinerState tyname name uni fun ann)
  (QuoteT Identity)
  (Term tyname name uni fun ann)
-> InlinerState tyname name uni fun ann
-> Quote (Term tyname name uni fun ann)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT InlinerState tyname name uni fun ann
forall a. Monoid a => a
mempty (StateT
   (InlinerState tyname name uni fun ann)
   (QuoteT Identity)
   (Term tyname name uni fun ann)
 -> Quote (Term tyname name uni fun ann))
-> StateT
     (InlinerState tyname name uni fun ann)
     (QuoteT Identity)
     (Term tyname name uni fun ann)
-> Quote (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ (ReaderT
   (InlineInfo tyname name uni fun ann)
   (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
   (Term tyname name uni fun ann)
 -> InlineInfo tyname name uni fun ann
 -> StateT
      (InlinerState tyname name uni fun ann)
      (QuoteT Identity)
      (Term tyname name uni fun ann))
-> InlineInfo tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Term tyname name uni fun ann)
-> StateT
     (InlinerState tyname name uni fun ann)
     (QuoteT Identity)
     (Term tyname name uni fun ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
  (Term tyname name uni fun ann)
-> InlineInfo tyname name uni fun ann
-> StateT
     (InlinerState tyname name uni fun ann)
     (QuoteT Identity)
     (Term tyname name uni fun ann)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT InlineInfo tyname name uni fun ann
inlineInfo (ReaderT
   (InlineInfo tyname name uni fun ann)
   (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
   (Term tyname name uni fun ann)
 -> StateT
      (InlinerState tyname name uni fun ann)
      (QuoteT Identity)
      (Term tyname name uni fun ann))
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Term tyname name uni fun ann)
-> StateT
     (InlinerState tyname name uni fun ann)
     (QuoteT Identity)
     (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm Term tyname name uni fun ann
t

{- Note [Removing inlined bindings]
We *do* remove bindings that we inline *unconditionally*. We *could*
leave this to the dead code pass, but it's helpful to do it here.
We *don't* remove bindings that we inline at the call site.
Crucially, we have to do the same reasoning wrt strict bindings and purity
(see Note [Inlining and purity]):
we can only inline *pure* strict bindings, which is effectively the same as what we do in the dead
code pass.

Annoyingly, this requires us to redo the analysis that we do for the dead binding pass.
TODO: merge them or figure out a way to share more work, especially since there's similar logic.
This might mean reinventing GHC's OccAnal...
-}

{- Note [Processing multi-lets]

When we process a term in the inliner, if it is a multi-let, we split it and process the
bindings one by one, because the bindings after `b` need to be considered to determine
whether `b` can be unconditionally inlined. Consider e.g.
`let !x = <effectful>; !y = <effectful> in x`, we need to look at the binding for
`y` to know that inlining `x` would change the order of effects.
It's awkward to do this when they are part of the same term, (we would be
looking at "the let term but only considering all the bindings after x") and
much easier when they are just separate terms.
-}

-- | Run the inliner on a `Core.Type.Term`.
processTerm
    :: forall tyname name uni fun ann. InliningConstraints tyname name uni fun
    => Term tyname name uni fun ann -- ^ Term to be processed.
    -> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm = Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
handleTerm (Term tyname name uni fun ann
 -> InlineM tyname name uni fun ann (Term tyname name uni fun ann))
-> (Term tyname name uni fun ann
    -> InlineM tyname name uni fun ann (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< LensLike
  (ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity)))
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
-> LensLike
     (ReaderT
        (InlineInfo tyname name uni fun ann)
        (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity)))
     (Term tyname name uni fun ann)
     (Term tyname name uni fun ann)
     (Type tyname uni ann)
     (Type tyname uni ann)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike
  (ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity)))
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubtypes Type tyname uni ann
-> InlineM tyname name uni fun ann (Type tyname uni ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Type tyname uni ann
-> InlineM tyname name uni fun ann (Type tyname uni ann)
applyTypeSubstitution where
    handleTerm ::
        Term tyname name uni fun ann
        -> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
    handleTerm :: Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
handleTerm = \case
        v :: Term tyname name uni fun ann
v@(Var ann
_ name
n) -> Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
-> Term tyname name uni fun ann
forall a. a -> Maybe a -> a
fromMaybe Term tyname name uni fun ann
v (Maybe (Term tyname name uni fun ann)
 -> Term tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Maybe (Term tyname name uni fun ann))
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Maybe (Term tyname name uni fun ann))
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
name
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
substName name
n
        Let ann
ann Recursivity
NonRec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
t -> case NonEmpty (Binding tyname name uni fun ann)
bs of
            Binding tyname name uni fun ann
b :| [] -> do
                -- Process the binding, eliminating it if it will be inlined unconditionally,
                -- and accumulating the new substitutions.
                -- See Note [Removing inlined bindings]
                -- Note that we don't *remove* the binding or scope the state, so the state will
                -- carry over into "sibling" terms. This is fine because we have global uniqueness
                -- (see Note [Inlining and global uniqueness]), if somewhat wasteful.
                Maybe (Binding tyname name uni fun ann)
b' <- Term tyname name uni fun ann
-> Binding tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> Binding tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
processSingleBinding Term tyname name uni fun ann
t Binding tyname name uni fun ann
b
                Term tyname name uni fun ann
t' <- Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm Term tyname name uni fun ann
t
                -- Use 'mkLet': which takes a possibly empty list of bindings (rather than
                -- a non-empty list)
                Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun ann
 -> InlineM tyname name uni fun ann (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Recursivity
-> [Binding tyname name uni fun ann]
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a tyname name (uni :: * -> *) fun.
a
-> Recursivity
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Term tyname name uni fun a
mkLet ann
ann Recursivity
NonRec (Maybe (Binding tyname name uni fun ann)
-> [Binding tyname name uni fun ann]
forall a. Maybe a -> [a]
maybeToList Maybe (Binding tyname name uni fun ann)
b') Term tyname name uni fun ann
t'
            -- See Note [Processing multi-lets]
            Binding tyname name uni fun ann
b :| [Binding tyname name uni fun ann]
rest -> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
handleTerm (ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
ann Recursivity
NonRec (Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun ann
b) (ann
-> Recursivity
-> [Binding tyname name uni fun ann]
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a tyname name (uni :: * -> *) fun.
a
-> Recursivity
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Term tyname name uni fun a
mkLet ann
ann Recursivity
NonRec [Binding tyname name uni fun ann]
rest Term tyname name uni fun ann
t))
        -- This includes recursive let terms, we don't even consider inlining them at the moment
        Term tyname name uni fun ann
t -> do
            -- See Note [Processing order of call site inlining]
            let (Term tyname name uni fun ann
hd, AppContext tyname name uni fun ann
args) = Term tyname name uni fun ann
-> (Term tyname name uni fun ann,
    AppContext tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> (Term tyname name uni fun ann,
    AppContext tyname name uni fun ann)
splitApplication Term tyname name uni fun ann
t
                processArgs ::
                    AppContext tyname name uni fun ann ->
                    InlineM tyname name uni fun ann (AppContext tyname name uni fun ann)
                processArgs :: AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
processArgs (TermAppContext Term tyname name uni fun ann
arg ann
ann AppContext tyname name uni fun ann
ctx) = do
                    Term tyname name uni fun ann
processedArg <- Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm Term tyname name uni fun ann
arg
                    AppContext tyname name uni fun ann
processedArgs <- AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
processArgs AppContext tyname name uni fun ann
ctx
                    AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AppContext tyname name uni fun ann
 -> InlineM
      tyname name uni fun ann (AppContext tyname name uni fun ann))
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TermAppContext Term tyname name uni fun ann
processedArg ann
ann AppContext tyname name uni fun ann
processedArgs
                processArgs (TypeAppContext Type tyname uni ann
ty ann
ann AppContext tyname name uni fun ann
ctx) = do
                    AppContext tyname name uni fun ann
processedArgs <- AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
processArgs AppContext tyname name uni fun ann
ctx
                    Type tyname uni ann
ty' <- Type tyname uni ann
-> InlineM tyname name uni fun ann (Type tyname uni ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Type tyname uni ann
-> InlineM tyname name uni fun ann (Type tyname uni ann)
applyTypeSubstitution Type tyname uni ann
ty
                    AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AppContext tyname name uni fun ann
 -> InlineM
      tyname name uni fun ann (AppContext tyname name uni fun ann))
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni ann
ty' ann
ann AppContext tyname name uni fun ann
processedArgs
                processArgs AppContext tyname name uni fun ann
AppContextEnd = AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
AppContext tyname name uni fun ann
AppContextEnd
            case AppContext tyname name uni fun ann
args of
                -- not really an application, so hd is the term itself. Processing it will loop.
                AppContext tyname name uni fun ann
AppContextEnd -> LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo tyname name uni fun ann)
        (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))))
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
-> Term tyname name uni fun ann
-> (Term tyname name uni fun ann
    -> InlineM tyname name uni fun ann (Term tyname name uni fun ann))
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall (m :: * -> *) s t a b.
LensLike (WrappedMonad m) s t a b -> s -> (a -> m b) -> m t
forMOf LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo tyname name uni fun ann)
        (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))))
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun ann
t Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm
                AppContext tyname name uni fun ann
_ -> do
                    Term tyname name uni fun ann
hd' <- Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm Term tyname name uni fun ann
hd
                    AppContext tyname name uni fun ann
args' <- AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (AppContext tyname name uni fun ann)
processArgs AppContext tyname name uni fun ann
args
                    let reconstructed :: Term tyname name uni fun ann
reconstructed = Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext Term tyname name uni fun ann
hd' AppContext tyname name uni fun ann
args'
                    case Term tyname name uni fun ann
hd' of
                        Var ann
_ name
name -> do
                            (InlinerState tyname name uni fun ann
 -> Maybe (InlineVarInfo tyname name uni fun ann))
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Maybe (InlineVarInfo tyname name uni fun ann))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (name
-> InlinerState tyname name uni fun ann
-> Maybe (InlineVarInfo tyname name uni fun ann)
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
name
-> InlinerState tyname name uni fun ann
-> Maybe (InlineVarInfo tyname name uni fun ann)
lookupVarInfo name
name) ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
  (Maybe (InlineVarInfo tyname name uni fun ann))
-> (Maybe (InlineVarInfo tyname name uni fun ann)
    -> InlineM tyname name uni fun ann (Term tyname name uni fun ann))
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall a b.
ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
  a
-> (a
    -> ReaderT
         (InlineInfo tyname name uni fun ann)
         (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
         b)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                                Just InlineVarInfo tyname name uni fun ann
varInfo -> do
                                    Maybe (Term tyname name uni fun ann)
maybeInlined <-
                                        Size
-> InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Maybe (Term tyname name uni fun ann))
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Size
-> InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
callSiteInline
                                            (Term tyname name uni fun ann -> Size
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Size
termSize Term tyname name uni fun ann
reconstructed)
                                            InlineVarInfo tyname name uni fun ann
varInfo
                                            AppContext tyname name uni fun ann
args'
                                    Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun ann
 -> InlineM tyname name uni fun ann (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
-> Term tyname name uni fun ann
forall a. a -> Maybe a -> a
fromMaybe Term tyname name uni fun ann
reconstructed Maybe (Term tyname name uni fun ann)
maybeInlined
                                Maybe (InlineVarInfo tyname name uni fun ann)
Nothing -> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
reconstructed
                        Term tyname name uni fun ann
_ -> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
reconstructed

{- Note [Processing order of call site inlining]
We have two options on how we process terms for the call site inliner:

1. process the subterms first, then go up each node
2. process the whole term first, then process the subterms

Depending on which option we choose we get different results after one `inline` pass. For example:

For the `letFunConstMulti` test:

let
  constFun :: Integer -> Integer -> Integer
  constFun = \x y -> x
in  constFun (constFun 3 5)

With option 1, we first look at the subterms `constFun 3` and `5`. The application of `constFun` to
3 is safe, so it is applied and beta reduced, turning

constFun (constFun 3 5) to constFun ((\y -> 3) 5)

Then, we look at the term constFun ((\y -> 3) 5). I.e., application of constFun to ((\y -> 3) 5).
Because the argument ((\y -> 3) 5) is an application, it is considered unsafe.
So no application applies here and the golden file returns:

let
  constFun :: Integer -> Integer -> Integer
  constFun = \x y -> x
in  constFun ((\y -> 3) 5)

With option 2, we first look at `constFun (constFun 3 5)`. The application of constFun to
(constFun 3 5) is unsafe because the argument (constFun 3 5) is an application.
So no application applies here and we move on to the subterm (constFun 3 5). Application of constFun
3 to the argument 5 is safe. Thus

constFun 3 5 ==> (((\x y -> x) 3) 5) ==> (\x -> x) 3 and again application of 3 is safe and is
applied and beta reduced to 3.

So in this case, we get more reduction in 1 pass with option 2. However, in some cases we get
more reduction in 1 pass with option 1. Consider the `letOverAppMulti` test case (with unconditional
inlining already done):

let
    idFun :: Integer -> Integer
    idFun = \y -> y
    k :: (Integer -> Integer) -> (Integer -> Integer)
    k = \x -> idFun
in (k (k idFun)) 6

With option 1, we look at the subterms (k idFun) and 6 first. The argument idFun is a variable that
is safe to beta reduce, so

k idFun reduces to (\x -> idFun) idFun which reduces to idFun

Now we have the term k idFun 6. Applying k to idFun is safe so it is reduced to idFun. idFun 6
reduces to 6.

With option 2, we look at the whole term (k (k idFun)) 6. The argument (k idFun) is an application
and thus it is unsafe. No inlining happens here. Then we look at the subterm (k idFun), again it can
be reduced to idFun and we have

let
    idFun :: Integer -> Integer
    idFun = \y -> y
    k :: (Integer -> Integer) -> (Integer -> Integer)
    k = \x -> idFun
in (k idFun) 6

in the golden file in 1 inline pass.

We can see from this eg that we are not reducing as much because the arguments are unsafe,
frequently because they are applications. So if we process the arguments first, then we will be
reducing the most in 1 pass. Thus, how we process the terms is actually the third option:

First, split the term into an application context. Then, process the head and arguments of the
application context. If the head is a variable, consider call site inlining, starting with the whole
term, but with the head (the rhs of the variable) and the arguments already processed.

-}

-- | Run the inliner on a single non-recursive let binding.
processSingleBinding
    :: forall tyname name uni fun ann. InliningConstraints tyname name uni fun
    => Term tyname name uni fun ann -- ^ The body of the let binding.
    -> Binding tyname name uni fun ann -- ^ The binding.
    -> InlineM tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
processSingleBinding :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> Binding tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
processSingleBinding Term tyname name uni fun ann
body = \case
    (TermBind ann
ann Strictness
s v :: VarDecl tyname name uni ann
v@(VarDecl ann
_ name
n Type tyname uni ann
_) Term tyname name uni fun ann
rhs0) -> do
        -- we want to do unconditional inline if possible
        Term tyname name uni fun ann
-> ann
-> Strictness
-> name
-> Term tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> ann
-> Strictness
-> name
-> Term tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
maybeAddSubst Term tyname name uni fun ann
body ann
ann Strictness
s name
n Term tyname name uni fun ann
rhs0 InlineM
  tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
-> (Maybe (Term tyname name uni fun ann)
    -> InlineM
         tyname name uni fun ann (Maybe (Binding tyname name uni fun ann)))
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall a b.
ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
  a
-> (a
    -> ReaderT
         (InlineInfo tyname name uni fun ann)
         (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
         b)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            -- this binding is going to be unconditionally inlined
            Maybe (Term tyname name uni fun ann)
Nothing -> Maybe (Binding tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Binding tyname name uni fun ann)
forall a. Maybe a
Nothing
            Just Term tyname name uni fun ann
rhs -> do
                -- when we encounter a binding, we add it to
                -- the global map `Utils.NonRecInScopeSet`.
                -- The `varRhs` added to the map has been unconditionally inlined.
                -- When we check the body of the let binding we look in this map for
                -- call site inlining.
                -- We don't remove the binding because we decide *at the call site*
                -- whether we want to inline, and it may be called more than once.
                (InlinerState tyname name uni fun ann
 -> InlinerState tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((InlinerState tyname name uni fun ann
  -> InlinerState tyname name uni fun ann)
 -> ReaderT
      (InlineInfo tyname name uni fun ann)
      (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
      ())
-> (InlinerState tyname name uni fun ann
    -> InlinerState tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     ()
forall a b. (a -> b) -> a -> b
$
                    name
-> InlineVarInfo tyname name uni fun ann
-> InlinerState tyname name uni fun ann
-> InlinerState tyname name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
name
-> InlineVarInfo tyname name uni fun ann
-> InlinerState tyname name uni fun ann
-> InlinerState tyname name uni fun ann
extendVarInfo
                        name
n
                        -- no need to rename here when we enter the rhs into the map. Renaming needs
                        -- to be done at each call site, because each substituted instance has to
                        -- have unique names
                        (Strictness
-> InlineTerm tyname name uni fun ann
-> InlineVarInfo tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Strictness
-> InlineTerm tyname name uni fun ann
-> InlineVarInfo tyname name uni fun ann
MkVarInfo Strictness
s (Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
Done (Term tyname name uni fun ann
-> Dupable (Term tyname name uni fun ann)
forall a. a -> Dupable a
dupable Term tyname name uni fun ann
rhs)))
                Maybe (Binding tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Binding tyname name uni fun ann)
 -> InlineM
      tyname name uni fun ann (Maybe (Binding tyname name uni fun ann)))
-> Maybe (Binding tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Binding tyname name uni fun ann
-> Maybe (Binding tyname name uni fun ann)
forall a. a -> Maybe a
Just (Binding tyname name uni fun ann
 -> Maybe (Binding tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> Maybe (Binding tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Strictness
-> VarDecl tyname name uni ann
-> Term tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
ann Strictness
s VarDecl tyname name uni ann
v Term tyname name uni fun ann
rhs
    (TypeBind ann
ann v :: TyVarDecl tyname ann
v@(TyVarDecl ann
_ tyname
n Kind ann
_) Type tyname uni ann
rhs) -> do
        Maybe (Type tyname uni ann)
maybeRhs' <- tyname
-> Type tyname uni ann
-> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann))
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
tyname
-> Type tyname uni ann
-> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann))
maybeAddTySubst tyname
n Type tyname uni ann
rhs
        Maybe (Binding tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Binding tyname name uni fun ann)
 -> InlineM
      tyname name uni fun ann (Maybe (Binding tyname name uni fun ann)))
-> Maybe (Binding tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> TyVarDecl tyname ann
-> Type tyname uni ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
ann TyVarDecl tyname ann
v (Type tyname uni ann -> Binding tyname name uni fun ann)
-> Maybe (Type tyname uni ann)
-> Maybe (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type tyname uni ann)
maybeRhs'
    Binding tyname name uni fun ann
b -> -- Just process all the subterms
        Binding tyname name uni fun ann
-> Maybe (Binding tyname name uni fun ann)
forall a. a -> Maybe a
Just (Binding tyname name uni fun ann
 -> Maybe (Binding tyname name uni fun ann))
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Binding tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Binding tyname name uni fun ann))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo tyname name uni fun ann)
        (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))))
  (Binding tyname name uni fun ann)
  (Binding tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
-> Binding tyname name uni fun ann
-> (Term tyname name uni fun ann
    -> ReaderT
         (InlineInfo tyname name uni fun ann)
         (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
         (Term tyname name uni fun ann))
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Binding tyname name uni fun ann)
forall (m :: * -> *) s t a b.
LensLike (WrappedMonad m) s t a b -> s -> (a -> m b) -> m t
forMOf LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo tyname name uni fun ann)
        (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))))
  (Binding tyname name uni fun ann)
  (Binding tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms Binding tyname name uni fun ann
b Term tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm

-- | 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 tyname name uni fun ann. InliningConstraints tyname name uni fun
    => Term tyname name uni fun ann
    -> ann
    -> Strictness
    -> name
    -> Term tyname name uni fun ann
    -> InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
maybeAddSubst :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> ann
-> Strictness
-> name
-> Term tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
maybeAddSubst Term tyname name uni fun ann
body ann
ann Strictness
s name
n Term tyname name uni fun ann
rhs0 = do
    Term tyname name uni fun ann
rhs <- Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> InlineM tyname name uni fun ann (Term tyname name uni fun ann)
processTerm Term tyname name uni fun ann
rhs0

    -- Check whether we've been told specifically to inline this
    InlineHints name ann
hints <- Getting
  (InlineHints name ann)
  (InlineInfo tyname name uni fun ann)
  (InlineHints name ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (InlineHints name ann)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (InlineHints name ann)
  (InlineInfo tyname name uni fun ann)
  (InlineHints name ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(InlineHints name ann -> f (InlineHints name ann))
-> InlineInfo tyname name uni fun ann
-> f (InlineInfo tyname name uni fun ann)
iiHints
    let hinted :: Bool
hinted = InlineHints name ann -> ann -> name -> Bool
forall name a. InlineHints name a -> a -> name -> Bool
shouldInline InlineHints name ann
hints ann
ann name
n

    if Bool
hinted -- if we've been told specifically, then do it right away
    then InlineTerm tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall b.
InlineTerm tyname name uni fun ann
-> InlineM tyname name uni fun ann (Maybe b)
extendAndDrop (Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
Done (Dupable (Term tyname name uni fun ann)
 -> InlineTerm tyname name uni fun ann)
-> Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Dupable (Term tyname name uni fun ann)
forall a. a -> Dupable a
dupable Term tyname name uni fun ann
rhs)
    else
        ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
  Bool
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM
            (Strictness
-> name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     Bool
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Strictness
-> name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
shouldUnconditionallyInline Strictness
s name
n Term tyname name uni fun ann
rhs Term tyname name uni fun ann
body)
            (InlineTerm tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall b.
InlineTerm tyname name uni fun ann
-> InlineM tyname name uni fun ann (Maybe b)
extendAndDrop (Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
Done (Dupable (Term tyname name uni fun ann)
 -> InlineTerm tyname name uni fun ann)
-> Dupable (Term tyname name uni fun ann)
-> InlineTerm tyname name uni fun ann
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Dupable (Term tyname name uni fun ann)
forall a. a -> Dupable a
dupable Term tyname name uni fun ann
rhs))
            (Maybe (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun ann)
 -> InlineM
      tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> Maybe (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just Term tyname name uni fun ann
rhs)
    where
        extendAndDrop ::
            forall b . InlineTerm tyname name uni fun ann
            -> InlineM tyname name uni fun ann (Maybe b)
        extendAndDrop :: forall b.
InlineTerm tyname name uni fun ann
-> InlineM tyname name uni fun ann (Maybe b)
extendAndDrop InlineTerm tyname name uni fun ann
t = (InlinerState tyname name uni fun ann
 -> InlinerState tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (name
-> InlineTerm tyname name uni fun ann
-> InlinerState tyname name uni fun ann
-> InlinerState tyname name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
name
-> InlineTerm tyname name uni fun ann
-> InlinerState tyname name uni fun ann
-> InlinerState tyname name uni fun ann
extendTerm name
n InlineTerm tyname name uni fun ann
t) ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
  ()
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Maybe b)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Maybe b)
forall a b.
ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
  a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     b
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe b
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     (Maybe b)
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe b
forall a. Maybe a
Nothing

-- | Check against the inlining heuristics for types and either inline it, returning Nothing, or
-- just return the type without inlining.
-- We only inline if (1) the type is used at most once OR (2) it's a `trivialType`.
maybeAddTySubst
    :: forall tyname name uni fun ann . InliningConstraints tyname name uni fun
    => tyname -- ^ The type variable
    -> Type tyname uni ann -- ^  The value of the type variable.
    -> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann))
maybeAddTySubst :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
tyname
-> Type tyname uni ann
-> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann))
maybeAddTySubst tyname
tn Type tyname uni ann
rhs = do
    Usages
usgs <- Getting Usages (InlineInfo tyname name uni fun ann) Usages
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     Usages
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Usages (InlineInfo tyname name uni fun ann) Usages
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(Usages -> f Usages)
-> InlineInfo tyname name uni fun ann
-> f (InlineInfo tyname name uni fun ann)
iiUsages
    -- No need for multiple phases here
    let typeUsedAtMostOnce :: Bool
typeUsedAtMostOnce = tyname -> Usages -> Int
forall n unique. HasUnique n unique => n -> Usages -> Int
Usages.getUsageCount tyname
tn Usages
usgs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
    if Bool
typeUsedAtMostOnce Bool -> Bool -> Bool
|| Type tyname uni ann -> Bool
forall tyname (uni :: * -> *) ann. Type tyname uni ann -> Bool
trivialType Type tyname uni ann
rhs
    then do
        (InlinerState tyname name uni fun ann
 -> InlinerState tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (tyname
-> Type tyname uni ann
-> InlinerState tyname name uni fun ann
-> InlinerState tyname name uni fun ann
forall tyname (uni :: * -> *) ann name fun.
HasUnique tyname TypeUnique =>
tyname
-> Type tyname uni ann
-> InlinerState tyname name uni fun ann
-> InlinerState tyname name uni fun ann
extendType tyname
tn Type tyname uni ann
rhs)
        Maybe (Type tyname uni ann)
-> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Type tyname uni ann)
forall a. Maybe a
Nothing
    else Maybe (Type tyname uni ann)
-> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) (QuoteT Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Type tyname uni ann)
 -> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann)))
-> Maybe (Type tyname uni ann)
-> InlineM tyname name uni fun ann (Maybe (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Maybe (Type tyname uni ann)
forall a. a -> Maybe a
Just Type tyname uni ann
rhs