-- editorconfig-checker-disable-file
{-# LANGUAGE GADTs         #-}
{-# LANGUAGE TypeOperators #-}
module PlutusIR.Transform.RewriteRules.UnConstrConstrData
    ( unConstrConstrData
    ) where

import PlutusCore.Default
import PlutusCore.Quote
import PlutusIR
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo
import PlutusIR.Transform.RewriteRules.Common

{- | This rule rewrites terms of form `BUILTIN(unConstrData(constrData(x,y)))`
, where builtin stands for `FstPair` or `SndPair`, to "x" or "y" respectively.

This rewrite-rule was originally meant to rewrite `unConstrData(constrData(x,y)) => (x,y)`,
however we do not have a (polymorphic or monomorphic) builtin constructor to create a `BuiltinPair`
"(x,y)". See Note [Representable built-in functions over polymorphic built-in types].

So we adapted the original rewrite rule to try to achieve a similar goal.
Unfortunately, the adapted rule is less applicable and will most likely never fire
(at least for PIR code generated by plutus-tx).
The reason is that the TH code in plutus-tx does not create such "tight" code, but uses
way more lets that get in the way preventing the rule from firing.

Possible solutions: Some more aggressive PIR inlining, rewriting the PlutusTx TH code, or
introducing specialised pattern-matching builtins as last resort.
Plutus Tx TH code responsible:
<https://github.com/IntersectMBO/plutus/blob/9364099b38e3aa27fb311af3299d2210e7e33e45/plutus-tx/src/PlutusTx/IsData/TH.hs#L174-L192>
-}
unConstrConstrData :: (MonadQuote m, t ~ Term tyname Name DefaultUni DefaultFun a, Monoid a)
                   => BuiltinsInfo DefaultUni DefaultFun
                   -> VarsInfo tyname Name DefaultUni a
                   -> t
                   -> m t
unConstrConstrData :: forall (m :: * -> *) t tyname a.
(MonadQuote m, t ~ Term tyname Name DefaultUni DefaultFun a,
 Monoid a) =>
BuiltinsInfo DefaultUni DefaultFun
-> VarsInfo tyname Name DefaultUni a -> t -> m t
unConstrConstrData BuiltinsInfo DefaultUni DefaultFun
binfo VarsInfo tyname Name DefaultUni a
vinfo t
t = case t
t of
    -- This rule might as well have been split into two separate rules, but kept as one
    -- so as to reuse most of the matching pattern.

    -- builtin({t1}, {t2}, unConstr(constrData(i, data)))
    (A (I (I (B DefaultFun
builtin) Type tyname DefaultUni a
tyFst) Type tyname DefaultUni a
tySnd)
     (A (B DefaultFun
UnConstrData) (A (A (B DefaultFun
ConstrData) Term tyname Name DefaultUni DefaultFun a
arg1) Term tyname Name DefaultUni DefaultFun a
arg2))) ->
        case DefaultFun
builtin of
            -- sndPair({t1}, {t2}, unConstr(constrData(i, data))) = i `seq` data
            DefaultFun
SndPair -> (Type tyname DefaultUni a
tyFst,Term tyname Name DefaultUni DefaultFun a
arg1) (Type tyname DefaultUni a,
 Term tyname Name DefaultUni DefaultFun a)
-> Term tyname Name DefaultUni DefaultFun a
-> m (Term tyname Name DefaultUni DefaultFun a)
`seQ` Term tyname Name DefaultUni DefaultFun a
arg2

            -- fstPair({t1}, {t2}, unConstr(constrData(i, data))) = let !gen = i in data `seq` gen
            DefaultFun
FstPair ->  do
                  (Term tyname Name DefaultUni DefaultFun a
genVar, Term tyname Name DefaultUni DefaultFun a
-> Term tyname Name DefaultUni DefaultFun a
genLetIn) <- Type tyname DefaultUni a
-> Term tyname Name DefaultUni DefaultFun a
-> m (Term tyname Name DefaultUni DefaultFun a,
      Term tyname Name DefaultUni DefaultFun a
      -> Term tyname Name DefaultUni DefaultFun 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 DefaultUni a
tyFst Term tyname Name DefaultUni DefaultFun a
arg1
                  Term tyname Name DefaultUni DefaultFun a -> t
Term tyname Name DefaultUni DefaultFun a
-> Term tyname Name DefaultUni DefaultFun a
genLetIn (Term tyname Name DefaultUni DefaultFun a -> t)
-> m (Term tyname Name DefaultUni DefaultFun a) -> m t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                      (Type tyname DefaultUni a
tySnd, Term tyname Name DefaultUni DefaultFun a
arg2) (Type tyname DefaultUni a,
 Term tyname Name DefaultUni DefaultFun a)
-> Term tyname Name DefaultUni DefaultFun a
-> m (Term tyname Name DefaultUni DefaultFun a)
`seQ` Term tyname Name DefaultUni DefaultFun a
genVar
            DefaultFun
_ -> t -> m t
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
t
    t
_ -> t -> m t
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
t

  where
      infixr 5 `seQ` -- 5 so it has more precedence than <$>
      seQ :: (Type tyname DefaultUni a,
 Term tyname Name DefaultUni DefaultFun a)
-> Term tyname Name DefaultUni DefaultFun a
-> m (Term tyname Name DefaultUni DefaultFun a)
seQ = BuiltinsInfo DefaultUni DefaultFun
-> VarsInfo tyname Name DefaultUni a
-> (Type tyname DefaultUni a,
    Term tyname Name DefaultUni DefaultFun a)
-> Term tyname Name DefaultUni DefaultFun a
-> m (Term tyname Name DefaultUni DefaultFun 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)
-> Term tyname Name uni fun a
-> m (Term tyname Name uni fun a)
seqP BuiltinsInfo DefaultUni DefaultFun
binfo VarsInfo tyname Name DefaultUni a
vinfo