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 :: yes -> f (Reduced no yes)
yes yes
t          = (Simplification -> yes -> Reduced no yes)
-> yes -> Simplification -> Reduced no yes
forall a b c. (a -> b -> c) -> b -> a -> c
flip Simplification -> yes -> Reduced no yes
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction yes
t (Simplification -> Reduced no yes)
-> f Simplification -> f (Reduced no yes)
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 ArgName]
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 :: * -> *) yes no.
MonadTCEnv f =>
yes -> f (Reduced no yes)
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 ArgName -> Term -> Term) -> Term -> [Arg ArgName] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg ArgName -> Term -> Term
lam Term
t (Int -> [Arg ArgName] -> [Arg ArgName]
forall a. Int -> [a] -> [a]
drop Int
m [Arg ArgName]
xs)
        -- otherwise, just apply instantiation to body
        -- apply the result to any extra arguments
        | Bool
otherwise -> Term -> ReduceM (Reduced (Blocked Elims) Term)
forall (f :: * -> *) yes no.
MonadTCEnv f =>
yes -> f (Reduced no yes)
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 ArgName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg ArgName]
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 ArgName -> Term -> Term
lam Arg ArgName
x Term
t        = ArgInfo -> Abs Term -> Term
Lam (Arg ArgName -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg ArgName
x) (ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs (Arg ArgName -> ArgName
forall e. Arg e -> e
unArg Arg ArgName
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
$ ArgName
-> Int
-> ArgName
-> ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
traceSLn ArgName
"impossible" Int
10
        (ArgName
"Incomplete pattern matching when applying " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
f)
        ReduceM (Reduced (Blocked Elims) Term)
forall a. HasCallStack => a
__IMPOSSIBLE__