{-# LANGUAGE GADTs           #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators   #-}
module PlutusIR.Transform.RewriteRules.Common
    ( seqA
    , seqP
    , mkFreshTermLet -- from MkPlc
    , pattern A
    , pattern B
    , pattern I
    ) where

import PlutusCore.Builtin
import PlutusCore.Quote
import PlutusIR
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo
import PlutusIR.MkPir
import PlutusIR.Purity

{- | A wrapper that can be more easily turned into an infix operator.

e.g. `infixr 5 (***) = seqA binfo vInfo`
-}
seqA :: (MonadQuote m, Monoid a, ToBuiltinMeaning uni fun)
     => BuiltinsInfo uni fun
     -> VarsInfo tyname Name uni a
     -> (Type tyname uni a, Term tyname Name uni fun a)
     ->  m (Term tyname Name uni fun a)
     -> m (Term tyname Name uni fun a)
seqA :: forall (m :: * -> *) a (uni :: * -> *) fun tyname.
(MonadQuote m, Monoid a, ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> (Type tyname uni a, Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
seqA BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo (Type tyname uni a
a,Term tyname Name uni fun a
aT) m (Term tyname Name uni fun a)
y = BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Type tyname uni a
-> Term tyname Name uni fun a
-> m (Term tyname Name uni fun a -> Term tyname Name uni fun a)
forall (m :: * -> *) a (uni :: * -> *) fun t tyname.
(MonadQuote m, Monoid a, ToBuiltinMeaning uni fun,
 t ~ Term tyname Name uni fun a) =>
BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Type tyname uni a
-> t
-> m (t -> t)
seqOpt BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo Type tyname uni a
a Term tyname Name uni fun a
aT m (Term tyname Name uni fun a -> Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a) -> m (Term tyname Name uni fun a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Term tyname Name uni fun a)
y


{- | Another "infix" wrapper where second operand is a Haskell pure value.

e.g. `infixr 5 (***) = seqP binfo vInfo`
-}
seqP :: (MonadQuote m, Monoid a, ToBuiltinMeaning uni fun)
     => BuiltinsInfo uni fun
     -> VarsInfo tyname Name uni a
     -> (Type tyname uni a, Term tyname Name uni fun a)
     -> Term tyname Name uni fun a
     -> m (Term tyname Name uni fun a)
seqP :: forall (m :: * -> *) a (uni :: * -> *) fun tyname.
(MonadQuote m, Monoid a, ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> (Type tyname uni a, Term tyname Name uni fun a)
-> Term tyname Name uni fun a
-> m (Term tyname Name uni fun a)
seqP BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo (Type tyname uni a, Term tyname Name uni fun a)
p Term tyname Name uni fun a
y = BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> (Type tyname uni a, Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
forall (m :: * -> *) a (uni :: * -> *) fun tyname.
(MonadQuote m, Monoid a, ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> (Type tyname uni a, Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
seqA BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo (Type tyname uni a, Term tyname Name uni fun a)
p (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
y)

-- | An optimized version to omit call to `seq` if left operand `isPure`.
seqOpt :: ( MonadQuote m
       , Monoid a
       , ToBuiltinMeaning uni fun
       , t ~ Term tyname Name uni fun a
       )
     => BuiltinsInfo uni fun
     -> VarsInfo tyname Name uni a
     -> Type tyname uni a -- ^ the type of left operand a
     -> t -- ^ left operand a
     -> m (t -> t) -- ^ how to modify right operand b
seqOpt :: forall (m :: * -> *) a (uni :: * -> *) fun t tyname.
(MonadQuote m, Monoid a, ToBuiltinMeaning uni fun,
 t ~ Term tyname Name uni fun a) =>
BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Type tyname uni a
-> t
-> m (t -> t)
seqOpt BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo Type tyname uni a
aT t
a | 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 t
Term tyname Name uni fun a
a = (t -> t) -> m (t -> t)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t -> t
forall a. a -> a
id
                        | Bool
otherwise = Type tyname uni a -> t -> m (t -> t)
forall (m :: * -> *) a t tyname (uni :: * -> *) fun.
(MonadQuote m, Monoid a, t ~ Term tyname Name uni fun a) =>
Type tyname uni a -> t -> m (t -> t)
seqUnOpt Type tyname uni a
aT t
a

{- | Takes as input a term `a` with its type `aT`,
and constructs a function that expects another term `b`.
When the returned function is applied to a term, the execution of the applied term
would strictly evaluate the first term `a` only for its effects (i.e. ignoring its result)
while returning the result of the second term `b`.

The name is intentionally taken from Haskell's `GHC.Prim.seq`.
Currently, the need for this `seq` "combinator" is in `RewriteRules`,
to trying to retain the effects, that would otherwise be lost if that code was instead considered
completely dead.

Unfortunately, unlike Haskell's `seq`, we need the pass the correct `Type` of `a`,
so as to apply this `seq` combinator. This is usually not a problem because we are generating
code and we should have the type of `a` somewhere available.
-}
seqUnOpt :: (MonadQuote m, Monoid a, t ~ Term tyname Name uni fun a)
    => Type tyname uni a -- ^ the type of left operand a
    -> t  -- ^ left operand a
    -> m (t -> t) -- ^ how to modify right operand b
seqUnOpt :: forall (m :: * -> *) a t tyname (uni :: * -> *) fun.
(MonadQuote m, Monoid a, t ~ Term tyname Name uni fun a) =>
Type tyname uni a -> t -> m (t -> t)
seqUnOpt Type tyname uni a
aT t
a = (Term tyname Name uni fun a, t -> t) -> t -> t
forall a b. (a, b) -> b
snd ((Term tyname Name uni fun a, t -> t) -> t -> t)
-> m (Term tyname Name uni fun a, t -> t) -> m (t -> t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a
-> 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)
forall (m :: * -> *) (t :: * -> *) tyname (uni :: * -> *) fun a.
(MonadQuote m, TermLike t tyname Name uni fun, Monoid a) =>
Type tyname uni a -> t a -> m (t a, t a -> t a)
mkFreshTermLet Type tyname uni a
aT t
Term tyname Name uni fun a
a

-- Some shorthands for easier pattern-matching when creating rewrite rules
-- TODO: these patterns ignores annotations. Find a better way for easier writing rules that does
-- not ignore annotations e.g. (pattern-PIR-quasiquoters?)
pattern A :: Term tyname name uni fun a -> Term tyname name uni fun a -> Term tyname name uni fun a
pattern $mA :: forall {r} {tyname} {name} {uni :: * -> *} {fun} {a}.
Term tyname name uni fun a
-> (Term tyname name uni fun a -> Term tyname name uni fun a -> r)
-> ((# #) -> r)
-> r
A l r <- Apply _ l r
pattern B :: fun -> Term tyname name uni fun a
pattern $mB :: forall {r} {fun} {tyname} {name} {uni :: * -> *} {a}.
Term tyname name uni fun a -> (fun -> r) -> ((# #) -> r) -> r
B b <- Builtin _ b
pattern I :: Term tyname name uni fun a -> Type tyname uni a -> Term tyname name uni fun a
pattern $mI :: forall {r} {tyname} {name} {uni :: * -> *} {fun} {a}.
Term tyname name uni fun a
-> (Term tyname name uni fun a -> Type tyname uni a -> r)
-> ((# #) -> r)
-> r
I e t <- TyInst _ e t