module Agda.TypeChecking.CompiledClause.Match where
import qualified Data.Map as Map
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.Impossible
matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
matchCompiled :: CompiledClauses
-> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
matchCompiled c :: CompiledClauses
c args :: 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 simpl :: Simplification
simpl v :: 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 bes :: 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 :: CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
matchCompiledE :: CompiledClauses
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
matchCompiledE c :: CompiledClauses
c args :: 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' ((c :: CompiledClauses
c, es :: MaybeReducedElims
es, patch :: Elims -> Elims
patch) : stack :: Stack
stack) = do
let no :: (Elims -> no) -> MaybeReducedElims -> m (Reduced no yes)
no blocking :: Elims -> no
blocking es :: MaybeReducedElims
es = Reduced no yes -> m (Reduced no yes)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced no yes -> m (Reduced no yes))
-> Reduced no yes -> m (Reduced no yes)
forall a b. (a -> b) -> a -> b
$ no -> Reduced no yes
forall no yes. no -> Reduced no yes
NoReduction (no -> Reduced no yes) -> no -> Reduced no yes
forall a b. (a -> b) -> a -> b
$ Elims -> no
blocking (Elims -> no) -> Elims -> no
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 t :: 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
Fail -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) no yes.
Monad m =>
(Elims -> no) -> MaybeReducedElims -> m (Reduced no yes)
no (NotBlocked -> Elims -> Blocked Elims
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
AbsurdMatch) MaybeReducedElims
es
Done xs :: [Arg ArgName]
xs t :: Term
t
| 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' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> 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)
| 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' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> 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
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)
(es0 :: MaybeReducedElims
es0, es1 :: MaybeReducedElims
es1) = Int -> MaybeReducedElims -> (MaybeReducedElims, MaybeReducedElims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n MaybeReducedElims
es
lam :: Arg ArgName -> Term -> Term
lam x :: Arg ArgName
x t :: 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)
Case (Arg _ n :: Int
n) Branches{etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch = Just (c :: ConHead
c, cc :: 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
(_, []) -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) no yes.
Monad m =>
(Elims -> no) -> MaybeReducedElims -> m (Reduced no yes)
no (NotBlocked -> Elims -> Blocked Elims
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
Underapplied) MaybeReducedElims
es
(es0 :: MaybeReducedElims
es0, MaybeRed _ e :: Elim' Term
e@(Apply (Arg _ v0 :: Term
v0)) : es1 :: 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 ai :: ArgInfo
ai f :: QName
f <- [Arg QName]
fs ]
catchAllFrame :: Stack -> Stack
catchAllFrame stack :: Stack
stack = Stack
-> (CompiledClauses -> Stack) -> Maybe CompiledClauses -> Stack
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Stack
stack (\c :: 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 es :: 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 (es0 :: Elims
es0, es' :: Elims
es') = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
(_, es1 :: 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'
_ -> ReduceM (Reduced (Blocked Elims) Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
Case (Arg _ n :: Int
n) bs :: Case CompiledClauses
bs -> do
case Int -> MaybeReducedElims -> (MaybeReducedElims, MaybeReducedElims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n MaybeReducedElims
es of
(_, []) -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) no yes.
Monad m =>
(Elims -> no) -> MaybeReducedElims -> m (Reduced no yes)
no (NotBlocked -> Elims -> Blocked Elims
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
Underapplied) MaybeReducedElims
es
(es0 :: MaybeReducedElims
es0, MaybeRed red :: IsReduced
red e0 :: Elim' Term
e0 : es1 :: MaybeReducedElims
es1) -> do
Blocked (Elim' Term)
eb :: Blocked Elim <- do
case IsReduced
red of
Reduced b :: 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
NotReduced -> Elim' Term -> ReduceM (Blocked (Elim' Term))
unfoldCorecursionE Elim' Term
e0
let e :: Elim' Term
e = Blocked (Elim' Term) -> Elim' Term
forall t. Blocked t -> t
ignoreBlocking Blocked (Elim' Term)
eb
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
catchAllFrame :: Stack -> Stack
catchAllFrame stack :: Stack
stack = Stack
-> (CompiledClauses -> Stack) -> Maybe CompiledClauses -> Stack
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Stack
stack (\c :: 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 -> Stack -> Stack
litFrame l :: Literal
l stack :: 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
Nothing -> Stack
stack
Just cc :: 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 -> ConInfo -> Elims -> Stack -> Stack
conFrame c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs stack :: 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' q :: QName
q f :: Elims -> Term
f vs :: Elims
vs stack :: 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
Nothing -> Stack
stack
Just cc :: 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
projFrame :: QName -> Stack -> Stack
projFrame p :: QName
p stack :: 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
Nothing -> Stack
stack
Just cc :: 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 -> Elims
patchLit es :: 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 (es0 :: Elims
es0, es1 :: Elims
es1) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
patchCon :: (Elims -> Term) -> Int -> Elims -> Elims
patchCon f :: Elims -> Term
f m :: Int
m es :: 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 (es0 :: Elims
es0, rest :: Elims
rest) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Elims
es
(es1 :: Elims
es1, es2 :: Elims
es2) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m Elims
rest
vs :: Elims
vs = Elims
es1
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 -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (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 (Elim' Term) -> Maybe Term
isCon b :: Blocked (Elim' Term)
b =
case Blocked (Elim' Term) -> Elim' Term
forall t. Blocked t -> t
ignoreBlocking Blocked (Elim' Term)
b of
Apply a :: 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
_ -> Maybe Term
forall a. Maybe a
Nothing
ReduceM (Reduced (Blocked Elims) Term)
-> ReduceM (Reduced (Blocked Elims) Term)
forall a. a -> a
id (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
$
case Blocked (Elim' Term)
eb of
NotBlocked _ (Apply (Arg info :: ArgInfo
info v :: Term
v@(Lit l :: 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
stack = case Term
cv of
Con c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs -> ConHead -> ConInfo -> Elims -> Stack -> Stack
conFrame ConHead
c ConInfo
ci Elims
vs Stack
stack
_ -> 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 _ (Apply (Arg info :: ArgInfo
info v :: Term
v@(Def q :: QName
q vs :: 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
b :: Blocked (Elim' Term)
b | Just (Con c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs) <- Blocked (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
NotBlocked _ (Proj _ p :: 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
_ | 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 x :: MetaId
x _ -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) no yes.
Monad m =>
(Elims -> no) -> MaybeReducedElims -> m (Reduced no yes)
no (MetaId -> Elims -> Blocked Elims
forall t. MetaId -> t -> Blocked t
Blocked MetaId
x) MaybeReducedElims
es'
NotBlocked _ (Apply (Arg info :: ArgInfo
info (MetaV x :: MetaId
x _))) -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) no yes.
Monad m =>
(Elims -> no) -> MaybeReducedElims -> m (Reduced no yes)
no (MetaId -> Elims -> Blocked Elims
forall t. MetaId -> t -> Blocked t
Blocked MetaId
x) MaybeReducedElims
es'
NotBlocked blocked :: NotBlocked
blocked e :: Elim' Term
e -> (Elims -> Blocked Elims)
-> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
forall (m :: * -> *) no yes.
Monad m =>
(Elims -> no) -> MaybeReducedElims -> m (Reduced no yes)
no (NotBlocked -> Elims -> Blocked Elims
forall t. NotBlocked -> t -> Blocked t
NotBlocked (NotBlocked -> Elims -> Blocked Elims)
-> NotBlocked -> Elims -> Blocked Elims
forall a b. (a -> b) -> a -> b
$ Elim' Term -> NotBlocked -> NotBlocked
stuckOn Elim' Term
e NotBlocked
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
$ \ f :: 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 -> Elims -> Blocked Elims
forall t. NotBlocked -> t -> Blocked t
NotBlocked NotBlocked
MissingClauses [])
else do
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 "impossible" 10
("Incomplete pattern matching when applying " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Show a => a -> ArgName
show QName
f)
ReduceM (Reduced (Blocked Elims) Term)
forall a. HasCallStack => a
__IMPOSSIBLE__