{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.CompiledClause.Match where
import qualified Data.Map as Map
import Agda.Interaction.Options (optRewriting)
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Monad hiding (constructorForm)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad as RedM
import Agda.TypeChecking.Substitute
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Impossible
matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
matchCompiled :: CompiledClauses
-> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
matchCompiled CompiledClauses
c MaybeReducedArgs
args = do
r <- CompiledClauses
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
matchCompiledE CompiledClauses
c (MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term))
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ (MaybeReduced (Arg Term) -> MaybeReduced Elim)
-> MaybeReducedArgs -> MaybeReducedElims
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Term -> Elim) -> MaybeReduced (Arg Term) -> MaybeReduced Elim
forall a b. (a -> b) -> MaybeReduced a -> MaybeReduced b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) MaybeReducedArgs
args
case r of
YesReduction Simplification
simpl Term
v -> Reduced (Blocked Args) Term
-> ReduceM (Reduced (Blocked Args) Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked Args) Term
-> ReduceM (Reduced (Blocked Args) Term))
-> Reduced (Blocked Args) Term
-> ReduceM (Reduced (Blocked Args) Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced (Blocked Args) Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
simpl Term
v
NoReduction Blocked Elims
bes -> Reduced (Blocked Args) Term
-> ReduceM (Reduced (Blocked Args) Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked Args) Term
-> ReduceM (Reduced (Blocked Args) Term))
-> Reduced (Blocked Args) Term
-> ReduceM (Reduced (Blocked Args) Term)
forall a b. (a -> b) -> a -> b
$ Blocked Args -> Reduced (Blocked Args) Term
forall no yes. no -> Reduced no yes
NoReduction (Blocked Args -> Reduced (Blocked Args) Term)
-> Blocked Args -> Reduced (Blocked Args) Term
forall a b. (a -> b) -> a -> b
$ (Elims -> Args) -> Blocked Elims -> Blocked Args
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Elim -> Arg Term) -> Elims -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Maybe (Arg Term) -> Arg Term
forall a. a -> Maybe a -> a
fromMaybe Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term)
-> (Elim -> Maybe (Arg Term)) -> Elim -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim)) Blocked Elims
bes
matchCompiledE :: 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)]
type Frame = (CompiledClauses, MaybeReducedElims, Elims -> Elims)
type Stack = [Frame]
match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' ((CompiledClauses
c, MaybeReducedElims
es, Elims -> Elims
patch) : Stack
stack) = do
let no :: (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
no Elims -> Blocked Elims
blocking MaybeReducedElims
es = Reduced (Blocked Elims) Term
-> ReduceM (Reduced (Blocked Elims) Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (Blocked Elims) Term
-> ReduceM (Reduced (Blocked Elims) Term))
-> Reduced (Blocked Elims) Term
-> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ Blocked Elims -> Reduced (Blocked Elims) Term
forall no yes. no -> Reduced no yes
NoReduction (Blocked Elims -> Reduced (Blocked Elims) Term)
-> Blocked Elims -> Reduced (Blocked Elims) Term
forall a b. (a -> b) -> a -> b
$ Elims -> Blocked Elims
blocking (Elims -> Blocked Elims) -> Elims -> Blocked Elims
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
patch (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$ (MaybeReduced Elim -> Elim) -> MaybeReducedElims -> Elims
forall a b. (a -> b) -> [a] -> [b]
map MaybeReduced Elim -> Elim
forall a. MaybeReduced a -> a
ignoreReduced MaybeReducedElims
es
yes :: b -> f (Reduced no b)
yes b
t = (Simplification -> b -> Reduced no b)
-> b -> Simplification -> Reduced no b
forall a b c. (a -> b -> c) -> b -> a -> c
flip Simplification -> b -> Reduced no b
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction b
t (Simplification -> Reduced no b)
-> f Simplification -> f (Reduced no b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Simplification) -> f Simplification
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Simplification
envSimplification
do
case CompiledClauses
c of
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 [Arg [Char]]
xs Term
t
| Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n -> Term -> ReduceM (Reduced (Blocked Elims) Term)
forall {f :: * -> *} {b} {no}.
MonadTCEnv f =>
b -> f (Reduced no b)
yes (Term -> ReduceM (Reduced (Blocked Elims) Term))
-> Term -> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (MaybeReducedElims -> Substitution' Term
toSubst MaybeReducedElims
es) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg [Char] -> Term -> Term
lam Term
t (Int -> [Arg [Char]] -> [Arg [Char]]
forall a. Int -> [a] -> [a]
drop Int
m [Arg [Char]]
xs)
| Bool
otherwise -> Term -> ReduceM (Reduced (Blocked Elims) Term)
forall {f :: * -> *} {b} {no}.
MonadTCEnv f =>
b -> f (Reduced no b)
yes (Term -> ReduceM (Reduced (Blocked Elims) Term))
-> Term -> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (MaybeReducedElims -> Substitution' Term
toSubst MaybeReducedElims
es0) Term
t Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` (MaybeReduced Elim -> Elim) -> MaybeReducedElims -> Elims
forall a b. (a -> b) -> [a] -> [b]
map MaybeReduced Elim -> Elim
forall a. MaybeReduced a -> a
ignoreReduced MaybeReducedElims
es1
where
n :: Int
n = [Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs
m :: Int
m = MaybeReducedElims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length MaybeReducedElims
es
toSubst :: MaybeReducedElims -> Substitution' Term
toSubst = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term)
-> (MaybeReducedElims -> [Term])
-> MaybeReducedElims
-> Substitution' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term])
-> (MaybeReducedElims -> [Term]) -> MaybeReducedElims -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MaybeReduced Elim -> Term) -> MaybeReducedElims -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term)
-> (MaybeReduced Elim -> Arg Term) -> MaybeReduced Elim -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Maybe (Arg Term) -> Arg Term
forall a. a -> Maybe a -> a
fromMaybe Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term)
-> (MaybeReduced Elim -> Maybe (Arg Term))
-> MaybeReduced Elim
-> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim (Elim -> Maybe (Arg Term))
-> (MaybeReduced Elim -> Elim)
-> MaybeReduced Elim
-> Maybe (Arg Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeReduced Elim -> Elim
forall a. MaybeReduced a -> a
ignoreReduced)
(MaybeReducedElims
es0, MaybeReducedElims
es1) = Int -> MaybeReducedElims -> (MaybeReducedElims, MaybeReducedElims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n MaybeReducedElims
es
lam :: Arg [Char] -> Term -> Term
lam Arg [Char]
x Term
t = ArgInfo -> Abs Term -> Term
Lam (Arg [Char] -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg [Char]
x) ([Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs (Arg [Char] -> [Char]
forall e. Arg e -> e
unArg Arg [Char]
x) Term
t)
Case (Arg ArgInfo
_ Int
n) Branches{etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch = Just (ConHead
c, WithArity CompiledClauses
cc), catchAllBranch :: forall c. Case c -> Maybe c
catchAllBranch = Maybe CompiledClauses
ca} ->
case Int -> MaybeReducedElims -> (MaybeReducedElims, MaybeReducedElims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n MaybeReducedElims
es of
(MaybeReducedElims
_, []) -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
no (NotBlocked' Term -> Elims -> Blocked Elims
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
Underapplied) MaybeReducedElims
es
(MaybeReducedElims
es0, MaybeRed IsReduced
_ e :: Elim
e@(Apply (Arg ArgInfo
_ Term
v0)) : MaybeReducedElims
es1) ->
let projs :: MaybeReducedElims
projs = [ IsReduced -> Elim -> MaybeReduced Elim
forall a. IsReduced -> a -> MaybeReduced a
MaybeRed IsReduced
NotReduced (Elim -> MaybeReduced Elim) -> Elim -> MaybeReduced Elim
forall a b. (a -> b) -> a -> b
$ Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare ArgInfo
ai (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
v0 Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f] | Arg ArgInfo
ai QName
f <- [Arg QName]
fs ]
catchAllFrame :: Stack -> Stack
catchAllFrame Stack
stack = Stack
-> (CompiledClauses -> Stack) -> Maybe CompiledClauses -> Stack
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Stack
stack (\CompiledClauses
c -> (CompiledClauses
c, MaybeReducedElims
es, Elims -> Elims
patch) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
-> Stack -> Stack
forall a. a -> [a] -> [a]
: Stack
stack) Maybe CompiledClauses
ca in
Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
-> Stack -> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ (WithArity CompiledClauses -> CompiledClauses
forall c. WithArity c -> c
content WithArity CompiledClauses
cc, MaybeReducedElims
es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
projs MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1, Elims -> Elims
patchEta) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
-> Stack -> Stack
forall a. a -> [a] -> [a]
: Stack -> Stack
catchAllFrame Stack
stack
where
fs :: [Arg QName]
fs = ConHead -> [Arg QName]
conFields ConHead
c
patchEta :: Elims -> Elims
patchEta Elims
es = Elims -> Elims
patch (Elims
es0 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim
e] Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es1)
where (Elims
es0, Elims
es') = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
(Elims
_, Elims
es1) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt ([Arg QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg QName]
fs) Elims
es'
(MaybeReducedElims, MaybeReducedElims)
_ -> ReduceM (Reduced (Blocked Elims) Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
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
(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
red Elim
e0 : MaybeReducedElims
es1) -> do
eb :: Blocked Elim <- do
case IsReduced
red of
Reduced Blocked ()
b -> Blocked Elim -> ReduceM (Blocked Elim)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Elim -> ReduceM (Blocked Elim))
-> Blocked Elim -> ReduceM (Blocked Elim)
forall a b. (a -> b) -> a -> b
$ Elim
e0 Elim -> Blocked () -> Blocked Elim
forall a b. a -> Blocked' Term b -> Blocked' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked ()
b
IsReduced
NotReduced -> Elim -> ReduceM (Blocked Elim)
unfoldCorecursionE Elim
e0
let e = Blocked Elim -> Elim
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Elim
eb
es' = MaybeReducedElims
es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
forall a. [a] -> [a] -> [a]
++ [IsReduced -> Elim -> MaybeReduced Elim
forall a. IsReduced -> a -> MaybeReduced a
MaybeRed (Blocked () -> IsReduced
Reduced (Blocked () -> IsReduced) -> Blocked () -> IsReduced
forall a b. (a -> b) -> a -> b
$ () () -> Blocked Elim -> Blocked ()
forall a b. a -> Blocked' Term b -> Blocked' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked Elim
eb) Elim
e] MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1
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)
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
conFrame ConHead
c ConInfo
ci Elims
vs Stack
stack = QName -> (Elims -> Term) -> Elims -> Stack -> Stack
conFrame' (ConHead -> QName
conName ConHead
c) (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
vs Stack
stack
conFrame' QName
q Elims -> Term
f Elims
vs Stack
stack =
case QName
-> Map QName (WithArity CompiledClauses)
-> Maybe (WithArity CompiledClauses)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
q (Case CompiledClauses -> Map QName (WithArity CompiledClauses)
forall c. Case c -> Map QName (WithArity c)
conBranches Case CompiledClauses
bs) of
Maybe (WithArity CompiledClauses)
Nothing -> Stack
stack
Just WithArity CompiledClauses
cc -> ( WithArity CompiledClauses -> CompiledClauses
forall c. WithArity c -> c
content WithArity CompiledClauses
cc
, MaybeReducedElims
es0 MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
forall a. [a] -> [a] -> [a]
++ (Elim -> MaybeReduced Elim) -> Elims -> MaybeReducedElims
forall a b. (a -> b) -> [a] -> [b]
map (IsReduced -> Elim -> MaybeReduced Elim
forall a. IsReduced -> a -> MaybeReduced a
MaybeRed IsReduced
NotReduced) Elims
vs MaybeReducedElims -> MaybeReducedElims -> MaybeReducedElims
forall a. [a] -> [a] -> [a]
++ MaybeReducedElims
es1
, (Elims -> Term) -> Int -> Elims -> Elims
patchCon Elims -> Term
f (Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
vs)
) (CompiledClauses, MaybeReducedElims, Elims -> Elims)
-> Stack -> Stack
forall a. a -> [a] -> [a]
: Stack
stack
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
patchLit Elims
es = Elims -> Elims
patch (Elims
es0 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim
e] Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es1)
where (Elims
es0, Elims
es1) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
patchCon Elims -> Term
f Int
m Elims
es = Elims -> Elims
patch (Elims
es0 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elims -> Term
f Elims
vs Term -> Elim -> Elim
forall a b. a -> Elim' b -> Elim' a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Elim
e] Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es2)
where (Elims
es0, Elims
rest) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
(Elims
es1, Elims
es2) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m Elims
rest
vs :: Elims
vs = Elims
es1
fallThrough <- return $ Just True == fallThrough bs && isJust (catchAllBranch bs)
let
isCon Blocked' t Elim
b =
case Blocked' t Elim -> Elim
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t Elim
b of
Apply Arg Term
a | c :: Term
c@Con{} <- Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
c
Elim
_ -> Maybe Term
forall a. Maybe a
Nothing
case eb of
NotBlocked NotBlocked' Term
_ (Apply (Arg ArgInfo
info v :: Term
v@(Lit Literal
l))) -> ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification (ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term))
-> ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ do
cv <- Term -> ReduceM Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v
let cFrame Stack
stack = case Term
cv of
Con ConHead
c ConInfo
ci Elims
vs -> ConHead -> ConInfo -> Elims -> Stack -> Stack
conFrame ConHead
c ConInfo
ci Elims
vs Stack
stack
Term
_ -> Stack
stack
match' $ litFrame l $ cFrame $ catchAllFrame stack
NotBlocked NotBlocked' Term
_ (Apply (Arg ArgInfo
info v :: Term
v@(Def QName
q Elims
vs))) | Just{} <- QName
-> Map QName (WithArity CompiledClauses)
-> Maybe (WithArity CompiledClauses)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
q (Case CompiledClauses -> Map QName (WithArity CompiledClauses)
forall c. Case c -> Map QName (WithArity c)
conBranches Case CompiledClauses
bs) -> ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification (ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term))
-> ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ do
Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
-> Stack -> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ QName -> (Elims -> Term) -> Elims -> Stack -> Stack
conFrame' QName
q (QName -> Elims -> Term
Def QName
q) Elims
vs (Stack -> Stack) -> Stack -> Stack
forall a b. (a -> b) -> a -> b
$ Stack -> Stack
catchAllFrame (Stack -> Stack) -> Stack -> Stack
forall a b. (a -> b) -> a -> b
$ Stack
stack
Blocked Elim
b | Just (Con ConHead
c ConInfo
ci Elims
vs) <- Blocked Elim -> Maybe Term
forall {t}. Blocked' t Elim -> Maybe Term
isCon Blocked Elim
b -> ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification (ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term))
-> ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$
Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
-> Stack -> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Stack -> Stack
conFrame ConHead
c ConInfo
ci Elims
vs (Stack -> Stack) -> Stack -> Stack
forall a b. (a -> b) -> a -> b
$ Stack -> Stack
catchAllFrame (Stack -> Stack) -> Stack -> Stack
forall a b. (a -> b) -> a -> b
$ Stack
stack
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
Blocked Elim
_ | Bool
fallThrough -> Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' (Stack -> ReduceM (Reduced (Blocked Elims) Term))
-> Stack -> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ Stack -> Stack
catchAllFrame (Stack -> Stack) -> Stack -> Stack
forall a b. (a -> b) -> a -> b
$ Stack
stack
Blocked Blocker
x Elim
_ -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
no (Blocker -> Elims -> Blocked Elims
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
x) MaybeReducedElims
es'
NotBlocked NotBlocked' Term
blocked Elim
e -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
no (NotBlocked' Term -> Elims -> Blocked Elims
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (NotBlocked' Term -> Elims -> Blocked Elims)
-> NotBlocked' Term -> Elims -> Blocked Elims
forall a b. (a -> b) -> a -> b
$ Elim -> NotBlocked' Term -> NotBlocked' Term
forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn Elim
e NotBlocked' Term
blocked) MaybeReducedElims
es'
match' [] =
ReduceM (Maybe QName)
-> ReduceM (Reduced (Blocked Elims) Term)
-> (QName -> ReduceM (Reduced (Blocked Elims) Term))
-> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM ((TCEnv -> Maybe QName) -> ReduceM (Maybe QName)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe QName
envAppDef) ReduceM (Reduced (Blocked Elims) Term)
forall a. HasCallStack => a
__IMPOSSIBLE__ ((QName -> ReduceM (Reduced (Blocked Elims) Term))
-> ReduceM (Reduced (Blocked Elims) Term))
-> (QName -> ReduceM (Reduced (Blocked Elims) Term))
-> ReduceM (Reduced (Blocked Elims) Term)
forall a b. (a -> b) -> a -> b
$ \ QName
f -> do
pds <- ReduceM (Set QName)
forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs
if f `elem` pds
then return (NoReduction $ NotBlocked (MissingClauses f) [])
else do
ifM (optRewriting <$> pragmaOptions)
(return (NoReduction $ NotBlocked ReallyNotBlocked []))
$ traceSLn "impossible" 10
("Incomplete pattern matching when applying " ++ prettyShow f)
__IMPOSSIBLE__