{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
module PlutusIR.Contexts where
import Control.Lens
import Data.DList qualified as DList
import Data.Functor (void)
import PlutusCore.Arity
import PlutusCore.Name.Unique qualified as PLC
import PlutusIR.Analysis.VarInfo
import PlutusIR.Core
import PlutusIR.MkPir
data AppContext tyname name uni fun ann =
TermAppContext (Term tyname name uni fun ann) ann (AppContext tyname name uni fun ann)
| TypeAppContext (Type tyname uni ann) ann (AppContext tyname name uni fun ann)
| AppContextEnd
splitApplication :: Term tyname name uni fun ann
-> (Term tyname name uni fun ann, AppContext tyname name uni fun ann)
splitApplication :: 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 ann
tm
= Term tyname name uni fun ann
-> AppContext 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
-> AppContext tyname name uni fun ann
-> (Term tyname name uni fun ann,
AppContext tyname name uni fun ann)
go Term tyname name uni fun ann
tm AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
AppContext tyname name uni fun ann
AppContextEnd
where
go :: Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> (Term tyname name uni fun ann,
AppContext tyname name uni fun ann)
go (Apply ann
ann Term tyname name uni fun ann
f Term tyname name uni fun ann
arg) AppContext tyname name uni fun ann
ctx = Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> (Term tyname name uni fun ann,
AppContext tyname name uni fun ann)
go Term tyname name uni fun ann
f (Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
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 ann
arg ann
ann AppContext tyname name uni fun ann
ctx)
go (TyInst ann
ann Term tyname name uni fun ann
f Type tyname uni ann
tyArg) AppContext tyname name uni fun ann
ctx = Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> (Term tyname name uni fun ann,
AppContext tyname name uni fun ann)
go Term tyname name uni fun ann
f (Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni ann
tyArg ann
ann AppContext tyname name uni fun ann
ctx)
go Term tyname name uni fun ann
t AppContext tyname name uni fun ann
ctx = (Term tyname name uni fun ann
t, AppContext tyname name uni fun ann
ctx)
fillAppContext
:: Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext :: 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 ann
t = \case
AppContext tyname name uni fun ann
AppContextEnd -> Term tyname name uni fun ann
t
TermAppContext Term tyname name uni fun ann
arg ann
ann AppContext tyname name uni fun ann
ctx -> Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
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 (ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
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 ann
ann Term tyname name uni fun ann
t Term tyname name uni fun ann
arg) AppContext tyname name uni fun ann
ctx
TypeAppContext Type tyname uni ann
tyArg ann
ann AppContext tyname name uni fun ann
ctx -> Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
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 (ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst ann
ann Term tyname name uni fun ann
t Type tyname uni ann
tyArg) AppContext tyname name uni fun ann
ctx
dropAppContext :: Int -> AppContext tyname name uni fun a -> AppContext tyname name uni fun a
dropAppContext :: forall tyname name (uni :: * -> *) fun a.
Int
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
dropAppContext Int
i AppContext tyname name uni fun a
ctx | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = AppContext tyname name uni fun a
ctx
dropAppContext Int
i AppContext tyname name uni fun a
ctx = case AppContext tyname name uni fun a
ctx of
AppContext tyname name uni fun a
AppContextEnd -> AppContext tyname name uni fun a
ctx
TermAppContext Term tyname name uni fun a
_ a
_ AppContext tyname name uni fun a
ctx' -> Int
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Int
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
dropAppContext (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) AppContext tyname name uni fun a
ctx'
TypeAppContext Type tyname uni a
_ a
_ AppContext tyname name uni fun a
ctx' -> Int
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Int
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
dropAppContext (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) AppContext tyname name uni fun a
ctx'
lengthContext :: AppContext tyname name uni fun a -> Int
lengthContext :: forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Int
lengthContext = Int -> AppContext tyname name uni fun a -> Int
forall {t} {tyname} {name} {uni :: * -> *} {fun} {ann}.
Num t =>
t -> AppContext tyname name uni fun ann -> t
go Int
0
where
go :: t -> AppContext tyname name uni fun ann -> t
go t
acc = \case
AppContext tyname name uni fun ann
AppContextEnd -> t
acc
TermAppContext Term tyname name uni fun ann
_ ann
_ AppContext tyname name uni fun ann
ctx -> t -> AppContext tyname name uni fun ann -> t
go (t
acct -> t -> t
forall a. Num a => a -> a -> a
+t
1) AppContext tyname name uni fun ann
ctx
TypeAppContext Type tyname uni ann
_ ann
_ AppContext tyname name uni fun ann
ctx -> t -> AppContext tyname name uni fun ann -> t
go (t
acct -> t -> t
forall a. Num a => a -> a -> a
+t
1) AppContext tyname name uni fun ann
ctx
splitAppContext
:: Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a, AppContext tyname name uni fun a)
splitAppContext :: forall tyname name (uni :: * -> *) fun a.
Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
splitAppContext = (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
(AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
go AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall a. a -> a
id
where
go
:: (AppContext tyname name uni fun a -> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a, AppContext tyname name uni fun a)
go :: forall tyname name (uni :: * -> *) fun a.
(AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
go AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
acc Int
i AppContext tyname name uni fun a
ctx | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
acc AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
AppContext tyname name uni fun ann
AppContextEnd, AppContext tyname name uni fun a
ctx)
go AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
acc Int
i AppContext tyname name uni fun a
ctx = case AppContext tyname name uni fun a
ctx of
c :: AppContext tyname name uni fun a
c@AppContext tyname name uni fun a
AppContextEnd -> (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
acc AppContext tyname name uni fun a
c, AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
AppContext tyname name uni fun ann
AppContextEnd)
TermAppContext Term tyname name uni fun a
arg a
ann AppContext tyname name uni fun a
ctx' -> (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
(AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
go (\AppContext tyname name uni fun a
end -> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
acc (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall a b. (a -> b) -> a -> b
$ 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
arg a
ann AppContext tyname name uni fun a
end) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) AppContext tyname name uni fun a
ctx'
TypeAppContext Type tyname uni a
arg a
ann AppContext tyname name uni fun a
ctx' -> (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
(AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
go (\AppContext tyname name uni fun a
end -> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
acc (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall a b. (a -> b) -> a -> b
$ Type tyname uni a
-> a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni a
arg a
ann AppContext tyname name uni fun a
end) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) AppContext tyname name uni fun a
ctx'
appendAppContext
:: AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
appendAppContext :: forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
appendAppContext AppContext tyname name uni fun a
ctx1 AppContext tyname name uni fun a
ctx2 = AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
go AppContext tyname name uni fun a
ctx1
where
go :: AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
go AppContext tyname name uni fun a
AppContextEnd = AppContext tyname name uni fun a
ctx2
go (TermAppContext Term tyname name uni fun a
arg 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
arg a
ann (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall a b. (a -> b) -> a -> b
$ AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
go AppContext tyname name uni fun a
ctx'
go (TypeAppContext Type tyname uni a
arg a
ann AppContext tyname name uni fun a
ctx') = Type tyname uni a
-> a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni a
arg a
ann (AppContext tyname name uni fun a
-> AppContext tyname name uni fun a)
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall a b. (a -> b) -> a -> b
$ AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
go AppContext tyname name uni fun a
ctx'
instance Semigroup (AppContext tyname name uni fun a) where
<> :: AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
(<>) = AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
appendAppContext
instance Monoid (AppContext tyname name uni fun a) where
mempty :: AppContext tyname name uni fun a
mempty = AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
AppContext tyname name uni fun ann
AppContextEnd
data Saturation = Oversaturated | Undersaturated | Saturated
saturates :: AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates :: forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name uni fun a
AppContextEnd [] = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Saturated
saturates AppContext tyname name uni fun a
AppContextEnd Arity
_ = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Undersaturated
saturates (TermAppContext Term tyname name uni fun a
_ a
_ AppContext tyname name uni fun a
ctx) (Param
TermParam:Arity
arities) = AppContext tyname name uni fun a -> Arity -> Maybe Saturation
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name uni fun a
ctx Arity
arities
saturates (TypeAppContext Type tyname uni a
_ a
_ AppContext tyname name uni fun a
ctx) (Param
TypeParam:Arity
arities) = AppContext tyname name uni fun a -> Arity -> Maybe Saturation
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name uni fun a
ctx Arity
arities
saturates (TermAppContext{}) (Param
TypeParam:Arity
_) = Maybe Saturation
forall a. Maybe a
Nothing
saturates (TypeAppContext{}) (Param
TermParam:Arity
_) = Maybe Saturation
forall a. Maybe a
Nothing
saturates (TermAppContext{}) [] = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Oversaturated
saturates (TypeAppContext{}) [] = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Oversaturated
data SplitMatchContext tyname name uni fun a = SplitMatchContext
{ forall tyname name (uni :: * -> *) fun a.
SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
smTyVars :: AppContext tyname name uni fun a
, forall tyname name (uni :: * -> *) fun a.
SplitMatchContext tyname name uni fun a
-> (Term tyname name uni fun a, Type tyname uni (), a)
smScrutinee :: (Term tyname name uni fun a, Type tyname uni (), a)
, forall tyname name (uni :: * -> *) fun a.
SplitMatchContext tyname name uni fun a -> (Type tyname uni a, a)
smResTy :: (Type tyname uni a, a)
, forall tyname name (uni :: * -> *) fun a.
SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
smBranches :: AppContext tyname name uni fun a
}
extractTyArgs :: AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
= DList (Type tyname uni a)
-> AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
forall {tyname} {uni :: * -> *} {ann} {name} {fun}.
DList (Type tyname uni ann)
-> AppContext tyname name uni fun ann
-> Maybe [Type tyname uni ann]
go DList (Type tyname uni a)
forall a. DList a
DList.empty
where
go :: DList (Type tyname uni ann)
-> AppContext tyname name uni fun ann
-> Maybe [Type tyname uni ann]
go DList (Type tyname uni ann)
acc = \case
TypeAppContext Type tyname uni ann
ty ann
_ann AppContext tyname name uni fun ann
ctx -> DList (Type tyname uni ann)
-> AppContext tyname name uni fun ann
-> Maybe [Type tyname uni ann]
go (DList (Type tyname uni ann)
-> Type tyname uni ann -> DList (Type tyname uni ann)
forall a. DList a -> a -> DList a
DList.snoc DList (Type tyname uni ann)
acc Type tyname uni ann
ty) AppContext tyname name uni fun ann
ctx
TermAppContext{} -> Maybe [Type tyname uni ann]
forall a. Maybe a
Nothing
AppContext tyname name uni fun ann
AppContextEnd -> [Type tyname uni ann] -> Maybe [Type tyname uni ann]
forall a. a -> Maybe a
Just (DList (Type tyname uni ann) -> [Type tyname uni ann]
forall a. DList a -> [a]
DList.toList DList (Type tyname uni ann)
acc)
splitNormalDatatypeMatch
:: (PLC.HasUnique name PLC.TermUnique, PLC.HasUnique tyname PLC.TypeUnique)
=> VarsInfo tyname name uni a
-> name
-> AppContext tyname name uni fun a -> Maybe (SplitMatchContext tyname name uni fun a)
splitNormalDatatypeMatch :: forall name tyname (uni :: * -> *) a fun.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
VarsInfo tyname name uni a
-> name
-> AppContext tyname name uni fun a
-> Maybe (SplitMatchContext tyname name uni fun a)
splitNormalDatatypeMatch VarsInfo tyname name uni a
vinfo name
matcherName AppContext tyname name uni fun a
args
| Just dmInfo :: VarInfo tyname name uni a
dmInfo@(DatatypeMatcher tyname
dmParentTyname) <- 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
, Just Arity
dmArity <- VarInfo tyname name uni a
-> VarsInfo tyname name uni a -> Maybe Arity
forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
VarInfo tyname name uni a
-> VarsInfo tyname name uni a -> Maybe Arity
varInfoArity VarInfo tyname name uni a
dmInfo VarsInfo tyname name uni a
vinfo
, Just Saturation
Saturated <- AppContext tyname name uni fun a -> Arity -> Maybe Saturation
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name uni fun a
args Arity
dmArity
, Just (DatatypeTyVar (Datatype a
_ TyVarDecl tyname a
tyname [TyVarDecl tyname a]
tyvars name
_ [VarDecl tyname name uni a]
_)) <- tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
lookupTyVarInfo tyname
dmParentTyname VarsInfo tyname name uni a
vinfo
, (AppContext tyname name uni fun a
vars, TermAppContext Term tyname name uni fun a
scrut a
scrutAnn (TypeAppContext Type tyname uni a
resTy a
resTyAnn AppContext tyname name uni fun a
branches)) <-
Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
splitAppContext ([TyVarDecl tyname a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarDecl tyname a]
tyvars) AppContext tyname name uni fun a
args
, Just [Type tyname uni a]
tvs <- AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
extractTyArgs AppContext tyname name uni fun a
vars
=
let
scrutTy :: Type tyname uni ()
scrutTy = Type tyname uni ()
-> [((), Type tyname uni ())] -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyApp (() -> TyVarDecl tyname () -> Type tyname uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () (TyVarDecl tyname a -> TyVarDecl tyname ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyVarDecl tyname a
tyname)) ([((), Type tyname uni ())] -> Type tyname uni ())
-> [((), Type tyname uni ())] -> Type tyname uni ()
forall a b. (a -> b) -> a -> b
$ ((),) (Type tyname uni () -> ((), Type tyname uni ()))
-> (Type tyname uni a -> Type tyname uni ())
-> Type tyname uni a
-> ((), Type tyname uni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni a -> Type tyname uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Type tyname uni a -> ((), Type tyname uni ()))
-> [Type tyname uni a] -> [((), Type tyname uni ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type tyname uni a]
tvs
sm :: SplitMatchContext tyname name uni fun a
sm = 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
vars (Term tyname name uni fun a
scrut, Type tyname uni ()
scrutTy, a
scrutAnn) (Type tyname uni a
resTy, a
resTyAnn) AppContext tyname name uni fun a
branches
in SplitMatchContext tyname name uni fun a
-> Maybe (SplitMatchContext tyname name uni fun a)
forall a. a -> Maybe a
Just SplitMatchContext tyname name uni fun a
sm
| Bool
otherwise = Maybe (SplitMatchContext tyname name uni fun a)
forall a. Maybe a
Nothing
reconstructNormalDatatypeMatch
:: SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
reconstructNormalDatatypeMatch :: forall tyname name (uni :: * -> *) fun a.
SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
reconstructNormalDatatypeMatch
(SplitMatchContext AppContext tyname name uni fun a
vars (Term tyname name uni fun a
scrut, Type tyname uni ()
_, a
scrutAnn) (Type tyname uni a
resTy, a
resTyAnn) AppContext tyname name uni fun a
branches) =
AppContext tyname name uni fun a
vars AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> 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
scrut a
scrutAnn (Type tyname uni a
-> a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni a
resTy a
resTyAnn AppContext tyname name uni fun a
branches)
asNormalDatatypeMatch
:: (PLC.HasUnique name PLC.TermUnique, PLC.HasUnique tyname PLC.TypeUnique)
=> VarsInfo tyname name uni a
-> name
-> Prism' (AppContext tyname name uni fun a) (SplitMatchContext tyname name uni fun a)
asNormalDatatypeMatch :: 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
name =
(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))
-> Prism
(AppContext tyname name uni fun a)
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a)
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism
SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
reconstructNormalDatatypeMatch
(\AppContext tyname name uni fun a
args -> case VarsInfo tyname name uni a
-> name
-> AppContext tyname name uni fun a
-> Maybe (SplitMatchContext tyname name uni fun a)
forall name tyname (uni :: * -> *) a fun.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
VarsInfo tyname name uni a
-> name
-> AppContext tyname name uni fun a
-> Maybe (SplitMatchContext tyname name uni fun a)
splitNormalDatatypeMatch VarsInfo tyname name uni a
vinfo name
name AppContext tyname name uni fun a
args of
{ Just SplitMatchContext tyname name uni fun a
sm -> SplitMatchContext tyname name uni fun a
-> Either
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a)
forall a b. b -> Either a b
Right SplitMatchContext tyname name uni fun a
sm; Maybe (SplitMatchContext tyname name uni fun a)
Nothing -> AppContext tyname name uni fun a
-> Either
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a)
forall a b. a -> Either a b
Left AppContext tyname name uni fun a
args; })