{-# LANGUAGE BangPatterns      #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TupleSections     #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE ViewPatterns      #-}

-- | Float bindings inwards.
module PlutusIR.Transform.LetFloatIn (floatTerm, floatTermPass, floatTermPassSC) where

import PlutusCore qualified as PLC
import PlutusCore.Builtin qualified as PLC
import PlutusCore.Name.Unique qualified as PLC
import PlutusIR
import PlutusIR.Analysis.Usages qualified as Usages
import PlutusIR.Purity
import PlutusIR.Transform.Rename ()

import Control.Lens hiding (Strict)
import Control.Monad.Extra
import Control.Monad.Trans.Reader
import Data.Foldable (foldrM)
import Data.List.Extra qualified as List
import Data.List.NonEmpty.Extra (NonEmpty (..))
import Data.List.NonEmpty.Extra qualified as NonEmpty
import Data.Set (Set)
import Data.Set qualified as Set
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo
import PlutusIR.Pass
import PlutusIR.TypeCheck qualified as TC

{- Note [Float-in]

-------------------------------------------------------------------------------
1. Which term bindings can be floated in?
-------------------------------------------------------------------------------

Strict bindings whose RHSs are impure should never be moved, since they can change the
semantics of the program. We can only move non-strict bindings or strict bindings
whose RHSs are pure.

We also need to be very careful about moving a strict binding whose RHS is not a work-free
(though pure). Consider a strict binding whose RHS is a pure, expensive application. If we
move it into, e.g., a lambda, its RHS may end up being evaluated more times. Although this
doesn't change the semantics of the program, it can make it much more expensive. For
simplicity, we do not move such bindings either.

In the rest of this Note, we may simply use "binding" to refer to either a non-strict
binding, or a strict binding whose RHS is work-free. Usually there's no need to distinguish
between these two, since `let x (nonstrict) = rhs` is essentially equivalent to
`let x (strict) = all a rhs`.

-------------------------------------------------------------------------------
2. What about type and datatype bindings?
-------------------------------------------------------------------------------

Type bindings can always be floated in. Doing so has no impact on cost since the a type
binding is compiled into a `force`/`delay` pair that will be optimized away. However,
doing so may enable other type and datatype bindings to be floated inwards.

Datatype bindings can also always be floated inwards. A `DatatypeBind` defines both new types
and new terms. The types can always be floated in, and the terms are all lambda abstractions
or type abstractions, which are essentially work free.

-------------------------------------------------------------------------------
3. The effect of floating in
-------------------------------------------------------------------------------

If we only float in bindings that are either non-strict, or whose RHSs is a work-free, then
why does that make a difference? Because such bindings are not completely free: when we
move a non-strict binding `let x (nonstrict) = rhs`, what we are really moving around is
`delay rhs`, lambda abstractions and lambda applications. None of them is free because
they incur CEK machine costs.

Here's a concrete example where floating a non-strict binding inwards saves cost:

let a (nonstrict) = rhs in if True then t else ..a..

Without floating `a` into the `else` branch, it is compiled into (in pseudo-UPLC)

[(\a -> if True then t else ..a..) (delay rhs)]

If we float `a` into the `else` branch, then it is compiled into

if True then t else [(\a -> ..a..) rhs]

Since the `else` branch is not taken, the former incurs additional `LamAbs`, `Apply`
and `Delay` steps when evaluated by the CEK machine. Note that `rhs` itself is
evaluated the same number of times (i.e., zero time) in both cases.

And floating a binding inwards can also increases cost. Here's an example:

let a (nonstrict) = rhs in let b (nonstrict) = a in b+b

Because `b` is non-strict and occurs twice in the body, floating the definition of `a` into
the RHS of `b` will incur one more of each of these steps: `Delay`, `LamAbs` and `Apply`.

-------------------------------------------------------------------------------
4. When can floating-in increase costs?
-------------------------------------------------------------------------------

Floating-in a binding can increase cost only if the binding is originally outside of `X`,
and is floated into `X`, and `X` satisfies both of the following conditions:

(1) `X` is a lambda abstraction, a type abstraction, or the RHS of a non-strict binding
(recall that the RHS of a non-strict binding is equivalent to a type abstraction).

(2) `X` is in the RHS of a (either strict or non-strict) binding whose LHS is used more than once.

Note the "only if" - the above are the necessary conditions, but not sufficient. Also note
that this is in the context of the float-in pass itself. Floating a binding in /can/ affect
ther subsequent optimizations in a negative way (e.g., inlining).

Therefore, to avoid the possibility of float-in increasing costs, we should avoid
floating-in if the above conditions are met.

-------------------------------------------------------------------------------
5. Implementation of the float-in pass
-------------------------------------------------------------------------------

This float-in pass is a conservative optimization which tries to avoid increasing costs.
The implementation recurses into the top-level `Term` using the following context type:

data FloatInContext = FloatInContext
    { _ctxtInManyOccRhs :: Bool
    , _ctxtUsages       :: Usages.Usages
    }

`ctxtUsages` is the usage counts of variables, and `ctxtInManyOccRhs` is initially `False`.
`ctxtInManyOccRhs` is set to `True` if we descend into:

(1) The RHS of a binding whose LHS is used more than once
(2) The argument of an application, unless the function is a LamAbs whose bound variable
is used at most once, or a Builtin.

The value of `ctxtInManyOccRhs` is used as follows:

(1) When `ctxtInManyOccRhs = False`, we avoid descending into the RHS of a non-strict binding
whose LHS is used more than once, and we descend in all other cases;
(2) When `ctxtInManyOccRhs = True`, we additionally avoid descending into `LamAbs`, `TyAbs`,
and the RHS of a non-strict binding whose LHS is used only once.

-------------------------------------------------------------------------------
6. Relaxation of the float-in criteria
-------------------------------------------------------------------------------

Experimentation using our test suites indicates that the above criteria is too
conservative (there's no cost saving if we adhere to them). We relax the criteria
by allowing a binding to be floated into lambda abstractions or type abstractions,
even if they are in the RHS of a multi-use binding or the argument of an application.

Why does that make sense? Because, as said before, the savings created by float-in
comes from floating bindings into unused branches. A branch of an `if`-expression
is either a value, or a type abstraction (see Note [Case expressions and laziness]).
If it is a value and contains an unused variable, the unused variable is most likely
(if not always) behind a lambda abstraction or a type abstraction. Therefore, by
always allowing a binding to be floated into lambda/type abstractions, the chance
that it is floated into an unused branch is greatly increased.

The relaxation reduces the costs of several test cases (in one case, "formulaBudget",
the saving is significant), although it does increase the cost of one test case ("knightsBudget").

The relaxation is on by default, and can be turned off with flag `no-relaxed-float-in`
or flag `conservative-optimisation`.

-}

-- | The uniques of all used variables in a term.
type Uniques = Set PLC.Unique

data FloatInContext = FloatInContext
  { FloatInContext -> Bool
_ctxtInManyOccRhs :: Bool
  -- ^ Whether we are in the RHS of a binding whose LHS is used more than once.
  -- See Note [Float-in] #5
  , FloatInContext -> Usages
_ctxtUsages       :: Usages.Usages
  , FloatInContext -> Bool
_ctxtRelaxed      :: Bool
  -- ^ Whether to float-in more aggressively. See Note [Float-in] #6
  }

makeLenses ''FloatInContext

floatTermPassSC ::
    forall m uni fun a.
    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
    , PLC.MonadQuote m
    ) =>
    TC.PirTCConfig uni fun ->
    BuiltinsInfo uni fun ->
    Bool ->
    Pass m TyName Name uni fun a
floatTermPassSC :: forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, Ord a, MonadQuote m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Bool -> Pass m TyName Name uni fun a
floatTermPassSC PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo Bool
relaxed =
    Pass m TyName Name uni fun a
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 a
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall a. Semigroup a => a -> a -> a
<> PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Bool -> Pass m TyName Name uni fun a
forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, Ord a, Applicative m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Bool -> Pass m TyName Name uni fun a
floatTermPass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo Bool
relaxed

floatTermPass ::
    forall m uni fun a.
    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
    , Applicative m
    ) =>
    TC.PirTCConfig uni fun ->
    BuiltinsInfo uni fun ->
    -- | Whether to float-in more aggressively. See Note [Float-in] #6
    Bool ->
    Pass m TyName Name uni fun a
