-- editorconfig-checker-disable-file
{-# LANGUAGE ImpredicativeTypes  #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}
module PlutusIR.Transform.CaseOfCase (caseOfCase, caseOfCasePass, caseOfCasePassSC) where

import Control.Lens hiding (Strict, cons)
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Maybe
import Data.Maybe
import PlutusCore qualified as PLC
import PlutusCore.Arity
import PlutusCore.Name.Unique qualified as PLC
import PlutusCore.Quote
import PlutusIR
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo (VarInfo (DatatypeConstructor, DatatypeMatcher), VarsInfo,
                                  getConstructorArities, lookupVarInfo, termVarInfo)
import PlutusIR.Contexts
import PlutusIR.Core
import PlutusIR.MkPir
import PlutusIR.Pass
import PlutusIR.Transform.Rename ()
import PlutusIR.TypeCheck qualified as TC
import PlutusPrelude

caseOfCasePassSC ::
    forall m uni fun a.
    (PLC.Typecheckable uni fun, PLC.GEq uni, PLC.MonadQuote m, Ord a) =>
    TC.PirTCConfig uni fun ->
    BuiltinsInfo uni fun ->
    Bool ->
    a ->
    Pass m TyName Name uni fun a
caseOfCasePassSC :: forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, MonadQuote m, Ord a) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun
-> Bool
-> a
-> Pass m TyName Name uni fun a
caseOfCasePassSC PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo Bool
conservative a
newAnn =
  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
-> BuiltinsInfo uni fun
-> Bool
-> a
-> Pass m TyName Name uni fun a
forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, MonadQuote m, Ord a) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun
-> Bool
-> a
-> Pass m TyName Name uni fun a
caseOfCasePass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo Bool
conservative a
newAnn

caseOfCasePass ::
    forall m uni fun a.
    ( PLC.Typecheckable uni fun, PLC.GEq uni, MonadQuote m, Ord a) =>
    TC.PirTCConfig uni fun ->
    BuiltinsInfo uni fun ->
    Bool ->
    a ->
    Pass m TyName Name uni fun a
caseOfCasePass :: forall (m :: * -> *) (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni, MonadQuote m, Ord a) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun
-> Bool
-> a
-> Pass m TyName Name uni fun a
caseOfCasePass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo Bool
conservative a
newAnn =
  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
"case-of-case" (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
      (BuiltinsInfo uni fun
-> Bool
-> a
-> Term TyName Name uni fun a
-> m (Term TyName Name uni fun a)
forall (m :: * -> *) tyname (uni :: * -> *) fun a.
(Ord fun, HasUnique tyname TypeUnique, MonadQuote m) =>
BuiltinsInfo uni fun
-> Bool
-> a
-> Term tyname Name uni fun a
-> m (Term tyname Name uni fun a)
caseOfCase BuiltinsInfo uni fun
binfo Bool
conservative a
newAnn)
      [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)]

{-|
Perform the case-of-case transformation. This pushes
case expressions into the case branches of other case
expressions, which can often yield optimization opportunities.

Example:
@
    case (case s of { C1 a -> x; C2 b -> y; }) of
      D1 -> w
      D2 -> z

    -->

    case s of
      C1 a -> case x of { D1 -> w; D2 -> z; }
      C2 b -> case y of { D1 -> w; D2 -> z; }
@
-}
caseOfCase ::
    forall m tyname uni fun a.
    ( Ord fun, PLC.HasUnique tyname PLC.TypeUnique
    , PLC.MonadQuote m -- we need this because we do generate new names
    ) =>
    BuiltinsInfo uni fun ->
    Bool ->
    a ->
    Term tyname Name uni fun a ->
    m (Term tyname Name uni fun a)
-- See Note [Case-of-case and conapps]
caseOfCase :: forall (m :: * -> *) tyname (uni :: * -> *) fun a.
(Ord fun, HasUnique tyname TypeUnique, MonadQuote m) =>
BuiltinsInfo uni fun
-> Bool
-> a
-> Term tyname Name uni fun a
-> m (Term tyname Name uni fun a)
caseOfCase BuiltinsInfo uni fun
binfo Bool
conservative a
newAnn Term tyname Name uni fun a
t = do
    let vinfo :: VarsInfo tyname Name uni a
vinfo = Term tyname Name uni fun a -> VarsInfo tyname Name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname Name uni fun a
t
    Quote (Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Term tyname Name uni fun a)
 -> m (Term tyname Name uni fun a))
-> Quote (Term tyname Name uni fun a)
-> m (Term tyname Name uni fun a)
forall a b. (a -> b) -> a -> b
$ LensLike
  (WrappedMonad (QuoteT Identity))
  (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
    -> Quote (Term tyname Name uni fun a))
