{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE TemplateHaskell  #-}
{-# LANGUAGE TypeFamilies     #-}
{-# LANGUAGE TypeOperators    #-}
{-|
An inlining pass.

Note that there is (essentially) a copy of this in the UPLC inliner, and the two
should be KEPT IN SYNC, so if you make changes here please either make them in the other
one too or add to the comment that summarises the differences.
-}
module PlutusIR.Transform.Inline (inline, InlineHints (..)) where

import PlutusIR
import PlutusIR.Analysis.Dependencies qualified as Deps
import PlutusIR.Analysis.Usages qualified as Usages
import PlutusIR.MkPir
import PlutusIR.Purity
import PlutusIR.Transform.Rename ()
import PlutusPrelude

import PlutusCore qualified as PLC
import PlutusCore.Builtin.Meaning qualified as PLC
import PlutusCore.InlineUtils
import PlutusCore.Name
import PlutusCore.Quote
import PlutusCore.Subst (typeSubstTyNamesM)

import Control.Lens hiding (Strict)
import Control.Monad.Reader
import Control.Monad.State

import Algebra.Graph qualified as G
import Data.Map qualified as Map
import Data.Semigroup.Generic (GenericSemigroupMonoid (..))
import Witherable

{- 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
------------

PreInlineUncoditional: we don't do it, since we don't bother using usage information.
We *could* do it, but it doesn't seem worth it. We also don't need to worry about
inlining nested let-bindings, since we don't inline any.

CallSiteInline: not worth it.

Inlining recursive bindings: not worth it, complicated.

Context-based inlining: we don't do CallSiteInline, so no point.

Beta reduction: not worth it, but would be easy. We could do the inlining of the argument
here and also detect dead immediately-applied-lambdas in the dead code pass.

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

In-scope set: we don't bother keeping it, since we only ever substitute in things that
don't have bound variables. This is largely because we don't do PreInlineUnconditional, which
would inline big things that were only used once, including lambdas etc.

Suspended substitutions for values: we don't do it, since you only need it for
PreInlineUnconditional

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 eliminated datatypes, because they look like
this (see Note [Abstract data types]):

(/\ ty :: * .
  ...
  -- ty abstract
  \match : <destructor type> .
    <user term>
)
<defn of ty>
...
-- ty concrete
<defn of match>

This doesn't look like a let-binding because there is a type abstraction in between the lambda
and its argument! And this abstraction is important: the body of the matcher only typechecks
if it is *outside* the type abstraction, so we can't just push it inside or something.

We *could* inline 'ty', 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.
-}

-- 'SubstRng' in the paper, no 'Susp' case
-- See Note [Inlining approach and 'Secrets of the GHC Inliner']
newtype InlineTerm tyname name uni fun a = Done (Term tyname name uni fun a)

newtype TermEnv tyname name uni fun a = TermEnv { TermEnv tyname name uni fun a
-> UniqueMap TermUnique (InlineTerm tyname name uni fun a)
_unTermEnv :: UniqueMap TermUnique (InlineTerm tyname name uni fun a) }
    deriving newtype (b -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
NonEmpty (TermEnv tyname name uni fun a)
-> TermEnv tyname name uni fun a
TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
(TermEnv tyname name uni fun a
 -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a)
-> (NonEmpty (TermEnv tyname name uni fun a)
    -> TermEnv tyname name uni fun a)
-> (forall b.
    Integral b =>
    b
    -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a)
-> Semigroup (TermEnv tyname name uni fun a)
forall b.
Integral b =>
b -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall tyname name (uni :: * -> *) fun a.
NonEmpty (TermEnv tyname name uni fun a)
-> TermEnv tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
Integral b =>
b -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
stimes :: b -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
$cstimes :: forall tyname name (uni :: * -> *) fun a b.
Integral b =>
b -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
sconcat :: NonEmpty (TermEnv tyname name uni fun a)
-> TermEnv tyname name uni fun a
$csconcat :: forall tyname name (uni :: * -> *) fun a.
NonEmpty (TermEnv tyname name uni fun a)
-> TermEnv tyname name uni fun a
<> :: TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
$c<> :: forall tyname name (uni :: * -> *) fun a.
TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
Semigroup, Semigroup (TermEnv tyname name uni fun a)
TermEnv tyname name uni fun a
Semigroup (TermEnv tyname name uni fun a)
-> TermEnv tyname name uni fun a
-> (TermEnv tyname name uni fun a
    -> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a)
-> ([TermEnv tyname name uni fun a]
    -> TermEnv tyname name uni fun a)
-> Monoid (TermEnv tyname name uni fun a)
[TermEnv tyname name uni fun a] -> TermEnv tyname name uni fun a
TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall tyname name (uni :: * -> *) fun a.
Semigroup (TermEnv tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
TermEnv tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
[TermEnv tyname name uni fun a] -> TermEnv tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
mconcat :: [TermEnv tyname name uni fun a] -> TermEnv tyname name uni fun a
$cmconcat :: forall tyname name (uni :: * -> *) fun a.
[TermEnv tyname name uni fun a] -> TermEnv tyname name uni fun a
mappend :: TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
$cmappend :: forall tyname name (uni :: * -> *) fun a.
TermEnv tyname name uni fun a
-> TermEnv tyname name uni fun a -> TermEnv tyname name uni fun a
mempty :: TermEnv tyname name uni fun a
$cmempty :: forall tyname name (uni :: * -> *) fun a.
TermEnv tyname name uni fun a
$cp1Monoid :: forall tyname name (uni :: * -> *) fun a.
Semigroup (TermEnv tyname name uni fun a)
Monoid)

newtype TypeEnv tyname uni a = TypeEnv { TypeEnv tyname uni a -> UniqueMap TypeUnique (Type tyname uni a)
_unTypeEnv :: UniqueMap TypeUnique (Type tyname uni a) }
    deriving newtype (b -> TypeEnv tyname uni a -> TypeEnv tyname uni a
NonEmpty (TypeEnv tyname uni a) -> TypeEnv tyname uni a
TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
(TypeEnv tyname uni a
 -> TypeEnv tyname uni a -> TypeEnv tyname uni a)
-> (NonEmpty (TypeEnv tyname uni a) -> TypeEnv tyname uni a)
-> (forall b.
    Integral b =>
    b -> TypeEnv tyname uni a -> TypeEnv tyname uni a)
-> Semigroup (TypeEnv tyname uni a)
forall b.
Integral b =>
b -> TypeEnv tyname uni a -> TypeEnv tyname uni a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall tyname (uni :: * -> *) a.
NonEmpty (TypeEnv tyname uni a) -> TypeEnv tyname uni a
forall tyname (uni :: * -> *) a.
TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
forall tyname (uni :: * -> *) a b.
Integral b =>
b -> TypeEnv tyname uni a -> TypeEnv tyname uni a
stimes :: b -> TypeEnv tyname uni a -> TypeEnv tyname uni a
$cstimes :: forall tyname (uni :: * -> *) a b.
Integral b =>
b -> TypeEnv tyname uni a -> TypeEnv tyname uni a
sconcat :: NonEmpty (TypeEnv tyname uni a) -> TypeEnv tyname uni a
$csconcat :: forall tyname (uni :: * -> *) a.
NonEmpty (TypeEnv tyname uni a) -> TypeEnv tyname uni a
<> :: TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
$c<> :: forall tyname (uni :: * -> *) a.
TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
Semigroup, Semigroup (TypeEnv tyname uni a)
TypeEnv tyname uni a
Semigroup (TypeEnv tyname uni a)
-> TypeEnv tyname uni a
-> (TypeEnv tyname uni a
    -> TypeEnv tyname uni a -> TypeEnv tyname uni a)
-> ([TypeEnv tyname uni a] -> TypeEnv tyname uni a)
-> Monoid (TypeEnv tyname uni a)
[TypeEnv tyname uni a] -> TypeEnv tyname uni a
TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall tyname (uni :: * -> *) a. Semigroup (TypeEnv tyname uni a)
forall tyname (uni :: * -> *) a. TypeEnv tyname uni a
forall tyname (uni :: * -> *) a.
[TypeEnv tyname uni a] -> TypeEnv tyname uni a
forall tyname (uni :: * -> *) a.
TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
mconcat :: [TypeEnv tyname uni a] -> TypeEnv tyname uni a
$cmconcat :: forall tyname (uni :: * -> *) a.
[TypeEnv tyname uni a] -> TypeEnv tyname uni a
mappend :: TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
$cmappend :: forall tyname (uni :: * -> *) a.
TypeEnv tyname uni a
-> TypeEnv tyname uni a -> TypeEnv tyname uni a
mempty :: TypeEnv tyname uni a
$cmempty :: forall tyname (uni :: * -> *) a. TypeEnv tyname uni a
$cp1Monoid :: forall tyname (uni :: * -> *) a. Semigroup (TypeEnv tyname uni a)
Monoid)

data Subst tyname name uni fun a = Subst { Subst tyname name uni fun a -> TermEnv tyname name uni fun a
_termEnv :: TermEnv tyname name uni fun a
                                         , Subst tyname name uni fun a -> TypeEnv tyname uni a
_typeEnv :: TypeEnv tyname uni a
                                         }
    deriving stock ((forall x.
 Subst tyname name uni fun a -> Rep (Subst tyname name uni fun a) x)
-> (forall x.
    Rep (Subst tyname name uni fun a) x -> Subst tyname name uni fun a)
-> Generic (Subst tyname name uni fun a)
forall x.
Rep (Subst tyname name uni fun a) x -> Subst tyname name uni fun a
forall x.
Subst tyname name uni fun a -> Rep (Subst tyname name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun a x.
Rep (Subst tyname name uni fun a) x -> Subst tyname name uni fun a
forall tyname name (uni :: * -> *) fun a x.
Subst tyname name uni fun a -> Rep (Subst tyname name uni fun a) x
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Subst tyname name uni fun a) x -> Subst tyname name uni fun a
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Subst tyname name uni fun a -> Rep (Subst tyname name uni fun a) x
Generic)
    deriving (b -> Subst tyname name uni fun a -> Subst tyname name uni fun a
NonEmpty (Subst tyname name uni fun a)
-> Subst tyname name uni fun a
Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
(Subst tyname name uni fun a
 -> Subst tyname name uni fun a -> Subst tyname name uni fun a)
-> (NonEmpty (Subst tyname name uni fun a)
    -> Subst tyname name uni fun a)
-> (forall b.
    Integral b =>
    b -> Subst tyname name uni fun a -> Subst tyname name uni fun a)
-> Semigroup (Subst tyname name uni fun a)
forall b.
Integral b =>
b -> Subst tyname name uni fun a -> Subst tyname name uni fun a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall tyname name (uni :: * -> *) fun a.
NonEmpty (Subst tyname name uni fun a)
-> Subst tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
Integral b =>
b -> Subst tyname name uni fun a -> Subst tyname name uni fun a
stimes :: b -> Subst tyname name uni fun a -> Subst tyname name uni fun a
$cstimes :: forall tyname name (uni :: * -> *) fun a b.
Integral b =>
b -> Subst tyname name uni fun a -> Subst tyname name uni fun a
sconcat :: NonEmpty (Subst tyname name uni fun a)
-> Subst tyname name uni fun a
$csconcat :: forall tyname name (uni :: * -> *) fun a.
NonEmpty (Subst tyname name uni fun a)
-> Subst tyname name uni fun a
<> :: Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
$c<> :: forall tyname name (uni :: * -> *) fun a.
Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
Semigroup, Semigroup (Subst tyname name uni fun a)
Subst tyname name uni fun a
Semigroup (Subst tyname name uni fun a)
-> Subst tyname name uni fun a
-> (Subst tyname name uni fun a
    -> Subst tyname name uni fun a -> Subst tyname name uni fun a)
-> ([Subst tyname name uni fun a] -> Subst tyname name uni fun a)
-> Monoid (Subst tyname name uni fun a)
[Subst tyname name uni fun a] -> Subst tyname name uni fun a
Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall tyname name (uni :: * -> *) fun a.
Semigroup (Subst tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Subst tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
[Subst tyname name uni fun a] -> Subst tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
mconcat :: [Subst tyname name uni fun a] -> Subst tyname name uni fun a
$cmconcat :: forall tyname name (uni :: * -> *) fun a.
[Subst tyname name uni fun a] -> Subst tyname name uni fun a
mappend :: Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
$cmappend :: forall tyname name (uni :: * -> *) fun a.
Subst tyname name uni fun a
-> Subst tyname name uni fun a -> Subst tyname name uni fun a
mempty :: Subst tyname name uni fun a
$cmempty :: forall tyname name (uni :: * -> *) fun a.
Subst tyname name uni fun a
$cp1Monoid :: forall tyname name (uni :: * -> *) fun a.
Semigroup (Subst tyname name uni fun a)
Monoid) via (GenericSemigroupMonoid (Subst tyname name uni fun a))

makeLenses ''TermEnv
makeLenses ''TypeEnv
makeLenses ''Subst

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

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


data InlineInfo name a = InlineInfo
    { InlineInfo name a -> StrictnessMap
_strictnessMap :: Deps.StrictnessMap
    , InlineInfo name a -> Usages
_usages        :: Usages.Usages
    , InlineInfo name a -> InlineHints name a
_hints         :: InlineHints name a
    }

-- Using a concrete monad makes a very large difference to the performance of this module (determined from profiling)
type InlineM tyname name uni fun a = ReaderT (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote)

lookupTerm
    :: (HasUnique name TermUnique)
    => name
    -> Subst tyname name uni fun a
    -> Maybe (InlineTerm tyname name uni fun a)
lookupTerm :: name
-> Subst tyname name uni fun a
-> Maybe (InlineTerm tyname name uni fun a)
lookupTerm name
n Subst tyname name uni fun a
subst = name
-> UniqueMap TermUnique (InlineTerm tyname name uni fun a)
-> Maybe (InlineTerm tyname name uni fun a)
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName name
n (UniqueMap TermUnique (InlineTerm tyname name uni fun a)
 -> Maybe (InlineTerm tyname name uni fun a))
-> UniqueMap TermUnique (InlineTerm tyname name uni fun a)
-> Maybe (InlineTerm tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ Subst tyname name uni fun a
subst Subst tyname name uni fun a
-> Getting
     (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
     (Subst tyname name uni fun a)
     (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
-> UniqueMap TermUnique (InlineTerm tyname name uni fun a)
forall s a. s -> Getting a s a -> a
^. (TermEnv tyname name uni fun a
 -> Const
      (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
      (TermEnv tyname name uni fun a))
-> Subst tyname name uni fun a
-> Const
     (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
     (Subst tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a name fun.
Lens
  (Subst tyname name uni fun a)
  (Subst tyname name uni fun a)
  (TermEnv tyname name uni fun a)
  (TermEnv tyname name uni fun a)
termEnv ((TermEnv tyname name uni fun a
  -> Const
       (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
       (TermEnv tyname name uni fun a))
 -> Subst tyname name uni fun a
 -> Const
      (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
      (Subst tyname name uni fun a))
-> ((UniqueMap TermUnique (InlineTerm tyname name uni fun a)
     -> Const
          (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
          (UniqueMap TermUnique (InlineTerm tyname name uni fun a)))
    -> TermEnv tyname name uni fun a
    -> Const
         (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
         (TermEnv tyname name uni fun a))
-> Getting
     (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
     (Subst tyname name uni fun a)
     (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueMap TermUnique (InlineTerm tyname name uni fun a)
 -> Const
      (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
      (UniqueMap TermUnique (InlineTerm tyname name uni fun a)))
-> TermEnv tyname name uni fun a
-> Const
     (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
     (TermEnv tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a tyname name
       (uni :: * -> *) fun a.
Iso
  (TermEnv tyname name uni fun a)
  (TermEnv tyname name uni fun a)
  (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
  (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
unTermEnv

extendTerm
    :: (HasUnique name TermUnique)
    => name
    -> InlineTerm tyname name uni fun a
    -> Subst tyname name uni fun a
    -> Subst tyname name uni fun a
extendTerm :: name
-> InlineTerm tyname name uni fun a
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
extendTerm name
n InlineTerm tyname name uni fun a
clos Subst tyname name uni fun a
subst = Subst tyname name uni fun a
subst Subst tyname name uni fun a
-> (Subst tyname name uni fun a -> Subst tyname name uni fun a)
-> Subst tyname name uni fun a
forall a b. a -> (a -> b) -> b
& (TermEnv tyname name uni fun a
 -> Identity (TermEnv tyname name uni fun a))
-> Subst tyname name uni fun a
-> Identity (Subst tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a name fun.
Lens
  (Subst tyname name uni fun a)
  (Subst tyname name uni fun a)
  (TermEnv tyname name uni fun a)
  (TermEnv tyname name uni fun a)
termEnv ((TermEnv tyname name uni fun a
  -> Identity (TermEnv tyname name uni fun a))
 -> Subst tyname name uni fun a
 -> Identity (Subst tyname name uni fun a))
-> ((UniqueMap TermUnique (InlineTerm tyname name uni fun a)
     -> Identity
          (UniqueMap TermUnique (InlineTerm tyname name uni fun a)))
    -> TermEnv tyname name uni fun a
    -> Identity (TermEnv tyname name uni fun a))
-> (UniqueMap TermUnique (InlineTerm tyname name uni fun a)
    -> Identity
         (UniqueMap TermUnique (InlineTerm tyname name uni fun a)))
-> Subst tyname name uni fun a
-> Identity (Subst tyname name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueMap TermUnique (InlineTerm tyname name uni fun a)
 -> Identity
      (UniqueMap TermUnique (InlineTerm tyname name uni fun a)))
-> TermEnv tyname name uni fun a
-> Identity (TermEnv tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a tyname name
       (uni :: * -> *) fun a.
Iso
  (TermEnv tyname name uni fun a)
  (TermEnv tyname name uni fun a)
  (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
  (UniqueMap TermUnique (InlineTerm tyname name uni fun a))
unTermEnv ((UniqueMap TermUnique (InlineTerm tyname name uni fun a)
  -> Identity
       (UniqueMap TermUnique (InlineTerm tyname name uni fun a)))
 -> Subst tyname name uni fun a
 -> Identity (Subst tyname name uni fun a))
-> (UniqueMap TermUnique (InlineTerm tyname name uni fun a)
    -> UniqueMap TermUnique (InlineTerm tyname name uni fun a))
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ name
-> InlineTerm tyname name uni fun a
-> UniqueMap TermUnique (InlineTerm tyname name uni fun a)
-> UniqueMap TermUnique (InlineTerm tyname name uni fun a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName name
n InlineTerm tyname name uni fun a
clos

lookupType
    :: (HasUnique tyname TypeUnique)
    => tyname
    -> Subst tyname name uni fun a
    -> Maybe (Type tyname uni a)
lookupType :: tyname -> Subst tyname name uni fun a -> Maybe (Type tyname uni a)
lookupType tyname
tn Subst tyname name uni fun a
subst = tyname
-> UniqueMap TypeUnique (Type tyname uni a)
-> Maybe (Type tyname uni a)
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName tyname
tn (UniqueMap TypeUnique (Type tyname uni a)
 -> Maybe (Type tyname uni a))
-> UniqueMap TypeUnique (Type tyname uni a)
-> Maybe (Type tyname uni a)
forall a b. (a -> b) -> a -> b
$ Subst tyname name uni fun a
subst Subst tyname name uni fun a
-> Getting
     (UniqueMap TypeUnique (Type tyname uni a))
     (Subst tyname name uni fun a)
     (UniqueMap TypeUnique (Type tyname uni a))
-> UniqueMap TypeUnique (Type tyname uni a)
forall s a. s -> Getting a s a -> a
^. (TypeEnv tyname uni a
 -> Const
      (UniqueMap TypeUnique (Type tyname uni a)) (TypeEnv tyname uni a))
-> Subst tyname name uni fun a
-> Const
     (UniqueMap TypeUnique (Type tyname uni a))
     (Subst tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Lens' (Subst tyname name uni fun a) (TypeEnv tyname uni a)
typeEnv ((TypeEnv tyname uni a
  -> Const
       (UniqueMap TypeUnique (Type tyname uni a)) (TypeEnv tyname uni a))
 -> Subst tyname name uni fun a
 -> Const
      (UniqueMap TypeUnique (Type tyname uni a))
      (Subst tyname name uni fun a))
-> ((UniqueMap TypeUnique (Type tyname uni a)
     -> Const
          (UniqueMap TypeUnique (Type tyname uni a))
          (UniqueMap TypeUnique (Type tyname uni a)))
    -> TypeEnv tyname uni a
    -> Const
         (UniqueMap TypeUnique (Type tyname uni a)) (TypeEnv tyname uni a))
-> Getting
     (UniqueMap TypeUnique (Type tyname uni a))
     (Subst tyname name uni fun a)
     (UniqueMap TypeUnique (Type tyname uni a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueMap TypeUnique (Type tyname uni a)
 -> Const
      (UniqueMap TypeUnique (Type tyname uni a))
      (UniqueMap TypeUnique (Type tyname uni a)))
-> TypeEnv tyname uni a
-> Const
     (UniqueMap TypeUnique (Type tyname uni a)) (TypeEnv tyname uni a)
forall tyname (uni :: * -> *) a tyname (uni :: * -> *) a.
Iso
  (TypeEnv tyname uni a)
  (TypeEnv tyname uni a)
  (UniqueMap TypeUnique (Type tyname uni a))
  (UniqueMap TypeUnique (Type tyname uni a))
unTypeEnv

isTypeSubstEmpty :: Subst tyname name uni fun a -> Bool
isTypeSubstEmpty :: Subst tyname name uni fun a -> Bool
isTypeSubstEmpty (Subst TermEnv tyname name uni fun a
_ (TypeEnv UniqueMap TypeUnique (Type tyname uni a)
tyEnv)) = UniqueMap TypeUnique (Type tyname uni a) -> Bool
forall unique a. UniqueMap unique a -> Bool
isEmpty UniqueMap TypeUnique (Type tyname uni a)
tyEnv

extendType
    :: (HasUnique tyname TypeUnique)
    => tyname
    -> Type tyname uni a
    -> Subst tyname name uni fun a
    -> Subst tyname name uni fun a
extendType :: tyname
-> Type tyname uni a
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
extendType tyname
tn Type tyname uni a
ty Subst tyname name uni fun a
subst = Subst tyname name uni fun a
subst Subst tyname name uni fun a
-> (Subst tyname name uni fun a -> Subst tyname name uni fun a)
-> Subst tyname name uni fun a
forall a b. a -> (a -> b) -> b
&  (TypeEnv tyname uni a -> Identity (TypeEnv tyname uni a))
-> Subst tyname name uni fun a
-> Identity (Subst tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Lens' (Subst tyname name uni fun a) (TypeEnv tyname uni a)
typeEnv ((TypeEnv tyname uni a -> Identity (TypeEnv tyname uni a))
 -> Subst tyname name uni fun a
 -> Identity (Subst tyname name uni fun a))
-> ((UniqueMap TypeUnique (Type tyname uni a)
     -> Identity (UniqueMap TypeUnique (Type tyname uni a)))
    -> TypeEnv tyname uni a -> Identity (TypeEnv tyname uni a))
-> (UniqueMap TypeUnique (Type tyname uni a)
    -> Identity (UniqueMap TypeUnique (Type tyname uni a)))
-> Subst tyname name uni fun a
-> Identity (Subst tyname name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueMap TypeUnique (Type tyname uni a)
 -> Identity (UniqueMap TypeUnique (Type tyname uni a)))
-> TypeEnv tyname uni a -> Identity (TypeEnv tyname uni a)
forall tyname (uni :: * -> *) a tyname (uni :: * -> *) a.
Iso
  (TypeEnv tyname uni a)
  (TypeEnv tyname uni a)
  (UniqueMap TypeUnique (Type tyname uni a))
  (UniqueMap TypeUnique (Type tyname uni a))
unTypeEnv ((UniqueMap TypeUnique (Type tyname uni a)
  -> Identity (UniqueMap TypeUnique (Type tyname uni a)))
 -> Subst tyname name uni fun a
 -> Identity (Subst tyname name uni fun a))
-> (UniqueMap TypeUnique (Type tyname uni a)
    -> UniqueMap TypeUnique (Type tyname uni a))
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ tyname
-> Type tyname uni a
-> UniqueMap TypeUnique (Type tyname uni a)
-> UniqueMap TypeUnique (Type tyname uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName tyname
tn Type tyname uni a
ty

{- Note [Inlining and global uniqueness]
Inlining relies on global uniqueness (we store things in a unique map), and *does* currently
preserve it because we don't currently inline anything with binders.

If we do start inlining things with binders in them, we should probably try and preserve it by
doing something like 'The rapier' section from the paper. We could also just bite the bullet
and rename everything when we substitute in, which GHC considers too expensive but we might accept.
-}

-- | Inline simple bindings. Relies on global uniqueness, and preserves it.
-- See Note [Inlining and global uniqueness]
inline
    :: forall tyname name uni fun a m
    . ExternalConstraints tyname name uni fun m
    => InlineHints name a
    -> Term tyname name uni fun a
    -> m (Term tyname name uni fun a)
inline :: InlineHints name a
-> Term tyname name uni fun a -> m (Term tyname name uni fun a)
inline InlineHints name a
hints Term tyname name uni fun a
t = let
        inlineInfo :: InlineInfo name a
        inlineInfo :: InlineInfo name a
inlineInfo = StrictnessMap -> Usages -> InlineHints name a -> InlineInfo name a
forall name a.
StrictnessMap -> Usages -> InlineHints name a -> InlineInfo name a
InlineInfo ((Graph Node, StrictnessMap) -> StrictnessMap
forall a b. (a, b) -> b
snd (Graph Node, StrictnessMap)
deps) Usages
usgs InlineHints name a
hints
        -- We actually just want the variable strictness information here!
        deps :: (G.Graph Deps.Node, Map.Map PLC.Unique Strictness)
        deps :: (Graph Node, StrictnessMap)
deps = Term tyname name uni fun a -> (Graph Node, StrictnessMap)
forall g tyname name (uni :: * -> *) fun a.
(DepGraph g, HasUnique tyname TypeUnique,
 HasUnique name TermUnique, ToBuiltinMeaning uni fun) =>
Term tyname name uni fun a -> (g, StrictnessMap)
Deps.runTermDeps Term tyname name uni fun a
t
        usgs :: Map.Map Unique Int
        usgs :: Usages
usgs = Term tyname name uni fun a -> Usages
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> Usages
Usages.runTermUsages Term tyname name uni fun a
t
    in Quote (Term tyname name uni fun a)
-> m (Term tyname name uni fun a)
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Term tyname name uni fun a)
 -> m (Term tyname name uni fun a))
-> Quote (Term tyname name uni fun a)
-> m (Term tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ (StateT
   (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
 -> Subst tyname name uni fun a
 -> Quote (Term tyname name uni fun a))
-> Subst tyname name uni fun a
-> StateT
     (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
-> Quote (Term tyname name uni fun a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
-> Subst tyname name uni fun a
-> Quote (Term tyname name uni fun a)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Subst tyname name uni fun a
forall a. Monoid a => a
mempty (StateT
   (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
 -> Quote (Term tyname name uni fun a))
-> StateT
     (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
-> Quote (Term tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ (ReaderT
   (InlineInfo name a)
   (StateT (Subst tyname name uni fun a) Quote)
   (Term tyname name uni fun a)
 -> InlineInfo name a
 -> StateT
      (Subst tyname name uni fun a) Quote (Term tyname name uni fun a))
-> InlineInfo name a
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Term tyname name uni fun a)
-> StateT
     (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (InlineInfo name a)
  (StateT (Subst tyname name uni fun a) Quote)
  (Term tyname name uni fun a)
-> InlineInfo name a
-> StateT
     (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT InlineInfo name a
inlineInfo (ReaderT
   (InlineInfo name a)
   (StateT (Subst tyname name uni fun a) Quote)
   (Term tyname name uni fun a)
 -> StateT
      (Subst tyname name uni fun a) Quote (Term tyname name uni fun a))
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Term tyname name uni fun a)
-> StateT
     (Subst tyname name uni fun a) Quote (Term tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
processTerm Term tyname name uni fun a
t

{- Note [Removing inlined bindings]
We *do* remove bindings that we inline (since we only do unconditional inlining). We *could*
leave this to the dead code pass, but it's helpful to do it here.
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...
-}

processTerm
    :: forall tyname name uni fun a. InliningConstraints tyname name uni fun
    => Term tyname name uni fun a
    -> InlineM tyname name uni fun a (Term tyname name uni fun a)
processTerm :: Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
processTerm = Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
handleTerm (Term tyname name uni fun a
 -> InlineM tyname name uni fun a (Term tyname name uni fun a))
-> (Term tyname name uni fun a
    -> InlineM tyname name uni fun a (Term tyname name uni fun a))
-> Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< LensLike
  (ReaderT
     (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote))
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Type tyname uni a)
  (Type tyname uni a)
-> LensLike
     (ReaderT
        (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote))
     (Term tyname name uni fun a)
     (Term tyname name uni fun a)
     (Type tyname uni a)
     (Type tyname uni a)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike
  (ReaderT
     (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote))
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Type tyname uni a)
  (Type tyname uni a)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Term tyname name uni fun a) (Type tyname uni a)
termSubtypes Type tyname uni a
-> InlineM tyname name uni fun a (Type tyname uni a)
applyTypeSubstitution where
    handleTerm :: Term tyname name uni fun a -> InlineM tyname name uni fun a (Term tyname name uni fun a)
    handleTerm :: Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
handleTerm = \case
        v :: Term tyname name uni fun a
v@(Var a
_ name
n) -> Term tyname name uni fun a
-> Maybe (Term tyname name uni fun a) -> Term tyname name uni fun a
forall a. a -> Maybe a -> a
fromMaybe Term tyname name uni fun a
v (Maybe (Term tyname name uni fun a) -> Term tyname name uni fun a)
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Maybe (Term tyname name uni fun a))
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Maybe (Term tyname name uni fun a))
substName name
n
        Let a
a Recursivity
NonRec NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
t -> do
            -- Process bindings, eliminating those which will be inlined unconditionally,
            -- and accumulating the new substitutions
            -- See Note [Removing inlined bindings]
            -- Note that we don't *remove* the bindings 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.
            [Binding tyname name uni fun a]
bs' <- (Binding tyname name uni fun a
 -> ReaderT
      (InlineInfo name a)
      (StateT (Subst tyname name uni fun a) Quote)
      (Maybe (Binding tyname name uni fun a)))
-> [Binding tyname name uni fun a]
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     [Binding tyname name uni fun a]
forall (t :: * -> *) (f :: * -> *) a b.
(Witherable t, Applicative f) =>
(a -> f (Maybe b)) -> t a -> f (t b)
wither Binding tyname name uni fun a
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Maybe (Binding tyname name uni fun a))
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
Binding tyname name uni fun a
-> InlineM
     tyname name uni fun a (Maybe (Binding tyname name uni fun a))
processSingleBinding (NonEmpty (Binding tyname name uni fun a)
-> [Binding tyname name uni fun a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Binding tyname name uni fun a)
bs)
            Term tyname name uni fun a
t' <- Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
processTerm Term tyname name uni fun a
t
            -- Use 'mkLet': we're using lists of bindings rather than NonEmpty since we might actually
            -- have got rid of all of them!
            Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun a
 -> InlineM tyname name uni fun a (Term tyname name uni fun a))
-> Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ a
-> Recursivity
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 a
a Recursivity
NonRec [Binding tyname name uni fun a]
bs' Term tyname name uni fun a
t'
        -- We cannot currently soundly do beta for types (see SCP-2570), so we just recognize
        -- immediately instantiated type abstractions here directly.
        (TyInst a
a (TyAbs a
a' tyname
tn Kind a
k Term tyname name uni fun a
t) Type tyname uni a
rhs) -> do
            Maybe (Type tyname uni a)
b' <- tyname
-> Type tyname uni a
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
tyname
-> Type tyname uni a
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
maybeAddTySubst tyname
tn Type tyname uni a
rhs
            Term tyname name uni fun a
t' <- Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
processTerm Term tyname name uni fun a
t
            case Maybe (Type tyname uni a)
b' of
                Just Type tyname uni a
rhs' -> Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun a
 -> InlineM tyname name uni fun a (Term tyname name uni fun a))
-> Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst a
a (a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs a
a' tyname
tn Kind a
k Term tyname name uni fun a
t') Type tyname uni a
rhs'
                Maybe (Type tyname uni a)
Nothing   -> Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t'
        -- This includes recursive let terms, we don't even consider inlining them at the moment
        Term tyname name uni fun a
t -> LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote)))
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> Term tyname name uni fun a
-> (Term tyname name uni fun a
    -> InlineM tyname name uni fun a (Term tyname name uni fun a))
-> InlineM tyname name uni fun a (Term tyname name uni fun 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 a) (StateT (Subst tyname name uni fun a) Quote)))
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Term tyname name uni fun a) (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a
t Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
processTerm
    applyTypeSubstitution :: Type tyname uni a -> InlineM tyname name uni fun a (Type tyname uni a)
    applyTypeSubstitution :: Type tyname uni a
-> InlineM tyname name uni fun a (Type tyname uni a)
applyTypeSubstitution Type tyname uni a
t = (Subst tyname name uni fun a -> Bool)
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Subst tyname name uni fun a -> Bool
forall tyname name (uni :: * -> *) fun a.
Subst tyname name uni fun a -> Bool
isTypeSubstEmpty ReaderT
  (InlineInfo name a)
  (StateT (Subst tyname name uni fun a) Quote)
  Bool
-> (Bool -> InlineM tyname name uni fun a (Type tyname uni a))
-> InlineM tyname name uni fun a (Type tyname uni a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        -- The type substitution is very often empty, and there are lots of types in the program, so this saves a lot of work (determined from profiling)
        Bool
True -> Type tyname uni a
-> InlineM tyname name uni fun a (Type tyname uni a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
t
        Bool
_    -> (tyname
 -> InlineM tyname name uni fun a (Maybe (Type tyname uni a)))
-> Type tyname uni a
-> InlineM tyname name uni fun a (Type tyname uni a)
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
typeSubstTyNamesM tyname -> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
substTyName Type tyname uni a
t
    -- See Note [Renaming strategy]
    substTyName :: tyname -> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
    substTyName :: tyname -> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
substTyName tyname
tyname = (Subst tyname name uni fun a -> Maybe (Type tyname uni a))
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (tyname -> Subst tyname name uni fun a -> Maybe (Type tyname uni a)
forall tyname name (uni :: * -> *) fun a.
HasUnique tyname TypeUnique =>
tyname -> Subst tyname name uni fun a -> Maybe (Type tyname uni a)
lookupType tyname
tyname) InlineM tyname name uni fun a (Maybe (Type tyname uni a))
-> (Maybe (Type tyname uni a)
    -> InlineM tyname name uni fun a (Maybe (Type tyname uni a)))
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Type tyname uni a
 -> InlineM tyname name uni fun a (Type tyname uni a))
-> Maybe (Type tyname uni a)
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type tyname uni a
-> InlineM tyname name uni fun a (Type tyname uni a)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
PLC.rename
    -- See Note [Renaming strategy]
    substName :: name -> InlineM tyname name uni fun a (Maybe (Term tyname name uni fun a))
    substName :: name
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Maybe (Term tyname name uni fun a))
substName name
name = (Subst tyname name uni fun a
 -> Maybe (InlineTerm tyname name uni fun a))
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Maybe (InlineTerm tyname name uni fun a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (name
-> Subst tyname name uni fun a
-> Maybe (InlineTerm tyname name uni fun a)
forall name tyname (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name
-> Subst tyname name uni fun a
-> Maybe (InlineTerm tyname name uni fun a)
lookupTerm name
name) ReaderT
  (InlineInfo name a)
  (StateT (Subst tyname name uni fun a) Quote)
  (Maybe (InlineTerm tyname name uni fun a))
-> (Maybe (InlineTerm tyname name uni fun a)
    -> ReaderT
         (InlineInfo name a)
         (StateT (Subst tyname name uni fun a) Quote)
         (Maybe (Term tyname name uni fun a)))
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Maybe (Term tyname name uni fun a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (InlineTerm tyname name uni fun a
 -> InlineM tyname name uni fun a (Term tyname name uni fun a))
-> Maybe (InlineTerm tyname name uni fun a)
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Maybe (Term tyname name uni fun a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse InlineTerm tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
renameTerm
    -- See Note [Inlining approach and 'Secrets of the GHC Inliner']
    renameTerm :: InlineTerm tyname name uni fun a -> InlineM tyname name uni fun a (Term tyname name uni fun a)
    renameTerm :: InlineTerm tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
renameTerm = \case
        -- Already processed term, just rename and put it in, don't do any
        -- further optimization here.
        Done Term tyname name uni fun a
t -> Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
PLC.rename Term tyname name uni fun a
t

{- Note [Renaming strategy]
Since we assume global uniqueness, we can take a slightly different approach to
renaming:  we rename the term we are substituting in, instead of renaming
every binder that our substitution encounters, which should guarantee that we
avoid any variable capture.

We rename both terms and types as both may have binders in them.
-}

processSingleBinding
    :: forall tyname name uni fun a. InliningConstraints tyname name uni fun
    => Binding tyname name uni fun a
    -> InlineM tyname name uni fun a (Maybe (Binding tyname name uni fun a))
processSingleBinding :: Binding tyname name uni fun a
-> InlineM
     tyname name uni fun a (Maybe (Binding tyname name uni fun a))
processSingleBinding = \case
    TermBind a
a Strictness
s v :: VarDecl tyname name uni fun a
v@(VarDecl a
_ name
n Type tyname uni a
_) Term tyname name uni fun a
rhs -> do
        Maybe (Term tyname name uni fun a)
maybeRhs' <- a
-> Strictness
-> name
-> Term tyname name uni fun a
-> InlineM
     tyname name uni fun a (Maybe (Term tyname name uni fun a))
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
a
-> Strictness
-> name
-> Term tyname name uni fun a
-> InlineM
     tyname name uni fun a (Maybe (Term tyname name uni fun a))
maybeAddSubst a
a Strictness
s name
n Term tyname name uni fun a
rhs
        Maybe (Binding tyname name uni fun a)
-> InlineM
     tyname name uni fun a (Maybe (Binding tyname name uni fun a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Binding tyname name uni fun a)
 -> InlineM
      tyname name uni fun a (Maybe (Binding tyname name uni fun a)))
-> Maybe (Binding tyname name uni fun a)
-> InlineM
     tyname name uni fun a (Maybe (Binding tyname name uni fun a))
forall a b. (a -> b) -> a -> b
$ a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
a Strictness
s VarDecl tyname name uni fun a
v (Term tyname name uni fun a -> Binding tyname name uni fun a)
-> Maybe (Term tyname name uni fun a)
-> Maybe (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Term tyname name uni fun a)
maybeRhs'
    TypeBind a
a v :: TyVarDecl tyname a
v@(TyVarDecl a
_ tyname
n Kind a
_) Type tyname uni a
rhs -> do
        Maybe (Type tyname uni a)
maybeRhs' <- tyname
-> Type tyname uni a
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
tyname
-> Type tyname uni a
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
maybeAddTySubst tyname
n Type tyname uni a
rhs
        Maybe (Binding tyname name uni fun a)
-> InlineM
     tyname name uni fun a (Maybe (Binding tyname name uni fun a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Binding tyname name uni fun a)
 -> InlineM
      tyname name uni fun a (Maybe (Binding tyname name uni fun a)))
-> Maybe (Binding tyname name uni fun a)
-> InlineM
     tyname name uni fun a (Maybe (Binding tyname name uni fun a))
forall a b. (a -> b) -> a -> b
$ a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind a
a TyVarDecl tyname a
v (Type tyname uni a -> Binding tyname name uni fun a)
-> Maybe (Type tyname uni a)
-> Maybe (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type tyname uni a)
maybeRhs'
    -- Just process all the subterms
    Binding tyname name uni fun a
b -> Binding tyname name uni fun a
-> Maybe (Binding tyname name uni fun a)
forall a. a -> Maybe a
Just (Binding tyname name uni fun a
 -> Maybe (Binding tyname name uni fun a))
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Binding tyname name uni fun a)
-> InlineM
     tyname name uni fun a (Maybe (Binding tyname name uni fun a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LensLike
  (WrappedMonad
     (ReaderT
        (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote)))
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> Binding tyname name uni fun a
-> (Term tyname name uni fun a
    -> ReaderT
         (InlineInfo name a)
         (StateT (Subst tyname name uni fun a) Quote)
         (Term tyname name uni fun a))
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Binding tyname name uni fun 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 a) (StateT (Subst tyname name uni fun a) Quote)))
  (Binding tyname name uni fun a)
  (Binding tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Binding tyname name uni fun a) (Term tyname name uni fun a)
bindingSubterms Binding tyname name uni fun a
b Term tyname name uni fun a
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun a
-> InlineM tyname name uni fun a (Term tyname name uni fun a)
processTerm

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

    -- Check whether we've been told specifically to inline this
    InlineHints name a
hints <- (InlineInfo name a -> InlineHints name a)
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     (InlineHints name a)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InlineInfo name a -> InlineHints name a
forall name a. InlineInfo name a -> InlineHints name a
_hints
    let hinted :: Bool
hinted = InlineHints name a -> a -> name -> Bool
forall name a. InlineHints name a -> a -> name -> Bool
shouldInline InlineHints name a
hints a
a name
n

    Bool
preUnconditional <- Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
preInlineUnconditional Term tyname name uni fun a
rhs'
    if Bool
preUnconditional
    then InlineTerm tyname name uni fun a
-> InlineM
     tyname name uni fun a (Maybe (Term tyname name uni fun a))
forall b.
InlineTerm tyname name uni fun a
-> InlineM tyname name uni fun a (Maybe b)
extendAndDrop (Term tyname name uni fun a -> InlineTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> InlineTerm tyname name uni fun a
Done Term tyname name uni fun a
rhs')
    else do
        -- See Note [Inlining approach and 'Secrets of the GHC Inliner']
        Bool
postUnconditional <- Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
postInlineUnconditional Term tyname name uni fun a
rhs'
        if Bool
hinted Bool -> Bool -> Bool
|| Bool
postUnconditional
        then InlineTerm tyname name uni fun a
-> InlineM
     tyname name uni fun a (Maybe (Term tyname name uni fun a))
forall b.
InlineTerm tyname name uni fun a
-> InlineM tyname name uni fun a (Maybe b)
extendAndDrop (Term tyname name uni fun a -> InlineTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> InlineTerm tyname name uni fun a
Done Term tyname name uni fun a
rhs')
        else Maybe (Term tyname name uni fun a)
-> InlineM
     tyname name uni fun a (Maybe (Term tyname name uni fun a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun a)
 -> InlineM
      tyname name uni fun a (Maybe (Term tyname name uni fun a)))
-> Maybe (Term tyname name uni fun a)
-> InlineM
     tyname name uni fun a (Maybe (Term tyname name uni fun a))
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a -> Maybe (Term tyname name uni fun a)
forall a. a -> Maybe a
Just Term tyname name uni fun a
rhs'
    where
        extendAndDrop :: forall b . InlineTerm tyname name uni fun a -> InlineM tyname name uni fun a (Maybe b)
        extendAndDrop :: InlineTerm tyname name uni fun a
-> InlineM tyname name uni fun a (Maybe b)
extendAndDrop InlineTerm tyname name uni fun a
t = (Subst tyname name uni fun a -> Subst tyname name uni fun a)
-> ReaderT
     (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (name
-> InlineTerm tyname name uni fun a
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
forall name tyname (uni :: * -> *) fun a.
HasUnique name TermUnique =>
name
-> InlineTerm tyname name uni fun a
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
extendTerm name
n InlineTerm tyname name uni fun a
t) ReaderT
  (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote) ()
-> InlineM tyname name uni fun a (Maybe b)
-> InlineM tyname name uni fun a (Maybe b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe b -> InlineM tyname name uni fun a (Maybe b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe b
forall a. Maybe a
Nothing

        checkPurity :: Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
        checkPurity :: Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
checkPurity Term tyname name uni fun a
t = do
            StrictnessMap
strctMap <- (InlineInfo name a -> StrictnessMap)
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     StrictnessMap
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InlineInfo name a -> StrictnessMap
forall name a. InlineInfo name a -> StrictnessMap
_strictnessMap
            let strictnessFun :: name -> Strictness
strictnessFun = \name
n' -> Strictness -> Unique -> StrictnessMap -> Strictness
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Strictness
NonStrict (name
n' name -> Getting Unique name Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique name Unique
forall name unique. HasUnique name unique => Lens' name Unique
theUnique) StrictnessMap
strctMap
            Bool -> InlineM tyname name uni fun a Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> InlineM tyname name uni fun a Bool)
-> Bool -> InlineM tyname name uni fun a Bool
forall a b. (a -> b) -> a -> b
$ (name -> Strictness) -> Term tyname name uni fun a -> Bool
forall (uni :: * -> *) fun name tyname a.
ToBuiltinMeaning uni fun =>
(name -> Strictness) -> Term tyname name uni fun a -> Bool
isPure name -> Strictness
strictnessFun Term tyname name uni fun a
t

        preInlineUnconditional :: Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
        preInlineUnconditional :: Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
preInlineUnconditional Term tyname name uni fun a
t = do
            Usages
usgs <- (InlineInfo name a -> Usages)
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     Usages
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InlineInfo name a -> Usages
forall name a. InlineInfo name a -> Usages
_usages
            -- 'inlining' terms used 0 times is a cheap way to remove dead code while we're here
            let termUsedAtMostOnce :: Bool
termUsedAtMostOnce = 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
            -- See Note [Inlining and purity]
            Bool
termIsPure <- Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
checkPurity Term tyname name uni fun a
t
            Bool -> InlineM tyname name uni fun a Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> InlineM tyname name uni fun a Bool)
-> Bool -> InlineM tyname name uni fun a Bool
forall a b. (a -> b) -> a -> b
$ Bool
termUsedAtMostOnce Bool -> Bool -> Bool
&& case Strictness
s of { Strictness
Strict -> Bool
termIsPure; Strictness
NonStrict -> Bool
True; }

        -- | Should we inline? Should only inline things that won't duplicate work or code.
        -- See Note [Inlining approach and 'Secrets of the GHC Inliner']
        postInlineUnconditional ::  Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
        postInlineUnconditional :: Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
postInlineUnconditional Term tyname name uni fun a
t = do
            -- See Note [Inlining criteria]
            let acceptable :: Bool
acceptable = Term tyname name uni fun a -> Bool
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Bool
costIsAcceptable Term tyname name uni fun a
t Bool -> Bool -> Bool
&& Term tyname name uni fun a -> Bool
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Bool
sizeIsAcceptable Term tyname name uni fun a
t
            -- See Note [Inlining and purity]
            Bool
termIsPure <- Term tyname name uni fun a -> InlineM tyname name uni fun a Bool
checkPurity Term tyname name uni fun a
t
            Bool -> InlineM tyname name uni fun a Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> InlineM tyname name uni fun a Bool)
-> Bool -> InlineM tyname name uni fun a Bool
forall a b. (a -> b) -> a -> b
$ Bool
acceptable Bool -> Bool -> Bool
&& case Strictness
s of { Strictness
Strict -> Bool
termIsPure; Strictness
NonStrict -> Bool
True; }

{- Note [Inlining criteria]
What gets inlined? Our goals are simple:
- Make the resulting program faster (or at least no slower)
- Make the resulting program smaller (or at least no bigger)
- Inline as much as we can, since it exposes optimization opportunities

There are two easy cases:
- Inlining approximately variable-sized and variable-costing terms (e.g. builtins, other variables)
- Inlining single-use terms

After that it gets more difficult. As soon as we're inlining things that are not variable-sized
and are used more than once, we are at risk of doing more work or making things bigger.

There are a few things we could do to do this in a more principled way, such as call-site inlining
based on whether a funciton is fully applied.

For now, we have one special case that is a little questionable: inlining functions whose body is small
(motivating example: const). This *could* lead to code duplication, but it's a limited enough case that
we're just going to accept that risk for now. We'll need to be more careful if we inline more functions.

NOTE(MPJ): turns out this *does* lead to moderate size increases. We should fix this with some arity analysis
and context-sensitive inlining.
-}

{- Note [Inlining and purity]
When can we inline something that might have effects? We must remember that we often also
remove a binding that we inline.

For strict bindings, the answer is that we can't: we will delay the effects to the use site,
so they may happen multiple times (or none). So we can only inline bindings whose RHS is pure.

For non-strict bindings, the effects already happened at the use site, so it's fine to inline it
unconditionally.
-}

maybeAddTySubst
    :: forall tyname name uni fun a . InliningConstraints tyname name uni fun
    => tyname
    -> Type tyname uni a
    -> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
maybeAddTySubst :: tyname
-> Type tyname uni a
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
maybeAddTySubst tyname
tn Type tyname uni a
rhs = do
    Usages
usgs <- (InlineInfo name a -> Usages)
-> ReaderT
     (InlineInfo name a)
     (StateT (Subst tyname name uni fun a) Quote)
     Usages
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InlineInfo name a -> Usages
forall name a. InlineInfo name a -> Usages
_usages
    -- 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 a -> Bool
forall tyname (uni :: * -> *) a. Type tyname uni a -> Bool
trivialType Type tyname uni a
rhs
    then do
        (Subst tyname name uni fun a -> Subst tyname name uni fun a)
-> ReaderT
     (InlineInfo name a) (StateT (Subst tyname name uni fun a) Quote) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (tyname
-> Type tyname uni a
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
forall tyname (uni :: * -> *) a name fun.
HasUnique tyname TypeUnique =>
tyname
-> Type tyname uni a
-> Subst tyname name uni fun a
-> Subst tyname name uni fun a
extendType tyname
tn Type tyname uni a
rhs)
        Maybe (Type tyname uni a)
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Type tyname uni a)
forall a. Maybe a
Nothing
    else Maybe (Type tyname uni a)
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Type tyname uni a)
 -> InlineM tyname name uni fun a (Maybe (Type tyname uni a)))
-> Maybe (Type tyname uni a)
-> InlineM tyname name uni fun a (Maybe (Type tyname uni a))
forall a b. (a -> b) -> a -> b
$ Type tyname uni a -> Maybe (Type tyname uni a)
forall a. a -> Maybe a
Just Type tyname uni a
rhs

-- | Is the cost increase (in terms of evaluation work) of inlining a variable whose RHS is
-- the given term acceptable?
costIsAcceptable :: Term tyname name uni fun a -> Bool
costIsAcceptable :: Term tyname 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
  TyAbs{}    -> Bool
True

  -- Arguably we could allow these two, but they're uncommon anyway
  IWrap{}    -> Bool
False
  Unwrap{}   -> Bool
False
  Apply{}    -> Bool
False
  TyInst{}   -> Bool
False
  Let{}      -> Bool
False

-- | Is the size increase (in the AST) of inlining a variable whose RHS is
-- the given term acceptable?
sizeIsAcceptable :: Term tyname name uni fun a -> Bool
sizeIsAcceptable :: Term tyname name uni fun a -> Bool
sizeIsAcceptable = \case
  Builtin{}      -> Bool
True
  Var{}          -> Bool
True
  Error{}        -> Bool
True
  -- See Note [Inlining criteria]
  LamAbs a
_ name
_ Type tyname uni a
_ Term tyname name uni fun a
t -> Term tyname name uni fun a -> Bool
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Bool
sizeIsAcceptable Term tyname name uni fun a
t
  TyAbs a
_ tyname
_ Kind a
_ Term tyname name uni fun a
t  -> Term tyname name uni fun a -> Bool
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Bool
sizeIsAcceptable Term tyname name uni fun a
t

  -- Arguably we could allow these two, but they're uncommon anyway
  IWrap{}        -> Bool
False
  Unwrap{}       -> Bool
False
  -- Constants can be big! We could check the size here and inline if they're
  -- small, but probably not worth it
  Constant{}     -> Bool
False
  Apply{}        -> Bool
False
  TyInst{}       -> Bool
False
  Let{}          -> Bool
False

-- | Is this a an utterly trivial type which might as well be inlined?
trivialType :: Type tyname uni a -> Bool
trivialType :: Type tyname uni a -> Bool
trivialType = \case
    TyBuiltin{} -> Bool
True
    TyVar{}     -> Bool
True
    Type tyname uni a
_           -> Bool
False