{-# LANGUAGE CPP #-}
module Agda.TypeChecking.CompiledClause.Match where
import Control.Monad.Reader (asks)
import qualified Data.List as List
import qualified Data.Map as Map
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad as RedM
import Agda.TypeChecking.Substitute
import Agda.Utils.Maybe
#include "undefined.h"
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 argFromElim) 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 <$> asks 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 . argFromElim . 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 $ defaultArg $ v0 `applyE` [Proj ProjSystem f] | 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 =
case Map.lookup (conName c) (conBranches bs) of
Nothing -> stack
Just cc -> ( content cc
, es0 ++ map (MaybeRed NotReduced) vs ++ es1
, patchCon c ci (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 c ci m es = patch (es0 ++ [Con c ci vs <$ e] ++ es2)
where (es0, rest) = splitAt n es
(es1, es2) = splitAt m rest
vs = es1
id $
case eb of
Blocked x _ -> no (Blocked x) es'
NotBlocked _ (Apply (Arg info (MetaV x _))) -> no (Blocked x) es'
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 (Con c ci vs))) -> performedSimplification $
match' $ conFrame c ci vs $ catchAllFrame $ stack
NotBlocked _ (Proj _ p) -> performedSimplification $
match' $ projFrame p $ stack
NotBlocked blocked e -> no (NotBlocked $ stuckOn e blocked) es'
match' [] =
caseMaybeM (asks 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__