-> Term tyname Name uni fun a
-> Quote (Term tyname Name uni fun a)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad (QuoteT Identity))
  (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 (BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Bool
-> a
-> Term tyname Name uni fun a
-> Quote (Term tyname Name uni fun a)
forall tyname (uni :: * -> *) fun a.
(Ord fun, HasUnique tyname TypeUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Bool
-> a
-> Term tyname Name uni fun a
-> Quote (Term tyname Name uni fun a)
processTerm BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo Bool
conservative a
newAnn) Term tyname Name uni fun a
t

processTerm ::
    forall tyname uni fun a .
    (Ord fun, PLC.HasUnique tyname PLC.TypeUnique) =>
    BuiltinsInfo uni fun ->
    VarsInfo tyname Name uni a ->
    Bool ->
    a ->
    Term tyname Name uni fun a ->
    Quote (Term tyname Name uni fun a)
processTerm :: forall tyname (uni :: * -> *) fun a.
(Ord fun, HasUnique tyname TypeUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Bool
-> a
-> Term tyname Name uni fun a
-> Quote (Term tyname Name uni fun a)
processTerm BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo Bool
conservative a
newAnn Term tyname Name uni fun a
t
    -- We have a saturated datatype matcher application
    | Just (smcO :: SplitMatchContext tyname Name uni fun a
smcO@(SplitMatchContext AppContext tyname Name uni fun a
_ (Term tyname Name uni fun a
outerScrut, Type tyname uni ()
_, a
_) (Type tyname uni a, a)
_ AppContext tyname Name uni fun a
_), SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructOuter, [Arity]
_) <- BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Term tyname Name uni fun a
-> Maybe
     (SplitMatchContext tyname Name uni fun a,
      SplitMatchContext tyname Name uni fun a
      -> Term tyname Name uni fun a,
      [Arity])
forall tyname name (uni :: * -> *) fun a.
(Ord fun, HasUnique name TermUnique,
 HasUnique tyname TypeUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Maybe
     (SplitMatchContext tyname name uni fun a,
      SplitMatchContext tyname name uni fun a
      -> Term tyname name uni fun a,
      [Arity])
splitMatch BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo Term tyname Name uni fun a
t
    -- The scrutinee is itself an application
    , Just (SplitMatchContext tyname Name uni fun a
smcI, SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructInner, [Arity]
innerBranchArities) <- BuiltinsInfo uni fun
-> VarsInfo tyname Name uni a
-> Term tyname Name uni fun a
-> Maybe
     (SplitMatchContext tyname Name uni fun a,
      SplitMatchContext tyname Name uni fun a
      -> Term tyname Name uni fun a,
      [Arity])
forall tyname name (uni :: * -> *) fun a.
(Ord fun, HasUnique name TermUnique,
 HasUnique tyname TypeUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Maybe
     (SplitMatchContext tyname name uni fun a,
      SplitMatchContext tyname name uni fun a
      -> Term tyname name uni fun a,
      [Arity])
splitMatch BuiltinsInfo uni fun
binfo VarsInfo tyname Name uni a
vinfo Term tyname Name uni fun a
outerScrut
    = do
        Maybe (Term tyname Name uni fun a)
nt <- MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
-> QuoteT Identity (Maybe (Term tyname Name uni fun a))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
 -> QuoteT Identity (Maybe (Term tyname Name uni fun a)))
-> MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
-> QuoteT Identity (Maybe (Term tyname Name uni fun a))
forall a b. (a -> b) -> a -> b
$ VarsInfo tyname Name uni a
-> Bool
-> a
-> (SplitMatchContext tyname Name uni fun a,
    SplitMatchContext tyname Name uni fun a
    -> Term tyname Name uni fun a)
-> (SplitMatchContext tyname Name uni fun a,
    SplitMatchContext tyname Name uni fun a
    -> Term tyname Name uni fun a)
-> [Arity]
-> MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
forall tyname (uni :: * -> *) a fun.
VarsInfo tyname Name uni a
-> Bool
-> a
-> (SplitMatchContext tyname Name uni fun a,
    SplitMatchContext tyname Name uni fun a
    -> Term tyname Name uni fun a)
-> (SplitMatchContext tyname Name uni fun a,
    SplitMatchContext tyname Name uni fun a
    -> Term tyname Name uni fun a)
-> [Arity]
-> MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
tryDoCaseOfCase VarsInfo tyname Name uni a
vinfo Bool
conservative a
newAnn (SplitMatchContext tyname Name uni fun a
smcO, SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructOuter) (SplitMatchContext tyname Name uni fun a
smcI, SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructInner) [Arity]
innerBranchArities
        case Maybe (Term tyname Name uni fun a)
nt of
          Just Term tyname Name uni fun a
newTerm -> Term tyname Name uni fun a -> Quote (Term tyname Name uni fun a)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname Name uni fun a
newTerm
          Maybe (Term tyname Name uni fun a)
Nothing      -> Term tyname Name uni fun a -> Quote (Term tyname Name uni fun a)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname Name uni fun a
t
    | Bool
otherwise = Term tyname Name uni fun a -> Quote (Term tyname Name uni fun a)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname Name uni fun a
t

tryDoCaseOfCase ::
  VarsInfo tyname Name uni a
  -> Bool
  -> a
  -> (SplitMatchContext tyname Name uni fun a, SplitMatchContext tyname Name uni fun a -> Term tyname Name uni fun a)
  -> (SplitMatchContext tyname Name uni fun a, SplitMatchContext tyname Name uni fun a -> Term tyname Name uni fun a)
  -> [Arity]
  -> MaybeT Quote (Term tyname Name uni fun a)
tryDoCaseOfCase :: forall tyname (uni :: * -> *) a fun.
VarsInfo tyname Name uni a
-> Bool
-> a
-> (SplitMatchContext tyname Name uni fun a,
    SplitMatchContext tyname Name uni fun a
    -> Term tyname Name uni fun a)
-> (SplitMatchContext tyname Name uni fun a,
    SplitMatchContext tyname Name uni fun a
    -> Term tyname Name uni fun a)
-> [Arity]
-> MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
tryDoCaseOfCase
  VarsInfo tyname Name uni a
vinfo
  Bool
conservative
  a
newAnn
  (SplitMatchContext AppContext tyname Name uni fun a
outerVars (Term tyname Name uni fun a
_, Type tyname uni ()
outerScrutTy, a
outerScrutAnn) (Type tyname uni a
outerResTy, a
outerResTyAnn) AppContext tyname Name uni fun a
outerBranches, SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructOuter)
  -- Note: we don't use the inner result type, we're going to replace it
  (SplitMatchContext AppContext tyname Name uni fun a
innerVars (Term tyname Name uni fun a
innerScrut, Type tyname uni ()
innerScrutTy, a
innerScrutAnn) (Type tyname uni a, a)
_ AppContext tyname Name uni fun a
innerBranches, SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructInner)
  [Arity]
innerBranchArities
  = do
  Name
kName <- Quote Name -> MaybeT (QuoteT Identity) Name
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Quote Name -> MaybeT (QuoteT Identity) Name)
-> Quote Name -> MaybeT (QuoteT Identity) Name
forall a b. (a -> b) -> a -> b
$ Text -> Quote Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"k_caseOfCase"
  Name
sName <- Quote Name -> MaybeT (QuoteT Identity) Name
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Quote Name -> MaybeT (QuoteT Identity) Name)
-> Quote Name -> MaybeT (QuoteT Identity) Name
forall a b. (a -> b) -> a -> b
$ Text -> Quote Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"scrutinee"
  let
    -- If a term is a constructor application, returns the name of the constructor
    conAppHead :: Term tyname Name uni fun ann -> Maybe Name
conAppHead (Term tyname Name uni fun ann
-> (Term tyname Name uni fun ann,
    AppContext tyname Name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> (Term tyname name uni fun ann,
    AppContext tyname name uni fun ann)
splitApplication -> (Var ann
_ Name
n, AppContext tyname Name uni fun ann
_)) | Just (DatatypeConstructor{}) <- Name
-> VarsInfo tyname Name uni a -> Maybe (VarInfo tyname Name uni a)
forall name tyname (uni :: * -> *) a.
HasUnique name TermUnique =>
name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
lookupVarInfo Name
n VarsInfo tyname Name uni a
vinfo = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
    conAppHead Term tyname Name uni fun ann
_ = Maybe Name
forall a. Maybe a
Nothing
    -- Gets all the constructor application heads from inside the branches of the inner match
    innerBranchConAppHeads :: [Name]
innerBranchConAppHeads = (Term tyname Name uni fun a -> Maybe Name)
-> [Term tyname Name uni fun a] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Term tyname Name uni fun a -> Maybe Name
forall {tyname} {uni :: * -> *} {fun} {ann}.
Term tyname Name uni fun ann -> Maybe Name
conAppHead ([Term tyname Name uni fun a] -> [Name])
-> [Term tyname Name uni fun a] -> [Name]
forall a b. (a -> b) -> a -> b
$ AppContext tyname Name uni fun a
innerBranches AppContext tyname Name uni fun a
-> Getting
     (Endo [Term tyname Name uni fun a])
     (AppContext tyname Name uni fun a)
     (Term tyname Name uni fun a)
-> [Term tyname Name uni fun a]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. [Arity]
-> Traversal'
     (AppContext tyname Name uni fun a) (Term tyname Name uni fun a)
forall tyname name (uni :: * -> *) fun a.
[Arity]
-> Traversal'
     (AppContext tyname name uni fun a) (Term tyname name uni fun a)
underBranches [Arity]
innerBranchArities
    -- Check whether a) all the branches are conapps, and b) all the conapps are distinct.
    -- See Note [Case-of-case and conapps]
    allDistinctBranchConApps :: Bool
allDistinctBranchConApps =
      let
        -- Otherwise we've lost something when we did the traversal and we don't know what's going on
        lengthsMatch :: Bool
lengthsMatch = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
innerBranchConAppHeads Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Arity] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arity]
innerBranchArities
        distinctCons :: Bool
