module Agda.TypeChecking.Patterns.Match where
import Data.Monoid
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad hiding (reportSDoc)
import Agda.TypeChecking.Pretty
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
data Match a = Yes Simplification [a]
| No
| DontKnow (Maybe MetaId)
deriving Functor
instance Monoid (Match a) where
mempty = Yes mempty []
Yes s us `mappend` Yes s' vs = Yes (s `mappend` s') (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
foldMatch
:: forall a b . (a -> b -> ReduceM (Match Term, b))
-> [a] -> [b] -> ReduceM (Match Term, [b])
foldMatch match = loop where
loop :: [a] -> [b] -> ReduceM (Match Term, [b])
loop ps0 vs0 = do
case (ps0, vs0) of
([], []) -> return (mempty, [])
(p : ps, v : vs) -> do
(r, v') <- match p v
case r of
No -> return (No , v' : vs)
DontKnow m -> return (DontKnow m, v' : vs)
Yes s us -> do
(r', vs') <- loop ps vs
let vs1 = v' : vs'
case r' of
Yes s' us' -> return (Yes (s `mappend` s') (us ++ us'), vs1)
No -> return (No , vs1)
DontKnow m -> return (DontKnow m , vs1)
_ -> __IMPOSSIBLE__
matchCopatterns :: [I.NamedArg Pattern] -> [Elim] -> ReduceM (Match Term, [Elim])
matchCopatterns ps vs = do
traceSDoc "tc.match" 50
(vcat [ text "matchCopatterns"
, nest 2 $ text "ps =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) ps)
, nest 2 $ text "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
]) $ do
foldMatch (matchCopattern . namedArg) ps vs
matchCopattern :: Pattern -> Elim -> ReduceM (Match Term, Elim)
matchCopattern (ProjP p) elim@(Proj q)
| p == q = return (Yes YesSimplification [], elim)
| otherwise = return (No , elim)
matchCopattern (ProjP p) elim@Apply{}
= return (DontKnow Nothing, elim)
matchCopattern _ elim@Proj{} = return (DontKnow Nothing, elim)
matchCopattern p (Apply v) = mapSnd Apply <$> matchPattern p v
matchPatterns :: [I.NamedArg Pattern] -> [I.Arg Term] -> ReduceM (Match Term, [I.Arg Term])
matchPatterns ps vs = do
traceSDoc "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)
]) $ do
foldMatch (matchPattern . namedArg) ps vs
matchPattern :: Pattern -> I.Arg Term -> ReduceM (Match Term, I.Arg Term)
matchPattern p u = case (p, u) of
(ProjP{}, _ ) -> __IMPOSSIBLE__
(VarP _ , arg@(Arg _ v)) -> return (Yes NoSimplification [v], arg)
(DotP _ , arg@(Arg _ v)) -> return (Yes NoSimplification [v], arg)
(LitP l , arg@(Arg _ v)) -> do
w <- reduceB' v
let arg' = arg $> ignoreBlocking w
case ignoreSharing <$> w of
NotBlocked (Lit l')
| l == l' -> return (Yes YesSimplification [] , arg')
| otherwise -> return (No , arg')
NotBlocked (MetaV x _) -> return (DontKnow $ Just x , arg')
Blocked x _ -> return (DontKnow $ Just x , arg')
_ -> return (DontKnow Nothing , arg')
(ConP con@(ConHead c _ ds) Just{} ps, arg@(Arg info v))
| size ds == size ps -> mapSnd (Arg info . Con con) <$> do
matchPatterns ps $ for ds $ \ d -> Arg info $ v `applyE` [Proj d]
| otherwise -> __IMPOSSIBLE__
(ConP c _ ps, Arg info v) ->
do w <- traverse constructorForm =<< reduceB' v
w <- case ignoreSharing <$> w of
NotBlocked (Def f es) ->
unfoldDefinitionE True reduceB' (Def f []) f es
_ -> return w
let v = ignoreBlocking w
case ignoreSharing <$> w of
NotBlocked (Con c' vs)
| c == c' -> do
(m, vs) <- yesSimplification <$> matchPatterns ps vs
return (m, Arg info $ Con c' vs)
| otherwise -> return (No, Arg info v)
NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg info v)
Blocked x _ -> return (DontKnow $ Just x, Arg info v)
_ -> return (DontKnow Nothing, Arg info v)
yesSimplification :: (Match a, b) -> (Match a, b)
yesSimplification (Yes _ vs, us) = (Yes YesSimplification vs, us)
yesSimplification r = r