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.TypeChecking.Pretty
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 :: [Arg Pattern] -> [Arg Term] -> TCM (Match, [Arg Term])
matchPatterns ps vs = do
reportSDoc "tc.match" 50 $
vcat [ text "matchPatterns"
, nest 2 $ text "ps =" <+> fsep (punctuate comma $ map (text . show) ps)
, nest 2 $ text "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
]
(ms,vs) <- unzip <$> zipWithM' matchPattern ps vs
return (mconcat ms, vs)
matchPattern :: 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' r' (LitP l)) arg@(Arg h r v) = do
w <- reduceB v
let v = ignoreBlocking w
case ignoreSharing <$> w of
NotBlocked (Lit l')
| l == l' -> return (Yes [], Arg h r v)
| otherwise -> return (No, Arg h r v)
NotBlocked (MetaV x _) -> return (DontKnow $ Just x, Arg h r v)
Blocked x _ -> return (DontKnow $ Just x, Arg h r v)
_ -> return (DontKnow Nothing, Arg h r v)
matchPattern (Arg h' r' (ConP c _ ps)) (Arg h r v) =
do w <- traverse constructorForm =<< reduceB v
w <- case ignoreSharing <$> w of
NotBlocked (Def f args) ->
unfoldDefinition True reduceB (Def f []) f args
_ -> return w
let v = ignoreBlocking w
case ignoreSharing <$> w of
_ | r == Irrelevant -> do
(m, vs) <- matchPatterns ps $
repeat $ Arg NotHidden Irrelevant $ Sort Prop
return (m, Arg h r $ Con c vs)
NotBlocked (Con c' vs)
| c == c' -> do
(m, vs) <- matchPatterns ps vs
return (m, Arg h r $ Con c' vs)
| otherwise -> return (No, Arg h r v)
NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg h r v)
Blocked x _ -> return (DontKnow $ Just x, Arg h r v)
_ -> return (DontKnow Nothing, Arg h r v)