distinctCons = [Name] -> Bool
forall a. Eq a => [a] -> Bool
distinct [Name]
innerBranchConAppHeads
      in Bool
lengthsMatch Bool -> Bool -> Bool
&& Bool
distinctCons
    -- If we're being conservative (so trying to avoid code growth), and we don't know that the inlined
    -- version will reduce, then bind the outer case to a function to avoid code growth
    bindOuterCase :: Bool
bindOuterCase = Bool
conservative Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
allDistinctBranchConApps

  let
    mkNewOuterMatch :: Term tyname Name uni fun a -> Term tyname Name uni fun a
mkNewOuterMatch Term tyname Name uni fun a
newScrut =
      SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructOuter (SplitMatchContext tyname Name uni fun a
 -> Term tyname Name uni fun a)
-> SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
forall a b. (a -> b) -> a -> b
$ AppContext tyname Name uni fun a
-> (Term tyname Name uni fun a, Type tyname uni (), a)
-> (Type tyname uni a, a)
-> AppContext tyname Name uni fun a
-> SplitMatchContext tyname Name uni fun a
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a
-> (Term tyname name uni fun a, Type tyname uni (), a)
-> (Type tyname uni a, a)
-> AppContext tyname name uni fun a
-> SplitMatchContext tyname name uni fun a
SplitMatchContext AppContext tyname Name uni fun a
outerVars (Term tyname Name uni fun a
newScrut, Type tyname uni ()
outerScrutTy, a
outerScrutAnn) (Type tyname uni a
outerResTy, a
outerResTyAnn) AppContext tyname Name uni fun a
outerBranches
    -- \(x :: scrutTy) -> case x of ...
    newOuterMatchFn :: Term tyname Name uni fun a
