{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
module PlutusIR.Transform.LetFloatOut (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.Purity
import PlutusIR.Subst
import Control.Arrow ((>>>))
import Control.Lens hiding (Strict)
import Control.Monad.Extra
import Control.Monad.Reader
import Control.Monad.Writer
import Data.Coerce
import Data.List.NonEmpty qualified as NE
import Data.Map.Monoidal qualified as MM
import Data.Semigroup.Foldable
import Data.Semigroup.Generic
import GHC.Generics
import PlutusCore.Name.UniqueMap qualified as UMap
import PlutusCore.Name.UniqueSet qualified as USet
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo
import PlutusIR.Pass
import PlutusIR.TypeCheck qualified as TC
newtype Depth = Depth Int
deriving newtype (Depth -> Depth -> Bool
(Depth -> Depth -> Bool) -> (Depth -> Depth -> Bool) -> Eq Depth
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Depth -> Depth -> Bool
== :: Depth -> Depth -> Bool
$c/= :: Depth -> Depth -> Bool
/= :: Depth -> Depth -> Bool
Eq, Eq Depth
Eq Depth =>
(Depth -> Depth -> Ordering)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> Ord Depth
Depth -> Depth -> Bool
Depth -> Depth -> Ordering
Depth -> Depth -> Depth
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Depth -> Depth -> Ordering
compare :: Depth -> Depth -> Ordering
$c< :: Depth -> Depth -> Bool
< :: Depth -> Depth -> Bool
$c<= :: Depth -> Depth -> Bool
<= :: Depth -> Depth -> Bool
$c> :: Depth -> Depth -> Bool
> :: Depth -> Depth -> Bool
$c>= :: Depth -> Depth -> Bool
>= :: Depth -> Depth -> Bool
$cmax :: Depth -> Depth -> Depth
max :: Depth -> Depth -> Depth
$cmin :: Depth -> Depth -> Depth
min :: Depth -> Depth -> Depth
Ord, Int -> Depth -> ShowS
[Depth] -> ShowS
Depth -> String
(Int -> Depth -> ShowS)
-> (Depth -> String) -> ([Depth] -> ShowS) -> Show Depth
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Depth -> ShowS
showsPrec :: Int -> Depth -> ShowS
$cshow :: Depth -> String
show :: Depth -> String
$cshowList :: [Depth] -> ShowS
showList :: [Depth] -> ShowS
Show, Integer -> Depth
Depth -> Depth
Depth -> Depth -> Depth
(Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth)
-> (Depth -> Depth)
-> (Depth -> Depth)
-> (Integer -> Depth)
-> Num Depth
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Depth -> Depth -> Depth
+ :: Depth -> Depth -> Depth
$c- :: Depth -> Depth -> Depth
- :: Depth -> Depth -> Depth
$c* :: Depth -> Depth -> Depth
* :: Depth -> Depth -> Depth
$cnegate :: Depth -> Depth
negate :: Depth -> Depth
$cabs :: Depth -> Depth
abs :: Depth -> Depth
$csignum :: Depth -> Depth
signum :: Depth -> Depth
$cfromInteger :: Integer -> Depth
fromInteger :: Integer -> Depth
Num)
data Pos = Pos
{ Pos -> Depth
_posDepth :: Depth
, Pos -> Unique
_posUnique :: PLC.Unique
, Pos -> PosType
_posType :: PosType
}
deriving stock (Pos -> Pos -> Bool
(Pos -> Pos -> Bool) -> (Pos -> Pos -> Bool) -> Eq Pos
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pos -> Pos -> Bool
== :: Pos -> Pos -> Bool
$c/= :: Pos -> Pos -> Bool
/= :: Pos -> Pos -> Bool
Eq, Eq Pos
Eq Pos =>
(Pos -> Pos -> Ordering)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Pos)
-> (Pos -> Pos -> Pos)
-> Ord Pos
Pos -> Pos -> Bool
Pos -> Pos -> Ordering
Pos -> Pos -> Pos
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Pos -> Pos -> Ordering
compare :: Pos -> Pos -> Ordering
$c< :: Pos -> Pos -> Bool
< :: Pos -> Pos -> Bool
$c<= :: Pos -> Pos -> Bool
<= :: Pos -> Pos -> Bool
$c> :: Pos -> Pos -> Bool
> :: Pos -> Pos -> Bool
$c>= :: Pos -> Pos -> Bool
>= :: Pos -> Pos -> Bool
$cmax :: Pos -> Pos -> Pos
max :: Pos -> Pos -> Pos
$cmin :: Pos -> Pos -> Pos
min :: Pos -> Pos -> Pos
Ord, Int -> Pos -> ShowS
[Pos] -> ShowS
Pos -> String
(Int -> Pos -> ShowS)
-> (Pos -> String) -> ([Pos] -> ShowS) -> Show Pos
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Pos -> ShowS
showsPrec :: Int -> Pos -> ShowS
$cshow :: Pos -> String
show :: Pos -> String
$cshowList :: [Pos] -> ShowS
showList :: [Pos] -> ShowS
Show)
data PosType = LamBody
| LetRhs
deriving stock (PosType -> PosType -> Bool
(PosType -> PosType -> Bool)
-> (PosType -> PosType -> Bool) -> Eq PosType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PosType -> PosType -> Bool
== :: PosType -> PosType -> Bool
$c/= :: PosType -> PosType -> Bool
/= :: PosType -> PosType -> Bool
Eq, Eq PosType
Eq PosType =>
(PosType -> PosType -> Ordering)
-> (PosType -> PosType -> Bool)
-> (PosType -> PosType -> Bool)
-> (PosType -> PosType -> Bool)
-> (PosType -> PosType -> Bool)
-> (PosType -> PosType -> PosType)
-> (PosType -> PosType -> PosType)
-> Ord PosType
PosType -> PosType -> Bool
PosType -> PosType -> Ordering
PosType -> PosType -> PosType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: PosType -> PosType -> Ordering
compare :: PosType -> PosType -> Ordering
$c< :: PosType -> PosType -> Bool
< :: PosType -> PosType -> Bool
$c<= :: PosType -> PosType -> Bool
<= :: PosType -> PosType -> Bool
$c> :: PosType -> PosType -> Bool
> :: PosType -> PosType -> Bool
$c>= :: PosType -> PosType -> Bool
>= :: PosType -> PosType -> Bool
$cmax :: PosType -> PosType -> PosType
max :: PosType -> PosType -> PosType
$cmin :: PosType -> PosType -> PosType
min :: PosType -> PosType -> PosType
Ord, Int -> PosType -> ShowS
[PosType] -> ShowS
PosType -> String
(Int -> PosType -> ShowS)
-> (PosType -> String) -> ([PosType] -> ShowS) -> Show PosType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PosType -> ShowS
showsPrec :: Int -> PosType -> ShowS
$cshow :: PosType -> String
show :: PosType -> String
$cshowList :: [PosType] -> ShowS
showList :: [PosType] -> ShowS
Show)
topPos :: Pos
topPos :: Pos
topPos = Depth -> Unique -> PosType -> Pos
Pos Depth
topDepth Unique
topUnique PosType
topType
topUnique :: PLC.Unique
topUnique :: Unique
topUnique = Int -> Unique
forall a b. Coercible a b => a -> b
coerce (-Int
1 :: Int)
topDepth :: Depth
topDepth :: Depth
topDepth = -Depth
1
topType :: PosType
topType :: PosType
topType = PosType
LamBody
representativeBindingUnique
:: (PLC.HasUnique name PLC.TermUnique, PLC.HasUnique tyname PLC.TypeUnique)
=> NE.NonEmpty (Binding tyname name uni fun a) -> PLC.Unique
representativeBindingUnique :: forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a) -> Unique
representativeBindingUnique =
Getting (First Unique) (Binding tyname name uni fun a) Unique
-> Binding tyname name uni fun a -> Unique
forall a s. Getting (First a) s a -> s -> a
first1Of Getting (First Unique) (Binding tyname name uni fun a) 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) Unique
bindingIds (Binding tyname name uni fun a -> Unique)
-> (NonEmpty (Binding tyname name uni fun a)
-> Binding tyname name uni fun a)
-> NonEmpty (Binding tyname name uni fun a)
-> Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Binding tyname name uni fun a)
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
NonEmpty (Binding tyname name uni fun a)
-> Binding tyname name uni fun a
representativeBinding
where
representativeBinding :: NE.NonEmpty (Binding tyname name uni fun a) -> Binding tyname name uni fun a
representativeBinding :: forall tyname name (uni :: * -> *) fun a.
NonEmpty (Binding tyname name uni fun a)
-> Binding tyname name uni fun a
representativeBinding = NonEmpty (Binding tyname name uni fun a)
-> Binding tyname name uni fun a
forall a. NonEmpty a -> a
NE.head
type Scope = PLC.UniqueMap PLC.Unique Pos
data MarkCtx tyname name uni fun a = MarkCtx
{ forall tyname name (uni :: * -> *) fun a.
MarkCtx tyname name uni fun a -> Depth
_markCtxDepth :: Depth
, forall tyname name (uni :: * -> *) fun a.
MarkCtx tyname name uni fun a -> Scope
_markCtxScope :: Scope
, forall tyname name (uni :: * -> *) fun a.
MarkCtx tyname name uni fun a -> BuiltinsInfo uni fun
_markBuiltinsInfo :: BuiltinsInfo uni fun
, forall tyname name (uni :: * -> *) fun a.
MarkCtx tyname name uni fun a -> VarsInfo tyname name uni a
_markVarsInfo :: VarsInfo tyname name uni a
}
makeLenses ''MarkCtx
type Marks = Scope
data BindingGrp tyname name uni fun a = BindingGrp {
forall tyname name (uni :: * -> *) fun a.
BindingGrp tyname name uni fun a -> a
_bgAnn :: a,
forall tyname name (uni :: * -> *) fun a.
BindingGrp tyname name uni fun a -> Recursivity
_bgRec :: Recursivity,
forall tyname name (uni :: * -> *) fun a.
BindingGrp tyname name uni fun a
-> NonEmpty (Binding tyname name uni fun a)
_bgBindings :: NE.NonEmpty (Binding tyname name uni fun a)
}
deriving stock (forall x.
BindingGrp tyname name uni fun a
-> Rep (BindingGrp tyname name uni fun a) x)
-> (forall x.
Rep (BindingGrp tyname name uni fun a) x
-> BindingGrp tyname name uni fun a)
-> Generic (BindingGrp tyname name uni fun a)
forall x.
Rep (BindingGrp tyname name uni fun a) x
-> BindingGrp tyname name uni fun a
forall x.
BindingGrp tyname name uni fun a
-> Rep (BindingGrp tyname name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun a x.
Rep (BindingGrp tyname name uni fun a) x
-> BindingGrp tyname name uni fun a
forall tyname name (uni :: * -> *) fun a x.
BindingGrp tyname name uni fun a
-> Rep (BindingGrp tyname name uni fun a) x
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
BindingGrp tyname name uni fun a
-> Rep (BindingGrp tyname name uni fun a) x
from :: forall x.
BindingGrp tyname name uni fun a
-> Rep (BindingGrp tyname name uni fun a) x
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (BindingGrp tyname name uni fun a) x
-> BindingGrp tyname name uni fun a
to :: forall x.
Rep (BindingGrp tyname name uni fun a) x
-> BindingGrp tyname name uni fun a
Generic
deriving NonEmpty (BindingGrp tyname name uni fun a)
-> BindingGrp tyname name uni fun a
BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
(BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a)
-> (NonEmpty (BindingGrp tyname name uni fun a)
-> BindingGrp tyname name uni fun a)
-> (forall b.
Integral b =>
b
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a)
-> Semigroup (BindingGrp tyname name uni fun a)
forall b.
Integral b =>
b
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall tyname name (uni :: * -> *) fun a.
Semigroup a =>
NonEmpty (BindingGrp tyname name uni fun a)
-> BindingGrp tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Semigroup a =>
BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(Semigroup a, Integral b) =>
b
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
$c<> :: forall tyname name (uni :: * -> *) fun a.
Semigroup a =>
BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
<> :: BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
$csconcat :: forall tyname name (uni :: * -> *) fun a.
Semigroup a =>
NonEmpty (BindingGrp tyname name uni fun a)
-> BindingGrp tyname name uni fun a
sconcat :: NonEmpty (BindingGrp tyname name uni fun a)
-> BindingGrp tyname name uni fun a
$cstimes :: forall tyname name (uni :: * -> *) fun a b.
(Semigroup a, Integral b) =>
b
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
stimes :: forall b.
Integral b =>
b
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
Semigroup via (GenericSemigroupMonoid (BindingGrp tyname name uni fun a))
makeLenses ''BindingGrp
bindingGrpToLet :: Recursivity
-> BindingGrp tyname name uni fun a
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
bindingGrpToLet :: forall tyname name (uni :: * -> *) fun a.
Recursivity
-> BindingGrp tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
bindingGrpToLet Recursivity
r (BindingGrp a
a Recursivity
r' NonEmpty (Binding tyname name uni fun a)
bs) = a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 (Recursivity
rRecursivity -> Recursivity -> Recursivity
forall a. Semigroup a => a -> a -> a
<>Recursivity
r') NonEmpty (Binding tyname name uni fun a)
bs
type FloatTable tyname name uni fun a = MM.MonoidalMap Pos (NE.NonEmpty (BindingGrp tyname name uni fun a))
mark :: forall tyname name uni fun a.
(PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique, PLC.ToBuiltinMeaning uni fun)
=> BuiltinsInfo uni fun
-> Term tyname name uni fun a
-> Marks
mark :: forall tyname name (uni :: * -> *) fun a.
(HasUnique tyname TypeUnique, HasUnique name TermUnique,
ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun -> Term tyname name uni fun a -> Scope
mark BuiltinsInfo uni fun
binfo Term tyname name uni fun a
tm = ((), Scope) -> Scope
forall a b. (a, b) -> b
snd (((), Scope) -> Scope) -> ((), Scope) -> Scope
forall a b. (a -> b) -> a -> b
$ Writer Scope () -> ((), Scope)
forall w a. Writer w a -> (a, w)
runWriter (Writer Scope () -> ((), Scope)) -> Writer Scope () -> ((), Scope)
forall a b. (a -> b) -> a -> b
$ (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> MarkCtx tyname name uni fun a -> Writer Scope ())
-> MarkCtx tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> Writer Scope ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> MarkCtx tyname name uni fun a -> Writer Scope ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Depth
-> Scope
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> MarkCtx tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Depth
-> Scope
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> MarkCtx tyname name uni fun a
MarkCtx Depth
topDepth Scope
forall a. Monoid a => a
mempty BuiltinsInfo uni fun
binfo (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
tm)) (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> Writer Scope ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> Writer Scope ()
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go Term tyname name uni fun a
tm
where
go :: Term tyname name uni fun a -> ReaderT (MarkCtx tyname name uni fun a) (Writer Marks) ()
go :: Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go = Term tyname name uni fun a -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
breakNonRec (Term tyname name uni fun a -> Term tyname name uni fun a)
-> (Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
LamAbs a
_ name
n Type tyname uni a
_ Term tyname name uni fun a
tBody -> name
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) unique a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique name unique) =>
name -> m a -> m a
withLam name
n (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go Term tyname name uni fun a
tBody
TyAbs a
_ tyname
n Kind a
_ Term tyname name uni fun a
tBody -> tyname
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) unique a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique tyname unique) =>
tyname -> m a -> m a
withAbs tyname
n (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go Term tyname name uni fun a
tBody
Let a
ann Recursivity
r bs :: NonEmpty (Binding tyname name uni fun a)
bs@(NonEmpty (Binding tyname name uni fun a) -> Unique
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a) -> Unique
representativeBindingUnique -> Unique
letU) Term tyname name uni fun a
tIn ->
let letN :: BindingGrp tyname name uni fun a
letN = a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> BindingGrp tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> BindingGrp tyname name uni fun a
BindingGrp a
ann Recursivity
r NonEmpty (Binding tyname name uni fun a)
bs in
ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) Bool
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (BindingGrp tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) Bool
forall tyname name (uni :: * -> *) fun a (m :: * -> *).
(MonadReader (MarkCtx tyname name uni fun a) m,
ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BindingGrp tyname name uni fun a -> m Bool
floatable BindingGrp tyname name uni fun a
letN)
(do
Scope
scope <- Getting Scope (MarkCtx tyname name uni fun a) Scope
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) Scope
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Scope (MarkCtx tyname name uni fun a) Scope
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Scope -> f Scope)
-> MarkCtx tyname name uni fun a
-> f (MarkCtx tyname name uni fun a)
markCtxScope
let freeVars :: UniqueSet Unique
freeVars =
Recursivity
-> (UniqueSet Unique -> UniqueSet Unique)
-> UniqueSet Unique
-> UniqueSet Unique
forall a. Recursivity -> (a -> a) -> a -> a
ifRec Recursivity
r (UniqueSet Unique -> UniqueSet Unique -> UniqueSet Unique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
USet.\\ Getting
(UniqueSet Unique)
(NonEmpty (Binding tyname name uni fun a))
Unique
-> NonEmpty (Binding tyname name uni fun a) -> UniqueSet Unique
forall unique s.
Coercible unique Unique =>
Getting (UniqueSet unique) s unique -> s -> UniqueSet unique
USet.setOfByUnique ((Binding tyname name uni fun a
-> Const (UniqueSet Unique) (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> Const
(UniqueSet Unique) (NonEmpty (Binding tyname name uni fun a))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Binding tyname name uni fun a)
(Binding tyname name uni fun a)
traversed((Binding tyname name uni fun a
-> Const (UniqueSet Unique) (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> Const
(UniqueSet Unique) (NonEmpty (Binding tyname name uni fun a)))
-> ((Unique -> Const (UniqueSet Unique) Unique)
-> Binding tyname name uni fun a
-> Const (UniqueSet Unique) (Binding tyname name uni fun a))
-> Getting
(UniqueSet Unique)
(NonEmpty (Binding tyname name uni fun a))
Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Unique -> Const (UniqueSet Unique) Unique)
-> Binding tyname name uni fun a
-> Const (UniqueSet Unique) (Binding tyname name uni fun a)
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) Unique
bindingIds) NonEmpty (Binding tyname name uni fun a)
bs) (UniqueSet Unique -> UniqueSet Unique)
-> UniqueSet Unique -> UniqueSet Unique
forall a b. (a -> b) -> a -> b
$
BindingGrp tyname name uni fun a -> UniqueSet Unique
forall tyname name (uni :: * -> *) fun a.
(HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
BindingGrp tyname name uni fun a -> UniqueSet Unique
calcFreeVars BindingGrp tyname name uni fun a
letN
let floatPos :: Pos
floatPos@(Pos Depth
floatDepth Unique
_ PosType
_) = Scope -> Pos
forall k. UniqueMap k Pos -> Pos
maxPos (Scope -> Pos) -> Scope -> Pos
forall a b. (a -> b) -> a -> b
$ Scope
scope Scope -> UniqueSet Unique -> Scope
forall unique v.
UniqueMap unique v -> UniqueSet unique -> UniqueMap unique v
`UMap.restrictKeys` UniqueSet Unique
freeVars
(Depth -> Depth)
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m) =>
(Depth -> Depth) -> m a -> m a
withDepth (Depth -> Depth -> Depth
forall a b. a -> b -> a
const Depth
floatDepth) (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$
Recursivity
-> (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a. Recursivity -> (a -> a) -> a -> a
ifRec Recursivity
r (NonEmpty (Binding tyname name uni fun a)
-> Pos
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a3 a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a3) -> Pos -> m a -> m a
withBs NonEmpty (Binding tyname name uni fun a)
bs Pos
floatPos) (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$
Getting
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a))
(Term tyname name uni fun a)
-> (Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> NonEmpty (Binding tyname name uni fun a)
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall (f :: * -> *) r s a.
Functor f =>
Getting (Traversed r f) s a -> (a -> f r) -> s -> f ()
traverseOf_ ((Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Binding tyname name uni fun a)
(Binding tyname name uni fun a)
traversed ((Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a)))
-> ((Term tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a))
-> Getting
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a))
(Term tyname name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms) Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go NonEmpty (Binding tyname name uni fun a)
bs
NonEmpty (Binding tyname name uni fun a)
-> Pos
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a3 a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a3) -> Pos -> m a -> m a
withBs NonEmpty (Binding tyname name uni fun a)
bs Pos
floatPos (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go Term tyname name uni fun a
tIn
Scope -> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Scope
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> Scope
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ [(Unique, Pos)] -> Scope
forall (f :: * -> *) unique a.
(Foldable f, Coercible Unique unique) =>
f (unique, a) -> UniqueMap unique a
UMap.fromUniques [(Unique
letU, Pos
floatPos)]
)
(ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ do
(Depth -> Depth)
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m) =>
(Depth -> Depth) -> m a -> m a
withDepth (Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+Depth
1) (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ do
Depth
depth <- Getting Depth (MarkCtx tyname name uni fun a) Depth
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) Depth
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Depth (MarkCtx tyname name uni fun a) Depth
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Depth -> f Depth)
-> MarkCtx tyname name uni fun a
-> f (MarkCtx tyname name uni fun a)
markCtxDepth
let toPos :: PosType -> Pos
toPos = Depth -> Unique -> PosType -> Pos
Pos Depth
depth Unique
letU
Recursivity
-> (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a. Recursivity -> (a -> a) -> a -> a
ifRec Recursivity
r (NonEmpty (Binding tyname name uni fun a)
-> Pos
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a3 a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a3) -> Pos -> m a -> m a
withBs NonEmpty (Binding tyname name uni fun a)
bs (Pos
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> Pos
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ PosType -> Pos
toPos PosType
LetRhs) (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ Getting
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a))
(Term tyname name uni fun a)
-> (Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> NonEmpty (Binding tyname name uni fun a)
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall (f :: * -> *) r s a.
Functor f =>
Getting (Traversed r f) s a -> (a -> f r) -> s -> f ()
traverseOf_ ((Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Binding tyname name uni fun a)
(Binding tyname name uni fun a)
traversed ((Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a)))
-> ((Term tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a))
-> Getting
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(NonEmpty (Binding tyname name uni fun a))
(Term tyname name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> Const
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Binding tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms) Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go NonEmpty (Binding tyname name uni fun a)
bs
NonEmpty (Binding tyname name uni fun a)
-> Pos
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a3 a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a3) -> Pos -> m a -> m a
withBs NonEmpty (Binding tyname name uni fun a)
bs (PosType -> Pos
toPos PosType
LamBody) (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go Term tyname name uni fun a
tIn
Term tyname name uni fun a
t -> Getting
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Term tyname name uni fun a)
(Term tyname name uni fun a)
-> (Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ())
-> Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
forall (f :: * -> *) r s a.
Functor f =>
Getting (Traversed r f) s a -> (a -> f r) -> s -> f ()
traverseOf_ Getting
(Traversed
() (ReaderT (MarkCtx tyname name uni fun a) (Writer Scope)))
(Term tyname name uni fun a)
(Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a
-> ReaderT (MarkCtx tyname name uni fun a) (Writer Scope) ()
go Term tyname name uni fun a
t
calcFreeVars :: forall tyname name uni fun a.
(PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique)
=> BindingGrp tyname name uni fun a
-> PLC.UniqueSet PLC.Unique
calcFreeVars :: forall tyname name (uni :: * -> *) fun a.
(HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
BindingGrp tyname name uni fun a -> UniqueSet Unique
calcFreeVars (BindingGrp a
_ Recursivity
r NonEmpty (Binding tyname name uni fun a)
bs) = (Binding tyname name uni fun a -> UniqueSet Unique)
-> NonEmpty (Binding tyname name uni fun a) -> UniqueSet Unique
forall m a. Semigroup m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1 Binding tyname name uni fun a -> UniqueSet Unique
calcBinding NonEmpty (Binding tyname name uni fun a)
bs
where
calcBinding :: Binding tyname name uni fun a -> PLC.UniqueSet PLC.Unique
calcBinding :: Binding tyname name uni fun a -> UniqueSet Unique
calcBinding Binding tyname name uni fun a
b =
Getting (UniqueSet Unique) (Binding tyname name uni fun a) Unique
-> Binding tyname name uni fun a -> UniqueSet Unique
forall unique s.
Coercible unique Unique =>
Getting (UniqueSet unique) s unique -> s -> UniqueSet unique
USet.setOfByUnique ((name -> Const (UniqueSet Unique) name)
-> Binding tyname name uni fun a
-> Const (UniqueSet Unique) (Binding tyname name uni fun a)
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Traversal' (Binding tyname name uni fun ann) name
Traversal' (Binding tyname name uni fun a) name
fvBinding ((name -> Const (UniqueSet Unique) name)
-> Binding tyname name uni fun a
-> Const (UniqueSet Unique) (Binding tyname name uni fun a))
-> ((Unique -> Const (UniqueSet Unique) Unique)
-> name -> Const (UniqueSet Unique) name)
-> Getting
(UniqueSet Unique) (Binding tyname name uni fun a) Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> Const (UniqueSet Unique) Unique)
-> name -> Const (UniqueSet Unique) name
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique) Binding tyname name uni fun a
b
UniqueSet Unique -> UniqueSet Unique -> UniqueSet Unique
forall a. Semigroup a => a -> a -> a
<> Getting (UniqueSet Unique) (Binding tyname name uni fun a) Unique
-> Binding tyname name uni fun a -> UniqueSet Unique
forall unique s.
Coercible unique Unique =>
Getting (UniqueSet unique) s unique -> s -> UniqueSet unique
USet.setOfByUnique (Recursivity -> Traversal' (Binding tyname name uni fun a) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity -> Traversal' (Binding tyname name uni fun ann) tyname
ftvBinding Recursivity
r ((tyname -> Const (UniqueSet Unique) tyname)
-> Binding tyname name uni fun a
-> Const (UniqueSet Unique) (Binding tyname name uni fun a))
-> ((Unique -> Const (UniqueSet Unique) Unique)
-> tyname -> Const (UniqueSet Unique) tyname)
-> Getting
(UniqueSet Unique) (Binding tyname name uni fun a) Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> Const (UniqueSet Unique) Unique)
-> tyname -> Const (UniqueSet Unique) tyname
forall name unique. HasUnique name unique => Lens' name Unique
Lens' tyname Unique
PLC.theUnique) Binding tyname name uni fun a
b
removeLets :: forall tyname name uni fun a term.
(term~Term tyname name uni fun a
,PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique)
=> Marks
-> term
-> (term, FloatTable tyname name uni fun a)
removeLets :: forall tyname name (uni :: * -> *) fun a term.
(term ~ Term tyname name uni fun a, HasUnique tyname TypeUnique,
HasUnique name TermUnique) =>
Scope -> term -> (term, FloatTable tyname name uni fun a)
removeLets Scope
marks term
term = Writer (FloatTable tyname name uni fun a) term
-> (term, FloatTable tyname name uni fun a)
forall w a. Writer w a -> (a, w)
runWriter (Writer (FloatTable tyname name uni fun a) term
-> (term, FloatTable tyname name uni fun a))
-> Writer (FloatTable tyname name uni fun a) term
-> (term, FloatTable tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ term -> Writer (FloatTable tyname name uni fun a) term
go term
term
where
go :: term -> Writer (FloatTable tyname name uni fun a) term
go :: term -> Writer (FloatTable tyname name uni fun a) term
go = Term tyname name uni fun a -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
breakNonRec (Term tyname name uni fun a -> Term tyname name uni fun a)
-> (Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a))
-> Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
Let a
a Recursivity
r bs :: NonEmpty (Binding tyname name uni fun a)
bs@(NonEmpty (Binding tyname name uni fun a) -> Unique
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a) -> Unique
representativeBindingUnique -> Unique
letU) Term tyname name uni fun a
tIn -> do
NonEmpty (Binding tyname name uni fun a)
bs' <- NonEmpty (Binding tyname name uni fun a)
bs NonEmpty (Binding tyname name uni fun a)
-> (NonEmpty (Binding tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(NonEmpty (Binding tyname name uni fun a)))
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(NonEmpty (Binding tyname name uni fun a))
forall a b. a -> (a -> b) -> b
& ((Binding tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(NonEmpty (Binding tyname name uni fun a))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Binding tyname name uni fun a)
(Binding tyname name uni fun a)
traversed ((Binding tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(NonEmpty (Binding tyname name uni fun a)))
-> ((Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Binding tyname name uni fun a))
-> (Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(NonEmpty (Binding tyname name uni fun a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Binding tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms) term -> Writer (FloatTable tyname name uni fun a) term
Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
go
term
tIn' <- term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
tIn
case Unique -> Scope -> Maybe Pos
forall unique a.
Coercible unique Unique =>
unique -> UniqueMap unique a -> Maybe a
UMap.lookupUnique Unique
letU Scope
marks of
Maybe Pos
Nothing -> Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a.
a -> WriterT (FloatTable tyname name uni fun a) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a))
-> Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 Recursivity
r NonEmpty (Binding tyname name uni fun a)
bs' term
Term tyname name uni fun a
tIn'
Just Pos
pos -> do
FloatTable tyname name uni fun a
-> WriterT (FloatTable tyname name uni fun a) Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Pos
-> NonEmpty (BindingGrp tyname name uni fun a)
-> FloatTable tyname name uni fun a
forall k a. k -> a -> MonoidalMap k a
MM.singleton Pos
pos (BindingGrp tyname name uni fun a
-> NonEmpty (BindingGrp tyname name uni fun a)
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BindingGrp tyname name uni fun a
-> NonEmpty (BindingGrp tyname name uni fun a))
-> BindingGrp tyname name uni fun a
-> NonEmpty (BindingGrp tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> BindingGrp tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> BindingGrp tyname name uni fun a
BindingGrp a
a Recursivity
r NonEmpty (Binding tyname name uni fun a)
bs'))
Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a.
a -> WriterT (FloatTable tyname name uni fun a) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure term
Term tyname name uni fun a
tIn'
Apply a
a Term tyname name uni fun a
t1 Term tyname name uni fun a
t2 -> a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply a
a (Term tyname name uni fun a
-> Term tyname name uni fun a -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
t1 WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a b.
WriterT (FloatTable tyname name uni fun a) Identity (a -> b)
-> WriterT (FloatTable tyname name uni fun a) Identity a
-> WriterT (FloatTable tyname name uni fun a) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
t2
TyInst a
a Term tyname name uni fun a
t Type tyname uni a
ty -> a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst a
a (Term tyname name uni fun a
-> Type tyname uni a -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Type tyname uni a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
t WriterT
(FloatTable tyname name uni fun a)
Identity
(Type tyname uni a -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a) Identity (Type tyname uni a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a b.
WriterT (FloatTable tyname name uni fun a) Identity (a -> b)
-> WriterT (FloatTable tyname name uni fun a) Identity a
-> WriterT (FloatTable tyname name uni fun a) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni a
-> WriterT
(FloatTable tyname name uni fun a) Identity (Type tyname uni a)
forall a.
a -> WriterT (FloatTable tyname name uni fun a) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
ty
TyAbs a
a tyname
tyname Kind a
k Term tyname name uni fun a
t -> a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs a
a tyname
tyname Kind a
k (Term tyname name uni fun a -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
t
LamAbs a
a name
name Type tyname uni a
ty Term tyname name uni fun a
t -> a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 name
name Type tyname uni a
ty (Term tyname name uni fun a -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
t
IWrap a
a Type tyname uni a
ty1 Type tyname uni a
ty2 Term tyname name uni fun a
t -> a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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
ty1 Type tyname uni a
ty2 (Term tyname name uni fun a -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
t
Unwrap a
a Term tyname name uni fun a
t -> a -> Term tyname name uni fun a -> Term tyname name uni fun a
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 -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
t
Constr a
a Type tyname uni a
ty Word64
i [Term tyname name uni fun a]
es -> a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
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 Type tyname uni a
ty Word64
i ([Term tyname name uni fun a] -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
[Term tyname name uni fun a]
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (term
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a))
-> [term]
-> WriterT
(FloatTable tyname name uni fun a)
Identity
[Term tyname name uni fun a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse term -> Writer (FloatTable tyname name uni fun a) term
term
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
go [term]
[Term tyname name uni fun a]
es
Case a
a Type tyname uni a
ty Term tyname name uni fun a
arg [Term tyname name uni fun a]
cs -> a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
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 Type tyname uni a
ty (Term tyname name uni fun a
-> [Term tyname name uni fun a] -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
([Term tyname name uni fun a] -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Writer (FloatTable tyname name uni fun a) term
go term
Term tyname name uni fun a
arg WriterT
(FloatTable tyname name uni fun a)
Identity
([Term tyname name uni fun a] -> Term tyname name uni fun a)
-> WriterT
(FloatTable tyname name uni fun a)
Identity
[Term tyname name uni fun a]
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a b.
WriterT (FloatTable tyname name uni fun a) Identity (a -> b)
-> WriterT (FloatTable tyname name uni fun a) Identity a
-> WriterT (FloatTable tyname name uni fun a) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (term
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a))
-> [term]
-> WriterT
(FloatTable tyname name uni fun a)
Identity
[Term tyname name uni fun a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse term -> Writer (FloatTable tyname name uni fun a) term
term
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
go [term]
[Term tyname name uni fun a]
cs
t :: Term tyname name uni fun a
t@Var{} -> Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a.
a -> WriterT (FloatTable tyname name uni fun a) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
t :: Term tyname name uni fun a
t@Constant{} -> Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a.
a -> WriterT (FloatTable tyname name uni fun a) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
t :: Term tyname name uni fun a
t@Builtin{} -> Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a.
a -> WriterT (FloatTable tyname name uni fun a) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
t :: Term tyname name uni fun a
t@Error{} -> Term tyname name uni fun a
-> WriterT
(FloatTable tyname name uni fun a)
Identity
(Term tyname name uni fun a)
forall a.
a -> WriterT (FloatTable tyname name uni fun a) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
floatBackLets :: forall tyname name uni fun a term m.
( term~Term tyname name uni fun a
, m~Reader Depth
, PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique, Semigroup a)
=> term
-> FloatTable tyname name uni fun a
-> term
floatBackLets :: forall tyname name (uni :: * -> *) fun a term (m :: * -> *).
(term ~ Term tyname name uni fun a, m ~ Reader Depth,
HasUnique tyname TypeUnique, HasUnique name TermUnique,
Semigroup a) =>
term -> FloatTable tyname name uni fun a -> term
floatBackLets term
term FloatTable tyname name uni fun a
fTable =
(m term -> Depth -> term) -> Depth -> m term -> term
forall a b c. (a -> b -> c) -> b -> a -> c
flip m term -> Depth -> term
Reader Depth term -> Depth -> term
forall r a. Reader r a -> r -> a
runReader Depth
topDepth (m term -> term) -> m term -> term
forall a b. (a -> b) -> a -> b
$ term -> m term
goTop term
term
where
goTop, go :: term -> m term
goTop :: term -> m term
goTop = Unique -> term -> m term
floatLam Unique
topUnique (term -> m term) -> (term -> m term) -> term -> m term
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< term -> m term
go
go :: term -> m term
go = \case
LamAbs a
a name
n Type tyname uni a
ty Term tyname name uni fun a
tBody -> (Depth -> Depth) -> m term -> m term
forall a. (Depth -> Depth) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+Depth
1) (m term -> m term) -> m term -> m term
forall a b. (a -> b) -> a -> b
$
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 name
n Type tyname uni a
ty (Term tyname name uni fun a -> term)
-> m (Term tyname name uni fun a) -> m term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Unique -> term -> m term
floatLam (name
nname -> 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) (term -> m (Term tyname name uni fun a))
-> m term -> m (Term tyname name uni fun a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< term -> m term
go term
Term tyname name uni fun a
tBody)
TyAbs a
a tyname
n Kind a
k Term tyname name uni fun a
tBody -> (Depth -> Depth) -> m term -> m term
forall a. (Depth -> Depth) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+Depth
1) (m term -> m term) -> m term -> m term
forall a b. (a -> b) -> a -> b
$
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs a
a tyname
n Kind a
k (Term tyname name uni fun a -> term)
-> m (Term tyname name uni fun a) -> m term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Unique -> term -> m term
floatLam (tyname
ntyname -> 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) (term -> m (Term tyname name uni fun a))
-> m term -> m (Term tyname name uni fun a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< term -> m term
go term
Term tyname name uni fun a
tBody)
Let a
a Recursivity
r bs :: NonEmpty (Binding tyname name uni fun a)
bs@(NonEmpty (Binding tyname name uni fun a) -> Unique
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a) -> Unique
representativeBindingUnique -> Unique
letU) Term tyname name uni fun a
tIn -> (Depth -> Depth) -> m term -> m term
forall a. (Depth -> Depth) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+Depth
1) (m term -> m term) -> m term -> m term
forall a b. (a -> b) -> a -> b
$ do
BindingGrp tyname name uni fun a
unfloatableGrp <- a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> BindingGrp tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> BindingGrp tyname name uni fun a
BindingGrp a
a Recursivity
r (NonEmpty (Binding tyname name uni fun a)
-> BindingGrp tyname name uni fun a)
-> m (NonEmpty (Binding tyname name uni fun a))
-> m (BindingGrp tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LensLike
m
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Term tyname name uni fun a)
(Term tyname name uni fun a)
-> LensLike
m
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Term tyname name uni fun a)
(Term tyname name uni fun a)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf ((Binding tyname name uni fun a
-> m (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> m (NonEmpty (Binding tyname name uni fun a))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Binding tyname name uni fun a)
(Binding tyname name uni fun a)
traversed((Binding tyname name uni fun a
-> m (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> m (NonEmpty (Binding tyname name uni fun a)))
-> ((Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> m (Binding tyname name uni fun a))
-> LensLike
m
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Term tyname name uni fun a)
(Term tyname name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> m (Binding tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms) term -> m term
Term tyname name uni fun a -> m (Term tyname name uni fun a)
go NonEmpty (Binding tyname name uni fun a)
bs
Recursivity
-> BindingGrp tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Recursivity
-> BindingGrp tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
bindingGrpToLet Recursivity
NonRec
(BindingGrp tyname name uni fun a
-> Term tyname name uni fun a -> term)
-> m (BindingGrp tyname name uni fun a)
-> m (Term tyname name uni fun a -> term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Unique
-> BindingGrp tyname name uni fun a
-> m (BindingGrp tyname name uni fun a)
forall grp.
(grp ~ BindingGrp tyname name uni fun a) =>
Unique -> grp -> m grp
floatRhs Unique
letU BindingGrp tyname name uni fun a
unfloatableGrp
m (Term tyname name uni fun a -> term)
-> m (Term tyname name uni fun a) -> m term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Unique -> term -> m term
floatLam Unique
letU (term -> m (Term tyname name uni fun a))
-> m term -> m (Term tyname name uni fun a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< term -> m term
go term
Term tyname name uni fun a
tIn)
term
t -> term
t term -> (term -> m term) -> m term
forall a b. a -> (a -> b) -> b
& (Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> Term tyname name uni fun a -> m (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms term -> m term
Term tyname name uni fun a -> m (Term tyname name uni fun a)
go
floatLam :: PLC.Unique -> term -> m term
floatLam :: Unique -> term -> m term
floatLam Unique
lamU term
t = do
Pos
herePos <- (Depth -> Pos) -> m Pos
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Depth -> Pos) -> m Pos) -> (Depth -> Pos) -> m Pos
forall a b. (a -> b) -> a -> b
$ \Depth
d -> Depth -> Unique -> PosType -> Pos
Pos Depth
d Unique
lamU PosType
LamBody
Pos
-> (BindingGrp tyname name uni fun a -> term -> term)
-> term
-> m term
forall c.
Pos -> (BindingGrp tyname name uni fun a -> c -> c) -> c -> m c
floatAt Pos
herePos (Recursivity
-> BindingGrp tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Recursivity
-> BindingGrp tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
bindingGrpToLet Recursivity
Rec) term
t
floatRhs :: (grp ~ BindingGrp tyname name uni fun a)
=> PLC.Unique
-> grp
-> m grp
floatRhs :: forall grp.
(grp ~ BindingGrp tyname name uni fun a) =>
Unique -> grp -> m grp
floatRhs Unique
letU grp
bs = do
Pos
herePos <- (Depth -> Pos) -> m Pos
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Depth -> Pos) -> m Pos) -> (Depth -> Pos) -> m Pos
forall a b. (a -> b) -> a -> b
$ \Depth
d -> Depth -> Unique -> PosType -> Pos
Pos Depth
d Unique
letU PosType
LetRhs
Pos
-> (BindingGrp tyname name uni fun a -> grp -> grp) -> grp -> m grp
forall c.
Pos -> (BindingGrp tyname name uni fun a -> c -> c) -> c -> m c
floatAt Pos
herePos BindingGrp tyname name uni fun a -> grp -> grp
BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
-> BindingGrp tyname name uni fun a
forall a. Semigroup a => a -> a -> a
(<>) grp
bs
floatAt :: Pos
-> (BindingGrp tyname name uni fun a -> c -> c)
-> c
-> m c
floatAt :: forall c.
Pos -> (BindingGrp tyname name uni fun a -> c -> c) -> c -> m c
floatAt Pos
herePos BindingGrp tyname name uni fun a -> c -> c
placeIntoFn c
termOrBindings = do
case Pos
-> FloatTable tyname name uni fun a
-> Maybe (NonEmpty (BindingGrp tyname name uni fun a))
forall k a. Ord k => k -> MonoidalMap k a -> Maybe a
MM.lookup Pos
herePos FloatTable tyname name uni fun a
fTable of
Maybe (NonEmpty (BindingGrp tyname name uni fun a))
Nothing -> c -> m c
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
termOrBindings
Just NonEmpty (BindingGrp tyname name uni fun a)
floatableGrps -> do
NonEmpty (BindingGrp tyname name uni fun a)
floatableGrps' <- NonEmpty (BindingGrp tyname name uni fun a)
floatableGrps NonEmpty (BindingGrp tyname name uni fun a)
-> (NonEmpty (BindingGrp tyname name uni fun a)
-> m (NonEmpty (BindingGrp tyname name uni fun a)))
-> m (NonEmpty (BindingGrp tyname name uni fun a))
forall a b. a -> (a -> b) -> b
& ((BindingGrp tyname name uni fun a
-> m (BindingGrp tyname name uni fun a))
-> NonEmpty (BindingGrp tyname name uni fun a)
-> m (NonEmpty (BindingGrp tyname name uni fun a))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (BindingGrp tyname name uni fun a))
(NonEmpty (BindingGrp tyname name uni fun a))
(BindingGrp tyname name uni fun a)
(BindingGrp tyname name uni fun a)
traversed((BindingGrp tyname name uni fun a
-> m (BindingGrp tyname name uni fun a))
-> NonEmpty (BindingGrp tyname name uni fun a)
-> m (NonEmpty (BindingGrp tyname name uni fun a)))
-> ((Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> BindingGrp tyname name uni fun a
-> m (BindingGrp tyname name uni fun a))
-> (Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> NonEmpty (BindingGrp tyname name uni fun a)
-> m (NonEmpty (BindingGrp tyname name uni fun a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(NonEmpty (Binding tyname name uni fun a)
-> ReaderT
Depth Identity (NonEmpty (Binding tyname name uni fun a)))
-> BindingGrp tyname name uni fun a
-> m (BindingGrp tyname name uni fun a)
(NonEmpty (Binding tyname name uni fun a)
-> ReaderT
Depth Identity (NonEmpty (Binding tyname name uni fun a)))
-> BindingGrp tyname name uni fun a
-> ReaderT Depth Identity (BindingGrp tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a tyname name
(uni :: * -> *) fun (f :: * -> *).
Functor f =>
(NonEmpty (Binding tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a)))
-> BindingGrp tyname name uni fun a
-> f (BindingGrp tyname name uni fun a)
bgBindings((NonEmpty (Binding tyname name uni fun a)
-> ReaderT
Depth Identity (NonEmpty (Binding tyname name uni fun a)))
-> BindingGrp tyname name uni fun a
-> m (BindingGrp tyname name uni fun a))
-> ((Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> ReaderT
Depth Identity (NonEmpty (Binding tyname name uni fun a)))
-> (Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> BindingGrp tyname name uni fun a
-> m (BindingGrp tyname name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Binding tyname name uni fun a
-> ReaderT Depth Identity (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> ReaderT
Depth Identity (NonEmpty (Binding tyname name uni fun a))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (Binding tyname name uni fun a))
(NonEmpty (Binding tyname name uni fun a))
(Binding tyname name uni fun a)
(Binding tyname name uni fun a)
traversed((Binding tyname name uni fun a
-> ReaderT Depth Identity (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> ReaderT
Depth Identity (NonEmpty (Binding tyname name uni fun a)))
-> ((Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> ReaderT Depth Identity (Binding tyname name uni fun a))
-> (Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> ReaderT
Depth Identity (NonEmpty (Binding tyname name uni fun a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> m (Binding tyname name uni fun a)
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> ReaderT Depth Identity (Binding tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms) term -> m term
Term tyname name uni fun a -> m (Term tyname name uni fun a)
go
c -> m c
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> m c) -> c -> m c
forall a b. (a -> b) -> a -> b
$ NonEmpty (BindingGrp tyname name uni fun a)
-> BindingGrp tyname name uni fun a
forall m. Semigroup m => NonEmpty m -> m
forall (t :: * -> *) m. (Foldable1 t, Semigroup m) => t m -> m
fold1 NonEmpty (BindingGrp tyname name uni fun a)
floatableGrps' BindingGrp tyname name uni fun a -> c -> c
`placeIntoFn` c
termOrBindings
floatTermPassSC ::
forall m uni fun a.
( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
, Semigroup a, PLC.MonadQuote m
) =>
TC.PirTCConfig uni fun ->
BuiltinsInfo uni fun ->
Pass m TyName Name uni fun a
floatTermPassSC :: forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, Ord a, Semigroup a,
MonadQuote m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Pass m TyName Name uni fun a
floatTermPassSC PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo =
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 -> Pass m TyName Name uni fun a
forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, Ord a, Semigroup a,
Applicative m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Pass m TyName Name uni fun a
floatTermPass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo
floatTermPass ::
forall m uni fun a.
( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
, Semigroup a, Applicative m
) =>
TC.PirTCConfig uni fun ->
BuiltinsInfo uni fun ->
Pass m TyName Name uni fun a
floatTermPass :: forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, Ord a, Semigroup a,
Applicative m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Pass m TyName Name uni fun a
floatTermPass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo =
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-out" (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
-> Term TyName Name uni fun a -> Term TyName Name uni fun a
forall (uni :: * -> *) fun tyname name a.
(ToBuiltinMeaning uni fun, HasUnique tyname TypeUnique,
HasUnique name TermUnique, Semigroup a) =>
BuiltinsInfo uni fun
-> Term tyname name uni fun a -> Term tyname name uni fun a
floatTerm BuiltinsInfo uni fun
binfo)
[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 ::
(PLC.ToBuiltinMeaning uni fun,
PLC.HasUnique tyname PLC.TypeUnique,
PLC.HasUnique name PLC.TermUnique,
Semigroup a
)
=> BuiltinsInfo uni fun -> Term tyname name uni fun a -> Term tyname name uni fun a
floatTerm :: forall (uni :: * -> *) fun tyname name a.
(ToBuiltinMeaning uni fun, HasUnique tyname TypeUnique,
HasUnique name TermUnique, Semigroup a) =>
BuiltinsInfo uni fun
-> Term tyname name uni fun a -> Term tyname name uni fun a
floatTerm BuiltinsInfo uni fun
binfo Term tyname name uni fun a
t =
BuiltinsInfo uni fun -> Term tyname name uni fun a -> Scope
forall tyname name (uni :: * -> *) fun a.
(HasUnique tyname TypeUnique, HasUnique name TermUnique,
ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun -> Term tyname name uni fun a -> Scope
mark BuiltinsInfo uni fun
binfo Term tyname name uni fun a
t
Scope
-> (Scope
-> (Term tyname name uni fun a, FloatTable tyname name uni fun a))
-> (Term tyname name uni fun a, FloatTable tyname name uni fun a)
forall a b. a -> (a -> b) -> b
& (Scope
-> Term tyname name uni fun a
-> (Term tyname name uni fun a, FloatTable tyname name uni fun a))
-> Term tyname name uni fun a
-> Scope
-> (Term tyname name uni fun a, FloatTable tyname name uni fun a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Scope
-> Term tyname name uni fun a
-> (Term tyname name uni fun a, FloatTable tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a term.
(term ~ Term tyname name uni fun a, HasUnique tyname TypeUnique,
HasUnique name TermUnique) =>
Scope -> term -> (term, FloatTable tyname name uni fun a)
removeLets Term tyname name uni fun a
t
(Term tyname name uni fun a, FloatTable tyname name uni fun a)
-> ((Term tyname name uni fun a, FloatTable tyname name uni fun a)
-> Term tyname name uni fun a)
-> Term tyname name uni fun a
forall a b. a -> (a -> b) -> b
& (Term tyname name uni fun a
-> FloatTable tyname name uni fun a -> Term tyname name uni fun a)
-> (Term tyname name uni fun a, FloatTable tyname name uni fun a)
-> Term tyname name uni fun a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Term tyname name uni fun a
-> FloatTable tyname name uni fun a -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a term (m :: * -> *).
(term ~ Term tyname name uni fun a, m ~ Reader Depth,
HasUnique tyname TypeUnique, HasUnique name TermUnique,
Semigroup a) =>
term -> FloatTable tyname name uni fun a -> term
floatBackLets
maxPos :: PLC.UniqueMap k Pos -> Pos
maxPos :: forall k. UniqueMap k Pos -> Pos
maxPos = (Pos -> Pos -> Pos) -> Pos -> UniqueMap k Pos -> Pos
forall a b. (a -> b -> b) -> b -> UniqueMap k a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Pos -> Pos -> Pos
forall a. Ord a => a -> a -> a
max Pos
topPos
withDepth :: (r ~ MarkCtx tyname name uni fun a2, MonadReader r m)
=> (Depth -> Depth) -> m a -> m a
withDepth :: forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m) =>
(Depth -> Depth) -> m a -> m a
withDepth = (MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall a.
(MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a)
-> ((Depth -> Depth)
-> MarkCtx tyname name uni fun a2
-> MarkCtx tyname name uni fun a2)
-> (Depth -> Depth)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
(MarkCtx tyname name uni fun a2)
(MarkCtx tyname name uni fun a2)
Depth
Depth
-> (Depth -> Depth)
-> MarkCtx tyname name uni fun a2
-> MarkCtx tyname name uni fun a2
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(MarkCtx tyname name uni fun a2)
(MarkCtx tyname name uni fun a2)
Depth
Depth
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Depth -> f Depth)
-> MarkCtx tyname name uni fun a
-> f (MarkCtx tyname name uni fun a)
markCtxDepth
withLam :: (r ~ MarkCtx tyname name uni fun a2, MonadReader r m, PLC.HasUnique name unique)
=> name
-> m a -> m a
withLam :: forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) unique a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique name unique) =>
name -> m a -> m a
withLam (Getting Unique name Unique -> name -> Unique
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Unique name Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique -> Unique
u) = (MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall a.
(MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a)
-> (MarkCtx tyname name uni fun a2
-> MarkCtx tyname name uni fun a2)
-> m a
-> m a
forall a b. (a -> b) -> a -> b
$ \ (MarkCtx Depth
d Scope
scope BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a2
vinfo) ->
let d' :: Depth
d' = Depth
dDepth -> Depth -> Depth
forall a. Num a => a -> a -> a
+Depth
1
pos' :: Pos
pos' = Depth -> Unique -> PosType -> Pos
Pos Depth
d' Unique
u PosType
LamBody
in Depth
-> Scope
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a2
-> MarkCtx tyname name uni fun a2
forall tyname name (uni :: * -> *) fun a.
Depth
-> Scope
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> MarkCtx tyname name uni fun a
MarkCtx Depth
d' (Unique -> Pos -> Scope -> Scope
forall unique a.
Coercible unique Unique =>
unique -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByUnique Unique
u Pos
pos' Scope
scope) BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a2
vinfo
withAbs :: (r ~ MarkCtx tyname name uni fun a2, MonadReader r m, PLC.HasUnique tyname unique)
=> tyname
-> m a -> m a
withAbs :: forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) unique a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique tyname unique) =>
tyname -> m a -> m a
withAbs (Getting Unique tyname Unique -> tyname -> Unique
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Unique tyname Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' tyname Unique
PLC.theUnique -> Unique
u) = (MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall a.
(MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a)
-> (MarkCtx tyname name uni fun a2
-> MarkCtx tyname name uni fun a2)
-> m a
-> m a
forall a b. (a -> b) -> a -> b
$ \ (MarkCtx Depth
d Scope
scope BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a2
vinfo) ->
let d' :: Depth
d' = Depth
dDepth -> Depth -> Depth
forall a. Num a => a -> a -> a
+Depth
1
pos' :: Pos
pos' = Depth -> Unique -> PosType -> Pos
Pos Depth
d' Unique
u PosType
LamBody
in Depth
-> Scope
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a2
-> MarkCtx tyname name uni fun a2
forall tyname name (uni :: * -> *) fun a.
Depth
-> Scope
-> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> MarkCtx tyname name uni fun a
MarkCtx Depth
d' (Unique -> Pos -> Scope -> Scope
forall unique a.
Coercible unique Unique =>
unique -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByUnique Unique
u Pos
pos' Scope
scope) BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a2
vinfo
withBs :: (r ~ MarkCtx tyname name uni fun a2, MonadReader r m, PLC.HasUnique name PLC.TermUnique, PLC.HasUnique tyname PLC.TypeUnique)
=> NE.NonEmpty (Binding tyname name uni fun a3)
-> Pos
-> m a -> m a
withBs :: forall r tyname name (uni :: * -> *) fun a2 (m :: * -> *) a3 a.
(r ~ MarkCtx tyname name uni fun a2, MonadReader r m,
HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
NonEmpty (Binding tyname name uni fun a3) -> Pos -> m a -> m a
withBs NonEmpty (Binding tyname name uni fun a3)
bs Pos
pos = (MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall a.
(MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((MarkCtx tyname name uni fun a2 -> MarkCtx tyname name uni fun a2)
-> m a -> m a)
-> ((Scope -> Scope)
-> MarkCtx tyname name uni fun a2
-> MarkCtx tyname name uni fun a2)
-> (Scope -> Scope)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
(MarkCtx tyname name uni fun a2)
(MarkCtx tyname name uni fun a2)
Scope
Scope
-> (Scope -> Scope)
-> MarkCtx tyname name uni fun a2
-> MarkCtx tyname name uni fun a2
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(MarkCtx tyname name uni fun a2)
(MarkCtx tyname name uni fun a2)
Scope
Scope
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(Scope -> f Scope)
-> MarkCtx tyname name uni fun a
-> f (MarkCtx tyname name uni fun a)
markCtxScope ((Scope -> Scope) -> m a -> m a) -> (Scope -> Scope) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \Scope
scope ->
[(Unique, Pos)] -> Scope
forall (f :: * -> *) unique a.
(Foldable f, Coercible Unique unique) =>
f (unique, a) -> UniqueMap unique a
UMap.fromUniques [(Unique
bid, Pos
pos) | Unique
bid <- NonEmpty (Binding tyname name uni fun a3)
bsNonEmpty (Binding tyname name uni fun a3)
-> Getting
(Endo [Unique]) (NonEmpty (Binding tyname name uni fun a3)) Unique
-> [Unique]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^..(Binding tyname name uni fun a3
-> Const (Endo [Unique]) (Binding tyname name uni fun a3))
-> NonEmpty (Binding tyname name uni fun a3)
-> Const
(Endo [Unique]) (NonEmpty (Binding tyname name uni fun a3))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
(NonEmpty (Binding tyname name uni fun a3))
(NonEmpty (Binding tyname name uni fun a3))
(Binding tyname name uni fun a3)
(Binding tyname name uni fun a3)
traversed((Binding tyname name uni fun a3
-> Const (Endo [Unique]) (Binding tyname name uni fun a3))
-> NonEmpty (Binding tyname name uni fun a3)
-> Const
(Endo [Unique]) (NonEmpty (Binding tyname name uni fun a3)))
-> ((Unique -> Const (Endo [Unique]) Unique)
-> Binding tyname name uni fun a3
-> Const (Endo [Unique]) (Binding tyname name uni fun a3))
-> Getting
(Endo [Unique]) (NonEmpty (Binding tyname name uni fun a3)) Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Unique -> Const (Endo [Unique]) Unique)
-> Binding tyname name uni fun a3
-> Const (Endo [Unique]) (Binding tyname name uni fun a3)
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 a3) Unique
bindingIds] Scope -> Scope -> Scope
forall a. Semigroup a => a -> a -> a
<> Scope
scope
ifRec :: Recursivity -> (a -> a) -> a -> a
ifRec :: forall a. Recursivity -> (a -> a) -> a -> a
ifRec Recursivity
r a -> a
f a
a = case Recursivity
r of
Recursivity
Rec -> a -> a
f a
a
Recursivity
NonRec -> a
a
floatable
:: (MonadReader (MarkCtx tyname name uni fun a) m, PLC.ToBuiltinMeaning uni fun, PLC.HasUnique name PLC.TermUnique)
=> BindingGrp tyname name uni fun a
-> m Bool
floatable :: forall tyname name (uni :: * -> *) fun a (m :: * -> *).
(MonadReader (MarkCtx tyname name uni fun a) m,
ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BindingGrp tyname name uni fun a -> m Bool
floatable (BindingGrp a
_ Recursivity
_ NonEmpty (Binding tyname name uni fun a)
bs) = do
BuiltinsInfo uni fun
binfo <- Getting
(BuiltinsInfo uni fun)
(MarkCtx tyname name uni fun a)
(BuiltinsInfo uni fun)
-> m (BuiltinsInfo uni fun)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(BuiltinsInfo uni fun)
(MarkCtx tyname name uni fun a)
(BuiltinsInfo uni fun)
forall tyname name (uni :: * -> *) fun a fun (f :: * -> *).
Functor f =>
(BuiltinsInfo uni fun -> f (BuiltinsInfo uni fun))
-> MarkCtx tyname name uni fun a
-> f (MarkCtx tyname name uni fun a)
markBuiltinsInfo
VarsInfo tyname name uni a
vinfo <- Getting
(VarsInfo tyname name uni a)
(MarkCtx tyname name uni fun a)
(VarsInfo tyname name uni a)
-> m (VarsInfo tyname name uni a)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(VarsInfo tyname name uni a)
(MarkCtx tyname name uni fun a)
(VarsInfo tyname name uni a)
forall tyname name (uni :: * -> *) fun a tyname name a
(f :: * -> *).
Functor f =>
(VarsInfo tyname name uni a -> f (VarsInfo tyname name uni a))
-> MarkCtx tyname name uni fun a
-> f (MarkCtx tyname name uni fun a)
markVarsInfo
Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ (Binding tyname name uni fun a -> Bool)
-> NonEmpty (Binding tyname name uni fun a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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
hasNoEffects BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo) NonEmpty (Binding tyname name uni fun a)
bs
Bool -> Bool -> Bool
&&
(Binding tyname name uni fun a -> Bool)
-> NonEmpty (Binding tyname name uni fun a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
none Binding tyname name uni fun a -> Bool
forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun a -> Bool
isTypeBind NonEmpty (Binding tyname name uni fun a)
bs
hasNoEffects
:: (PLC.ToBuiltinMeaning uni fun, PLC.HasUnique name PLC.TermUnique)
=> BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Binding tyname name uni fun a -> Bool
hasNoEffects :: 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
hasNoEffects BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo = \case
TypeBind{} -> Bool
True
DatatypeBind{} -> Bool
True
TermBind a
_ Strictness
NonStrict VarDecl tyname name uni a
_ Term tyname name uni fun a
_ -> Bool
True
TermBind a
_ Strictness
Strict VarDecl tyname name uni a
_ Term tyname name uni fun a
t -> 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
isPure BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t
isTypeBind :: Binding tyname name uni fun a -> Bool
isTypeBind :: forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun a -> Bool
isTypeBind = \case TypeBind{} -> Bool
True; Binding tyname name uni fun a
_ -> Bool
False
breakNonRec :: Term tyname name uni fun a -> Term tyname name uni fun a
breakNonRec :: forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
breakNonRec = \case
Let a
a Recursivity
NonRec (NonEmpty (Binding tyname name uni fun a)
-> (Binding tyname name uni fun a,
Maybe (NonEmpty (Binding tyname name uni fun a)))
forall a. NonEmpty a -> (a, Maybe (NonEmpty a))
NE.uncons -> (Binding tyname name uni fun a
b, Just NonEmpty (Binding tyname name uni fun a)
bs)) Term tyname name uni fun a
tIn ->
(a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 Recursivity
NonRec (Binding tyname name uni fun a
-> NonEmpty (Binding tyname name uni fun a)
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun a
b) (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a -> Term tyname name uni fun a
forall a b. (a -> b) -> a -> b
$ a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 Recursivity
NonRec NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
tIn)
Term tyname name uni fun a
t -> Term tyname name uni fun a
t