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 c args = do
r <- matchCompiledE c $ map (fmap Apply) args
case r of
YesReduction simpl v -> return $ YesReduction simpl v
NoReduction bes -> return $ NoReduction $ fmap (map (fromMaybe __IMPOSSIBLE__ . isApplyElim)) bes
matchCompiledE :: CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
matchCompiledE c args = match' [(c, args, id)]
type Frame = (CompiledClauses, MaybeReducedElims, Elims -> Elims)
type Stack = [Frame]
match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term)
match' ((c, es, patch) : stack) = do
let no blocking es = return $ NoReduction $ blocking $ patch $ map ignoreReduced es
yes t = flip YesReduction t <$> asksTC envSimplification
do
case c of
Fail -> no (NotBlocked AbsurdMatch) es
Done xs t
| m < n -> yes $ applySubst (toSubst es) $ foldr lam t (drop m xs)
| otherwise -> yes $ applySubst (toSubst es0) t `applyE` map ignoreReduced es1
where
n = length xs
m = length es
toSubst = parallelS . reverse . map (unArg . fromMaybe __IMPOSSIBLE__ . isApplyElim . ignoreReduced)
(es0, es1) = splitAt n es
lam x t = Lam (argInfo x) (Abs (unArg x) t)
Case (Arg _ n) Branches{etaBranch = Just (c, cc), catchAllBranch = ca} ->
case splitAt n es of
(_, []) -> no (NotBlocked Underapplied) es
(es0, MaybeRed _ e@(Apply (Arg _ v0)) : es1) ->
let projs = [ MaybeRed NotReduced $ Apply $ Arg ai $ relToDontCare ai $ v0 `applyE` [Proj ProjSystem f] | Arg ai f <- fs ]
catchAllFrame stack = maybe stack (\c -> (c, es, patch) : stack) ca in
match' $ (content cc, es0 ++ projs ++ es1, patchEta) : catchAllFrame stack
where
fs = conFields c
patchEta es = patch (es0 ++ [e] ++ es1)
where (es0, es') = splitAt n es
(_, es1) = splitAt (length fs) es'
_ -> __IMPOSSIBLE__
Case (Arg _ n) bs -> do
case splitAt n es of
(_, []) -> no (NotBlocked Underapplied) es
(es0, MaybeRed red e0 : es1) -> do
eb :: Blocked Elim <- do
case red of
Reduced b -> return $ e0 <$ b
NotReduced -> unfoldCorecursionE e0
let e = ignoreBlocking eb
es' = es0 ++ [MaybeRed (Reduced $ () <$ eb) e] ++ es1
catchAllFrame stack = maybe stack (\c -> (c, es', patch) : stack) (catchAllBranch bs)
litFrame l stack =
case Map.lookup l (litBranches bs) of
Nothing -> stack
Just cc -> (cc, es0 ++ es1, patchLit) : stack
conFrame c ci vs stack = conFrame' (conName c) (Con c ci) vs stack
conFrame' q f vs stack =
case Map.lookup q (conBranches bs) of
Nothing -> stack
Just cc -> ( content cc
, es0 ++ map (MaybeRed NotReduced) vs ++ es1
, patchCon f (length vs)
) : stack
projFrame p stack =
case Map.lookup p (conBranches bs) of
Nothing -> stack
Just cc -> (content cc, es0 ++ es1, patchLit) : stack
patchLit es = patch (es0 ++ [e] ++ es1)
where (es0, es1) = splitAt n es
patchCon f m es = patch (es0 ++ [f vs <$ e] ++ es2)
where (es0, rest) = splitAt n es
(es1, es2) = splitAt m rest
vs = es1
fallThrough <- return $ fromMaybe False (fallThrough bs) && isJust (catchAllBranch bs)
let
isCon b =
case ignoreBlocking b of
Apply a | c@Con{} <- unArg a -> Just c
_ -> Nothing
id $
case eb of
NotBlocked _ (Apply (Arg info v@(Lit l))) -> performedSimplification $ do
cv <- constructorForm v
let cFrame stack = case cv of
Con c ci vs -> conFrame c ci vs stack
_ -> stack
match' $ litFrame l $ cFrame $ catchAllFrame stack
NotBlocked _ (Apply (Arg info v@(Def q vs))) | Just{} <- Map.lookup q (conBranches bs) -> performedSimplification $ do
match' $ conFrame' q (Def q) vs $ catchAllFrame $ stack
b | Just (Con c ci vs) <- isCon b -> performedSimplification $
match' $ conFrame c ci vs $ catchAllFrame $ stack
NotBlocked _ (Proj _ p) -> performedSimplification $
match' $ projFrame p $ stack
_ | fallThrough -> match' $ catchAllFrame $ stack
Blocked x _ -> no (Blocked x) es'
NotBlocked _ (Apply (Arg info (MetaV x _))) -> no (Blocked x) es'
NotBlocked blocked e -> no (NotBlocked $ stuckOn e blocked) es'
match' [] =
caseMaybeM (asksTC envAppDef) __IMPOSSIBLE__ $ \ f -> do
pds <- getPartialDefs
if f `elem` pds
then return (NoReduction $ NotBlocked MissingClauses [])
else do
traceSLn "impossible" 10
("Incomplete pattern matching when applying " ++ show f)
__IMPOSSIBLE__