module Agda.TypeChecking.Patterns.Match where
import Prelude hiding (null)
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.Null
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
data Match a = Yes Simplification [a]
| No
| DontKnow (Blocked ())
deriving Functor
instance Null (Match a) where
empty = Yes empty empty
null (Yes simpl as) = null simpl && null as
null _ = False
foldMatch
:: forall p v . (p -> v -> ReduceM (Match Term, v))
-> [p] -> [v] -> ReduceM (Match Term, [v])
foldMatch match = loop where
loop :: [p] -> [v] -> ReduceM (Match Term, [v])
loop ps0 vs0 = do
case (ps0, vs0) of
([], []) -> return (empty, [])
(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{} Apply{} = __IMPOSSIBLE__
matchCopattern _ Proj{} = __IMPOSSIBLE__
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 $ Blocked x () , arg')
Blocked x _ -> return (DontKnow $ Blocked x () , arg')
NotBlocked r t -> return (DontKnow $ NotBlocked r' () , arg')
where r' = stuckOn (Apply arg') r
(ConP con@(ConHead c _ ds) ConPatternInfo{conPRecord = 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 w of
NotBlocked r u -> unfoldCorecursion u
_ -> return w
let v = ignoreBlocking w
arg = Arg info v
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)
NotBlocked _ (MetaV x vs) -> return (DontKnow $ Blocked x () , arg)
Blocked x _ -> return (DontKnow $ Blocked x () , arg)
NotBlocked r _ -> return (DontKnow $ NotBlocked r' () , arg)
where r' = stuckOn (Apply arg) r
yesSimplification :: (Match a, b) -> (Match a, b)
yesSimplification (Yes _ vs, us) = (Yes YesSimplification vs, us)
yesSimplification r = r