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
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 :: [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 :: [NamedArg Pattern] -> [Arg Term] -> ReduceM (Match Term, [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 -> Arg Term -> ReduceM (Match Term, 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