    {-| Given

        1. the function clauses @cs@
        2. the patterns @ps@ of the split clause

    we want to compute a variable index (in the split clause) to split on next.

    The matcher here checks whether the split clause is covered by one of
    the given clauses @cs@ or whether further splitting is needed (and
    when yes, where).
    -}

    module Agda.TypeChecking.Coverage.Match
      ( Match(..), match, matchClause
      , SplitPattern, SplitPatVar(..), fromSplitPatterns, toSplitPatterns
      , toSplitPSubst, applySplitPSubst
      , isTrivialPattern
      , BlockingVar(..), BlockingVars, BlockedOnResult(..)
      , setBlockingVarOverlap
      , ApplyOrIApply(..)
      ) where

    import Control.Monad.State

    import Prelude hiding ( null )

    import qualified Data.List as List
    import Data.Maybe (mapMaybe, fromMaybe)
    import Data.Semigroup ( Semigroup, (<>))

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

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

    import Agda.Utils.Null
    import Agda.Utils.Pretty ( Pretty(..), text, (<+>), cat , prettyList_ )
    import Agda.Utils.Monad

    import Agda.Utils.Impossible

    -- | If matching is inconclusive (@Block@) we want to know which
    --   variables or projections are blocking the match.
    data Match a
      = Yes a   -- ^ Matches unconditionally.
      | No      -- ^ Definitely does not match.
      | Block
        { forall a. Match a -> BlockedOnResult
    blockedOnResult :: BlockedOnResult
          -- ^ @BlockedOnProj o@ if the clause has a result split.
        , forall a. Match a -> BlockingVars
    blockedOnVars :: BlockingVars
          -- ^ @BlockingVar i cs ls o@ means variable @i@ is blocked on
          -- constructors @cs@ and literals @ls@.
        }
      deriving ((forall a b. (a -> b) -> Match a -> Match b)
    -> (forall a b. a -> Match b -> Match a) -> Functor Match
    forall a b. a -> Match b -> Match a
    forall a b. (a -> b) -> Match a -> Match b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Match b -> Match a
    $c<$ :: forall a b. a -> Match b -> Match a
    fmap :: forall a b. (a -> b) -> Match a -> Match b
    $cfmap :: forall a b. (a -> b) -> Match a -> Match b
    Functor)

    -- | Missing elimination blocking a match.
    data BlockedOnResult
      = BlockedOnProj      -- ^ Blocked on unsplit projection.
         { BlockedOnResult -> Bool
    blockedOnResultOverlap :: Bool
           -- ^ True if there are also matching clauses without an unsplit
           -- copattern.
         }
      | BlockedOnApply     -- ^ Blocked on unintroduced argument.
         { BlockedOnResult -> ApplyOrIApply
    blockedOnResultIApply :: ApplyOrIApply
           -- ^ Is the unintroduced argument an 'IApply' pattern?
         }
      | NotBlockedOnResult

    data ApplyOrIApply = IsApply | IsIApply

    -- | Variable blocking a match.
    data BlockingVar = BlockingVar
      { BlockingVar -> Nat
    blockingVarNo  :: Nat
        -- ^ De Bruijn index of variable blocking the match.
      , BlockingVar -> [ConHead]
    blockingVarCons :: [ConHead]
        -- ^ Constructors in this position.
      , BlockingVar -> [Literal]
    blockingVarLits :: [Literal]
        -- ^ Literals in this position.
      , BlockingVar -> Bool
    blockingVarOverlap :: Bool
        -- ^ True if at least one clause has a variable pattern in this
        --   position.
      , BlockingVar -> Bool
    blockingVarLazy :: Bool
        -- ^ True if at least one clause has a lazy pattern in this position.
      } deriving (Nat -> BlockingVar -> ShowS
    BlockingVars -> ShowS
    BlockingVar -> String
    (Nat -> BlockingVar -> ShowS)
    -> (BlockingVar -> String)
    -> (BlockingVars -> ShowS)
    -> Show BlockingVar
    forall a.
    (Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: BlockingVars -> ShowS
    $cshowList :: BlockingVars -> ShowS
    show :: BlockingVar -> String
    $cshow :: BlockingVar -> String
    showsPrec :: Nat -> BlockingVar -> ShowS
    $cshowsPrec :: Nat -> BlockingVar -> ShowS
    Show)

    type BlockingVars = [BlockingVar]

    -- | Substitution of 'SplitPattern's for de Bruijn indices in covering
    --   clause to match 'SplitClause'.
    type SplitInstantiation = [(Nat,SplitPattern)]

    -- | Match the given patterns against a list of clauses.
    --
    -- If successful, return the index of the covering clause.
    --
    match :: PureTCM m
          => [Clause]                           -- ^ Search for clause that covers the patterns.
          -> [NamedArg SplitPattern]            -- ^ Patterns of the current 'SplitClause'.
          -> m (Match (Nat, SplitInstantiation))
    match :: forall (m :: * -> *).
    PureTCM m =>
    [Clause]
    -> [NamedArg SplitPattern] -> m (Match (Nat, SplitInstantiation))
    match [Clause]
    cs [NamedArg SplitPattern]
    ps = (m (Match (Nat, SplitInstantiation))
     -> m (Match (Nat, SplitInstantiation))
     -> m (Match (Nat, SplitInstantiation)))
    -> m (Match (Nat, SplitInstantiation))
    -> [m (Match (Nat, SplitInstantiation))]
    -> m (Match (Nat, SplitInstantiation))
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr m (Match (Nat, SplitInstantiation))
    -> m (Match (Nat, SplitInstantiation))
    -> m (Match (Nat, SplitInstantiation))
    forall (m :: * -> *) a.
    Monad m =>
    m (Match a) -> m (Match a) -> m (Match a)
    choice (Match (Nat, SplitInstantiation)
    -> m (Match (Nat, SplitInstantiation))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Match (Nat, SplitInstantiation)
    forall a. Match a
    No) ([m (Match (Nat, SplitInstantiation))]
     -> m (Match (Nat, SplitInstantiation)))
    -> [m (Match (Nat, SplitInstantiation))]
    -> m (Match (Nat, SplitInstantiation))
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Clause -> m (Match (Nat, SplitInstantiation)))
    -> [Nat] -> [Clause] -> [m (Match (Nat, SplitInstantiation))]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> Clause -> m (Match (Nat, SplitInstantiation))
    forall (m :: * -> *).
    PureTCM m =>
    Nat -> Clause -> m (Match (Nat, SplitInstantiation))
    matchIt [Nat
    0..] [Clause]
    cs
      where
        matchIt :: PureTCM m
                => Nat  -- Clause number.
                -> Clause
                -> m (Match (Nat, SplitInstantiation))
        matchIt :: forall (m :: * -> *).
    PureTCM m =>
    Nat -> Clause -> m (Match (Nat, SplitInstantiation))
    matchIt Nat
    i Clause
    c = (SplitInstantiation -> (Nat, SplitInstantiation))
    -> Match SplitInstantiation -> Match (Nat, SplitInstantiation)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Nat
    i,) (Match SplitInstantiation -> Match (Nat, SplitInstantiation))
    -> m (Match SplitInstantiation)
    -> m (Match (Nat, SplitInstantiation))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg SplitPattern] -> Clause -> m (Match SplitInstantiation)
    forall (m :: * -> *).
    PureTCM m =>
    [NamedArg SplitPattern] -> Clause -> m (Match SplitInstantiation)
    matchClause [NamedArg SplitPattern]
    ps Clause
    c

    -- | 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 -> String
    splitPatVarName   :: PatVarName
      , SplitPatVar -> Nat
    splitPatVarIndex  :: Int
      , SplitPatVar -> [Literal]
    splitExcludedLits :: [Literal]
      } deriving (Nat -> SplitPatVar -> ShowS
    [SplitPatVar] -> ShowS
    SplitPatVar -> String
    (Nat -> SplitPatVar -> ShowS)
    -> (SplitPatVar -> String)
    -> ([SplitPatVar] -> ShowS)
    -> Show SplitPatVar
    forall a.
    (Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [SplitPatVar] -> ShowS
    $cshowList :: [SplitPatVar] -> ShowS
    show :: SplitPatVar -> String
    $cshow :: SplitPatVar -> String
    showsPrec :: Nat -> SplitPatVar -> ShowS
    $cshowsPrec :: Nat -> SplitPatVar -> ShowS
    Show)

    instance Pretty SplitPatVar where
      prettyPrec :: Nat -> SplitPatVar -> Doc
    prettyPrec Nat
    _ SplitPatVar
    x =
        String -> Doc
    text (ShowS
    patVarNameToString (SplitPatVar -> String
    splitPatVarName SplitPatVar
    x)) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <>
        String -> Doc
    text (String
    "@" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Nat -> String
    forall a. Show a => a -> String
    show (SplitPatVar -> Nat
    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
    prettyTCM (Term -> m Doc) -> (SplitPatVar -> Term) -> SplitPatVar -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Term
    var (Nat -> Term) -> (SplitPatVar -> Nat) -> SplitPatVar -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SplitPatVar -> Nat
    splitPatVarIndex

    type SplitPattern = Pattern' SplitPatVar

    toSplitVar :: DBPatVar -> SplitPatVar
    toSplitVar :: DBPatVar -> SplitPatVar
    toSplitVar DBPatVar
    x = String -> Nat -> [Literal] -> SplitPatVar
    SplitPatVar (DBPatVar -> String
    dbPatVarName DBPatVar
    x) (DBPatVar -> Nat
    dbPatVarIndex DBPatVar
    x) []

    fromSplitVar :: SplitPatVar -> DBPatVar
    fromSplitVar :: SplitPatVar -> DBPatVar
    fromSplitVar SplitPatVar
    x = String -> Nat -> DBPatVar
    DBPatVar (SplitPatVar -> String
    splitPatVarName SplitPatVar
    x) (SplitPatVar -> Nat
    splitPatVarIndex SplitPatVar
    x)

    instance DeBruijn SplitPatVar where
      deBruijnView :: SplitPatVar -> Maybe Nat
    deBruijnView SplitPatVar
    x = DBPatVar -> Maybe Nat
    forall a. DeBruijn a => a -> Maybe Nat
    deBruijnView (SplitPatVar -> DBPatVar
    fromSplitVar SplitPatVar
    x)
      debruijnNamedVar :: String -> Nat -> SplitPatVar
    debruijnNamedVar String
    n Nat
    i = DBPatVar -> SplitPatVar
    toSplitVar (String -> Nat -> DBPatVar
    forall a. DeBruijn a => String -> Nat -> a
    debruijnNamedVar String
    n Nat
    i)

    toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
    toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
    toSplitPatterns = ((NamedArg DeBruijnPattern -> NamedArg SplitPattern)
    -> [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
    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 NamedName DeBruijnPattern -> Named NamedName SplitPattern)
    -> NamedArg DeBruijnPattern -> NamedArg SplitPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName DeBruijnPattern -> Named NamedName SplitPattern)
     -> NamedArg DeBruijnPattern -> NamedArg SplitPattern)
    -> ((DBPatVar -> SplitPatVar)
        -> Named NamedName DeBruijnPattern -> Named NamedName SplitPattern)
    -> (DBPatVar -> SplitPatVar)
    -> NamedArg DeBruijnPattern
    -> NamedArg SplitPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DeBruijnPattern -> SplitPattern)
    -> Named NamedName DeBruijnPattern -> Named NamedName SplitPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((DeBruijnPattern -> SplitPattern)
     -> Named NamedName DeBruijnPattern -> Named NamedName SplitPattern)
    -> ((DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern)
    -> (DBPatVar -> SplitPatVar)
    -> Named NamedName DeBruijnPattern
    -> Named NamedName SplitPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) DBPatVar -> SplitPatVar
    toSplitVar

    fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
    fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
    fromSplitPatterns = ((NamedArg SplitPattern -> NamedArg DeBruijnPattern)
    -> [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((NamedArg SplitPattern -> NamedArg DeBruijnPattern)
     -> [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern])
    -> ((SplitPatVar -> DBPatVar)
        -> NamedArg SplitPattern -> NamedArg DeBruijnPattern)
    -> (SplitPatVar -> DBPatVar)
    -> [NamedArg SplitPattern]
    -> [NamedArg DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName SplitPattern -> Named NamedName DeBruijnPattern)
    -> NamedArg SplitPattern -> NamedArg DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName SplitPattern -> Named NamedName DeBruijnPattern)
     -> NamedArg SplitPattern -> NamedArg DeBruijnPattern)
    -> ((SplitPatVar -> DBPatVar)
        -> Named NamedName SplitPattern -> Named NamedName DeBruijnPattern)
    -> (SplitPatVar -> DBPatVar)
    -> NamedArg SplitPattern
    -> NamedArg DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SplitPattern -> DeBruijnPattern)
    -> Named NamedName SplitPattern -> Named NamedName DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((SplitPattern -> DeBruijnPattern)
     -> Named NamedName SplitPattern -> Named NamedName DeBruijnPattern)
    -> ((SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern)
    -> (SplitPatVar -> DBPatVar)
    -> Named NamedName SplitPattern
    -> Named NamedName DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) SplitPatVar -> DBPatVar
    fromSplitVar

    type SplitPSubstitution = Substitution' SplitPattern

    toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
    toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
    toSplitPSubst = ((DeBruijnPattern -> SplitPattern)
    -> PatternSubstitution -> SplitPSubstitution
    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 (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 (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 (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
    $
          String -> SplitPattern -> SplitPattern
    useName (SplitPatVar -> String
    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 -> Nat -> SplitPattern
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS SplitPSubstitution
    Substitution' (SubstArg SplitPattern)
    rho (Nat -> SplitPattern) -> Nat -> SplitPattern
    forall a b. (a -> b) -> a -> b
    $ SplitPatVar -> Nat
    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
    $
          String -> SplitPattern -> SplitPattern
    useName (SplitPatVar -> String
    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 -> Nat -> SplitPattern
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS SplitPSubstitution
    Substitution' (SubstArg SplitPattern)
    rho (Nat -> SplitPattern) -> Nat -> SplitPattern
    forall a b. (a -> b) -> a -> b
    $ SplitPatVar -> Nat
    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 :: String -> SplitPattern -> SplitPattern
    useName String
    n (VarP PatternInfo
    o SplitPatVar
    x)
            | String -> Bool
    forall a. Underscore a => a -> Bool
    isUnderscore (SplitPatVar -> String
    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 :: String
    splitPatVarName = String
    n }
          useName String
    _ 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 :: [Literal]
    splitExcludedLits = [Literal]
    lits [Literal] -> [Literal] -> [Literal]
    forall a. [a] -> [a] -> [a]
    ++ SplitPatVar -> [Literal]
    splitExcludedLits SplitPatVar
    x }
            SplitPattern
    p -> SplitPattern
    p

    -- | 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 (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
      DotP{}      -> Bool -> m Bool
    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 (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      LitP{}      -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      ProjP{}     -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      IApplyP{}   -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

    -- | If matching succeeds, we return the instantiation of the clause pattern vector
    --   to obtain the split clause pattern vector.
    type MatchResult = Match SplitInstantiation

    instance Pretty BlockingVar where
      pretty :: BlockingVar -> Doc
    pretty (BlockingVar Nat
    i [ConHead]
    cs [Literal]
    ls Bool
    o Bool
    l) = [Doc] -> Doc
    cat
        [ String -> Doc
    text (String
    "variable " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Nat -> String
    forall a. Show a => a -> String
    show Nat
    i)
        , if [ConHead] -> Bool
    forall a. Null a => a -> Bool
    null [ConHead]
    cs then Doc
    forall a. Null a => a
    empty else Doc
    " blocked on constructors" Doc -> Doc -> Doc
    <+> [ConHead] -> Doc
    forall a. Pretty a => a -> Doc
    pretty [ConHead]
    cs
        , if [Literal] -> Bool
    forall a. Null a => a -> Bool
    null [Literal]
    ls then Doc
    forall a. Null a => a
    empty else Doc
    " blocked on literals" Doc -> Doc -> Doc
    <+> [Literal] -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Literal]
    ls
        , if Bool
    o then Doc
    " (overlapping)" else Doc
    forall a. Null a => a
    empty
        , if Bool
    l then Doc
    " (lazy)" else Doc
    forall a. Null a => a
    empty
        ]

    yes :: Monad m => a -> m (Match a)
    yes :: forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes = Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> (a -> Match a) -> a -> m (Match a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Match a
    forall a. a -> Match a
    Yes

    no :: Monad m => m (Match a)
    no :: forall (m :: * -> *) a. Monad m => m (Match a)
    no = Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Match a
    forall a. Match a
    No

    blockedOnConstructor :: Monad m => Nat -> ConHead -> ConPatternInfo -> m (Match a)
    blockedOnConstructor :: forall (m :: * -> *) a.
    Monad m =>
    Nat -> ConHead -> ConPatternInfo -> m (Match a)
    blockedOnConstructor Nat
    i ConHead
    c ConPatternInfo
    ci = Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block BlockedOnResult
    NotBlockedOnResult [Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
    BlockingVar Nat
    i [ConHead
    c] [] Bool
    False (Bool -> BlockingVar) -> Bool -> BlockingVar
    forall a b. (a -> b) -> a -> b
    $ ConPatternInfo -> Bool
    conPLazy ConPatternInfo
    ci]

    blockedOnLiteral :: Monad m => Nat -> Literal -> m (Match a)
    blockedOnLiteral :: forall (m :: * -> *) a. Monad m => Nat -> Literal -> m (Match a)
    blockedOnLiteral Nat
    i Literal
    l = Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block BlockedOnResult
    NotBlockedOnResult [Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
    BlockingVar Nat
    i [] [Literal
    l] Bool
    False Bool
    False]

    blockedOnProjection :: Monad m => m (Match a)
    blockedOnProjection :: forall (m :: * -> *) a. Monad m => m (Match a)
    blockedOnProjection = Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block (Bool -> BlockedOnResult
    BlockedOnProj Bool
    False) []

    blockedOnApplication :: Monad m => ApplyOrIApply -> m (Match a)
    blockedOnApplication :: forall (m :: * -> *) a. Monad m => ApplyOrIApply -> m (Match a)
    blockedOnApplication ApplyOrIApply
    b = Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block (ApplyOrIApply -> BlockedOnResult
    BlockedOnApply ApplyOrIApply
    b) []
    --UNUSED Liang-Ting Chen 2019-07-16
    ---- | Lens for 'blockingVarCons'.
    --mapBlockingVarCons :: ([ConHead] -> [ConHead]) -> BlockingVar -> BlockingVar
    --mapBlockingVarCons f b = b { blockingVarCons = f (blockingVarCons b) }
    --
    ---- | Lens for 'blockingVarLits'.
    --mapBlockingVarLits :: ([Literal] -> [Literal]) -> BlockingVar -> BlockingVar
    --mapBlockingVarLits f b = b { blockingVarLits = f (blockingVarLits b) }

    setBlockingVarOverlap :: BlockingVar -> BlockingVar
    setBlockingVarOverlap :: BlockingVar -> BlockingVar
    setBlockingVarOverlap = \BlockingVar
    x -> BlockingVar
    x { blockingVarOverlap :: Bool
    blockingVarOverlap = Bool
    True }

    overlapping :: BlockingVars -> BlockingVars
    overlapping :: BlockingVars -> BlockingVars
    overlapping = (BlockingVar -> BlockingVar) -> BlockingVars -> BlockingVars
    forall a b. (a -> b) -> [a] -> [b]
    map BlockingVar -> BlockingVar
    setBlockingVarOverlap

    -- | Left dominant merge of blocking vars.
    zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
    zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
    zipBlockingVars BlockingVars
    xs BlockingVars
    ys = (BlockingVar -> BlockingVar) -> BlockingVars -> BlockingVars
    forall a b. (a -> b) -> [a] -> [b]
    map BlockingVar -> BlockingVar
    upd BlockingVars
    xs
      where
        upd :: BlockingVar -> BlockingVar
    upd (BlockingVar Nat
    x [ConHead]
    cons [Literal]
    lits Bool
    o Bool
    l) = case (BlockingVar -> Bool) -> BlockingVars -> Maybe BlockingVar
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Nat
    x Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Nat -> Bool) -> (BlockingVar -> Nat) -> BlockingVar -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BlockingVar -> Nat
    blockingVarNo) BlockingVars
    ys of
          Just (BlockingVar Nat
    _ [ConHead]
    cons' [Literal]
    lits' Bool
    o' Bool
    l') -> Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
    BlockingVar Nat
    x ([ConHead]
    cons [ConHead] -> [ConHead] -> [ConHead]
    forall a. [a] -> [a] -> [a]
    ++ [ConHead]
    cons') ([Literal]
    lits [Literal] -> [Literal] -> [Literal]
    forall a. [a] -> [a] -> [a]
    ++ [Literal]
    lits') (Bool
    o Bool -> Bool -> Bool
    || Bool
    o') (Bool
    l Bool -> Bool -> Bool
    || Bool
    l')
          Maybe BlockingVar
    Nothing -> Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
    BlockingVar Nat
    x [ConHead]
    cons [Literal]
    lits Bool
    True Bool
    l

    setBlockedOnResultOverlap :: BlockedOnResult -> BlockedOnResult
    setBlockedOnResultOverlap :: BlockedOnResult -> BlockedOnResult
    setBlockedOnResultOverlap BlockedOnResult
    b = case BlockedOnResult
    b of
      BlockedOnProj{}      -> BlockedOnResult
    b { blockedOnResultOverlap :: Bool
    blockedOnResultOverlap = Bool
    True }
      BlockedOnApply{}     -> BlockedOnResult
    b
      NotBlockedOnResult{} -> BlockedOnResult
    b

    anyBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    anyBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    anyBlockedOnResult BlockedOnResult
    b1 BlockedOnResult
    b2 = case (BlockedOnResult
    b1,BlockedOnResult
    b2) of
      (BlockedOnResult
    NotBlockedOnResult , BlockedOnResult
    b2                ) -> BlockedOnResult
    b2
      (BlockedOnResult
    b1                 , BlockedOnResult
    NotBlockedOnResult) -> BlockedOnResult
    b1
      (BlockedOnResult
    _                  , BlockedOnResult
    _                 ) -> BlockedOnResult
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Left dominant merge of `BlockedOnResult`.
    choiceBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    choiceBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    choiceBlockedOnResult BlockedOnResult
    b1 BlockedOnResult
    b2 = case (BlockedOnResult
    b1,BlockedOnResult
    b2) of
      (BlockedOnResult
    NotBlockedOnResult  , BlockedOnResult
    _                 ) -> BlockedOnResult
    NotBlockedOnResult
      (BlockedOnProj Bool
    o1    , BlockedOnProj Bool
    o2  ) -> Bool -> BlockedOnResult
    BlockedOnProj (Bool
    o1 Bool -> Bool -> Bool
    || Bool
    o2)
      (BlockedOnProj Bool
    _     , BlockedOnResult
    _                 ) -> Bool -> BlockedOnResult
    BlockedOnProj Bool
    True
      (BlockedOnApply ApplyOrIApply
    b    , BlockedOnResult
    _                 ) -> ApplyOrIApply -> BlockedOnResult
    BlockedOnApply ApplyOrIApply
    b

    -- | @choice m m'@ combines the match results @m@ of a function clause
    --   with the (already combined) match results $m'$ of the later clauses.
    --   It is for skipping clauses that definitely do not match ('No').
    --   It is left-strict, to be used with @foldr@.
    --   If one clause unconditionally matches ('Yes') we do not look further.
    choice :: Monad m => m (Match a) -> m (Match a) -> m (Match a)
    choice :: forall (m :: * -> *) a.
    Monad m =>
    m (Match a) -> m (Match a) -> m (Match a)
    choice m (Match a)
    m m (Match a)
    m' = m (Match a)
    m m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Yes a
    a -> a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes a
    a
      Block BlockedOnResult
    r BlockingVars
    xs -> m (Match a)
    m' m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Block BlockedOnResult
    s BlockingVars
    ys -> Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block (BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    choiceBlockedOnResult BlockedOnResult
    r BlockedOnResult
    s) (BlockingVars -> Match a) -> BlockingVars -> Match a
    forall a b. (a -> b) -> a -> b
    $ BlockingVars -> BlockingVars -> BlockingVars
    zipBlockingVars BlockingVars
    xs BlockingVars
    ys
        Yes a
    _      -> Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block (BlockedOnResult -> BlockedOnResult
    setBlockedOnResultOverlap BlockedOnResult
    r) (BlockingVars -> Match a) -> BlockingVars -> Match a
    forall a b. (a -> b) -> a -> b
    $ BlockingVars -> BlockingVars
    overlapping BlockingVars
    xs
        Match a
    No         -> Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block BlockedOnResult
    r BlockingVars
    xs
      Match a
    No    -> m (Match a)
    m'

    -- | @matchClause qs i c@ checks whether clause @c@
    --   covers a split clause with patterns @qs@.
    matchClause
      :: PureTCM m
      => [NamedArg SplitPattern]
         -- ^ Split clause patterns @qs@.
      -> Clause
         -- ^ Clause @c@ to cover split clause.
      -> m MatchResult
         -- ^ Result.
         --   If 'Yes' the instantiation @rs@ such that @(namedClausePats c)[rs] == qs@.
    matchClause :: forall (m :: * -> *).
    PureTCM m =>
    [NamedArg SplitPattern] -> Clause -> m (Match SplitInstantiation)
    matchClause [NamedArg SplitPattern]
    qs Clause
    c = [NamedArg DeBruijnPattern]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    (PureTCM m, DeBruijn a) =>
    [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    matchPats (Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    c) [NamedArg SplitPattern]
    qs

    -- | @matchPats ps qs@ checks whether a function clause with patterns
    --   @ps@ covers a split clause with patterns @qs@.
    --
    --   Issue #842 / #1986: This is accepted:
    --   @
    --     F : Bool -> Set1
    --     F true = Set
    --     F      = \ x -> Set
    --   @
    --   For the second clause, the split clause is @F false@,
    --   so there are more patterns in the split clause than
    --   in the considered clause.  These additional patterns
    --   are simply dropped by @zipWith@.  This will result
    --   in @mconcat []@ which is @Yes []@.

    matchPats
      :: (PureTCM m, DeBruijn a)
      => [NamedArg (Pattern' a)]
         -- ^ Clause pattern vector @ps@ (to cover split clause pattern vector).
      -> [NamedArg SplitPattern]
         -- ^ Split clause pattern vector @qs@ (to be covered by clause pattern vector).
      -> m MatchResult
         -- ^ Result.
         --   If 'Yes' the instantiation @rs@ such that @ps[rs] == qs@.
    matchPats :: forall (m :: * -> *) a.
    (PureTCM m, DeBruijn a) =>
    [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    matchPats [] [] = SplitInstantiation -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes []
    matchPats (NamedArg (Pattern' a)
    p:[NamedArg (Pattern' a)]
    ps) (NamedArg SplitPattern
    q:[NamedArg SplitPattern]
    qs) =
      Pattern' a -> SplitPattern -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    (PureTCM m, DeBruijn a) =>
    Pattern' a -> SplitPattern -> m (Match SplitInstantiation)
    matchPat (NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' a)
    p) (NamedArg SplitPattern -> SplitPattern
    forall a. NamedArg a -> a
    namedArg NamedArg SplitPattern
    q) m (Match SplitInstantiation)
    -> m (Match SplitInstantiation) -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    (Monad m, Semigroup a) =>
    m (Match a) -> m (Match a) -> m (Match a)
    `combine` [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    (PureTCM m, DeBruijn a) =>
    [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    matchPats [NamedArg (Pattern' a)]
    ps [NamedArg SplitPattern]
    qs

    -- Patterns left in split clause:
    -- Andreas, 2016-06-03, issue #1986:
    -- catch-all for copatterns is inconsistent as found by Ulf.
    -- Thus, if the split clause has copatterns left,
    -- the current (shorter) clause is not considered covering.
    matchPats [] qs :: [NamedArg SplitPattern]
    qs@(NamedArg SplitPattern
    _:[NamedArg SplitPattern]
    _) = case (NamedArg SplitPattern -> Maybe (ProjOrigin, AmbiguousQName))
    -> [NamedArg SplitPattern] -> [(ProjOrigin, AmbiguousQName)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe NamedArg SplitPattern -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP [NamedArg SplitPattern]
    qs of
      [] -> SplitInstantiation -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes [] -- no proj. patterns left
      [(ProjOrigin, AmbiguousQName)]
    _  -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no     -- proj. patterns left

    -- Patterns left in candidate clause:
    -- If the current clause has additional copatterns in
    -- comparison to the split clause, we should split on them.
    matchPats (NamedArg (Pattern' a)
    p:[NamedArg (Pattern' a)]
    ps) [] = case NamedArg (Pattern' a) -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP NamedArg (Pattern' a)
    p of
      Just{}  -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    blockedOnProjection
      Maybe (ProjOrigin, AmbiguousQName)
    Nothing -> ApplyOrIApply -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => ApplyOrIApply -> m (Match a)
    blockedOnApplication (case NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' a)
    p of IApplyP{} -> ApplyOrIApply
    IsIApply; Pattern' a
    _ -> ApplyOrIApply
    IsApply)

    -- | Combine results of checking whether function clause patterns
    --   covers split clause patterns.
    --
    --   'No' is dominant: if one function clause pattern is disjoint to
    --   the corresponding split clause pattern, then
    --   the whole clauses are disjoint.
    --
    --   'Yes' is neutral: for a match, all patterns have to match.
    --
    --   'Block' accumulates variables of the split clause
    --   that have to be instantiated (an projection names of copattern matches)
    --   to make the split clause an instance of the function clause.
    combine :: (Monad m, Semigroup a) => m (Match a) -> m (Match a) -> m (Match a)
    combine :: forall (m :: * -> *) a.
    (Monad m, Semigroup a) =>
    m (Match a) -> m (Match a) -> m (Match a)
    combine m (Match a)
    m m (Match a)
    m' = m (Match a)
    m m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Yes a
    a -> m (Match a)
    m' m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Yes a
    b -> a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes (a
    a a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    b)
          Match a
    y     -> Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Match a
    y
        Match a
    No    -> m (Match a)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        x :: Match a
    x@(Block BlockedOnResult
    r BlockingVars
    xs) -> m (Match a)
    m' m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Match a
    No    -> m (Match a)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
          Block BlockedOnResult
    s BlockingVars
    ys -> Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match a -> m (Match a)) -> Match a -> m (Match a)
    forall a b. (a -> b) -> a -> b
    $ BlockedOnResult -> BlockingVars -> Match a
    forall a. BlockedOnResult -> BlockingVars -> Match a
    Block (BlockedOnResult -> BlockedOnResult -> BlockedOnResult
    anyBlockedOnResult BlockedOnResult
    r BlockedOnResult
    s) (BlockingVars
    xs BlockingVars -> BlockingVars -> BlockingVars
    forall a. [a] -> [a] -> [a]
    ++ BlockingVars
    ys)
          Yes{} -> Match a -> m (Match a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Match a
    x

    -- | @matchPat p q@ checks whether a function clause pattern @p@
    --   covers a split clause pattern @q@.  There are three results:
    --
    --   1. @Yes rs@ means it covers, because @p@ is a variable pattern. @rs@ collects
    --      the instantiations of the variables in @p@ s.t. @p[rs] = q@.
    --
    --   2. @No@ means it does not cover.
    --
    --   3. @Block [x]@ means @p@ is a proper instance of @q@ and could become
    --      a cover if @q@ was split on variable @x@.

    matchPat
      :: (PureTCM m, DeBruijn a)
      => Pattern' a
         -- ^ Clause pattern @p@ (to cover split clause pattern).
      -> SplitPattern
         -- ^ Split clause pattern @q@ (to be covered by clause pattern).
      -> m MatchResult
         -- ^ Result.
         --   If 'Yes', also the instantiation @rs@ of the clause pattern variables
         --   to produce the split clause pattern, @p[rs] = q@.
    matchPat :: forall (m :: * -> *) a.
    (PureTCM m, DeBruijn a) =>
    Pattern' a -> SplitPattern -> m (Match SplitInstantiation)
    matchPat Pattern' a
    p SplitPattern
    q = case Pattern' a
    p of

      VarP PatternInfo
    _ a
    x   -> SplitInstantiation -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes [(Nat -> Maybe Nat -> Nat
    forall a. a -> Maybe a -> a
    fromMaybe Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (a -> Maybe Nat
    forall a. DeBruijn a => a -> Maybe Nat
    deBruijnView a
    x),SplitPattern
    q)]

      DotP{}   -> SplitInstantiation -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes []
      -- Jesper, 2014-11-04: putting 'Yes [q]' here triggers issue 1333.
      -- Not checking for trivial patterns should be safe here, as dot patterns are
      -- guaranteed to match if the rest of the pattern does, so some extra splitting
      -- on them doesn't change the reduction behaviour.

      p :: Pattern' a
    p@(LitP PatternInfo
    _ Literal
    l) -> case SplitPattern
    q of
        VarP PatternInfo
    _ SplitPatVar
    x -> if Literal
    l Literal -> [Literal] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` SplitPatVar -> [Literal]
    splitExcludedLits SplitPatVar
    x
                    then m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
                    else Nat -> Literal -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => Nat -> Literal -> m (Match a)
    blockedOnLiteral (SplitPatVar -> Nat
    splitPatVarIndex SplitPatVar
    x) Literal
    l
        SplitPattern
    _ -> SplitPattern -> m (Maybe Literal)
    forall (m :: * -> *) a.
    PureTCM m =>
    Pattern' a -> m (Maybe Literal)
    isLitP SplitPattern
    q m (Maybe Literal)
    -> (Maybe Literal -> m (Match SplitInstantiation))
    -> m (Match SplitInstantiation)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just Literal
    l' -> if Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l' then SplitInstantiation -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes [] else m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
          Maybe Literal
    Nothing -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no

      ProjP ProjOrigin
    _ QName
    d -> case SplitPattern
    q of
        ProjP ProjOrigin
    _ QName
    d' -> do
          QName
    d <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    d
          if QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' then SplitInstantiation -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes [] else m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        SplitPattern
    _          -> m (Match SplitInstantiation)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      IApplyP PatternInfo
    _ Term
    _ Term
    _ a
    x -> SplitInstantiation -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
    yes [(Nat -> Maybe Nat -> Nat
    forall a. a -> Maybe a -> a
    fromMaybe Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (a -> Maybe Nat
    forall a. DeBruijn a => a -> Maybe Nat
    deBruijnView a
    x),SplitPattern
    q)]

                               --    Issue #4179: If the inferred pattern is a literal
                               -- v  we need to turn it into a constructor pattern.
      ConP ConHead
    c ConPatternInfo
    ci [NamedArg (Pattern' a)]
    ps -> SplitPattern -> m SplitPattern
    forall (m :: * -> *) a.
    (MonadReduce m, DeBruijn a) =>
    Pattern' a -> m (Pattern' a)
    unDotP SplitPattern
    q m SplitPattern
    -> (SplitPattern -> m SplitPattern) -> m SplitPattern
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= SplitPattern -> m SplitPattern
    forall (m :: * -> *) a.
    HasBuiltins m =>
    Pattern' a -> m (Pattern' a)
    unLitP m SplitPattern
    -> (SplitPattern -> m (Match SplitInstantiation))
    -> m (Match SplitInstantiation)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        VarP PatternInfo
    _ SplitPatVar
    x -> Nat -> ConHead -> ConPatternInfo -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    Monad m =>
    Nat -> ConHead -> ConPatternInfo -> m (Match a)
    blockedOnConstructor (SplitPatVar -> Nat
    splitPatVarIndex SplitPatVar
    x) ConHead
    c ConPatternInfo
    ci
        ConP ConHead
    c' ConPatternInfo
    i [NamedArg SplitPattern]
    qs
          | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c'   -> [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    (PureTCM m, DeBruijn a) =>
    [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    matchPats [NamedArg (Pattern' a)]
    ps [NamedArg SplitPattern]
    qs
          | Bool
    otherwise -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        DotP PatternInfo
    o Term
    t  -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        DefP{}   -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        LitP{}    -> m (Match SplitInstantiation)
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- excluded by typing and unLitP
        ProjP{}   -> m (Match SplitInstantiation)
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- excluded by typing
        IApplyP PatternInfo
    _ Term
    _ Term
    _ SplitPatVar
    x -> Nat -> ConHead -> ConPatternInfo -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    Monad m =>
    Nat -> ConHead -> ConPatternInfo -> m (Match a)
    blockedOnConstructor (SplitPatVar -> Nat
    splitPatVarIndex SplitPatVar
    x) ConHead
    c ConPatternInfo
    ci

      DefP PatternInfo
    o QName
    c [NamedArg (Pattern' a)]
    ps -> SplitPattern -> m SplitPattern
    forall (m :: * -> *) a.
    (MonadReduce m, DeBruijn a) =>
    Pattern' a -> m (Pattern' a)
    unDotP SplitPattern
    q m SplitPattern
    -> (SplitPattern -> m (Match SplitInstantiation))
    -> m (Match SplitInstantiation)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        VarP PatternInfo
    _ SplitPatVar
    x -> m (Match SplitInstantiation)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- blockedOnConstructor (splitPatVarIndex x) c
        ConP ConHead
    c' ConPatternInfo
    i [NamedArg SplitPattern]
    qs -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        DotP PatternInfo
    o Term
    t  -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        LitP{}    -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        DefP PatternInfo
    o QName
    c' [NamedArg SplitPattern]
    qs
          | QName
    c QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    c'   -> [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    forall (m :: * -> *) a.
    (PureTCM m, DeBruijn a) =>
    [NamedArg (Pattern' a)]
    -> [NamedArg SplitPattern] -> m (Match SplitInstantiation)
    matchPats [NamedArg (Pattern' a)]
    ps [NamedArg SplitPattern]
    qs
          | Bool
    otherwise -> m (Match SplitInstantiation)
    forall (m :: * -> *) a. Monad m => m (Match a)
    no
        ProjP{}   -> m (Match SplitInstantiation)
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- excluded by typing
        IApplyP PatternInfo
    _ Term
    _ Term
    _ SplitPatVar
    x -> m (Match SplitInstantiation)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- blockedOnConstructor (splitPatVarIndex x) c

    -- | Unfold one level of a dot pattern to a proper pattern if possible.
    unDotP :: (MonadReduce m, DeBruijn a) => Pattern' a -> m (Pattern' a)
    unDotP :: forall (m :: * -> *) a.
    (MonadReduce m, DeBruijn a) =>
    Pattern' a -> m (Pattern' a)
    unDotP (DotP PatternInfo
    o Term
    v) = Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v m Term -> (Term -> m (Pattern' a)) -> m (Pattern' a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Var Nat
    i [] -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Nat -> Pattern' a
    forall a. DeBruijn a => Nat -> a
    deBruijnVar Nat
    i
      Con ConHead
    c ConInfo
    _ [Elim]
    vs -> do
        let ps :: [Arg (Named NamedName (Pattern' a))]
    ps = (Arg Term -> Arg (Named NamedName (Pattern' a)))
    -> [Arg Term] -> [Arg (Named NamedName (Pattern' a))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> Named NamedName (Pattern' a))
    -> Arg Term -> Arg (Named NamedName (Pattern' a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Term -> Named NamedName (Pattern' a))
     -> Arg Term -> Arg (Named NamedName (Pattern' a)))
    -> (Term -> Named NamedName (Pattern' a))
    -> Arg Term
    -> Arg (Named NamedName (Pattern' a))
    forall a b. (a -> b) -> a -> b
    $ Pattern' a -> Named NamedName (Pattern' a)
    forall a name. a -> Named name a
    unnamed (Pattern' a -> Named NamedName (Pattern' a))
    -> (Term -> Pattern' a) -> Term -> Named NamedName (Pattern' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatternInfo -> Term -> Pattern' a
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    o) ([Arg Term] -> [Arg (Named NamedName (Pattern' a))])
    -> [Arg Term] -> [Arg (Named NamedName (Pattern' a))]
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims [Elim]
    vs
        Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ ConHead
    -> ConPatternInfo
    -> [Arg (Named NamedName (Pattern' a))]
    -> Pattern' a
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    noConPatternInfo [Arg (Named NamedName (Pattern' a))]
    ps
      Lit Literal
    l -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ PatternInfo -> Literal -> Pattern' a
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP (PatOrigin -> [Name] -> PatternInfo
    PatternInfo PatOrigin
    PatODot []) Literal
    l
      Term
    v     -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
    unDotP Pattern' a
    p = Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p

    isLitP :: PureTCM m => Pattern' a -> m (Maybe Literal)
    isLitP :: forall (m :: * -> *) a.
    PureTCM m =>
    Pattern' a -> m (Maybe Literal)
    isLitP (LitP PatternInfo
    _ Literal
    l) = Maybe Literal -> m (Maybe Literal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Literal -> m (Maybe Literal))
    -> Maybe Literal -> m (Maybe Literal)
    forall a b. (a -> b) -> a -> b
    $ Literal -> Maybe Literal
    forall a. a -> Maybe a
    Just Literal
    l
    isLitP (DotP PatternInfo
    _ Term
    u) = Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u m Term -> (Term -> m (Maybe Literal)) -> m (Maybe Literal)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Lit Literal
    l -> Maybe Literal -> m (Maybe Literal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Literal -> m (Maybe Literal))
    -> Maybe Literal -> m (Maybe Literal)
    forall a b. (a -> b) -> a -> b
    $ Literal -> Maybe Literal
    forall a. a -> Maybe a
    Just Literal
    l
      Term
    _ -> Maybe Literal -> m (Maybe Literal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Literal -> m (Maybe Literal))
    -> Maybe Literal -> m (Maybe Literal)
    forall a b. (a -> b) -> a -> b
    $ Maybe Literal
    forall a. Maybe a
    Nothing
    isLitP (ConP ConHead
    c ConPatternInfo
    ci []) = do
      Con ConHead
    zero ConInfo
    _ [] <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinZero
      if ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    zero
        then Maybe Literal -> m (Maybe Literal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Literal -> m (Maybe Literal))
    -> Maybe Literal -> m (Maybe Literal)
    forall a b. (a -> b) -> a -> b
    $ Literal -> Maybe Literal
    forall a. a -> Maybe a
    Just (Literal -> Maybe Literal) -> Literal -> Maybe Literal
    forall a b. (a -> b) -> a -> b
    $ Integer -> Literal
    LitNat Integer
    0
        else Maybe Literal -> m (Maybe Literal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Literal
    forall a. Maybe a
    Nothing
    isLitP (ConP ConHead
    c ConPatternInfo
    ci [NamedArg (Pattern' a)
    a]) | NamedArg (Pattern' a) -> Bool
    forall a. LensHiding a => a -> Bool
    visible NamedArg (Pattern' a)
    a Bool -> Bool -> Bool
    && NamedArg (Pattern' a) -> Bool
    forall a. LensRelevance a => a -> Bool
    isRelevant NamedArg (Pattern' a)
    a = do
      Con ConHead
    suc ConInfo
    _ [] <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSuc
      if ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    suc
        then (Literal -> Literal) -> Maybe Literal -> Maybe Literal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Literal -> Literal
    inc (Maybe Literal -> Maybe Literal)
    -> m (Maybe Literal) -> m (Maybe Literal)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern' a -> m (Maybe Literal)
    forall (m :: * -> *) a.
    PureTCM m =>
    Pattern' a -> m (Maybe Literal)
    isLitP (NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' a)
    a)
        else Maybe Literal -> m (Maybe Literal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Literal
    forall a. Maybe a
    Nothing
      where
        inc :: Literal -> Literal
        inc :: Literal -> Literal
    inc (LitNat Integer
    n) = Integer -> Literal
    LitNat (Integer -> Literal) -> Integer -> Literal
    forall a b. (a -> b) -> a -> b
    $ Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
        inc Literal
    _ = Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    isLitP Pattern' a
    _ = Maybe Literal -> m (Maybe Literal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Literal
    forall a. Maybe a
    Nothing

    unLitP :: HasBuiltins m => Pattern' a -> m (Pattern' a)
    unLitP :: forall (m :: * -> *) a.
    HasBuiltins m =>
    Pattern' a -> m (Pattern' a)
    unLitP (LitP PatternInfo
    info l :: Literal
    l@(LitNat Integer
    n)) | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0 = do
      Con ConHead
    c ConInfo
    ci [Elim]
    es <- m Term -> m Term -> Term -> m Term
    forall (m :: * -> *).
    Applicative m =>
    m Term -> m Term -> Term -> m Term
    constructorForm' (Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinZero)
                                      (Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSuc)
                                      (Literal -> Term
    Lit Literal
    l)
      let toP :: Elim -> Arg (Pattern' a)
    toP (Apply (Arg ArgInfo
    i (Lit Literal
    l))) = ArgInfo -> Pattern' a -> Arg (Pattern' a)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (PatternInfo -> Literal -> Pattern' a
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP PatternInfo
    info Literal
    l)
          toP Elim
    _ = Arg (Pattern' a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          cpi :: ConPatternInfo
    cpi   = ConPatternInfo
    noConPatternInfo { conPInfo :: PatternInfo
    conPInfo = PatternInfo
    info }
      Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    cpi ([NamedArg (Pattern' a)] -> Pattern' a)
    -> [NamedArg (Pattern' a)] -> Pattern' a
    forall a b. (a -> b) -> a -> b
    $ (Elim -> NamedArg (Pattern' a))
    -> [Elim] -> [NamedArg (Pattern' a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern' a -> Named NamedName (Pattern' a))
    -> Arg (Pattern' a) -> NamedArg (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' a -> Named NamedName (Pattern' a)
    forall a name. a -> Named name a
    unnamed (Arg (Pattern' a) -> NamedArg (Pattern' a))
    -> (Elim -> Arg (Pattern' a)) -> Elim -> NamedArg (Pattern' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim -> Arg (Pattern' a)
    toP) [Elim]
    es
    unLitP Pattern' a
    p = Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p