{-# OPTIONS -Wunused-imports #-}

module Agda.TypeChecking.Coverage.SplitPattern
  ( SplitPattern, SplitPatVar(..)
  , fromSplitPattern, fromSplitPatterns, toSplitPatterns
  , toSplitPSubst, applySplitPSubst
  , isTrivialPattern
  ) where

import Prelude hiding ( null )

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty ( PrettyTCM(..) )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute

import Agda.Utils.Null
import Agda.Syntax.Common.Pretty ( Pretty(..), text, prettyList_ )
import Agda.Utils.Monad

import Agda.Utils.Impossible
import Agda.Syntax.Position (KillRange, killRange, killRangeN)

{-# SPECIALIZE isTrivialPattern :: Pattern' a -> TCM Bool #-}
-- | A pattern that matches anything (modulo eta).
isTrivialPattern :: (HasConstInfo m) => Pattern' a -> m Bool
isTrivialPattern :: forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
isTrivialPattern = \case
  VarP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  DotP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps -> [m Bool] -> m Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([m Bool] -> m Bool) -> [m Bool] -> m Bool
forall a b. (a -> b) -> a -> b
$ ((ConPatternInfo -> Bool
conPLazy ConPatternInfo
i Bool -> Bool -> Bool
||) (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaCon (ConHead -> QName
conName ConHead
c))
                      m Bool -> [m Bool] -> [m Bool]
forall a. a -> [a] -> [a]
: ((NamedArg (Pattern' a) -> m Bool)
-> [NamedArg (Pattern' a)] -> [m Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Bool
forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
isTrivialPattern (Pattern' a -> m Bool)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
  DefP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  LitP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  ProjP{}     -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  IApplyP{}   -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- | For each variable in the patterns of a split clause, we remember the
--   de Bruijn-index and the literals excluded by previous matches.

--  (See issue #708.)
data SplitPatVar = SplitPatVar
  { SplitPatVar -> PatVarName
splitPatVarName   :: PatVarName
  , SplitPatVar -> Int
splitPatVarIndex  :: Int
  , SplitPatVar -> [Literal]
splitExcludedLits :: [Literal]
  } deriving (Int -> SplitPatVar -> ShowS
[SplitPatVar] -> ShowS
SplitPatVar -> PatVarName
(Int -> SplitPatVar -> ShowS)
-> (SplitPatVar -> PatVarName)
-> ([SplitPatVar] -> ShowS)
-> Show SplitPatVar
forall a.
(Int -> a -> ShowS)
-> (a -> PatVarName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SplitPatVar -> ShowS
showsPrec :: Int -> SplitPatVar -> ShowS
$cshow :: SplitPatVar -> PatVarName
show :: SplitPatVar -> PatVarName
$cshowList :: [SplitPatVar] -> ShowS
showList :: [SplitPatVar] -> ShowS
Show)

instance Pretty SplitPatVar where
  prettyPrec :: Int -> SplitPatVar -> Doc
prettyPrec Int
_ SplitPatVar
x =
    PatVarName -> Doc
forall a. PatVarName -> Doc a
text (ShowS
patVarNameToString (SplitPatVar -> PatVarName
splitPatVarName SplitPatVar
x)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
    PatVarName -> Doc
forall a. PatVarName -> Doc a
text (PatVarName
"@" PatVarName -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> PatVarName
forall a. Show a => a -> PatVarName
show (SplitPatVar -> Int
splitPatVarIndex SplitPatVar
x)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
    [Literal] -> Doc -> ([Literal] -> Doc) -> Doc
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) Doc
forall a. Null a => a
empty (\[Literal]
lits ->
      Doc
"\\{" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Literal] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList_ [Literal]
lits Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"}")

instance PrettyTCM SplitPatVar where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitPatVar -> m Doc
prettyTCM = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (SplitPatVar -> Term) -> SplitPatVar -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var (Int -> Term) -> (SplitPatVar -> Int) -> SplitPatVar -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitPatVar -> Int
splitPatVarIndex

instance KillRange SplitPatVar where
  killRange :: KillRangeT SplitPatVar
killRange (SplitPatVar PatVarName
n Int
i [Literal]
lits) = (PatVarName -> Int -> [Literal] -> SplitPatVar)
-> PatVarName -> Int -> [Literal] -> SplitPatVar
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatVarName -> Int -> [Literal] -> SplitPatVar
SplitPatVar PatVarName
n Int
i [Literal]
lits

type SplitPattern = Pattern' SplitPatVar

toSplitVar :: DBPatVar -> SplitPatVar
toSplitVar :: DBPatVar -> SplitPatVar
toSplitVar DBPatVar
x = PatVarName -> Int -> [Literal] -> SplitPatVar
SplitPatVar (DBPatVar -> PatVarName
dbPatVarName DBPatVar
x) (DBPatVar -> Int
dbPatVarIndex DBPatVar
x) []

fromSplitVar :: SplitPatVar -> DBPatVar
fromSplitVar :: SplitPatVar -> DBPatVar
fromSplitVar SplitPatVar
x = PatVarName -> Int -> DBPatVar
DBPatVar (SplitPatVar -> PatVarName
splitPatVarName SplitPatVar
x) (SplitPatVar -> Int
splitPatVarIndex SplitPatVar
x)

instance DeBruijn SplitPatVar where
  deBruijnView :: SplitPatVar -> Maybe Int
deBruijnView SplitPatVar
x = DBPatVar -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (SplitPatVar -> DBPatVar
fromSplitVar SplitPatVar
x)
  deBruijnNamedVar :: PatVarName -> Int -> SplitPatVar
deBruijnNamedVar PatVarName
n Int
i = DBPatVar -> SplitPatVar
toSplitVar (PatVarName -> Int -> DBPatVar
forall a. DeBruijn a => PatVarName -> Int -> a
deBruijnNamedVar PatVarName
n Int
i)

toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns = ((NamedArg DeBruijnPattern -> NamedArg SplitPattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NamedArg DeBruijnPattern -> NamedArg SplitPattern)
 -> [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern])
-> ((DBPatVar -> SplitPatVar)
    -> NamedArg DeBruijnPattern -> NamedArg SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> [NamedArg DeBruijnPattern]
-> [NamedArg SplitPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ DeBruijnPattern -> Named_ SplitPattern)
-> NamedArg DeBruijnPattern -> NamedArg SplitPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ DeBruijnPattern -> Named_ SplitPattern)
 -> NamedArg DeBruijnPattern -> NamedArg SplitPattern)
-> ((DBPatVar -> SplitPatVar)
    -> Named_ DeBruijnPattern -> Named_ SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> NamedArg DeBruijnPattern
-> NamedArg SplitPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeBruijnPattern -> SplitPattern)
-> Named_ DeBruijnPattern -> Named_ SplitPattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DeBruijnPattern -> SplitPattern)
 -> Named_ DeBruijnPattern -> Named_ SplitPattern)
-> ((DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> Named_ DeBruijnPattern
-> Named_ SplitPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) DBPatVar -> SplitPatVar
toSplitVar

fromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern
fromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern
fromSplitPattern = ((Named_ SplitPattern -> Named_ DeBruijnPattern)
-> NamedArg SplitPattern -> NamedArg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ SplitPattern -> Named_ DeBruijnPattern)
 -> NamedArg SplitPattern -> NamedArg DeBruijnPattern)
-> ((SplitPatVar -> DBPatVar)
    -> Named_ SplitPattern -> Named_ DeBruijnPattern)
-> (SplitPatVar -> DBPatVar)
-> NamedArg SplitPattern
-> NamedArg DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitPattern -> DeBruijnPattern)
-> Named_ SplitPattern -> Named_ DeBruijnPattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SplitPattern -> DeBruijnPattern)
 -> Named_ SplitPattern -> Named_ DeBruijnPattern)
-> ((SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern)
-> (SplitPatVar -> DBPatVar)
-> Named_ SplitPattern
-> Named_ DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) SplitPatVar -> DBPatVar
fromSplitVar

fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns = (NamedArg SplitPattern -> NamedArg DeBruijnPattern)
-> [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg SplitPattern -> NamedArg DeBruijnPattern
fromSplitPattern

type SplitPSubstitution = Substitution' SplitPattern

toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
toSplitPSubst = ((DeBruijnPattern -> SplitPattern)
-> PatternSubstitution -> SplitPSubstitution
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DeBruijnPattern -> SplitPattern)
 -> PatternSubstitution -> SplitPSubstitution)
-> ((DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> PatternSubstitution
-> SplitPSubstitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) DBPatVar -> SplitPatVar
toSplitVar

fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst = ((SplitPattern -> DeBruijnPattern)
-> SplitPSubstitution -> PatternSubstitution
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SplitPattern -> DeBruijnPattern)
 -> SplitPSubstitution -> PatternSubstitution)
-> ((SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern)
-> (SplitPatVar -> DBPatVar)
-> SplitPSubstitution
-> PatternSubstitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) SplitPatVar -> DBPatVar
fromSplitVar

applySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst :: forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst = PatternSubstitution -> a -> a
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst (PatternSubstitution -> a -> a)
-> (SplitPSubstitution -> PatternSubstitution)
-> SplitPSubstitution
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitPSubstitution -> PatternSubstitution
fromSplitPSubst

-- TODO: merge this instance and the one for DeBruijnPattern in
-- Substitute.hs into one for Subst (Pattern' a) (Pattern' a).
instance Subst SplitPattern where
  type SubstArg SplitPattern = SplitPattern

  applySubst :: Substitution' (SubstArg SplitPattern)
-> SplitPattern -> SplitPattern
applySubst Substitution' (SubstArg SplitPattern)
IdS = SplitPattern -> SplitPattern
forall a. a -> a
id
  applySubst Substitution' (SubstArg SplitPattern)
rho = \case
    VarP PatternInfo
i SplitPatVar
x        ->
      PatternInfo -> SplitPattern -> SplitPattern
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      PatVarName -> SplitPattern -> SplitPattern
useName (SplitPatVar -> PatVarName
splitPatVarName SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      [Literal] -> SplitPattern -> SplitPattern
useExcludedLits (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      SplitPSubstitution -> Int -> SplitPattern
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho (Int -> SplitPattern) -> Int -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar -> Int
splitPatVarIndex SplitPatVar
x
    DotP PatternInfo
i Term
u        -> PatternInfo -> Term -> SplitPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i (Term -> SplitPattern) -> Term -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPSubstitution -> Term -> Term
forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho Term
u
    ConP ConHead
c ConPatternInfo
ci [NamedArg SplitPattern]
ps    -> ConHead
-> ConPatternInfo -> [NamedArg SplitPattern] -> SplitPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci ([NamedArg SplitPattern] -> SplitPattern)
-> [NamedArg SplitPattern] -> SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg SplitPattern])
Substitution' (SubstArg SplitPattern)
rho [NamedArg SplitPattern]
ps
    DefP PatternInfo
i QName
q [NamedArg SplitPattern]
ps     -> PatternInfo -> QName -> [NamedArg SplitPattern] -> SplitPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q ([NamedArg SplitPattern] -> SplitPattern)
-> [NamedArg SplitPattern] -> SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg SplitPattern])
Substitution' (SubstArg SplitPattern)
rho [NamedArg SplitPattern]
ps
    p :: SplitPattern
p@LitP{}        -> SplitPattern
p
    p :: SplitPattern
p@ProjP{}       -> SplitPattern
p
    IApplyP PatternInfo
i Term
l Term
r SplitPatVar
x ->
      Term -> Term -> SplitPattern -> SplitPattern
useEndPoints (SplitPSubstitution -> Term -> Term
forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho Term
l) (SplitPSubstitution -> Term -> Term
forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho Term
r) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      PatternInfo -> SplitPattern -> SplitPattern
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      PatVarName -> SplitPattern -> SplitPattern
useName (SplitPatVar -> PatVarName
splitPatVarName SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      [Literal] -> SplitPattern -> SplitPattern
useExcludedLits (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      SplitPSubstitution -> Int -> SplitPattern
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho (Int -> SplitPattern) -> Int -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar -> Int
splitPatVarIndex SplitPatVar
x

    where
      -- see Subst for DeBruijnPattern
      useEndPoints :: Term -> Term -> SplitPattern -> SplitPattern
      useEndPoints :: Term -> Term -> SplitPattern -> SplitPattern
useEndPoints Term
l Term
r (VarP PatternInfo
o SplitPatVar
x)        = PatternInfo -> Term -> Term -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
l Term
r SplitPatVar
x
      useEndPoints Term
l Term
r (IApplyP PatternInfo
o Term
_ Term
_ SplitPatVar
x) = PatternInfo -> Term -> Term -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
l Term
r SplitPatVar
x
      useEndPoints Term
l Term
r SplitPattern
x                 = SplitPattern
forall a. HasCallStack => a
__IMPOSSIBLE__

      useName :: PatVarName -> SplitPattern -> SplitPattern
      useName :: PatVarName -> SplitPattern -> SplitPattern
useName PatVarName
n (VarP PatternInfo
o SplitPatVar
x)
        | PatVarName -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (SplitPatVar -> PatVarName
splitPatVarName SplitPatVar
x)
        = PatternInfo -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (SplitPatVar -> SplitPattern) -> SplitPatVar -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar
x { splitPatVarName = n }
      useName PatVarName
_ SplitPattern
x = SplitPattern
x

      useExcludedLits :: [Literal] -> SplitPattern -> SplitPattern
      useExcludedLits :: [Literal] -> SplitPattern -> SplitPattern
useExcludedLits [Literal]
lits = \case
        (VarP PatternInfo
o SplitPatVar
x) -> PatternInfo -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (SplitPatVar -> SplitPattern) -> SplitPatVar -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar
x
          { splitExcludedLits = lits ++ splitExcludedLits x }
        SplitPattern
p -> SplitPattern
p