{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
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
type Uniques = Set PLC.Unique
data FloatInContext = FloatInContext
{ FloatInContext -> Bool
_ctxtInManyOccRhs :: Bool
, FloatInContext -> Usages
_ctxtUsages :: Usages.Usages
, FloatInContext -> Bool
_ctxtRelaxed :: Bool
}
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 ->
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)]
floatTerm ::
forall tyname name uni fun a.
( PLC.HasUnique name PLC.TermUnique
, PLC.HasUnique tyname PLC.TypeUnique
, PLC.ToBuiltinMeaning uni fun
) =>
BuiltinsInfo uni fun ->
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
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
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 ->
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
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, 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) ->
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)
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'
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
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
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
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
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)
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
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
TypeBind{} -> Bool
True
DatatypeBind{} -> Bool
True
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 ->
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
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
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) ->
(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) ->
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 ->
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, 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
| 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
,
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
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)
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, 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, 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
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 ..])