floatTermPass :: forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, Ord a, Applicative m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Bool -> Pass m TyName Name uni fun a
floatTermPass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo Bool
relaxed =
  String
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
"let float-in" (Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a)
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall a b. (a -> b) -> a -> b
$
    (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
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
      (Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
-> Term TyName Name uni fun a
-> m (Term TyName Name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinsInfo uni fun
-> Bool -> Term TyName Name uni fun a -> Term TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> Bool -> Term tyname name uni fun a -> Term tyname name uni fun a
floatTerm BuiltinsInfo uni fun
binfo Bool
relaxed)
      [PirTCConfig uni fun -> Condition TyName Name uni fun a
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 a
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 a
-> BiCondition TyName Name uni fun a
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 a
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcconfig)]

-- | Float bindings in the given `Term` inwards.
floatTerm ::
  forall tyname name uni fun a.
  ( PLC.HasUnique name PLC.TermUnique
  , PLC.HasUnique tyname PLC.TypeUnique
  , PLC.ToBuiltinMeaning uni fun
  ) =>
  BuiltinsInfo uni fun ->
  -- | Whether to float-in more aggressively. See Note [Float-in] #6
  Bool ->
  Term tyname name uni fun a ->
  Term tyname name uni fun a
floatTerm :: forall tyname name (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> Bool -> Term tyname name uni fun a -> Term tyname name uni fun a
floatTerm BuiltinsInfo uni fun
binfo Bool
relaxed Term tyname name uni fun a
t0 =
  ((a, Uniques) -> a)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun a
forall a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Uniques) -> a
forall a b. (a, b) -> a
fst (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun a)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun a
forall a b. (a -> b) -> a -> b
$ Usages
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun (a, Uniques)
floatTermInner (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.termUsages Term tyname name uni fun a
t0) (Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t0) Term tyname name uni fun a
t0
  where
    floatTermInner ::
      Usages.Usages ->
      VarsInfo tyname name uni a ->
      Term tyname name uni fun a ->
      Term tyname name uni fun (a, Uniques)
    floatTermInner :: Usages
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun (a, Uniques)
floatTermInner Usages
usgs VarsInfo tyname name uni a
vinfo = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go
      where
        -- Float bindings in the given `Term` inwards, and annotate each term with the set of
        -- `Unique`s of used variables in the `Term`.
        go ::
          Term tyname name uni fun a ->
          Term tyname name uni fun (a, Uniques)
        go :: Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
t = case Term tyname name uni fun a
t of
          Apply a
a Term tyname name uni fun a
fun0 Term tyname name uni fun a
arg0 ->
            let fun :: Term tyname name uni fun (a, Uniques)
fun = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
fun0
                arg :: Term tyname name uni fun (a, Uniques)
arg = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
arg0
                us :: Uniques
us = Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
fun Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
arg
             in (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply (a
a, Uniques
us) Term tyname name uni fun (a, Uniques)
fun Term tyname name uni fun (a, Uniques)
arg
          LamAbs a
a name
n Type tyname uni a
ty0 Term tyname name uni fun a
body0 ->
            let ty :: Type tyname uni (a, Uniques)
ty = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
ty0
                body :: Term tyname name uni fun (a, Uniques)
body = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
body0
             in (a, Uniques)
-> name
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs (a
a, Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body) name
n Type tyname uni (a, Uniques)
ty Term tyname name uni fun (a, Uniques)
body
          TyAbs a
a tyname
n Kind a
k Term tyname name uni fun a
body0 ->
            let body :: Term tyname name uni fun (a, Uniques)
body = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
body0
             in (a, Uniques)
-> tyname
-> Kind (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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, Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body) tyname
n (Kind a -> Kind (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq Kind a
k) Term tyname name uni fun (a, Uniques)
body
          TyInst a
a Term tyname name uni fun a
body0 Type tyname uni a
ty0 ->
            let body :: Term tyname name uni fun (a, Uniques)
body = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
body0
                ty :: Type tyname uni (a, Uniques)
ty = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
ty0
             in (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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, Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty) Term tyname name uni fun (a, Uniques)
body Type tyname uni (a, Uniques)
ty
          IWrap a
a Type tyname uni a
patTy0 Type tyname uni a
argTy0 Term tyname name uni fun a
body0 ->
            let patTy :: Type tyname uni (a, Uniques)
patTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
patTy0
                argTy :: Type tyname uni (a, Uniques)
argTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
argTy0
                body :: Term tyname name uni fun (a, Uniques)
body = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
body0
             in (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
IWrap
                  (a
a, Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
patTy Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
argTy Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body)
                  Type tyname uni (a, Uniques)
patTy
                  Type tyname uni (a, Uniques)
argTy
                  Term tyname name uni fun (a, Uniques)
body
          Unwrap a
a Term tyname name uni fun a
body0 ->
            let body :: Term tyname name uni fun (a, Uniques)
body = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
body0
             in (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a -> Term tyname name uni fun a -> Term tyname name uni fun a
Unwrap (a
a, Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body) Term tyname name uni fun (a, Uniques)
body
          Let a
a Recursivity
NonRec NonEmpty (Binding tyname name uni fun a)
bs0 Term tyname name uni fun a
body0 ->
            let bs :: NonEmpty (Binding tyname name uni fun (a, Uniques))
bs = Binding tyname name uni fun a
-> Binding tyname name uni fun (a, Uniques)
goBinding (Binding tyname name uni fun a
 -> Binding tyname name uni fun (a, Uniques))
-> NonEmpty (Binding tyname name uni fun a)
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Binding tyname name uni fun a)
bs0
                body :: Term tyname name uni fun (a, Uniques)
body = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
body0
             in -- The bindings in `bs` should be processed from right to left, since
                -- a binding may depend on another binding to its left.
                -- e.g. let x = 1; y = x in ... y ...
                -- we want to float y in first otherwise it will block us from floating in x
                Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> FloatInContext -> Term tyname name uni fun (a, Uniques)
forall r a. Reader r a -> r -> a
runReader
                  ((Binding tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques)
 -> Reader FloatInContext (Term tyname name uni fun (a, Uniques)))
-> Term tyname name uni fun (a, Uniques)
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> a
-> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall tyname name (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> a
-> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
floatInBinding BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo a
a) Term tyname name uni fun (a, Uniques)
body NonEmpty (Binding tyname name uni fun (a, Uniques))
bs)
                  (Bool -> Usages -> Bool -> FloatInContext
FloatInContext Bool
False Usages
usgs Bool
relaxed)
          Let a
a Recursivity
Rec NonEmpty (Binding tyname name uni fun a)
bs0 Term tyname name uni fun a
body0 ->
            -- Currently we don't move recursive bindings, so we simply descend into the body.
            let bs :: NonEmpty (Binding tyname name uni fun (a, Uniques))
bs = Binding tyname name uni fun a
-> Binding tyname name uni fun (a, Uniques)
goBinding (Binding tyname name uni fun a
 -> Binding tyname name uni fun (a, Uniques))
-> NonEmpty (Binding tyname name uni fun a)
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Binding tyname name uni fun a)
bs0
                body :: Term tyname name uni fun (a, Uniques)
body = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
body0
                us :: Uniques
us = Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> (Binding tyname name uni fun (a, Uniques) -> Uniques)
-> NonEmpty (Binding tyname name uni fun (a, Uniques)) -> Uniques
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs NonEmpty (Binding tyname name uni fun (a, Uniques))
bs
             in (a, Uniques)
-> Recursivity
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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 (a
a, Uniques
us) Recursivity
Rec NonEmpty (Binding tyname name uni fun (a, Uniques))
bs Term tyname name uni fun (a, Uniques)
body
          Var a
a name
n -> (a, Uniques) -> name -> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var (a
a, Unique -> Uniques
forall a. a -> Set a
Set.singleton (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
Lens' name Unique
PLC.theUnique)) name
n
          Error a
a Type tyname uni a
ty0 ->
            let ty :: Type tyname uni (a, Uniques)
ty = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
ty0
             in (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error (a
a, Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty) Type tyname uni (a, Uniques)
ty
          Constr a
a Type tyname uni a
ty0 Word64
i [Term tyname name uni fun a]
es0 ->
            let
              ty :: Type tyname uni (a, Uniques)
ty = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
ty0
              es :: [Term tyname name uni fun (a, Uniques)]
es = (Term tyname name uni fun a
 -> Term tyname name uni fun (a, Uniques))
-> [Term tyname name uni fun a]
-> [Term tyname name uni fun (a, Uniques)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go [Term tyname name uni fun a]
es0
              us :: Uniques
us = Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> (Term tyname name uni fun (a, Uniques) -> Uniques)
-> [Term tyname name uni fun (a, Uniques)] -> Uniques
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs [Term tyname name uni fun (a, Uniques)]
es
             in
              (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Word64
-> [Term tyname name uni fun (a, Uniques)]
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Constr (a
a, Uniques
us) Type tyname uni (a, Uniques)
ty Word64
i [Term tyname name uni fun (a, Uniques)]
es
          Case a
a Type tyname uni a
ty0 Term tyname name uni fun a
arg0 [Term tyname name uni fun a]
cs0 ->
            let
              ty :: Type tyname uni (a, Uniques)
ty = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
ty0
              arg :: Term tyname name uni fun (a, Uniques)
arg = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
arg0
              cs :: [Term tyname name uni fun (a, Uniques)]
cs = (Term tyname name uni fun a
 -> Term tyname name uni fun (a, Uniques))
-> [Term tyname name uni fun a]
-> [Term tyname name uni fun (a, Uniques)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go [Term tyname name uni fun a]
cs0
              us :: Uniques
us = Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
arg Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> (Term tyname name uni fun (a, Uniques) -> Uniques)
-> [Term tyname name uni fun (a, Uniques)] -> Uniques
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs [Term tyname name uni fun (a, Uniques)]
cs
             in
              (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> [Term tyname name uni fun (a, Uniques)]
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case (a
a, Uniques
us) Type tyname uni (a, Uniques)
ty Term tyname name uni fun (a, Uniques)
arg [Term tyname name uni fun (a, Uniques)]
cs
          Constant{} -> Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq Term tyname name uni fun a
t
          Builtin{} -> Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq Term tyname name uni fun a
t

        -- Float bindings in the given `Binding` inwards, and calculate the set of
        -- `Unique`s of used variables in the result `Binding`.
        goBinding ::
          Binding tyname name uni fun a ->
          Binding tyname name uni fun (a, Uniques)
        goBinding :: Binding tyname name uni fun a
-> Binding tyname name uni fun (a, Uniques)
goBinding = \case
          TermBind a
a Strictness
s VarDecl tyname name uni a
var0 Term tyname name uni fun a
rhs0 ->
            let var :: VarDecl tyname name uni (a, Uniques)
var = VarDecl tyname name uni a -> VarDecl tyname name uni (a, Uniques)
goVarDecl VarDecl tyname name uni a
var0
                rhs :: Term tyname name uni fun (a, Uniques)
rhs = Term tyname name uni fun a -> Term tyname name uni fun (a, Uniques)
go Term tyname name uni fun a
rhs0
             in (a, Uniques)
-> Strictness
-> VarDecl tyname name uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Binding tyname name uni fun (a, Uniques)
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 (a
a, Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
rhs Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> VarDecl tyname name uni (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) a.
VarDecl tyname name uni (a, Uniques) -> Uniques
varDeclUniqs VarDecl tyname name uni (a, Uniques)
var) Strictness
s VarDecl tyname name uni (a, Uniques)
var Term tyname name uni fun (a, Uniques)
rhs
          TypeBind a
a TyVarDecl tyname a
tvar Type tyname uni a
rhs0 ->
            let rhs :: Type tyname uni (a, Uniques)
rhs = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
rhs0
             in -- A `TyVarDecl` does not use any variable, hence `noUniq`.
                (a, Uniques)
-> TyVarDecl tyname (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Binding tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind (a
a, Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
rhs) (TyVarDecl tyname a -> TyVarDecl tyname (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq TyVarDecl tyname a
tvar) Type tyname uni (a, Uniques)
rhs
          DatatypeBind a
a (Datatype a
a' TyVarDecl tyname a
tv [TyVarDecl tyname a]
tvs name
destr [VarDecl tyname name uni a]
constrs0) ->
            -- The constructors in a `Datatype` may use type variables.
            let constrs :: [VarDecl tyname name uni (a, Uniques)]
constrs = VarDecl tyname name uni a -> VarDecl tyname name uni (a, Uniques)
goVarDecl (VarDecl tyname name uni a -> VarDecl tyname name uni (a, Uniques))
-> [VarDecl tyname name uni a]
-> [VarDecl tyname name uni (a, Uniques)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [VarDecl tyname name uni a]
constrs0
                us :: Uniques
us = (VarDecl tyname name uni (a, Uniques) -> Uniques)
-> [VarDecl tyname name uni (a, Uniques)] -> Uniques
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap VarDecl tyname name uni (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) a.
VarDecl tyname name uni (a, Uniques) -> Uniques
varDeclUniqs [VarDecl tyname name uni (a, Uniques)]
constrs
             in (a, Uniques)
-> Datatype tyname name uni (a, Uniques)
-> Binding tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind
                  (a
a, Uniques
us)
                  ((a, Uniques)
-> TyVarDecl tyname (a, Uniques)
-> [TyVarDecl tyname (a, Uniques)]
-> name
-> [VarDecl tyname name uni (a, Uniques)]
-> Datatype tyname name uni (a, Uniques)
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype (a
a', Uniques
us) (TyVarDecl tyname a -> TyVarDecl tyname (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq TyVarDecl tyname a
tv) (TyVarDecl tyname a -> TyVarDecl tyname (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq (TyVarDecl tyname a -> TyVarDecl tyname (a, Uniques))
-> [TyVarDecl tyname a] -> [TyVarDecl tyname (a, Uniques)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVarDecl tyname a]
tvs) name
destr [VarDecl tyname name uni (a, Uniques)]
constrs)

        -- Calculate the set of `Unique`s of used variables in a `Type`.
        goType :: Type tyname uni a -> Type tyname uni (a, Uniques)
        goType :: Type tyname uni a -> Type tyname uni (a, Uniques)
goType = \case
          TyVar a
a tyname
n -> (a, Uniques) -> tyname -> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar (a
a, Unique -> Uniques
forall a. a -> Set a
Set.singleton (tyname
n tyname -> Getting Unique tyname Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique tyname Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' tyname Unique
PLC.theUnique)) tyname
n
          TyFun a
a Type tyname uni a
argTy0 Type tyname uni a
resTy0 ->
            let argTy :: Type tyname uni (a, Uniques)
argTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
argTy0
                resTy :: Type tyname uni (a, Uniques)
resTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
resTy0
                us :: Uniques
us = Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
argTy Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
resTy
             in (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun (a
a, Uniques
us) Type tyname uni (a, Uniques)
argTy Type tyname uni (a, Uniques)
resTy
          TyIFix a
a Type tyname uni a
patTy0 Type tyname uni a
argTy0 ->
            let patTy :: Type tyname uni (a, Uniques)
patTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
patTy0
                argTy :: Type tyname uni (a, Uniques)
argTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
argTy0
                us :: Uniques
us = Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
patTy Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
argTy
             in (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix (a
a, Uniques
us) Type tyname uni (a, Uniques)
patTy Type tyname uni (a, Uniques)
argTy
          TyForall a
a tyname
n Kind a
k Type tyname uni a
bodyTy0 ->
            let bodyTy :: Type tyname uni (a, Uniques)
bodyTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
bodyTy0
                us :: Uniques
us = Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
bodyTy
             in (a, Uniques)
-> tyname
-> Kind (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall (a
a, Uniques
us) tyname
n (Kind a -> Kind (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq Kind a
k) Type tyname uni (a, Uniques)
bodyTy
          TyBuiltin a
a SomeTypeIn uni
t -> (a, Uniques) -> SomeTypeIn uni -> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin (a
a, Uniques
forall a. Monoid a => a
mempty) SomeTypeIn uni
t
          TyLam a
a tyname
n Kind a
k Type tyname uni a
bodyTy0 ->
            let bodyTy :: Type tyname uni (a, Uniques)
bodyTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
bodyTy0
                us :: Uniques
us = Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
bodyTy
             in (a, Uniques)
-> tyname
-> Kind (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam (a
a, Uniques
us) tyname
n (Kind a -> Kind (a, Uniques)
forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq Kind a
k) Type tyname uni (a, Uniques)
bodyTy
          TyApp a
a Type tyname uni a
funTy0 Type tyname uni a
argTy0 ->
            let funTy :: Type tyname uni (a, Uniques)
funTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
funTy0
                argTy :: Type tyname uni (a, Uniques)
argTy = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
argTy0
                us :: Uniques
us = Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
funTy Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
argTy
             in (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp (a
a, Uniques
us) Type tyname uni (a, Uniques)
funTy Type tyname uni (a, Uniques)
argTy
          TySOP a
a [[Type tyname uni a]]
tyls ->
            let tyls' :: [[Type tyname uni (a, Uniques)]]
tyls' = (([Type tyname uni a] -> [Type tyname uni (a, Uniques)])
-> [[Type tyname uni a]] -> [[Type tyname uni (a, Uniques)]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Type tyname uni a] -> [Type tyname uni (a, Uniques)])
 -> [[Type tyname uni a]] -> [[Type tyname uni (a, Uniques)]])
-> ((Type tyname uni a -> Type tyname uni (a, Uniques))
    -> [Type tyname uni a] -> [Type tyname uni (a, Uniques)])
-> (Type tyname uni a -> Type tyname uni (a, Uniques))
-> [[Type tyname uni a]]
-> [[Type tyname uni (a, Uniques)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni a -> Type tyname uni (a, Uniques))
-> [Type tyname uni a] -> [Type tyname uni (a, Uniques)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Type tyname uni a -> Type tyname uni (a, Uniques)
goType [[Type tyname uni a]]
tyls
                us :: Uniques
us = (([Type tyname uni (a, Uniques)] -> Uniques)
-> [[Type tyname uni (a, Uniques)]] -> Uniques
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (([Type tyname uni (a, Uniques)] -> Uniques)
 -> [[Type tyname uni (a, Uniques)]] -> Uniques)
-> ((Type tyname uni (a, Uniques) -> Uniques)
    -> [Type tyname uni (a, Uniques)] -> Uniques)
-> (Type tyname uni (a, Uniques) -> Uniques)
-> [[Type tyname uni (a, Uniques)]]
-> Uniques
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni (a, Uniques) -> Uniques)
-> [Type tyname uni (a, Uniques)] -> Uniques
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap) Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs [[Type tyname uni (a, Uniques)]]
tyls'
             in (a, Uniques)
-> [[Type tyname uni (a, Uniques)]] -> Type tyname uni (a, Uniques)
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP (a
a, Uniques
us) [[Type tyname uni (a, Uniques)]]
tyls'

        -- Calculate the set of `Unique`s of used variables in a `VarDecl`.
        -- The type of the declared variable may use type variables.
        goVarDecl :: VarDecl tyname name uni a -> VarDecl tyname name uni (a, Uniques)
        goVarDecl :: VarDecl tyname name uni a -> VarDecl tyname name uni (a, Uniques)
goVarDecl (VarDecl a
a name
n Type tyname uni a
ty0) = (a, Uniques)
-> name
-> Type tyname uni (a, Uniques)
-> VarDecl tyname name uni (a, Uniques)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl (a
a, Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty) name
n Type tyname uni (a, Uniques)
ty
          where
            ty :: Type tyname uni (a, Uniques)
ty = Type tyname uni a -> Type tyname uni (a, Uniques)
goType Type tyname uni a
ty0

-- | The set of `Unique`s of used variables in a `Term`.
termUniqs :: Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs :: forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs = (a, Uniques) -> Uniques
forall a b. (a, b) -> b
snd ((a, Uniques) -> Uniques)
-> (Term tyname name uni fun (a, Uniques) -> (a, Uniques))
-> Term tyname name uni fun (a, Uniques)
-> Uniques
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun (a, Uniques) -> (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> a
termAnn

-- | The set of `Unique`s of used variables in a `Type`.
typeUniqs :: Type tyname uni (a, Uniques) -> Uniques
typeUniqs :: forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs = (a, Uniques) -> Uniques
forall a b. (a, b) -> b
snd ((a, Uniques) -> Uniques)
-> (Type tyname uni (a, Uniques) -> (a, Uniques))
-> Type tyname uni (a, Uniques)
-> Uniques
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni (a, Uniques) -> (a, Uniques)
forall tyname (uni :: * -> *) ann. Type tyname uni ann -> ann
PLC.typeAnn

-- | The set of `Unique`s of used variables in the RHS of a `Binding`.
bindingUniqs :: Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs :: forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs = (a, Uniques) -> Uniques
forall a b. (a, b) -> b
snd ((a, Uniques) -> Uniques)
-> (Binding tyname name uni fun (a, Uniques) -> (a, Uniques))
-> Binding tyname name uni fun (a, Uniques)
-> Uniques
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binding tyname name uni fun (a, Uniques) -> (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun a -> a
bindingAnn

-- | The set of `Unique`s of used variables in a `VarDecl`.
varDeclUniqs :: VarDecl tyname name uni (a, Uniques) -> Uniques
varDeclUniqs :: forall tyname name (uni :: * -> *) a.
VarDecl tyname name uni (a, Uniques) -> Uniques
varDeclUniqs = (a, Uniques) -> Uniques
forall a b. (a, b) -> b
snd ((a, Uniques) -> Uniques)
-> (VarDecl tyname name uni (a, Uniques) -> (a, Uniques))
-> VarDecl tyname name uni (a, Uniques)
-> Uniques
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (a, Uniques) (VarDecl tyname name uni (a, Uniques)) (a, Uniques)
-> VarDecl tyname name uni (a, Uniques) -> (a, Uniques)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (a, Uniques) (VarDecl tyname name uni (a, Uniques)) (a, Uniques)
forall tyname name (uni :: * -> *) ann (f :: * -> *).
Functor f =>
(ann -> f ann)
-> VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann)
PLC.varDeclAnn

noUniq :: (Functor f) => f a -> f (a, Uniques)
noUniq :: forall (f :: * -> *) a. Functor f => f a -> f (a, Uniques)
noUniq = (a -> (a, Uniques)) -> f a -> f (a, Uniques)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Uniques
forall a. Monoid a => a
mempty)

-- See Note [Float-in] #1
floatable
    :: (PLC.ToBuiltinMeaning uni fun, PLC.HasUnique name PLC.TermUnique)
    => BuiltinsInfo uni fun
    -> VarsInfo tyname name uni a
    -> Binding tyname name uni fun a
    -> Bool
floatable :: forall (uni :: * -> *) fun name tyname a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Binding tyname name uni fun a
-> Bool
floatable BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo = \case
  -- See Note [Float-in] #1
  TermBind a
_a Strictness
Strict VarDecl tyname name uni a
_var Term tyname name uni fun a
rhs     -> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool
forall (uni :: * -> *) fun name tyname a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool
isWorkFree BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
rhs
  TermBind a
_a Strictness
NonStrict VarDecl tyname name uni a
_var Term tyname name uni fun a
_rhs -> Bool
True
  -- See Note [Float-in] #2
  TypeBind{}                      -> Bool
True
  -- See Note [Float-in] #2
  DatatypeBind{}                  -> Bool
True

{- | Given a `Term` and a `Binding`, determine whether the `Binding` can be
 placed somewhere inside the `Term`.

 If yes, return the result `Term`. Otherwise, return a `Let` constructed from
 the given `Binding` and `Term`.
-}
floatInBinding ::
  forall tyname name uni fun a.
  ( PLC.HasUnique name PLC.TermUnique
  , PLC.HasUnique tyname PLC.TypeUnique
  , PLC.ToBuiltinMeaning uni fun
  ) =>
  BuiltinsInfo uni fun ->
  VarsInfo tyname name uni a ->
  -- | Annotation to be attached to the constructed `Let`.
  a ->
  Binding tyname name uni fun (a, Uniques) ->
  Term tyname name uni fun (a, Uniques) ->
  Reader FloatInContext (Term tyname name uni fun (a, Uniques))
floatInBinding :: forall tyname name (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> a
-> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
floatInBinding BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo a
letAnn = \Binding tyname name uni fun (a, Uniques)
b ->
  if BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Binding tyname name uni fun a
-> Bool
forall (uni :: * -> *) fun name tyname a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Binding tyname name uni fun a
-> Bool
floatable BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo (((a, Uniques) -> a)
-> Binding tyname name uni fun (a, Uniques)
-> Binding tyname name uni fun a
forall a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Uniques) -> a
forall a b. (a, b) -> a
fst Binding tyname name uni fun (a, Uniques)
b)
    then Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b
    else \Term tyname name uni fun (a, Uniques)
body ->
      let us :: Uniques
us = Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Binding tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs Binding tyname name uni fun (a, Uniques)
b
       in Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun (a, Uniques)
 -> Reader FloatInContext (Term tyname name uni fun (a, Uniques)))
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b. (a -> b) -> a -> b
$ (a, Uniques)
-> Recursivity
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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 (a
letAnn, Uniques
us) Recursivity
NonRec (Binding tyname name uni fun (a, Uniques)
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun (a, Uniques)
b) Term tyname name uni fun (a, Uniques)
body
  where
    go ::
      Binding tyname name uni fun (a, Uniques) ->
      Term tyname name uni fun (a, Uniques) ->
      Reader FloatInContext (Term tyname name uni fun (a, Uniques))
    go :: Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b !Term tyname name uni fun (a, Uniques)
body = case Term tyname name uni fun (a, Uniques)
body of
      Apply (a
a, Uniques
usBody) Term tyname name uni fun (a, Uniques)
fun Term tyname name uni fun (a, Uniques)
arg
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
fun) -> do
            -- `fun` does not mention the binding, so we can place the binding
            -- inside `arg`.
            -- See Note [Float-in] #4
            Usages
usgs <- (FloatInContext -> Usages)
-> ReaderT FloatInContext Identity Usages
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks (Getting Usages FloatInContext Usages -> FloatInContext -> Usages
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Usages FloatInContext Usages
Lens' FloatInContext Usages
ctxtUsages)
            let inManyOccRhs :: Bool
inManyOccRhs = case Term tyname name uni fun (a, Uniques)
fun of
                  LamAbs (a, Uniques)
_ name
name Type tyname uni (a, Uniques)
_ Term tyname name uni fun (a, Uniques)
_ ->
                    name -> Usages -> Int
forall n unique. HasUnique n unique => n -> Usages -> Int
Usages.getUsageCount name
name Usages
usgs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
                  Builtin{} -> Bool
False
                  -- We need to be conservative here, this could be something
                  -- that computes to a function that uses its argument repeatedly.
                  Term tyname name uni fun (a, Uniques)
_ -> Bool
True
            (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) Term tyname name uni fun (a, Uniques)
fun
              (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FloatInContext -> FloatInContext)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall r (m :: * -> *) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local (ASetter FloatInContext FloatInContext Bool Bool
-> (Bool -> Bool) -> FloatInContext -> FloatInContext
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter FloatInContext FloatInContext Bool Bool
Lens' FloatInContext Bool
ctxtInManyOccRhs (Bool -> Bool -> Bool
|| Bool
inManyOccRhs)) (Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
arg)
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
arg) ->
            -- `arg` does not mention the binding, so we can place the binding
            -- inside `fun`.
            (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> ReaderT
     FloatInContext
     Identity
     (Term tyname name uni fun (a, Uniques)
      -> Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
fun ReaderT
  FloatInContext
  Identity
  (Term tyname name uni fun (a, Uniques)
   -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b.
ReaderT FloatInContext Identity (a -> b)
-> ReaderT FloatInContext Identity a
-> ReaderT FloatInContext Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun (a, Uniques)
arg
      LamAbs (a
a, Uniques
usBody) name
n Type tyname uni (a, Uniques)
ty Term tyname name uni fun (a, Uniques)
lamAbsBody
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty) ->
            -- See Note [Float-in] #6
            ReaderT FloatInContext Identity Bool
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM
              ((FloatInContext -> Bool) -> ReaderT FloatInContext Identity Bool
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks (Getting Bool FloatInContext Bool -> FloatInContext -> Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool FloatInContext Bool
Lens' FloatInContext Bool
ctxtInManyOccRhs) ReaderT FloatInContext Identity Bool
-> ReaderT FloatInContext Identity Bool
-> ReaderT FloatInContext Identity Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
&&^ ReaderT FloatInContext Identity Bool
-> ReaderT FloatInContext Identity Bool
forall (m :: * -> *). Functor m => m Bool -> m Bool
notM ((FloatInContext -> Bool) -> ReaderT FloatInContext Identity Bool
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks (Getting Bool FloatInContext Bool -> FloatInContext -> Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool FloatInContext Bool
Lens' FloatInContext Bool
ctxtRelaxed)))
              Reader FloatInContext (Term tyname name uni fun (a, Uniques))
giveup
              ((a, Uniques)
-> name
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) name
n Type tyname uni (a, Uniques)
ty (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
lamAbsBody)
      TyAbs (a
a, Uniques
usBody) tyname
n Kind (a, Uniques)
k Term tyname name uni fun (a, Uniques)
tyAbsBody ->
        -- See Note [Float-in] #6
        ReaderT FloatInContext Identity Bool
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM
          ((FloatInContext -> Bool) -> ReaderT FloatInContext Identity Bool
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks (Getting Bool FloatInContext Bool -> FloatInContext -> Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool FloatInContext Bool
Lens' FloatInContext Bool
ctxtInManyOccRhs) ReaderT FloatInContext Identity Bool
-> ReaderT FloatInContext Identity Bool
-> ReaderT FloatInContext Identity Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
&&^ ReaderT FloatInContext Identity Bool
-> ReaderT FloatInContext Identity Bool
forall (m :: * -> *). Functor m => m Bool -> m Bool
notM ((FloatInContext -> Bool) -> ReaderT FloatInContext Identity Bool
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks (Getting Bool FloatInContext Bool -> FloatInContext -> Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool FloatInContext Bool
Lens' FloatInContext Bool
ctxtRelaxed)))
          Reader FloatInContext (Term tyname name uni fun (a, Uniques))
giveup
          ((a, Uniques)
-> tyname
-> Kind (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) tyname
n Kind (a, Uniques)
k (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
tyAbsBody)
      TyInst (a
a, Uniques
usBody) Term tyname name uni fun (a, Uniques)
tyInstBody Type tyname uni (a, Uniques)
ty
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty) ->
            -- A binding can always be placed inside the body a `TyInst` if `ty`
            -- doesn't use any of the `declaredUniqs`.
            (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) (Term tyname name uni fun (a, Uniques)
 -> Type tyname uni (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> ReaderT
     FloatInContext
     Identity
     (Type tyname uni (a, Uniques)
      -> Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
tyInstBody ReaderT
  FloatInContext
  Identity
  (Type tyname uni (a, Uniques)
   -> Term tyname name uni fun (a, Uniques))
-> ReaderT FloatInContext Identity (Type tyname uni (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b.
ReaderT FloatInContext Identity (a -> b)
-> ReaderT FloatInContext Identity a
-> ReaderT FloatInContext Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni (a, Uniques)
-> ReaderT FloatInContext Identity (Type tyname uni (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni (a, Uniques)
ty
      Let (a
a, Uniques
usBody) Recursivity
NonRec NonEmpty (Binding tyname name uni fun (a, Uniques))
bs Term tyname name uni fun (a, Uniques)
letBody
        -- The binding can be placed inside a `Let`, if the right hand sides of the
        -- bindings of the `Let` do not mention `var`.
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs ((Binding tyname name uni fun (a, Uniques) -> Uniques)
-> NonEmpty (Binding tyname name uni fun (a, Uniques)) -> Uniques
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs NonEmpty (Binding tyname name uni fun (a, Uniques))
bs) ->
            (a, Uniques)
-> Recursivity
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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 (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) Recursivity
NonRec NonEmpty (Binding tyname name uni fun (a, Uniques))
bs (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
letBody
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
letBody)
        , Just ([Binding tyname name uni fun (a, Uniques)]
before, TermBind (a
a', Uniques
usBind') Strictness
s' VarDecl tyname name uni (a, Uniques)
var' Term tyname name uni fun (a, Uniques)
rhs', [Binding tyname name uni fun (a, Uniques)]
after) <-
            Uniques
-> [Binding tyname name uni fun (a, Uniques)]
-> (Binding tyname name uni fun (a, Uniques) -> Uniques)
-> Maybe
     ([Binding tyname name uni fun (a, Uniques)],
      Binding tyname name uni fun (a, Uniques),
      [Binding tyname name uni fun (a, Uniques)])
forall t. Uniques -> [t] -> (t -> Uniques) -> Maybe ([t], t, [t])
findNonDisjoint Uniques
declaredUniqs (NonEmpty (Binding tyname name uni fun (a, Uniques))
-> [Binding tyname name uni fun (a, Uniques)]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty (Binding tyname name uni fun (a, Uniques))
bs) Binding tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs
        , -- The LHS (declared variable) must not use any uniques in `us`. Only the RHS is
          -- allowed to use them. Otherwise we cannot float a binding whose unique set is `us`
          -- into the RHS of this `TermBind`.
          Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (VarDecl tyname name uni (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) a.
VarDecl tyname name uni (a, Uniques) -> Uniques
varDeclUniqs VarDecl tyname name uni (a, Uniques)
var') ->
            do
              -- `letBody` does not mention `var`, and there is exactly one
              -- RHS in `bs` that mentions `var`, so we can place `b`
              -- inside one of the RHSs in `bs`.
              FloatInContext
ctxt <- ReaderT FloatInContext Identity FloatInContext
forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
              let usageCnt :: Int
usageCnt = VarDecl tyname name uni (a, Uniques) -> Usages -> Int
forall n unique. HasUnique n unique => n -> Usages -> Int
Usages.getUsageCount VarDecl tyname name uni (a, Uniques)
var' (FloatInContext
ctxt FloatInContext -> Getting Usages FloatInContext Usages -> Usages
forall s a. s -> Getting a s a -> a
^. Getting Usages FloatInContext Usages
Lens' FloatInContext Usages
ctxtUsages)
                  safe :: Bool
safe = case Strictness
s' of
                    Strictness
Strict -> Bool
True
                    Strictness
NonStrict ->
                      Bool -> Bool
not (FloatInContext
ctxt FloatInContext -> Getting Bool FloatInContext Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool FloatInContext Bool
Lens' FloatInContext Bool
ctxtInManyOccRhs)
                        -- Descending into a non-strict binding whose LHS is used
                        -- more than once should be avoided, regardless of
                        -- `ctxtInManyOccRhs`.
                        -- See Note [Float-in] #4
                        Bool -> Bool -> Bool
&& Int
usageCnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
                  inManyOccRhs :: Bool
inManyOccRhs = Int
usageCnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
              if Bool
safe
                then do
                  Binding tyname name uni fun (a, Uniques)
b'' <-
                    (a, Uniques)
-> Strictness
-> VarDecl tyname name uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Binding tyname name uni fun (a, Uniques)
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 (a
a', Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBind') Strictness
s' VarDecl tyname name uni (a, Uniques)
var'
                      (Term tyname name uni fun (a, Uniques)
 -> Binding tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> ReaderT
     FloatInContext Identity (Binding tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FloatInContext -> FloatInContext)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall r (m :: * -> *) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local
                        (ASetter FloatInContext FloatInContext Bool Bool
-> (Bool -> Bool) -> FloatInContext -> FloatInContext
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter FloatInContext FloatInContext Bool Bool
Lens' FloatInContext Bool
ctxtInManyOccRhs (Bool -> Bool -> Bool
|| Bool
inManyOccRhs))
                        (Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
rhs')
                  let bs' :: NonEmpty (Binding tyname name uni fun (a, Uniques))
bs' = [Binding tyname name uni fun (a, Uniques)]
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
forall a. [a] -> NonEmpty a -> NonEmpty a
NonEmpty.appendr [Binding tyname name uni fun (a, Uniques)]
before (Binding tyname name uni fun (a, Uniques)
b'' Binding tyname name uni fun (a, Uniques)
-> [Binding tyname name uni fun (a, Uniques)]
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
forall a. a -> [a] -> NonEmpty a
:| [Binding tyname name uni fun (a, Uniques)]
after)
                  Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun (a, Uniques)
 -> Reader FloatInContext (Term tyname name uni fun (a, Uniques)))
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b. (a -> b) -> a -> b
$ (a, Uniques)
-> Recursivity
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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 (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) Recursivity
NonRec NonEmpty (Binding tyname name uni fun (a, Uniques))
bs' Term tyname name uni fun (a, Uniques)
letBody
                else Reader FloatInContext (Term tyname name uni fun (a, Uniques))
giveup
      IWrap (a
a, Uniques
usBody) Type tyname uni (a, Uniques)
ty1 Type tyname uni (a, Uniques)
ty2 Term tyname name uni fun (a, Uniques)
iwrapBody
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty1)
        , Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty2) ->
            -- A binding can be placed inside an `IWrap`, if `ty1` and `ty2`
            -- do not use any of the `declaredUniqs`.
            (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
IWrap (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) Type tyname uni (a, Uniques)
ty1 Type tyname uni (a, Uniques)
ty2 (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
iwrapBody
      Unwrap (a
a, Uniques
usBody) Term tyname name uni fun (a, Uniques)
unwrapBody ->
        -- A binding can always be placed inside an `Unwrap`.
        (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a -> Term tyname name uni fun a -> Term tyname name uni fun a
Unwrap (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) (Term tyname name uni fun (a, Uniques)
 -> Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
unwrapBody
      Constr (a
a, Uniques
usBody) Type tyname uni (a, Uniques)
ty Word64
i [Term tyname name uni fun (a, Uniques)]
es
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty)
        , Just ([Term tyname name uni fun (a, Uniques)]
before, Term tyname name uni fun (a, Uniques)
t, [Term tyname name uni fun (a, Uniques)]
after) <-
            Uniques
-> [Term tyname name uni fun (a, Uniques)]
-> (Term tyname name uni fun (a, Uniques) -> Uniques)
-> Maybe
     ([Term tyname name uni fun (a, Uniques)],
      Term tyname name uni fun (a, Uniques),
      [Term tyname name uni fun (a, Uniques)])
forall t. Uniques -> [t] -> (t -> Uniques) -> Maybe ([t], t, [t])
findNonDisjoint Uniques
declaredUniqs [Term tyname name uni fun (a, Uniques)]
es Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs ->
            do
              Term tyname name uni fun (a, Uniques)
t' <- Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
t
              Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun (a, Uniques)
 -> Reader FloatInContext (Term tyname name uni fun (a, Uniques)))
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b. (a -> b) -> a -> b
$ (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Word64
-> [Term tyname name uni fun (a, Uniques)]
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Constr (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) Type tyname uni (a, Uniques)
ty Word64
i ([Term tyname name uni fun (a, Uniques)]
before [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
forall a. [a] -> [a] -> [a]
++ [Term tyname name uni fun (a, Uniques)
t'] [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
forall a. [a] -> [a] -> [a]
++ [Term tyname name uni fun (a, Uniques)]
after)
      Case (a
a, Uniques
usBody) Type tyname uni (a, Uniques)
ty Term tyname name uni fun (a, Uniques)
arg [Term tyname name uni fun (a, Uniques)]
cs
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty)
        , Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
arg)
        , Just ([Term tyname name uni fun (a, Uniques)]
before, Term tyname name uni fun (a, Uniques)
c, [Term tyname name uni fun (a, Uniques)]
after) <-
            Uniques
-> [Term tyname name uni fun (a, Uniques)]
-> (Term tyname name uni fun (a, Uniques) -> Uniques)
-> Maybe
     ([Term tyname name uni fun (a, Uniques)],
      Term tyname name uni fun (a, Uniques),
      [Term tyname name uni fun (a, Uniques)])
forall t. Uniques -> [t] -> (t -> Uniques) -> Maybe ([t], t, [t])
findNonDisjoint Uniques
declaredUniqs [Term tyname name uni fun (a, Uniques)]
cs Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs ->
            do
              Term tyname name uni fun (a, Uniques)
c' <- Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
c
              Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun (a, Uniques)
 -> Reader FloatInContext (Term tyname name uni fun (a, Uniques)))
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b. (a -> b) -> a -> b
$ (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> [Term tyname name uni fun (a, Uniques)]
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) Type tyname uni (a, Uniques)
ty Term tyname name uni fun (a, Uniques)
arg ([Term tyname name uni fun (a, Uniques)]
before [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
forall a. [a] -> [a] -> [a]
++ [Term tyname name uni fun (a, Uniques)
c'] [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
-> [Term tyname name uni fun (a, Uniques)]
forall a. [a] -> [a] -> [a]
++ [Term tyname name uni fun (a, Uniques)]
after)
        | Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Type tyname uni (a, Uniques) -> Uniques
forall tyname (uni :: * -> *) a.
Type tyname uni (a, Uniques) -> Uniques
typeUniqs Type tyname uni (a, Uniques)
ty)
        , (Term tyname name uni fun (a, Uniques) -> Bool)
-> [Term tyname name uni fun (a, Uniques)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Term tyname name uni fun (a, Uniques)
c -> Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Uniques
declaredUniqs (Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
c)) [Term tyname name uni fun (a, Uniques)]
cs ->
            do
              Term tyname name uni fun (a, Uniques)
arg' <- Binding tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
go Binding tyname name uni fun (a, Uniques)
b Term tyname name uni fun (a, Uniques)
arg
              Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun (a, Uniques)
 -> Reader FloatInContext (Term tyname name uni fun (a, Uniques)))
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b. (a -> b) -> a -> b
$ (a, Uniques)
-> Type tyname uni (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
-> [Term tyname name uni fun (a, Uniques)]
-> Term tyname name uni fun (a, Uniques)
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case (a
a, Uniques
usBind Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Uniques
usBody) Type tyname uni (a, Uniques)
ty Term tyname name uni fun (a, Uniques)
arg' [Term tyname name uni fun (a, Uniques)]
cs
      Term tyname name uni fun (a, Uniques)
_ -> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
giveup
      where
        giveup :: Reader FloatInContext (Term tyname name uni fun (a, Uniques))
giveup =
          let us :: Uniques
us = Term tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun (a, Uniques) -> Uniques
termUniqs Term tyname name uni fun (a, Uniques)
body Uniques -> Uniques -> Uniques
forall a. Semigroup a => a -> a -> a
<> Binding tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs Binding tyname name uni fun (a, Uniques)
b
           in Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a. a -> ReaderT FloatInContext Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun (a, Uniques)
 -> Reader FloatInContext (Term tyname name uni fun (a, Uniques)))
-> Term tyname name uni fun (a, Uniques)
-> Reader FloatInContext (Term tyname name uni fun (a, Uniques))
forall a b. (a -> b) -> a -> b
$ (a, Uniques)
-> Recursivity
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
-> Term tyname name uni fun (a, Uniques)
-> Term tyname name uni fun (a, Uniques)
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 (a
letAnn, Uniques
us) Recursivity
NonRec (Binding tyname name uni fun (a, Uniques)
-> NonEmpty (Binding tyname name uni fun (a, Uniques))
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun (a, Uniques)
b) Term tyname name uni fun (a, Uniques)
body
        declaredUniqs :: Uniques
declaredUniqs = [Unique] -> Uniques
forall a. Ord a => [a] -> Set a
Set.fromList ([Unique] -> Uniques) -> [Unique] -> Uniques
forall a b. (a -> b) -> a -> b
$ Binding tyname name uni fun (a, Uniques)
b Binding tyname name uni fun (a, Uniques)
-> Getting
     (Endo [Unique]) (Binding tyname name uni fun (a, Uniques)) Unique
-> [Unique]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. Getting
  (Endo [Unique]) (Binding tyname name uni fun (a, Uniques)) Unique
forall tyname name (uni :: * -> *) fun a.
(HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
Traversal1' (Binding tyname name uni fun a) Unique
Traversal1' (Binding tyname name uni fun (a, Uniques)) Unique
bindingIds
        usBind :: Uniques
usBind = Binding tyname name uni fun (a, Uniques) -> Uniques
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun (a, Uniques) -> Uniques
bindingUniqs Binding tyname name uni fun (a, Uniques)
b

{- |
Search the given list of elements for the unique one whose 'Uniques' are non-disjoint
with the given 'Uniques'. Then, split the list at that point.
-}
findNonDisjoint :: Uniques -> [t] -> (t -> Uniques) -> Maybe ([t], t, [t])
findNonDisjoint :: forall t. Uniques -> [t] -> (t -> Uniques) -> Maybe ([t], t, [t])
findNonDisjoint Uniques
us [t]
bs t -> Uniques
getUniques = case [(t, Int)]
is of
  [(t
t, Int
i)] -> ([t], t, [t]) -> Maybe ([t], t, [t])
forall a. a -> Maybe a
Just (Int -> [t] -> [t]
forall a. Int -> [a] -> [a]
take Int
i [t]
bs, t
t, Int -> [t] -> [t]
forall a. Int -> [a] -> [a]
drop (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [t]
bs)
  [(t, Int)]
_        -> Maybe ([t], t, [t])
forall a. Maybe a
Nothing
  where
    is :: [(t, Int)]
is = ((t, Int) -> Bool) -> [(t, Int)] -> [(t, Int)]
forall a. (a -> Bool) -> [a] -> [a]
List.filter (\(t
t, Int
_) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ t -> Uniques
getUniques t
t Uniques -> Uniques -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.disjoint` Uniques
us) ([t]
bs [t] -> [Int] -> [(t, Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0 ..])