{-# 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)]
caseOfCase ::
forall m tyname uni fun a.
( Ord fun, PLC.HasUnique tyname PLC.TypeUnique
, PLC.MonadQuote m
) =>
BuiltinsInfo uni fun ->
Bool ->
a ->
Term tyname Name uni fun a ->
m (Term tyname Name uni fun a)
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
| 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
, 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)
(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
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
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
allDistinctBranchConApps :: Bool
allDistinctBranchConApps =
let
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
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
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)
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
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
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
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) =
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
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
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
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 ->
(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