#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.TypeChecking.CompiledClause.Match where
import Control.Applicative
import Control.Monad.Reader (asks)
import Data.List
import qualified Data.Map as Map
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 blocking es = return $ NoReduction $ blocking $ patch $ map ignoreReduced es
yes t = flip YesReduction t <$> asks envSimplification
debug $ do
shared <- sharedFun
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 $ map (fmap $ fmap shared) es
lam x t = Lam (argInfo x) (Abs (unArg x) t)
Case (Arg _ n) bs -> do
case genericSplitAt 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 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
traceSLn "reduce.compiled" 100 ("caseing on raw " ++ show eb) $
case fmap ignoreSharing <$> 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 ignoreSharing cv of
Con c vs -> conFrame c vs stack
_ -> stack
traceSLn "reduce.compiled" 100 ("constructorForm = " ++ show cv) $
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 blocked e -> no (NotBlocked $ stuckOn e blocked) es'
match' [] =
caseMaybeM (asks envAppDef) __IMPOSSIBLE__ $ \ f -> do
traceSLn "impossible" 10
("Incomplete pattern matching when applying " ++ show f)
__IMPOSSIBLE__