    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.Utils.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
      Reduced (Blocked Elims) Term
    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' Term))
    -> MaybeReducedArgs -> MaybeReducedElims
    forall a b. (a -> b) -> [a] -> [b]
    map ((Arg Term -> Elim' Term)
    -> MaybeReduced (Arg Term) -> MaybeReduced (Elim' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply) MaybeReducedArgs
    args
      case Reduced (Blocked Elims) Term
    r of
        YesReduction Simplification
    simpl Term
    v -> Reduced (Blocked Args) Term
    -> ReduceM (Reduced (Blocked Args) Term)
    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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Elim' Term -> 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' Term -> Maybe (Arg Term)) -> Elim' Term -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' Term -> 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 (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' Term) -> Elim' Term)
    -> MaybeReducedElims -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map MaybeReduced (Elim' Term) -> Elim' Term
    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 (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' Term) -> Elim' Term)
    -> MaybeReducedElims -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map MaybeReduced (Elim' Term) -> Elim' Term
    forall a. MaybeReduced a -> a
    ignoreReduced MaybeReducedElims
    es1
            where
              n :: Int
    n              = [Arg [Char]] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    xs
              m :: Int
    m              = MaybeReducedElims -> 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) -> 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' Term) -> Arg Term)
    -> MaybeReduced (Elim' Term)
    -> 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' Term) -> Maybe (Arg Term))
    -> MaybeReduced (Elim' Term)
    -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' Term -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim (Elim' Term -> Maybe (Arg Term))
    -> (MaybeReduced (Elim' Term) -> Elim' Term)
    -> MaybeReduced (Elim' Term)
    -> Maybe (Arg Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MaybeReduced (Elim' Term) -> Elim' Term
    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' Term
    e@(Apply (Arg ArgInfo
    _ Term
    v0)) : MaybeReducedElims
    es1) ->
                  let projs :: MaybeReducedElims
    projs = [ IsReduced -> Elim' Term -> MaybeReduced (Elim' Term)
    forall a. IsReduced -> a -> MaybeReduced a
    MaybeRed IsReduced
    NotReduced (Elim' Term -> MaybeReduced (Elim' Term))
    -> Elim' Term -> MaybeReduced (Elim' Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    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' Term
    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' Term
    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 (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' Term
    e0 : MaybeReducedElims
    es1) -> do
                -- get the reduced form of @e0@
                Blocked (Elim' Term)
    eb :: Blocked Elim <- do
                      case IsReduced
    red of
                        Reduced Blocked ()
    b  -> Blocked (Elim' Term) -> ReduceM (Blocked (Elim' Term))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Blocked (Elim' Term) -> ReduceM (Blocked (Elim' Term)))
    -> Blocked (Elim' Term) -> ReduceM (Blocked (Elim' Term))
    forall a b. (a -> b) -> a -> b
    $ Elim' Term
    e0 Elim' Term -> Blocked () -> Blocked (Elim' Term)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Blocked ()
    b
                        IsReduced
    NotReduced -> Elim' Term -> ReduceM (Blocked (Elim' Term))
    unfoldCorecursionE Elim' Term
    e0
                let e :: Elim' Term
    e = Blocked (Elim' Term) -> Elim' Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Elim' Term)
    eb
                    -- replace the @n@th argument by its reduced form
                    es' :: MaybeReducedElims
    es' = MaybeReducedElims
    es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
    forall a. [a] -> [a] -> [a]
    ++ [IsReduced -> Elim' Term -> MaybeReduced (Elim' Term)
    forall a. IsReduced -> a -> MaybeReduced a
    MaybeRed (Blocked () -> IsReduced
    Reduced (Blocked () -> IsReduced) -> Blocked () -> IsReduced
    forall a b. (a -> b) -> a -> b
    $ () () -> Blocked (Elim' Term) -> Blocked ()
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Blocked (Elim' Term)
    eb) Elim' Term
    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
    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 -> Stack -> 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 -> ConInfo -> Elims -> Stack -> 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 -> (Elims -> Term) -> Elims -> 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' Term -> MaybeReduced (Elim' Term))
    -> Elims -> MaybeReducedElims
    forall a b. (a -> b) -> [a] -> [b]
    map (IsReduced -> Elim' Term -> MaybeReduced (Elim' Term)
    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 (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 -> Stack -> 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 -> Elims
    patchLit Elims
    es = Elims -> Elims
    patch (Elims
    es0 Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elim' Term
    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) -> Int -> Elims -> Elims
    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' Term -> Elim' Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Elim' Term
    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]

                Bool
    fallThrough <- Bool -> ReduceM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> ReduceM Bool) -> Bool -> ReduceM Bool
    forall a b. (a -> b) -> a -> b
    $ (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Case CompiledClauses -> Maybe Bool
    forall c. Case c -> Maybe Bool
    fallThrough Case CompiledClauses
    bs) Bool -> Bool -> Bool
    && Maybe CompiledClauses -> Bool
    forall a. Maybe a -> Bool
    isJust (Case CompiledClauses -> Maybe CompiledClauses
    forall c. Case c -> Maybe c
    catchAllBranch Case CompiledClauses
    bs)

                let
                  isCon :: Blocked' t (Elim' Term) -> Maybe Term
    isCon Blocked' t (Elim' Term)
    b =
                    case Blocked' t (Elim' Term) -> Elim' Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked' t (Elim' Term)
    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' Term
    _                            -> Maybe Term
    forall a. Maybe a
    Nothing
                -- Now do the matching on the @n@ths argument:
                case Blocked (Elim' Term)
    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
                    Term
    cv <- Term -> ReduceM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm Term
    v
                    let cFrame :: Stack -> Stack
    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
                    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
    $ Literal -> Stack -> Stack
    litFrame Literal
    l (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack -> Stack
    cFrame (Stack -> Stack) -> Stack -> Stack
    forall a b. (a -> b) -> a -> b
    $ Stack -> Stack
    catchAllFrame Stack
    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' Term)
    b | Just (Con ConHead
    c ConInfo
    ci Elims
    vs) <- Blocked (Elim' Term) -> Maybe Term
    forall {t}. Blocked' t (Elim' Term) -> Maybe Term
    isCon Blocked (Elim' Term)
    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' Term)
    _ | 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' Term
    _            -> (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' Term
    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' Term -> NotBlocked' Term -> NotBlocked' Term
    forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn Elim' Term
    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
        Set QName
    pds <- ReduceM (Set QName)
    forall (m :: * -> *). ReadTCState m => m (Set QName)
    getPartialDefs
        if QName
    f QName -> Set QName -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Set QName
    pds
        then Reduced (Blocked Elims) Term
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (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
    $ NotBlocked' Term -> Elims -> Blocked Elims
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    MissingClauses [])
        else do
          ReduceM Bool
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (PragmaOptions -> Bool
    optRewriting (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
          {-then-} (Reduced (Blocked Elims) Term
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (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
    $ NotBlocked' Term -> Elims -> Blocked Elims
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked [])) -- See #5396
          {-else-} (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
    $ [Char]
    -> Int
    -> [Char]
    -> ReduceM (Reduced (Blocked Elims) Term)
    -> ReduceM (Reduced (Blocked Elims) Term)
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    traceSLn [Char]
    "impossible" Int
    10
            ([Char]
    "Incomplete pattern matching when applying " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    f)
            ReduceM (Reduced (Blocked Elims) Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__