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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args
  case Reduced (Blocked Elims) Term
r of
    YesReduction Simplification
simpl Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl Term
v
    NoReduction Blocked Elims
bes      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ Elims -> Blocked Elims
blocking forall a b. (a -> b) -> a -> b
$ Elims -> Elims
patch forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. MaybeReduced a -> a
ignoreReduced MaybeReducedElims
es
      yes :: b -> f (Reduced no b)
yes b
t          = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall no yes. Simplification -> yes -> Reduced no yes
YesReduction b
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked 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 forall a. Ord a => a -> a -> Bool
< Int
n     -> forall {f :: * -> *} {b} {no}.
MonadTCEnv f =>
b -> f (Reduced no b)
yes forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (MaybeReducedElims -> Substitution' Term
toSubst MaybeReducedElims
es) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg [Char] -> Term -> Term
lam Term
t (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 -> forall {f :: * -> *} {b} {no}.
MonadTCEnv f =>
b -> f (Reduced no b)
yes forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (MaybeReducedElims -> Substitution' Term
toSubst MaybeReducedElims
es0) Term
t forall t. Apply t => t -> Elims -> t
`applyE` forall a b. (a -> b) -> [a] -> [b]
map forall a. MaybeReduced a -> a
ignoreReduced MaybeReducedElims
es1
        where
          n :: Int
n              = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs
          m :: Int
m              = 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        = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Elim' a -> Maybe (Arg a)
isApplyElim forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. MaybeReduced a -> a
ignoreReduced)
          (MaybeReducedElims
es0, MaybeReducedElims
es1)     = 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 (forall e. Arg e -> ArgInfo
argInfo Arg [Char]
x) (forall a. [Char] -> a -> Abs a
Abs (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 forall a. Int -> [a] -> ([a], [a])
splitAt Int
n MaybeReducedElims
es of
          (MaybeReducedElims
_, []) -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
no (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked 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 = [ forall a. IsReduced -> a -> MaybeReduced a
MaybeRed IsReduced
NotReduced forall a b. (a -> b) -> a -> b
$ forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Term -> Term
relToDontCare ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Term
v0 forall t. Apply t => t -> Elims -> t
`applyE` [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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Stack
stack (\CompiledClauses
c -> (CompiledClauses
c, MaybeReducedElims
es, Elims -> Elims
patch) forall a. a -> [a] -> [a]
: Stack
stack) Maybe CompiledClauses
ca in
              Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' forall a b. (a -> b) -> a -> b
$ (forall c. WithArity c -> c
content WithArity CompiledClauses
cc, MaybeReducedElims
es0 forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
projs forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1, Elims -> Elims
patchEta) 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 forall a. [a] -> [a] -> [a]
++ [Elim' Term
e] forall a. [a] -> [a] -> [a]
++ Elims
es1)
                where (Elims
es0, Elims
es') = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
                      (Elims
_, Elims
es1)   = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg QName]
fs) Elims
es'
          (MaybeReducedElims, MaybeReducedElims)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

      -- splitting on the @n@th elimination
      Case (Arg ArgInfo
_ Int
n) Case CompiledClauses
bs -> do
        case 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 (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked 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  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Elim' Term
e0 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 = 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 forall a. [a] -> [a] -> [a]
++ [forall a. IsReduced -> a -> MaybeReduced a
MaybeRed (Blocked () -> IsReduced
Reduced forall a b. (a -> b) -> a -> b
$ () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked (Elim' Term)
eb) Elim' Term
e] forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1
                -- if a catch-all clause exists, put it on the stack
                catchAllFrame :: Stack -> Stack
catchAllFrame Stack
stack = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Stack
stack (\CompiledClauses
c -> (CompiledClauses
c, MaybeReducedElims
es', Elims -> Elims
patch) forall a. a -> [a] -> [a]
: Stack
stack) (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 forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Literal
l (forall c. Case c -> Map Literal c
litBranches Case CompiledClauses
bs) of
                    Maybe CompiledClauses
Nothing -> Stack
stack
                    Just CompiledClauses
cc -> (CompiledClauses
cc, MaybeReducedElims
es0 forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1, Elims -> Elims
patchLit) 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 forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
q (forall c. Case c -> Map QName (WithArity c)
conBranches Case CompiledClauses
bs) of
                    Maybe (WithArity CompiledClauses)
Nothing -> Stack
stack
                    Just WithArity CompiledClauses
cc -> ( forall c. WithArity c -> c
content WithArity CompiledClauses
cc
                               , MaybeReducedElims
es0 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. IsReduced -> a -> MaybeReduced a
MaybeRed IsReduced
NotReduced) Elims
vs forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1
                               , (Elims -> Term) -> Int -> Elims -> Elims
patchCon Elims -> Term
f (forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
vs)
                               ) 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 forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
p (forall c. Case c -> Map QName (WithArity c)
conBranches Case CompiledClauses
bs) of
                    Maybe (WithArity CompiledClauses)
Nothing -> Stack
stack
                    Just WithArity CompiledClauses
cc -> (forall c. WithArity c -> c
content WithArity CompiledClauses
cc, MaybeReducedElims
es0 forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1, Elims -> Elims
patchLit) 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 forall a. [a] -> [a] -> [a]
++ [Elim' Term
e] forall a. [a] -> [a] -> [a]
++ Elims
es1)
                  where (Elims
es0, Elims
es1) = 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 forall a. [a] -> [a] -> [a]
++ [Elims -> Term
f Elims
vs forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Elim' Term
e] forall a. [a] -> [a] -> [a]
++ Elims
es2)
                  where (Elims
es0, Elims
rest) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
                        (Elims
es1, Elims
es2)  = 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 <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (forall a. a -> Maybe a
Just Bool
True forall a. Eq a => a -> a -> Bool
==) (forall c. Case c -> Maybe Bool
fallThrough Case CompiledClauses
bs) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isJust (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 forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t (Elim' Term)
b of
                 Apply Arg Term
a | c :: Term
c@Con{} <- forall e. Arg e -> e
unArg Arg Term
a -> forall a. a -> Maybe a
Just Term
c
                 Elim' 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))) -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification forall a b. (a -> b) -> a -> b
$ do
                Term
cv <- 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' forall a b. (a -> b) -> a -> b
$ Literal -> Stack -> Stack
litFrame Literal
l forall a b. (a -> b) -> a -> b
$ Stack -> Stack
cFrame 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{} <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
q (forall c. Case c -> Map QName (WithArity c)
conBranches Case CompiledClauses
bs) -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification forall a b. (a -> b) -> a -> b
$ do
                Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' forall a b. (a -> b) -> a -> b
$ QName -> (Elims -> Term) -> Elims -> Stack -> Stack
conFrame' QName
q (QName -> Elims -> Term
Def QName
q) Elims
vs forall a b. (a -> b) -> a -> b
$ Stack -> Stack
catchAllFrame 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) <- forall {t}. Blocked' t (Elim' Term) -> Maybe Term
isCon Blocked (Elim' Term)
b -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification forall a b. (a -> b) -> a -> b
$
                Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Stack -> Stack
conFrame ConHead
c ConInfo
ci Elims
vs forall a b. (a -> b) -> a -> b
$ Stack -> Stack
catchAllFrame forall a b. (a -> b) -> a -> b
$ Stack
stack

              -- In case of a projection, push the projFrame
              NotBlocked NotBlocked' Term
_ (Proj ProjOrigin
_ QName
p) -> forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification forall a b. (a -> b) -> a -> b
$
                Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' forall a b. (a -> b) -> a -> b
$ QName -> Stack -> Stack
projFrame QName
p 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' forall a b. (a -> b) -> a -> b
$ Stack -> Stack
catchAllFrame forall a b. (a -> b) -> a -> b
$ Stack
stack

              Blocked Blocker
x Elim' Term
_            -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
no (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 (forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall a b. (a -> b) -> a -> b
$ 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' -}
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe QName
envAppDef) forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ QName
f -> do
    Set QName
pds <- forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs
    if QName
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set QName
pds
    then forall (m :: * -> *) a. Monad m => a -> m a
return (forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (forall t. QName -> NotBlocked' t
MissingClauses QName
f) [])
    else do
      forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optRewriting forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
      {-then-} (forall (m :: * -> *) a. Monad m => a -> m a
return (forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked forall t. NotBlocked' t
ReallyNotBlocked [])) -- See #5396
      {-else-} forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
traceSLn [Char]
"impossible" Int
10
        ([Char]
"Incomplete pattern matching when applying " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
f)
        forall a. HasCallStack => a
__IMPOSSIBLE__