module Agda.TypeChecking.CompiledClause.Match where
import Control.Applicative
import qualified Data.Map as Map
import Data.Traversable
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Primitive
import Agda.Utils.List
import Agda.Utils.Impossible
#include "../../undefined.h"
matchCompiled :: CompiledClauses -> MaybeReducedArgs -> TCM (Reduced (Blocked Args) Term)
matchCompiled c args = match c args id []
type Stack = [(CompiledClauses, MaybeReducedArgs, Args -> Args)]
match :: CompiledClauses -> MaybeReducedArgs -> (Args -> Args) -> Stack -> TCM (Reduced (Blocked Args) Term)
match Fail args patch stack = return $ NoReduction $ NotBlocked (patch $ map ignoreReduced args)
match (Done _ t) args _ _ =
return $ YesReduction $ substs (reverse $ map (unArg . ignoreReduced) args) t
match (Case n bs) args patch stack = do
let (args0, MaybeRed red (Arg h r v0), args1) = extractNthElement' n args
w <- case red of
Reduced b -> return $ fmap (const v0) b
NotReduced ->
unfoldCorecursion =<< instantiate v0
cv <- constructorForm $ ignoreBlocking w
let v = ignoreBlocking w
args' = args0 ++ [MaybeRed red $ Arg h r v] ++ args1
stack' = maybe [] (\c -> [(c, args', patch)]) (catchAllBranch bs)
++ stack
patchLit args = patch (args0 ++ [Arg h r v] ++ args1)
where (args0, args1) = splitAt n args
patchCon c m args = patch (args0 ++ [Arg h r $ Con c vs] ++ args1)
where (args0, args1') = splitAt n args
(vs, args1) = splitAt m args1'
case w of
Blocked x _ -> return $ NoReduction $ Blocked x (patch $ map ignoreReduced args')
NotBlocked (MetaV x _) -> return $ NoReduction $ Blocked x (patch $ map ignoreReduced args')
NotBlocked (Lit l) -> case Map.lookup l (litBranches bs) of
Nothing -> match' stack''
Just cc -> match cc (args0 ++ args1) patchLit stack''
where
stack'' = (++ stack') $ case cv of
Con c vs -> case Map.lookup c (conBranches bs) of
Nothing -> []
Just cc -> [(cc, args0 ++ map (MaybeRed red) vs ++ args1, patchCon c (length vs))]
_ -> []
NotBlocked (Con c vs) -> case Map.lookup c (conBranches bs) of
Nothing -> match' stack'
Just cc -> match cc (args0 ++ map (MaybeRed red) vs ++ args1)
(patchCon c (length vs)) stack'
NotBlocked _ -> return $ NoReduction $ NotBlocked (patch $ map ignoreReduced args')
match' :: Stack -> TCM (Reduced (Blocked Args) Term)
match' ((c, args, patch):stack) = match c args patch stack
match' [] = typeError $ GenericError "Incomplete pattern matching"
unfoldCorecursion v = case v of
Def f args -> unfoldDefinition True reduceB (Def f []) f args
_ -> reduceB v