{-# LANGUAGE LambdaCase    #-}
{-# LANGUAGE RankNTypes    #-}
{-# LANGUAGE TupleSections #-}
-- | Datatypes representing 'contexts with holes' in Plutus IR terms.
--
-- Useful for focussing on a sub-part of a term and then reconstructing the term, but
-- with the context as a reified datatype that can be inspected and modified.
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

-- | A context for an iterated term/type application, with the hole at the head of the
-- application.
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

{- | Takes a term and views it as a head plus an 'AppContext', e.g.

@
    [{ f t } u v]
    -->
    (f, [{ _ t } u v])
    ==
    f (TypeAppContext t (TermAppContext u (TermAppContext v 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)

-- | Fills in the hole in an 'AppContext', the inverse of 'splitApplication'.
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

-- | Do the given arguments saturate the given arity?
saturates :: AppContext tyname name uni fun a -> Arity -> Maybe Saturation
-- Exactly right
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
-- Parameters left - undersaturated
saturates AppContext tyname name uni fun a
AppContextEnd Arity
_                              = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Undersaturated
-- Match a term parameter to a term arg
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
-- Match a type parameter to a type arg
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
-- Param/arg mismatch
saturates (TermAppContext{}) (Param
TypeParam:Arity
_)             = Maybe Saturation
forall a. Maybe a
Nothing
saturates (TypeAppContext{}) (Param
TermParam:Arity
_)             = Maybe Saturation
forall a. Maybe a
Nothing
-- Arguments left - undersaturated
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

-- | A split up version of the 'AppContext' for a datatype match, with the various
-- parts we might want to look at.
--
-- We have this datatype to make it easier to abstract over different ways that
-- a match might be constructed at the term level. For example, some builtin
-- "matchers" have the arguments in a different order to the matchers from normal
-- PIR datatypes.
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
  }

-- | Extract the type application arguments from an 'AppContext'.
-- Returns 'Nothing' if the context contains a TermAppContext.
-- See 'test_extractTyArgs'
extractTyArgs :: AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
extractTyArgs :: forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
extractTyArgs = 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)

-- | Split a normal datatype 'match'.
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
  -- Needs to be saturated otherwise we won't find the bits!
  , 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
  -- Split up the application into:
  -- 1. The initial datatype type instantiations
  -- 2. The scrutinee
  -- 3. The result type variable instantiation
  -- 4. The branches
  , (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

-- | Reconstruct a normal datatype 'match'.
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)

-- | Split a normal datatype 'match'.
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; })

{- Note [Context splitting in a recursive pass]
When writing a recursive pass that processes the whole program, you must be
a bit cautious when using a context split. The context split may traverse
part of the program, which will _also_ be traversed by the main recursive
traversal. This can lead to quadratic runtime.

This is usually okay for something like 'splitApplication', since it is
quadratic in the longest application in the program, which is usually not
significantly long.
-}