module Agda.TypeChecking.Patterns.Match where
import Control.Monad
import Data.Monoid
import Data.Traversable
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Primitive
import Agda.Utils.Monad
#include "../../undefined.h"
import Agda.Utils.Impossible
data Match = Yes [Term] | No | DontKnow (Maybe MetaId)
instance Monoid Match where
mempty = Yes []
Yes us `mappend` Yes vs = Yes (us ++ vs)
Yes _ `mappend` No = No
Yes _ `mappend` DontKnow m = DontKnow m
No `mappend` _ = No
DontKnow _ `mappend` DontKnow Nothing = DontKnow Nothing
DontKnow m `mappend` _ = DontKnow m
matchPatterns :: MonadTCM tcm => [Arg Pattern] -> [Arg Term] -> tcm (Match, [Arg Term])
matchPatterns ps vs =
do (ms,vs) <- unzip <$> zipWithM' matchPattern ps vs
return (mconcat ms, vs)
matchPattern :: MonadTCM tcm => Arg Pattern -> Arg Term -> tcm (Match, Arg Term)
matchPattern (Arg h' (VarP _)) arg@(Arg _ v) = return (Yes [v], arg)
matchPattern (Arg _ (DotP _)) arg@(Arg _ v) = return (Yes [v], arg)
matchPattern (Arg h' (LitP l)) arg@(Arg h v) = do
w <- reduceB v
let v = ignoreBlocking w
case w of
NotBlocked (Lit l')
| l == l' -> return (Yes [], Arg h v)
| otherwise -> return (No, Arg h v)
NotBlocked (MetaV x _) -> return (DontKnow $ Just x, Arg h v)
Blocked x _ -> return (DontKnow $ Just x, Arg h v)
_ -> return (DontKnow Nothing, Arg h v)
matchPattern (Arg h' (ConP c ps)) (Arg h v) =
do w <- traverse constructorForm =<< reduceB v
w <- case w of
NotBlocked (Def f args) ->
unfoldDefinition True reduceB (Def f []) f args
_ -> return w
let v = ignoreBlocking w
case w of
NotBlocked (Con c' vs)
| c == c' -> do
(m, vs) <- matchPatterns ps vs
return (m, Arg h $ Con c' vs)
| otherwise -> return (No, Arg h v)
NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg h v)
Blocked x _ -> return (DontKnow $ Just x, Arg h v)
_ -> return (DontKnow Nothing, Arg h v)