{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}
module PlutusIR.Transform.Beta (
beta,
betaPass,
betaPassSC
) where
import Control.Lens (over)
import Data.List.NonEmpty qualified as NE
import PlutusCore qualified as PLC
import PlutusIR
import PlutusIR.Pass
import PlutusIR.TypeCheck qualified as TC
extractBindings ::
Term tyname name uni fun a
-> Maybe (NE.NonEmpty (Binding tyname name uni fun a), Term tyname name uni fun a)
= [Term tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding 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
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
collectArgs []
where
collectArgs :: [Term tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
collectArgs [Term tyname name uni fun a]
argStack (Apply a
_ Term tyname name uni fun a
f Term tyname name uni fun a
arg) = [Term tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
collectArgs (Term tyname name uni fun a
argTerm tyname name uni fun a
-> [Term tyname name uni fun a] -> [Term tyname name uni fun a]
forall a. a -> [a] -> [a]
:[Term tyname name uni fun a]
argStack) Term tyname name uni fun a
f
collectArgs [Term tyname name uni fun a]
argStack Term tyname name uni fun a
t = [Term tyname name uni fun a]
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
forall {tyname} {name} {uni :: * -> *} {fun} {a} {fun}.
[Term tyname name uni fun a]
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
matchArgs [Term tyname name uni fun a]
argStack [] Term tyname name uni fun a
t
matchArgs :: [Term tyname name uni fun a]
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
matchArgs (Term tyname name uni fun a
arg:[Term tyname name uni fun a]
rest) [Binding tyname name uni fun a]
acc (LamAbs a
a name
n Type tyname uni a
ty Term tyname name uni fun a
body) =
[Term tyname name uni fun a]
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
matchArgs [Term tyname name uni fun a]
rest (a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
a Strictness
Strict (a -> name -> Type tyname uni a -> VarDecl tyname name uni a
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl a
a name
n Type tyname uni a
ty) Term tyname name uni fun a
argBinding tyname name uni fun a
-> [Binding tyname name uni fun a]
-> [Binding tyname name uni fun a]
forall a. a -> [a] -> [a]
:[Binding tyname name uni fun a]
acc) Term tyname name uni fun a
body
matchArgs [] [Binding tyname name uni fun a]
acc Term tyname name uni fun a
t =
case [Binding tyname name uni fun a]
-> Maybe (NonEmpty (Binding tyname name uni fun a))
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty ([Binding tyname name uni fun a] -> [Binding tyname name uni fun a]
forall a. [a] -> [a]
reverse [Binding tyname name uni fun a]
acc) of
Maybe (NonEmpty (Binding tyname name uni fun a))
Nothing -> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
forall a. Maybe a
Nothing
Just NonEmpty (Binding tyname name uni fun a)
acc' -> (NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
forall a. a -> Maybe a
Just (NonEmpty (Binding tyname name uni fun a)
acc', Term tyname name uni fun a
t)
matchArgs (Term tyname name uni fun a
_:[Term tyname name uni fun a]
_) [Binding tyname name uni fun a]
_ Term tyname name uni fun a
_ = Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
forall a. Maybe a
Nothing
beta
:: Term tyname name uni fun a
-> Term tyname name uni fun a
beta :: forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
beta = ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (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 -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
beta (Term tyname name uni fun a -> Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
localTransform
where
localTransform :: Term tyname name uni fun a -> Term tyname name uni fun a
localTransform = \case
(Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a
-> Maybe
(NonEmpty (Binding tyname name uni fun a),
Term tyname name uni fun a)
extractBindings -> Just (NonEmpty (Binding tyname name uni fun a)
bs, Term tyname name uni fun a
t)) -> 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 (Term tyname name uni fun a -> a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> a
termAnn Term tyname name uni fun a
t) Recursivity
NonRec NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
t
TyInst a
_ (TyAbs a
a tyname
n Kind a
k Term tyname name uni fun a
body) Type tyname uni a
tyArg ->
let b :: Binding tyname name uni fun a
b = a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind a
a (a -> tyname -> Kind a -> TyVarDecl tyname a
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl a
a tyname
n Kind a
k) Type tyname uni a
tyArg
in 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 (Term tyname name uni fun a -> a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> a
termAnn Term tyname name uni fun a
body) 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
forall {name} {fun}. Binding tyname name uni fun a
b) Term tyname name uni fun a
body
Term tyname name uni fun a
t -> Term tyname name uni fun a
t
betaPassSC
:: (PLC.Typecheckable uni fun, PLC.GEq uni, PLC.MonadQuote m, Ord a)
=> TC.PirTCConfig uni fun
-> Pass m TyName Name uni fun a
betaPassSC :: forall (uni :: * -> *) fun (m :: * -> *) a.
(Typecheckable uni fun, GEq uni, MonadQuote m, Ord a) =>
PirTCConfig uni fun -> Pass m TyName Name uni fun a
betaPassSC PirTCConfig uni fun
tcconfig = 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 -> Pass m TyName Name uni fun a
forall (uni :: * -> *) fun (m :: * -> *) a.
(Typecheckable uni fun, GEq uni, Applicative m, Ord a) =>
PirTCConfig uni fun -> Pass m TyName Name uni fun a
betaPass PirTCConfig uni fun
tcconfig
betaPass
:: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m, Ord a)
=> TC.PirTCConfig uni fun
-> Pass m TyName Name uni fun a
betaPass :: forall (uni :: * -> *) fun (m :: * -> *) a.
(Typecheckable uni fun, GEq uni, Applicative m, Ord a) =>
PirTCConfig uni fun -> Pass m TyName Name uni fun a
betaPass PirTCConfig uni fun
tcconfig =
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
"beta" (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
. 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
beta)
[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)]