    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.CompiledClause.Match where

    import qualified Data.Map as Map

    import Agda.Interaction.Options (optRewriting)

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

    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Monad hiding (constructorForm)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Reduce.Monad as RedM
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Syntax.Common.Pretty (prettyShow)

    import Agda.Utils.Impossible

    matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
    matchCompiled :: CompiledClauses
    -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
    matchCompiled CompiledClauses
    c MaybeReducedArgs
    args = do
      r <- CompiledClauses
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    matchCompiledE CompiledClauses
    c (MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term))
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ (MaybeReduced (Arg Term) -> MaybeReduced Elim)
    -> MaybeReducedArgs -> MaybeReducedElims
    forall a b. (a -> b) -> [a] -> [b]
    map ((Arg Term -> Elim) -> MaybeReduced (Arg Term) -> MaybeReduced Elim
    forall a b. (a -> b) -> MaybeReduced a -> MaybeReduced b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply) MaybeReducedArgs
    args
      case r of
        YesReduction Simplification
    simpl Term
    v -> Reduced (Blocked Args) Term
    -> ReduceM (Reduced (Blocked Args) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Args) Term
     -> ReduceM (Reduced (Blocked Args) Term))
    -> Reduced (Blocked Args) Term
    -> ReduceM (Reduced (Blocked Args) Term)
    forall a b. (a -> b) -> a -> b
    $ Simplification -> Term -> Reduced (Blocked Args) Term
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    simpl Term
    v
        NoReduction Blocked Elims
    bes      -> Reduced (Blocked Args) Term
    -> ReduceM (Reduced (Blocked Args) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Args) Term
     -> ReduceM (Reduced (Blocked Args) Term))
    -> Reduced (Blocked Args) Term
    -> ReduceM (Reduced (Blocked Args) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Args -> Reduced (Blocked Args) Term
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked Args -> Reduced (Blocked Args) Term)
    -> Blocked Args -> Reduced (Blocked Args) Term
    forall a b. (a -> b) -> a -> b
    $ (Elims -> Args) -> Blocked Elims -> Blocked Args
    forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Elim -> Arg Term) -> Elims -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map (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)
    -> (Elim -> Maybe (Arg Term)) -> Elim -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim)) Blocked Elims
    bes

    -- | @matchCompiledE c es@ takes a function given by case tree @c@ and
    --   and a spine @es@ and tries to apply the function to @es@.
    matchCompiledE :: CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    matchCompiledE :: CompiledClauses
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    matchCompiledE CompiledClauses
    c MaybeReducedElims
    args = Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' [(CompiledClauses
    c, MaybeReducedElims
    args, Elims -> Elims
    forall a. a -> a
    id)]

    -- | A stack entry is a triple consisting of
    --   1. the part of the case tree to continue matching,
    --   2. the current argument vector, and
    --   3. a patch function taking the current argument vector back
    --      to the original argument vector.
    type Frame = (CompiledClauses, MaybeReducedElims, Elims -> Elims)
    type Stack = [Frame]

    -- | @match'@ tries to solve the matching problems on the @Stack@.
    --   In each iteration, the top problem is removed and handled.
    --
    --   If the top problem was a @Done@, we succeed.
    --
    --   If the top problem was a @Case n@ and the @n@th argument of the problem
    --   is not a constructor or literal, we are stuck, thus, fail.
    --
    --   If we have a branch for the constructor/literal, we put it on the stack
    --   to continue.
    --   If we do not have a branch, we fall through to the next problem, which
    --   should be the corresponding catch-all branch.
    --
    --   An empty stack is an exception that can come only from an incomplete
    --   function definition.

    -- TODO: literal/constructor pattern conflict (for Nat)

    match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' ((CompiledClauses
    c, MaybeReducedElims
    es, Elims -> Elims
    patch) : Stack
    stack) = do
      let no :: (Elims -> Blocked Elims)
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    no Elims -> Blocked Elims
    blocking MaybeReducedElims
    es = Reduced (Blocked Elims) Term
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced (Blocked Elims) Term
     -> ReduceM (Reduced (Blocked Elims) Term))
    -> Reduced (Blocked Elims) Term
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ Blocked Elims -> Reduced (Blocked Elims) Term
    forall no yes. no -> Reduced no yes
    NoReduction (Blocked Elims -> Reduced (Blocked Elims) Term)
    -> Blocked Elims -> Reduced (Blocked Elims) Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Blocked Elims
    blocking (Elims -> Blocked Elims) -> Elims -> Blocked Elims
    forall a b. (a -> b) -> a -> b
    $ Elims -> Elims
    patch (Elims -> Elims) -> Elims -> Elims
    forall a b. (a -> b) -> a -> b
    $ (MaybeReduced Elim -> Elim) -> MaybeReducedElims -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map MaybeReduced Elim -> Elim
    forall a. MaybeReduced a -> a
    ignoreReduced MaybeReducedElims
    es
          yes :: b -> f (Reduced no b)
    yes b
    t          = (Simplification -> b -> Reduced no b)
    -> b -> Simplification -> Reduced no b
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Simplification -> b -> Reduced no b
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction b
    t (Simplification -> Reduced no b)
    -> f Simplification -> f (Reduced no b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Simplification) -> f Simplification
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Simplification
    envSimplification

      do

        case CompiledClauses
    c of

          -- impossible case
          Fail{} -> (Elims -> Blocked Elims)
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    no (NotBlocked' Term -> Elims -> Blocked Elims
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    AbsurdMatch) MaybeReducedElims
    es

          -- done matching
          Done [Arg [Char]]
    xs Term
    t
            -- if the function was partially applied, return a lambda
            | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n     -> Term -> ReduceM (Reduced (Blocked Elims) Term)
    forall {f :: * -> *} {b} {no}.
    MonadTCEnv f =>
    b -> f (Reduced no b)
    yes (Term -> ReduceM (Reduced (Blocked Elims) Term))
    -> Term -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (MaybeReducedElims -> Substitution' Term
    toSubst MaybeReducedElims
    es) (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Arg [Char] -> Term -> Term
    lam Term
    t (Int -> [Arg [Char]] -> [Arg [Char]]
    forall a. Int -> [a] -> [a]
    drop Int
    m [Arg [Char]]
    xs)
            -- otherwise, just apply instantiation to body
            -- apply the result to any extra arguments
            | Bool
    otherwise -> Term -> ReduceM (Reduced (Blocked Elims) Term)
    forall {f :: * -> *} {b} {no}.
    MonadTCEnv f =>
    b -> f (Reduced no b)
    yes (Term -> ReduceM (Reduced (Blocked Elims) Term))
    -> Term -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (MaybeReducedElims -> Substitution' Term
    toSubst MaybeReducedElims
    es0) Term
    t Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` (MaybeReduced Elim -> Elim) -> MaybeReducedElims -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map MaybeReduced Elim -> Elim
    forall a. MaybeReduced a -> a
    ignoreReduced MaybeReducedElims
    es1
            where
              n :: Int
    n              = [Arg [Char]] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    xs
              m :: Int
    m              = MaybeReducedElims -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length MaybeReducedElims
    es
              -- at least the first @n@ elims must be @Apply@s, so we can
              -- turn them into a subsitution
              toSubst :: MaybeReducedElims -> Substitution' Term
    toSubst        = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term)
    -> (MaybeReducedElims -> [Term])
    -> MaybeReducedElims
    -> Substitution' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> [Term]
    forall a. [a] -> [a]
    reverse ([Term] -> [Term])
    -> (MaybeReducedElims -> [Term]) -> MaybeReducedElims -> [Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MaybeReduced Elim -> Term) -> MaybeReducedElims -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term)
    -> (MaybeReduced Elim -> Arg Term) -> MaybeReduced Elim -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . 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)
    -> (MaybeReduced Elim -> Maybe (Arg Term))
    -> MaybeReduced Elim
    -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim (Elim -> Maybe (Arg Term))
    -> (MaybeReduced Elim -> Elim)
    -> MaybeReduced Elim
    -> Maybe (Arg Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MaybeReduced Elim -> Elim
    forall a. MaybeReduced a -> a
    ignoreReduced)
              (MaybeReducedElims
    es0, MaybeReducedElims
    es1)     = Int -> MaybeReducedElims -> (MaybeReducedElims, MaybeReducedElims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n MaybeReducedElims
    es
              lam :: Arg [Char] -> Term -> Term
    lam Arg [Char]
    x Term
    t        = ArgInfo -> Abs Term -> Term
    Lam (Arg [Char] -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg [Char]
    x) ([Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    Abs (Arg [Char] -> [Char]
    forall e. Arg e -> e
    unArg Arg [Char]
    x) Term
    t)

          -- splitting on an eta-record constructor
          Case (Arg ArgInfo
    _ Int
    n) Branches{etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
    etaBranch = Just (ConHead
    c, WithArity CompiledClauses
    cc), catchallBranch :: forall c. Case c -> Maybe c
    catchallBranch = Maybe CompiledClauses
    ca} ->
            case Int -> MaybeReducedElims -> (MaybeReducedElims, MaybeReducedElims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n MaybeReducedElims
    es of
              (MaybeReducedElims
    _, []) -> (Elims -> Blocked Elims)
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    no (NotBlocked' Term -> Elims -> Blocked Elims
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    Underapplied) MaybeReducedElims
    es
              (MaybeReducedElims
    es0, MaybeRed IsReduced
    _ e :: Elim
    e@(Apply (Arg ArgInfo
    _ Term
    v0)) : MaybeReducedElims
    es1) ->
                  let projs :: MaybeReducedElims
    projs = [ IsReduced -> Elim -> MaybeReduced Elim
    forall a. IsReduced -> a -> MaybeReduced a
    MaybeRed IsReduced
    NotReduced (Elim -> MaybeReduced Elim) -> Elim -> MaybeReduced Elim
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Arg Term -> Elim
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Term
    forall a. LensRelevance a => a -> Term -> Term
    relToDontCare ArgInfo
    ai (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Term
    v0 Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f] | Arg ArgInfo
    ai QName
    f <- [Arg QName]
    fs ]
                      catchallFrame :: Stack -> Stack
    catchallFrame Stack
    stack = Stack
    -> (CompiledClauses -> Stack) -> Maybe CompiledClauses -> Stack
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Stack
    stack (\CompiledClauses
    c -> (CompiledClauses
    c, MaybeReducedElims
    es, Elims -> Elims
    patch) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
    -> Stack -> Stack
    forall a. a -> [a] -> [a]
    : Stack
    stack) Maybe CompiledClauses
    ca in
                  Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
    -> Stack -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ (WithArity CompiledClauses -> CompiledClauses
    forall c. WithArity c -> c
    content WithArity CompiledClauses
    cc, MaybeReducedElims
    es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ MaybeReducedElims
    projs MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ MaybeReducedElims
    es1, Elims -> Elims
    patchEta) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
    -> Stack -> Stack
    forall a. a -> [a] -> [a]
    : Stack -> Stack
    catchallFrame Stack
    stack
                where
                  fs :: [Arg QName]
    fs = ConHead -> [Arg QName]
    conFields ConHead
    c
                  patchEta :: Elims -> Elims
    patchEta Elims
    es = Elims -> Elims
    patch (Elims
    es0 Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elim
    e] Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es1)
                    where (Elims
    es0, Elims
    es') = Int -> Elims -> (Elims, Elims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n Elims
    es
                          (Elims
    _, Elims
    es1)   = Int -> Elims -> (Elims, Elims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt ([Arg QName] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg QName]
    fs) Elims
    es'
              (MaybeReducedElims, MaybeReducedElims)
    _ -> ReduceM (Reduced (Blocked Elims) Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          -- splitting on the @n@th elimination
          Case (Arg ArgInfo
    _ Int
    n) Case CompiledClauses
    bs -> do
            case Int -> MaybeReducedElims -> (MaybeReducedElims, MaybeReducedElims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n MaybeReducedElims
    es of
              -- if the @n@th elimination is not supplied, no match
              (MaybeReducedElims
    _, []) -> (Elims -> Blocked Elims)
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    no (NotBlocked' Term -> Elims -> Blocked Elims
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    Underapplied) MaybeReducedElims
    es
              -- if the @n@th elimination is @e0@
              (MaybeReducedElims
    es0, MaybeRed IsReduced
    red Elim
    e0 : MaybeReducedElims
    es1) -> do
                -- get the reduced form of @e0@
                eb :: Blocked Elim <- do
                      case IsReduced
    red of
                        Reduced Blocked ()
    b  -> Blocked Elim -> ReduceM (Blocked Elim)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Blocked Elim -> ReduceM (Blocked Elim))
    -> Blocked Elim -> ReduceM (Blocked Elim)
    forall a b. (a -> b) -> a -> b
    $ Elim
    e0 Elim -> Blocked () -> Blocked Elim
    forall a b. a -> Blocked' Term b -> Blocked' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Blocked ()
    b
                        IsReduced
    NotReduced -> Elim -> ReduceM (Blocked Elim)
    unfoldCorecursionE Elim
    e0
                let e = Blocked Elim -> Elim
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Elim
    eb
                    -- replace the @n@th argument by its reduced form
                    es' = MaybeReducedElims
    es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ [IsReduced -> Elim -> MaybeReduced Elim
    forall a. IsReduced -> a -> MaybeReduced a
    MaybeRed (Blocked () -> IsReduced
    Reduced (Blocked () -> IsReduced) -> Blocked () -> IsReduced
    forall a b. (a -> b) -> a -> b
    $ () () -> Blocked Elim -> Blocked ()
    forall a b. a -> Blocked' Term b -> Blocked' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Blocked Elim
    eb) Elim
    e] MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ MaybeReducedElims
    es1
                    -- if a catch-all clause exists, put it on the stack
                    catchallFrame Stack
    stack = Stack
    -> (CompiledClauses -> Stack) -> Maybe CompiledClauses -> Stack
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Stack
    stack (\CompiledClauses
    c -> (CompiledClauses
    c, MaybeReducedElims
    es', Elims -> Elims
    patch) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
    -> Stack -> Stack
    forall a. a -> [a] -> [a]
    : Stack
    stack) (Case CompiledClauses -> Maybe CompiledClauses
    forall c. Case c -> Maybe c
    catchallBranch Case CompiledClauses
    bs)
                    -- If our argument is @Lit l@, we push @litFrame l@ onto the stack.
                    litFrame Literal
    l Stack
    stack =
                      case Literal -> Map Literal CompiledClauses -> Maybe CompiledClauses
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Literal
    l (Case CompiledClauses -> Map Literal CompiledClauses
    forall c. Case c -> Map Literal c
    litBranches Case CompiledClauses
    bs) of
                        Maybe CompiledClauses
    Nothing -> Stack
    stack
                        Just CompiledClauses
    cc -> (CompiledClauses
    cc, MaybeReducedElims
    es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ MaybeReducedElims
    es1, Elims -> Elims
    patchLit) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
    -> Stack -> Stack
    forall a. a -> [a] -> [a]
    : Stack
    stack
                    -- If our argument (or its constructor form) is @Con c ci vs@
                    -- we push @conFrame c vs@ onto the stack.
                    conFrame ConHead
    c ConInfo
    ci Elims
    vs Stack
    stack = QName -> (Elims -> Term) -> Elims -> Stack -> Stack
    conFrame' (ConHead -> QName
    conName ConHead
    c) (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) Elims
    vs Stack
    stack
                    conFrame' QName
    q Elims -> Term
    f Elims
    vs Stack
    stack =
                      case QName
    -> Map QName (WithArity CompiledClauses)
    -> Maybe (WithArity CompiledClauses)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    q (Case CompiledClauses -> Map QName (WithArity CompiledClauses)
    forall c. Case c -> Map QName (WithArity c)
    conBranches Case CompiledClauses
    bs) of
                        Maybe (WithArity CompiledClauses)
    Nothing -> Stack
    stack
                        Just WithArity CompiledClauses
    cc -> ( WithArity CompiledClauses -> CompiledClauses
    forall c. WithArity c -> c
    content WithArity CompiledClauses
    cc
                                   , MaybeReducedElims
    es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ (Elim -> MaybeReduced Elim) -> Elims -> MaybeReducedElims
    forall a b. (a -> b) -> [a] -> [b]
    map (IsReduced -> Elim -> MaybeReduced Elim
    forall a. IsReduced -> a -> MaybeReduced a
    MaybeRed IsReduced
    NotReduced) Elims
    vs MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ MaybeReducedElims
    es1
                                   , (Elims -> Term) -> Int -> Elims -> Elims
    patchCon Elims -> Term
    f (Elims -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Elims
    vs)
                                   ) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
    -> Stack -> Stack
    forall a. a -> [a] -> [a]
    : Stack
    stack
                    -- If our argument is @Proj p@, we push @projFrame p@ onto the stack.
                    projFrame QName
    p Stack
    stack =
                      case QName
    -> Map QName (WithArity CompiledClauses)
    -> Maybe (WithArity CompiledClauses)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    p (Case CompiledClauses -> Map QName (WithArity CompiledClauses)
    forall c. Case c -> Map QName (WithArity c)
    conBranches Case CompiledClauses
    bs) of
                        Maybe (WithArity CompiledClauses)
    Nothing -> Stack
    stack
                        Just WithArity CompiledClauses
    cc -> (WithArity CompiledClauses -> CompiledClauses
    forall c. WithArity c -> c
    content WithArity CompiledClauses
    cc, MaybeReducedElims
    es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ MaybeReducedElims
    es1, Elims -> Elims
    patchLit) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
    -> Stack -> Stack
    forall a. a -> [a] -> [a]
    : Stack
    stack
                    -- The new patch function restores the @n@th argument to @v@:
                    -- In case we matched a literal, just put @v@ back.
                    patchLit Elims
    es = Elims -> Elims
    patch (Elims
    es0 Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elim
    e] Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es1)
                      where (Elims
    es0, Elims
    es1) = Int -> Elims -> (Elims, Elims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n Elims
    es
                    -- In case we matched constructor @c@ with @m@ arguments,
                    -- contract these @m@ arguments @vs@ to @Con c ci vs@.
    --                patchCon c ci m es = patch (es0 ++ [Con c ci vs <$ e] ++ es2)
                    patchCon Elims -> Term
    f Int
    m Elims
    es = Elims -> Elims
    patch (Elims
    es0 Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elims -> Term
    f Elims
    vs Term -> Elim -> Elim
    forall a b. a -> Elim' b -> Elim' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Elim
    e] Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es2)
                      where (Elims
    es0, Elims
    rest) = Int -> Elims -> (Elims, Elims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n Elims
    es
                            (Elims
    es1, Elims
    es2)  = Int -> Elims -> (Elims, Elims)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    m Elims
    rest
                            vs :: Elims
    vs          = Elims
    es1
                -- zo <- do
                --    mi <- getBuiltinName' builtinIZero
                --    mo <- getBuiltinName' builtinIOne
                --    return $ Set.fromList $ catMaybes [mi,mo]

                fallThrough <- return $ Just True == fallThrough bs && isJust (catchallBranch bs)

                let
                  isCon Blocked' t Elim
    b =
                    case Blocked' t Elim -> Elim
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked' t Elim
    b of
                     Apply Arg Term
    a | c :: Term
    c@Con{} <- Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    c
                     Elim
    _                            -> Maybe Term
    forall a. Maybe a
    Nothing
                -- Now do the matching on the @n@ths argument:
                case eb of
                  -- In case of a literal, try also its constructor form
                  NotBlocked NotBlocked' Term
    _ (Apply (Arg ArgInfo
    info v :: Term
    v@(Lit Literal
    l))) -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    performedSimplification (ReduceM (Reduced (Blocked Elims) Term)
     -> ReduceM (Reduced (Blocked Elims) Term))
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ do
                    cv <- Term -> ReduceM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm Term
    v
                    let cFrame Stack
    stack = case Term
    cv of
                          Con ConHead
    c ConInfo
    ci Elims
    vs -> ConHead -> ConInfo -> Elims -> Stack -> Stack
    conFrame ConHead
    c ConInfo
    ci Elims
    vs Stack
    stack
                          Term
    _        -> Stack
    stack
                    match' $ litFrame l $ cFrame $ catchallFrame stack

                  NotBlocked NotBlocked' Term
    _ (Apply (Arg ArgInfo
    info v :: Term
    v@(Def QName
    q Elims
    vs))) | Just{} <- QName
    -> Map QName (WithArity CompiledClauses)
    -> Maybe (WithArity CompiledClauses)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    q (Case CompiledClauses -> Map QName (WithArity CompiledClauses)
    forall c. Case c -> Map QName (WithArity c)
    conBranches Case CompiledClauses
    bs) -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    performedSimplification (ReduceM (Reduced (Blocked Elims) Term)
     -> ReduceM (Reduced (Blocked Elims) Term))
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ do
                    Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
    -> Stack -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> (Elims -> Term) -> Elims -> Stack -> Stack
    conFrame' QName
    q (QName -> Elims -> Term
    Def QName
    q) Elims
    vs (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack -> Stack
    catchallFrame (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack
    stack

                  -- In case of a constructor, push the conFrame
                  Blocked Elim
    b | Just (Con ConHead
    c ConInfo
    ci Elims
    vs) <- Blocked Elim -> Maybe Term
    forall {t}. Blocked' t Elim -> Maybe Term
    isCon Blocked Elim
    b -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    performedSimplification (ReduceM (Reduced (Blocked Elims) Term)
     -> ReduceM (Reduced (Blocked Elims) Term))
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $
                    Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
    -> Stack -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Stack -> Stack
    conFrame ConHead
    c ConInfo
    ci Elims
    vs (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack -> Stack
    catchallFrame (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack
    stack

                  -- In case of a projection, push the projFrame
                  NotBlocked NotBlocked' Term
    _ (Proj ProjOrigin
    _ QName
    p) -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    performedSimplification (ReduceM (Reduced (Blocked Elims) Term)
     -> ReduceM (Reduced (Blocked Elims) Term))
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $
                    Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
    -> Stack -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> Stack -> Stack
    projFrame QName
    p (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack
    stack -- catchallFrame $ stack
                    -- Issue #1986: no catch-all for copattern matching!

                  Blocked Elim
    _ | Bool
    fallThrough -> Stack -> ReduceM (Reduced (Blocked Elims) Term)
    match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
    -> Stack -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ Stack -> Stack
    catchallFrame (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack
    stack

                  Blocked Blocker
    x Elim
    _            -> (Elims -> Blocked Elims)
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    no (Blocker -> Elims -> Blocked Elims
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    x) MaybeReducedElims
    es'

                  -- Otherwise, we are stuck.  If we were stuck before,
                  -- we keep the old reason, otherwise we give reason StuckOn here.
                  NotBlocked NotBlocked' Term
    blocked Elim
    e -> (Elims -> Blocked Elims)
    -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
    no (NotBlocked' Term -> Elims -> Blocked Elims
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (NotBlocked' Term -> Elims -> Blocked Elims)
    -> NotBlocked' Term -> Elims -> Blocked Elims
    forall a b. (a -> b) -> a -> b
    $ Elim -> NotBlocked' Term -> NotBlocked' Term
    forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn Elim
    e NotBlocked' Term
    blocked) MaybeReducedElims
    es'

    -- If we reach the empty stack, then pattern matching was incomplete
    match' [] = {- new line here since __IMPOSSIBLE__ does not like the ' in match' -}
      ReduceM (Maybe QName)
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> (QName -> ReduceM (Reduced (Blocked Elims) Term))
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM ((TCEnv -> Maybe QName) -> ReduceM (Maybe QName)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe QName
    envAppDef) ReduceM (Reduced (Blocked Elims) Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((QName -> ReduceM (Reduced (Blocked Elims) Term))
     -> ReduceM (Reduced (Blocked Elims) Term))
    -> (QName -> ReduceM (Reduced (Blocked Elims) Term))
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall a b. (a -> b) -> a -> b
    $ \ QName
    f -> do
        pds <- ReduceM (Set QName)
    forall (m :: * -> *). ReadTCState m => m (Set QName)
    getPartialDefs
        if f `elem` pds
        then return (NoReduction $ NotBlocked (MissingClauses f) [])
        else do
          ifM (optRewriting <$> pragmaOptions)
          {-then-} (return (NoReduction $ NotBlocked ReallyNotBlocked [])) -- See #5396
          {-else-} $ traceSLn "impossible" 10
            ("Incomplete pattern matching when applying " ++ prettyShow f)
            __IMPOSSIBLE__