{-# LANGUAGE LambdaCase    #-}
{-# LANGUAGE TupleSections #-}

module PlutusIR.Transform.CaseReduce
    ( caseReduce
    , caseReducePass
    ) where

import PlutusCore.MkPlc
import PlutusIR.Core

import Control.Lens (transformOf, (^?))
import Data.List.Extras
import PlutusCore qualified as PLC
import PlutusIR.Pass
import PlutusIR.TypeCheck qualified as TC

caseReducePass
  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
  => TC.PirTCConfig uni fun
  -> Pass m TyName Name uni fun a
caseReducePass :: forall (uni :: * -> *) fun (m :: * -> *) a.
(Typecheckable uni fun, GEq uni, Applicative m) =>
PirTCConfig uni fun -> Pass m TyName Name uni fun a
caseReducePass PirTCConfig uni fun
tcconfig = String
-> PirTCConfig uni fun
-> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
-> Pass m TyName Name uni fun a
forall (uni :: * -> *) fun (m :: * -> *) a.
(Typecheckable uni fun, GEq uni, Applicative m) =>
String
-> PirTCConfig uni fun
-> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
-> Pass m TyName Name uni fun a
simplePass String
"case reduce" PirTCConfig uni fun
tcconfig 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
caseReduce

caseReduce :: Term tyname name uni fun a -> Term tyname name uni fun a
caseReduce :: forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
caseReduce = 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 a b. ASetter a b a b -> (b -> b) -> a -> b
transformOf 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
processTerm

processTerm :: Term tyname name uni fun a -> Term tyname name uni fun a
processTerm :: forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
processTerm = \case
    Case a
ann Type tyname uni a
_ (Constr a
_ Type tyname uni a
_ Word64
i [Term tyname name uni fun a]
args) [Term tyname name uni fun a]
cs | Just Term tyname name uni fun a
c <- [Term tyname name uni fun a]
cs [Term tyname name uni fun a]
-> Getting
     (First (Term tyname name uni fun a))
     [Term tyname name uni fun a]
     (Term tyname name uni fun a)
-> Maybe (Term tyname name uni fun a)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Word64
-> Traversal'
     [Term tyname name uni fun a] (Term tyname name uni fun a)
forall a. Word64 -> Traversal' [a] a
wix Word64
i -> Term tyname name uni fun a
-> [(a, Term tyname name uni fun a)] -> Term tyname name uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp Term tyname name uni fun a
c ((a
ann,) (Term tyname name uni fun a -> (a, Term tyname name uni fun a))
-> [Term tyname name uni fun a]
-> [(a, Term tyname name uni fun a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term tyname name uni fun a]
args)
    Term tyname name uni fun a
t                                                         -> Term tyname name uni fun a
t