module Agda.TypeChecking.CompiledClause.Match where
import Control.Applicative
import Control.Monad.Reader (asks)
import qualified Data.Map as Map
import Data.List
import Debug.Trace (trace)
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Monad hiding (reportSDoc, reportSLn)
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 fromElim) bes
where fromElim (Apply v) = v
fromElim (Proj f ) = __IMPOSSIBLE__
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 debug = do
traceSDoc "reduce.compiled" 95 $ vcat $
[ text "reducing case" <+> do
caseMaybeM (asks envAppDef) __IMPOSSIBLE__ $ \ f -> do
sep $ prettyTCM f : map prettyTCM es
, text $ "trying clause " ++ show c
]
let no es = return $ NoReduction $ NotBlocked $ patch $ map ignoreReduced es
noBlocked x es = return $ NoReduction $ Blocked x $ patch $ map ignoreReduced es
yes t = flip YesReduction t <$> asks envSimplification
debug $ do
case c of
Fail -> no 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 $ map (fmap $ fmap shared) es
lam x t = Lam (argInfo x) (Abs (unArg x) t)
Case n bs -> do
case genericSplitAt n es of
(_, []) -> no 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 red 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 vs stack =
case Map.lookup (conName c) (conBranches bs) of
Nothing -> stack
Just cc -> ( content cc
, es0 ++ map (MaybeRed red . Apply) vs ++ es1
, patchCon c (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 m es = patch (es0 ++ [Con c vs <$ e] ++ es2)
where (es0, rest) = splitAt n es
(es1, es2) = splitAt m rest
vs = map argFromElim es1
case fmap ignoreSharing <$> eb of
Blocked x _ -> noBlocked x es'
NotBlocked (Apply (Arg info (MetaV x _))) -> noBlocked x es'
NotBlocked (Apply (Arg info v@(Lit l))) -> performedSimplification $ do
cv <- constructorForm v
let cFrame stack = case ignoreSharing cv of
Con c vs -> conFrame c vs stack
_ -> stack
match' $ litFrame l $ cFrame $ catchAllFrame stack
NotBlocked (Apply (Arg info (Con c vs))) -> performedSimplification $
match' $ conFrame c vs $ catchAllFrame $ stack
NotBlocked (Proj p) -> performedSimplification $
match' $ projFrame p $ stack
NotBlocked _ -> no es'
match' [] = do
caseMaybeM (asks envAppDef) __IMPOSSIBLE__ $ \ f -> do
error $ "Incomplete pattern matching when applying " ++ show f
unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
unfoldCorecursionE e@(Proj f) = return $ NotBlocked e
unfoldCorecursionE (Apply (Arg info v)) = fmap (Apply . Arg info) <$>
unfoldCorecursion v
unfoldCorecursion :: Term -> ReduceM (Blocked Term)
unfoldCorecursion v = do
v <- instantiate' v
case v of
Def f es -> unfoldDefinitionE True unfoldCorecursion (Def f []) f es
Shared{} -> fmap shared <$> unfoldCorecursion (ignoreSharing v)
_ -> reduceB' v