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

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

import PlutusCore.Builtin (CaseBuiltin (..))
import PlutusCore.MkPlc
import PlutusIR.Core

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

caseReducePass
  :: ( PLC.Typecheckable uni fun, CaseBuiltin uni
     , 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, CaseBuiltin uni, 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 (uni :: * -> *) tyname name fun a.
CaseBuiltin uni =>
Term tyname name uni fun a -> Term tyname name uni fun a
caseReduce

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

processTerm
    :: CaseBuiltin uni
    => Term tyname name uni fun a -> Term tyname name uni fun a
processTerm :: forall (uni :: * -> *) tyname name fun a.
CaseBuiltin uni =>
Term tyname name uni fun a -> Term tyname name uni fun a
processTerm = \case
    -- We could've rewritten those patterns as 'Error' in the 'Nothing' cases, but that would turn a
    -- structural error into an operational one, which would be unfortunate, so instead we decided
    -- not to fully optimize such scripts, since they aren't valid anyway.
    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)
    Case a
_ Type tyname uni a
_ (Constant a
_ Some (ValueOf uni)
con) [Term tyname name uni fun a]
cs | Right Term tyname name uni fun a
res <- Some (ValueOf uni)
-> Vector (Term tyname name uni fun a)
-> Either Text (Term tyname name uni fun a)
forall term.
(UniOf term ~ uni) =>
Some (ValueOf uni) -> Vector term -> Either Text term
forall (uni :: * -> *) term.
(CaseBuiltin uni, UniOf term ~ uni) =>
Some (ValueOf uni) -> Vector term -> Either Text term
caseBuiltin Some (ValueOf uni)
con ([Item (Vector (Term tyname name uni fun a))]
-> Vector (Term tyname name uni fun a)
forall l. IsList l => [Item l] -> l
fromList [Item (Vector (Term tyname name uni fun a))]
[Term tyname name uni fun a]
cs) -> Term tyname name uni fun a
res
    Term tyname name uni fun a
t -> Term tyname name uni fun a
t