newOuterMatchFn = a
-> Name
-> Type tyname uni a
-> Term tyname Name uni fun a
-> Term tyname Name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs a
newAnn Name
sName (a
newAnn a -> Type tyname uni () -> Type tyname uni a
forall a b. a -> Type tyname uni b -> Type tyname uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type tyname uni ()
outerScrutTy) (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. (a -> b) -> a -> b
$ Term tyname Name uni fun a -> Term tyname Name uni fun a
mkNewOuterMatch (a -> Name -> Term tyname Name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var a
newAnn Name
sName)
    -- k_caseOfCase :: scrutTy -> outerResTy = ...
    newOuterMatchFnBinding :: Binding tyname Name uni fun a
newOuterMatchFnBinding =
      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
newAnn 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
newAnn Name
kName (a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
newAnn (a
newAnn a -> Type tyname uni () -> Type tyname uni a
forall a b. a -> Type tyname uni b -> Type tyname uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type tyname uni ()
outerScrutTy) Type tyname uni a
outerResTy)) Term tyname Name uni fun a
newOuterMatchFn
    mkNewInnerBranchBody :: Term tyname Name uni fun a -> Term tyname Name uni fun a
mkNewInnerBranchBody Term tyname Name uni fun a
scrut =
      if Bool
bindOuterCase
      -- k_caseOfCase scrut
      then 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.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply a
newAnn (a -> Name -> Term tyname Name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var a
newAnn Name
kName) Term tyname Name uni fun a
scrut
      -- case scrut of ...
      else Term tyname Name uni fun a -> Term tyname Name uni fun a
mkNewOuterMatch Term tyname Name uni fun a
scrut

  AppContext tyname Name uni fun a
newInnerBranches <- Quote (Maybe (AppContext tyname Name uni fun a))
-> MaybeT (QuoteT Identity) (AppContext tyname Name uni fun a)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Quote (Maybe (AppContext tyname Name uni fun a))
 -> MaybeT (QuoteT Identity) (AppContext tyname Name uni fun a))
-> Quote (Maybe (AppContext tyname Name uni fun a))
-> MaybeT (QuoteT Identity) (AppContext tyname Name uni fun a)
forall a b. (a -> b) -> a -> b
$ Maybe (AppContext tyname Name uni fun a)
-> Quote (Maybe (AppContext tyname Name uni fun a))
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (AppContext tyname Name uni fun a)
 -> Quote (Maybe (AppContext tyname Name uni fun a)))
-> Maybe (AppContext tyname Name uni fun a)
-> Quote (Maybe (AppContext tyname Name uni fun a))
forall a b. (a -> b) -> a -> b
$ (Term tyname Name uni fun a -> Term tyname Name uni fun a)
-> AppContext tyname Name uni fun a
-> [Arity]
-> Maybe (AppContext tyname Name uni fun a)
forall tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> Term tyname name uni fun a)
-> AppContext tyname name uni fun a
-> [Arity]
-> Maybe (AppContext tyname name uni fun a)
mapBranches Term tyname Name uni fun a -> Term tyname Name uni fun a
mkNewInnerBranchBody AppContext tyname Name uni fun a
innerBranches [Arity]
innerBranchArities

  let
    newInnerMatch :: Term tyname Name uni fun a
newInnerMatch =
      SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
reconstructInner (SplitMatchContext tyname Name uni fun a
 -> Term tyname Name uni fun a)
-> SplitMatchContext tyname Name uni fun a
-> Term tyname Name uni fun a
forall a b. (a -> b) -> a -> b
$ AppContext tyname Name uni fun a
-> (Term tyname Name uni fun a, Type tyname uni (), a)
-> (Type tyname uni a, a)
-> AppContext tyname Name uni fun a
-> SplitMatchContext tyname Name uni fun a
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a
-> (Term tyname name uni fun a, Type tyname uni (), a)
-> (Type tyname uni a, a)
-> AppContext tyname name uni fun a
-> SplitMatchContext tyname name uni fun a
SplitMatchContext AppContext tyname Name uni fun a
innerVars (Term tyname Name uni fun a
innerScrut, Type tyname uni ()
innerScrutTy, a
innerScrutAnn) (Type tyname uni a
outerResTy, a
outerResTyAnn) AppContext tyname Name uni fun a
newInnerBranches

  Term tyname Name uni fun a
-> MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
forall a. a -> MaybeT (QuoteT Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname Name uni fun a
 -> MaybeT (QuoteT Identity) (Term tyname Name uni fun a))
-> Term tyname Name uni fun a
-> MaybeT (QuoteT Identity) (Term tyname Name uni fun a)
forall a b. (a -> b) -> a -> b
$
    if Bool
bindOuterCase
    then a
-> Recursivity
-> [Binding tyname Name uni fun a]
-> Term tyname Name uni fun a
-> Term tyname Name uni fun a
forall a tyname name (uni :: * -> *) fun.
a
-> Recursivity
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Term tyname name uni fun a
mkLet a
newAnn Recursivity
NonRec [Binding tyname Name uni fun a
newOuterMatchFnBinding] Term tyname Name uni fun a
newInnerMatch
    else Term tyname Name uni fun a
newInnerMatch

-- | Apply the given function to the term "inside" the case branches in the given 'AppContext'.
-- Must be given an arity for each branch so it knows how many binders to go under.
mapBranches ::
  forall tyname name uni fun a
  . (Term tyname name uni fun a -> Term tyname name uni fun a)
  -> AppContext tyname name uni fun a
  -> [Arity]
  -> Maybe (AppContext tyname name uni fun a)
mapBranches :: forall tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> Term tyname name uni fun a)
-> AppContext tyname name uni fun a
-> [Arity]
-> Maybe (AppContext tyname name uni fun a)
mapBranches Term tyname name uni fun a -> Term tyname name uni fun a
f = AppContext tyname name uni fun a
-> [Arity] -> Maybe (AppContext tyname name uni fun a)
go
    where
    go :: AppContext tyname name uni fun a -> [Arity] -> Maybe (AppContext tyname name uni fun a)
    go :: AppContext tyname name uni fun a
-> [Arity] -> Maybe (AppContext tyname name uni fun a)
go AppContext tyname name uni fun a
AppContextEnd [] = AppContext tyname name uni fun a
-> Maybe (AppContext tyname name uni fun a)
forall a. a -> Maybe a
Just AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
AppContext tyname name uni fun ann
AppContextEnd
    go (TermAppContext Term tyname name uni fun a
branch a
ann AppContext tyname name uni fun a
ctx) (Arity
arity:[Arity]
arities) =
      -- This makes the whole thing return Nothing if the traversal has no targets, i.e. if the
      -- arity doesn't match the term we're looking at. I can't see a way to do this with a more
      -- general traversal, so there's some duplication between this and the simpler 'underBranches'.
      Term tyname name uni fun a
-> a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TermAppContext (Term tyname name uni fun a
 -> a
 -> AppContext tyname name uni fun a
 -> AppContext tyname name uni fun a)
-> Maybe (Term tyname name uni fun a)
-> Maybe
     (a
      -> AppContext tyname name uni fun a
      -> AppContext tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LensLike
  ((,) Any)
  (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
-> Maybe (Term tyname name uni fun a)
forall (m :: * -> *) s t a b.
Alternative m =>
LensLike ((,) Any) s t a b -> (a -> b) -> s -> m t
failover (Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
underBinders Arity
arity) Term tyname name uni fun a -> Term tyname name uni fun a
f Term tyname name uni fun a
branch Maybe
  (a
   -> AppContext tyname name uni fun a
   -> AppContext tyname name uni fun a)
-> Maybe a
-> Maybe
     (AppContext tyname name uni fun a
      -> AppContext tyname name uni fun a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> Maybe a
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
ann Maybe
  (AppContext tyname name uni fun a
   -> AppContext tyname name uni fun a)
-> Maybe (AppContext tyname name uni fun a)
-> Maybe (AppContext tyname name uni fun a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AppContext tyname name uni fun a
-> [Arity] -> Maybe (AppContext tyname name uni fun a)
go AppContext tyname name uni fun a
ctx [Arity]
arities
    go AppContext tyname name uni fun a
_ [Arity]
_ = Maybe (AppContext tyname name uni fun a)
forall a. Maybe a
Nothing

-- | Traverses under the branches in the application context.
underBranches :: [Arity] -> Traversal' (AppContext tyname name uni fun a) (Term tyname name uni fun a)
underBranches :: forall tyname name (uni :: * -> *) fun a.
[Arity]
-> Traversal'
     (AppContext tyname name uni fun a) (Term tyname name uni fun a)
underBranches [Arity]
as Term tyname name uni fun a -> f (Term tyname name uni fun a)
f = [Arity]
-> AppContext tyname name uni fun a
-> f (AppContext tyname name uni fun a)
go [Arity]
as
    where
    go :: [Arity]
-> AppContext tyname name uni fun a
-> f (AppContext tyname name uni fun a)
go [] AppContext tyname name uni fun a
AppContextEnd = AppContext tyname name uni fun a
-> f (AppContext tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
AppContext tyname name uni fun ann
AppContextEnd
    go (Arity
arity:[Arity]
arities) (TermAppContext Term tyname name uni fun a
branch a
ann AppContext tyname name uni fun a
ctx) =
      Term tyname name uni fun a
-> a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TermAppContext (Term tyname name uni fun a
 -> a
 -> AppContext tyname name uni fun a
 -> AppContext tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f (a
      -> AppContext tyname name uni fun a
      -> AppContext tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
underBinders Arity
arity Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
branch f (a
   -> AppContext tyname name uni fun a
   -> AppContext tyname name uni fun a)
-> f a
-> f (AppContext tyname name uni fun a
      -> AppContext tyname name uni fun a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
ann f (AppContext tyname name uni fun a
   -> AppContext tyname name uni fun a)
-> f (AppContext tyname name uni fun a)
-> f (AppContext tyname name uni fun a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arity]
-> AppContext tyname name uni fun a
-> f (AppContext tyname name uni fun a)
go [Arity]
arities AppContext tyname name uni fun a
ctx
    go [Arity]
_ AppContext tyname name uni fun a
ctx = AppContext tyname name uni fun a
-> f (AppContext tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AppContext tyname name uni fun a
ctx

-- | Split a match, either a normal datatype match or a builtin 'match'.
splitMatch :: forall tyname name uni fun a . (Ord fun, PLC.HasUnique name PLC.TermUnique, PLC.HasUnique tyname PLC.TypeUnique) =>
  BuiltinsInfo uni fun
  -> VarsInfo tyname name uni a
  -> Term tyname name uni fun a
  -> Maybe (SplitMatchContext tyname name uni fun a, SplitMatchContext tyname name uni fun a -> Term tyname name uni fun a, [Arity])
splitMatch :: forall tyname name (uni :: * -> *) fun a.
(Ord fun, HasUnique name TermUnique,
 HasUnique tyname TypeUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Maybe
     (SplitMatchContext tyname name uni fun a,
      SplitMatchContext tyname name uni fun a
      -> Term tyname name uni fun a,
      [Arity])
splitMatch BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t = do
  let (Term tyname name uni fun a
hd, AppContext tyname name uni fun a
args) = Term tyname name uni fun a
-> (Term tyname name uni fun a, AppContext tyname name uni fun a)
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> (Term tyname name uni fun ann,
    AppContext tyname name uni fun ann)
splitApplication Term tyname name uni fun a
t
  (Market
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (Identity (SplitMatchContext tyname name uni fun a))
-> Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (AppContext tyname name uni fun a)
     (Identity (AppContext tyname name uni fun a))
p, [Arity]
arities) <- case Term tyname name uni fun a
hd of
    (Var a
_ name
matcherName)     -> do
      let p :: Market
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (Identity (SplitMatchContext tyname name uni fun a))
-> Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (AppContext tyname name uni fun a)
     (Identity (AppContext tyname name uni fun a))
p = VarsInfo tyname name uni a
-> name
-> Prism'
     (AppContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
forall name tyname (uni :: * -> *) a fun.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
VarsInfo tyname name uni a
-> name
-> Prism'
     (AppContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
asNormalDatatypeMatch VarsInfo tyname name uni a
vinfo name
matcherName
      VarInfo tyname name uni a
info <- name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
forall name tyname (uni :: * -> *) a.
HasUnique name TermUnique =>
name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
lookupVarInfo name
matcherName VarsInfo tyname name uni a
vinfo
      [Arity]
constrArities <- case VarInfo tyname name uni a
info of
        DatatypeMatcher tyname
parentTyName -> tyname -> VarsInfo tyname name uni a -> Maybe [Arity]
forall name tyname (uni :: * -> *) a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
tyname -> VarsInfo tyname name uni a -> Maybe [Arity]
getConstructorArities tyname
parentTyName VarsInfo tyname name uni a
vinfo
        VarInfo tyname name uni a
_                            -> Maybe [Arity]
forall a. Maybe a
Nothing
      -- The branch arities don't include the type arguments for the constructor
      let branchArities :: [Arity]
branchArities = (Arity -> Arity) -> [Arity] -> [Arity]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Param -> Bool) -> Arity -> Arity
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Param -> Param -> Bool
forall a. Eq a => a -> a -> Bool
(==) Param
TypeParam)) [Arity]
constrArities
      (Market
   (SplitMatchContext tyname name uni fun a)
   (SplitMatchContext tyname name uni fun a)
   (SplitMatchContext tyname name uni fun a)
   (Identity (SplitMatchContext tyname name uni fun a))
 -> Market
      (SplitMatchContext tyname name uni fun a)
      (SplitMatchContext tyname name uni fun a)
      (AppContext tyname name uni fun a)
      (Identity (AppContext tyname name uni fun a)),
 [Arity])
-> Maybe
     (Market
        (SplitMatchContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a)
        (Identity (SplitMatchContext tyname name uni fun a))
      -> Market
           (SplitMatchContext tyname name uni fun a)
           (SplitMatchContext tyname name uni fun a)
           (AppContext tyname name uni fun a)
           (Identity (AppContext tyname name uni fun a)),
      [Arity])
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Market
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (Identity (SplitMatchContext tyname name uni fun a))
-> Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (AppContext tyname name uni fun a)
     (Identity (AppContext tyname name uni fun a))
forall {fun}.
Market
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (Identity (SplitMatchContext tyname name uni fun a))
-> Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (AppContext tyname name uni fun a)
     (Identity (AppContext tyname name uni fun a))
p, [Arity]
branchArities)
    (Builtin a
_ fun
matcherName) -> do
      Market
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (Identity (SplitMatchContext tyname name uni fun a))
-> Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (AppContext tyname name uni fun a)
     (Identity (AppContext tyname name uni fun a))
p <- BuiltinsInfo uni fun
-> fun
-> Maybe
     (Market
        (SplitMatchContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a)
        (Identity (SplitMatchContext tyname name uni fun a))
      -> Market
           (SplitMatchContext tyname name uni fun a)
           (SplitMatchContext tyname name uni fun a)
           (AppContext tyname name uni fun a)
           (Identity (AppContext tyname name uni fun a)))
forall fun (uni :: * -> *) tyname name a.
Ord fun =>
BuiltinsInfo uni fun
-> fun
-> Maybe
     (APrism'
        (AppContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a))
asBuiltinDatatypeMatch BuiltinsInfo uni fun
binfo fun
matcherName
      [Arity]
branchArities <- BuiltinsInfo uni fun -> fun -> Maybe [Arity]
forall fun (uni :: * -> *).
Ord fun =>
BuiltinsInfo uni fun -> fun -> Maybe [Arity]
builtinDatatypeMatchBranchArities BuiltinsInfo uni fun
binfo fun
matcherName
      (Market
   (SplitMatchContext tyname name uni fun a)
   (SplitMatchContext tyname name uni fun a)
   (SplitMatchContext tyname name uni fun a)
   (Identity (SplitMatchContext tyname name uni fun a))
 -> Market
      (SplitMatchContext tyname name uni fun a)
      (SplitMatchContext tyname name uni fun a)
      (AppContext tyname name uni fun a)
      (Identity (AppContext tyname name uni fun a)),
 [Arity])
-> Maybe
     (Market
        (SplitMatchContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a)
        (Identity (SplitMatchContext tyname name uni fun a))
      -> Market
           (SplitMatchContext tyname name uni fun a)
           (SplitMatchContext tyname name uni fun a)
           (AppContext tyname name uni fun a)
           (Identity (AppContext tyname name uni fun a)),
      [Arity])
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Market
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (Identity (SplitMatchContext tyname name uni fun a))
-> Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (AppContext tyname name uni fun a)
     (Identity (AppContext tyname name uni fun a))
p, [Arity]
branchArities)
    Term tyname name uni fun a
_                       -> Maybe
  (Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (Identity (SplitMatchContext tyname name uni fun a))
   -> Market
        (SplitMatchContext tyname name uni fun a)
        (SplitMatchContext tyname name uni fun a)
        (AppContext tyname name uni fun a)
        (Identity (AppContext tyname name uni fun a)),
   [Arity])
forall a. Maybe a
Nothing
  (Market
   (SplitMatchContext tyname name uni fun a)
   (SplitMatchContext tyname name uni fun a)
   (SplitMatchContext tyname name uni fun a)
   (Identity (SplitMatchContext tyname name uni fun a))
 -> Market
      (SplitMatchContext tyname name uni fun a)
      (SplitMatchContext tyname name uni fun a)
      (AppContext tyname name uni fun a)
      (Identity (AppContext tyname name uni fun a)))
-> ((SplitMatchContext tyname name uni fun a
     -> AppContext tyname name uni fun a)
    -> (AppContext tyname name uni fun a
        -> Either
             (AppContext tyname name uni fun a)
             (SplitMatchContext tyname name uni fun a))
    -> Maybe
         (SplitMatchContext tyname name uni fun a,
          SplitMatchContext tyname name uni fun a
          -> Term tyname name uni fun a,
          [Arity]))
-> Maybe
     (SplitMatchContext tyname name uni fun a,
      SplitMatchContext tyname name uni fun a
      -> Term tyname name uni fun a,
      [Arity])
forall s t a b r.
APrism s t a b -> ((b -> t) -> (s -> Either t a) -> r) -> r
withPrism Market
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (SplitMatchContext tyname name uni fun a)
  (Identity (SplitMatchContext tyname name uni fun a))
-> Market
     (SplitMatchContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
     (AppContext tyname name uni fun a)
     (Identity (AppContext tyname name uni fun a))
p (((SplitMatchContext tyname name uni fun a
   -> AppContext tyname name uni fun a)
  -> (AppContext tyname name uni fun a
      -> Either
           (AppContext tyname name uni fun a)
           (SplitMatchContext tyname name uni fun a))
  -> Maybe
       (SplitMatchContext tyname name uni fun a,
        SplitMatchContext tyname name uni fun a
        -> Term tyname name uni fun a,
        [Arity]))
 -> Maybe
      (SplitMatchContext tyname name uni fun a,
       SplitMatchContext tyname name uni fun a
       -> Term tyname name uni fun a,
       [Arity]))
-> ((SplitMatchContext tyname name uni fun a
     -> AppContext tyname name uni fun a)
    -> (AppContext tyname name uni fun a
        -> Either
             (AppContext tyname name uni fun a)
             (SplitMatchContext tyname name uni fun a))
    -> Maybe
         (SplitMatchContext tyname name uni fun a,
          SplitMatchContext tyname name uni fun a
          -> Term tyname name uni fun a,
          [Arity]))
-> Maybe
     (SplitMatchContext tyname name uni fun a,
      SplitMatchContext tyname name uni fun a
      -> Term tyname name uni fun a,
      [Arity])
forall a b. (a -> b) -> a -> b
$ \SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
reconstruct AppContext tyname name uni fun a
-> Either
     (AppContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
match ->
    case AppContext tyname name uni fun a
-> Either
     (AppContext tyname name uni fun a)
     (SplitMatchContext tyname name uni fun a)
match AppContext tyname name uni fun a
args of
      Right SplitMatchContext tyname name uni fun a
sm ->
        -- wrangle the reconstruction function so it also puts the head back in, for
        -- convenience of use elsewhere
        (SplitMatchContext tyname name uni fun a,
 SplitMatchContext tyname name uni fun a
 -> Term tyname name uni fun a,
 [Arity])
-> Maybe
     (SplitMatchContext tyname name uni fun a,
      SplitMatchContext tyname name uni fun a
      -> Term tyname name uni fun a,
      [Arity])
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SplitMatchContext tyname name uni fun a
sm, \SplitMatchContext tyname name uni fun a
sm' -> Term tyname name uni fun a
-> AppContext tyname name uni fun a -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext Term tyname name uni fun a
hd (SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
reconstruct SplitMatchContext tyname name uni fun a
sm'), [Arity]
arities)
      Left AppContext tyname name uni fun a
_ -> Maybe
  (SplitMatchContext tyname name uni fun a,
   SplitMatchContext tyname name uni fun a
   -> Term tyname name uni fun a,
   [Arity])
forall a. Maybe a
Nothing

{- Note [Case-of-case and conapps]
Case-of-case is especially good if the bodies of the branches are all constructor applications.
Consider the following program we might typically get from Plutus Tx:

Bool_match {integer} (ifThenElse {Bool} (lessThanInteger 1 2) True False) 3 4
---> case-of-case
ifThenElse {integer} (lessThanInteger 1 2) (Bool_match {integer} True 3) (Bool_match {integer} False 4)
---> case-of-known-constructor
ifThenElse {integer} (lessThanInteger 1 2) 3

That is, this guarantees that case-of-known constructor will fire and get rid of one of the
matches entirely, which is great.

In order to be sure that it's definitely good, however, we need all of the branches to
be _distinct_ constructor applications, otherwise we can duplicate code, see
Note [Case-of-case and duplicating code].
-}

{- Note [Case-of-case and duplicating code]
Case-of-case can duplicate code.

Consider this schematic example:

case (case s of { C1 a -> x; C2 b -> y; }) of
  D1 -> w
  D2 -> z

-->

case s of
  C1 a -> case x of { D1 -> w; D2 -> z; }
  C2 b -> case y of { D1 -> w; D2 -> z; }

We duplicate the outer case (the matcher application, importantly including
the branches) for every branch of the inner case.

Any time we duplicate code we run the risk of exponential program growth,
since we might apply case-of-case inside the duplicated parts of the
program, thus leading to multiplicative growth. In particular, since we apply
case-of-case in a bottom-up fashion, we can apply it inside a subterm (creating
duplication), and then in the main term (multiplying the duplication) in a single
pass. This is not _too_ bad so long as case-of-known-constructor will clear
things up afterwards, but is something to be aware of.

If the inner branch bodies are conapps (see Note [Case-of-case and conapps]) then
that will reduce but not necessarily eliminate the duplication. Consider

case (case s of { C1 a -> True; C2 b -> True; C3 c -> False }) of
  True -> v
  False -> w

--> (case-of-case)

case s of
  C1 a -> case True of { True -> v; False -> w; }
  C2 b -> case True of { True -> v; False -> w; }
  C3 c -> case False of { True -> v; False -> w; }

--> (case-of-known-constructor)

case s of
  C1 a -> v
  C2 b -> v
  C3 c -> w

i.e. we still duplicate v! If however the conapps are all distinct constructors then
this won't happen.

We can mitigate the problem by binding the potentially-duplicated code to a variable
instead:

case (case s of { C1 a -> x; C2 b -> y; }) of
  D1 -> w
  D2 -> z

-->

let k_caseOfCase = \x -> case x of { D1 -> w; D2 -> z; }
in case s of
  C1 a -> k_caseOfCase x
  C2 b -> k_caseOfCase y

This avoids the code growth but is less good as an optimization, unless we can rely
on the inliner to see these as good inlining opportunities, which we currently can't.
-}