{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Patterns.Match where
import Prelude hiding (null)
import Control.Monad
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad hiding (constructorForm)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.Utils.Empty
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
data Match a = Yes Simplification (IntMap (Arg 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
matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a]
matchedArgs err n vs = map get [0..n-1]
where
get k = fromMaybe (absurd err) $ IntMap.lookup k vs
buildSubstitution :: (DeBruijn a)
=> Empty -> Int -> IntMap (Arg a) -> Substitution' a
buildSubstitution err n vs = parallelS $ map unArg $ matchedArgs err n vs
instance Semigroup (Match a) where
DontKnow b <> DontKnow b' = DontKnow $ b <> b'
DontKnow m <> _ = DontKnow m
_ <> DontKnow m = DontKnow m
No <> _ = No
_ <> No = No
Yes s us <> Yes s' vs = Yes (s <> s') (us <> vs)
instance Monoid (Match a) where
mempty = empty
mappend = (<>)
foldMatch
:: forall p v . IsProjP p => (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 | Just{} <- isProjP p -> return (No, v' : vs)
No -> do
(r', _vs') <- loop ps vs
return (r <> r', v' : vs)
DontKnow m -> return (DontKnow m, v' : vs)
Yes{} -> do
(r', vs') <- loop ps vs
return (r <> r', v' : vs')
_ -> __IMPOSSIBLE__
mergeElim :: Elim -> Arg Term -> Elim
mergeElim Apply{} arg = Apply arg
mergeElim (IApply x y _) arg = IApply x y (unArg arg)
mergeElim Proj{} _ = __IMPOSSIBLE__
mergeElims :: [Elim] -> [Arg Term] -> [Elim]
mergeElims = zipWith mergeElim
matchCopatterns :: [NamedArg DeBruijnPattern]
-> [Elim]
-> ReduceM (Match Term, [Elim])
matchCopatterns ps vs = do
traceSDoc "tc.match" 50
(vcat [ "matchCopatterns"
, nest 2 $ "ps =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) ps)
, nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
]) $ do
foldMatch (matchCopattern . namedArg) ps vs
matchCopattern :: DeBruijnPattern
-> Elim
-> ReduceM (Match Term, Elim)
matchCopattern pat@ProjP{} elim@(Proj _ q) = do
ProjP _ p <- normaliseProjP pat
q <- getOriginalProjection q
return $ if p == q then (Yes YesSimplification empty, elim)
else (No, elim)
matchCopattern ProjP{} elim@Apply{} = return (No , elim)
matchCopattern _ elim@Proj{} = return (No , elim)
matchCopattern p (Apply v) = mapSnd Apply <$> matchPattern p v
matchCopattern p e@(IApply x y r) = mapSnd (mergeElim e) <$> matchPattern p (defaultArg r)
matchPatterns :: [NamedArg DeBruijnPattern]
-> [Arg Term]
-> ReduceM (Match Term, [Arg Term])
matchPatterns ps vs = do
reportSDoc "tc.match" 20 $
vcat [ "matchPatterns"
, nest 2 $ "ps =" <+> prettyTCMPatternList ps
, nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
]
traceSDoc "tc.match" 50
(vcat [ "matchPatterns"
, nest 2 $ "ps =" <+> fsep (punctuate comma $ map (text . show) ps)
, nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
]) $ do
foldMatch (matchPattern . namedArg) ps vs
matchPattern :: DeBruijnPattern
-> Arg Term
-> ReduceM (Match Term, Arg Term)
matchPattern p u = case (p, u) of
(ProjP{}, _ ) -> __IMPOSSIBLE__
(IApplyP _ _ _ x , arg ) -> return (Yes NoSimplification entry, arg)
where entry = singleton (dbPatVarIndex x, arg)
(VarP _ x , arg ) -> return (Yes NoSimplification entry, arg)
where entry = singleton (dbPatVarIndex x, arg)
(DotP _ _ , arg@(Arg _ v)) -> return (Yes NoSimplification empty, arg)
(LitP _ l , arg@(Arg _ v)) -> do
w <- reduceB' v
let arg' = arg $> ignoreBlocking w
case w of
NotBlocked _ (Lit l')
| l == l' -> return (Yes YesSimplification empty , 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 c cpi ps, Arg info v) -> do
if not (conPRecord cpi) then fallback c ps (Arg info v) else do
isEtaRecordCon (conName c) >>= \case
Nothing -> fallback c ps (Arg info v)
Just fs -> do
unless (size fs == size ps) __IMPOSSIBLE__
mapSnd (Arg info . Con c (fromConPatternInfo cpi) . map Apply) <$> do
matchPatterns ps $ for fs $ \ (Arg ai f) -> Arg ai $ v `applyE` [Proj ProjSystem f]
where
isEtaRecordCon :: QName -> ReduceM (Maybe [Arg QName])
isEtaRecordCon c = do
(theDef <$> getConstInfo c) >>= \case
Constructor{ conData = d } -> do
(theDef <$> getConstInfo d) >>= \case
r@Record{ recFields = fs } | YesEta <- recEtaEquality r -> return $ Just $ map argFromDom fs
_ -> return Nothing
_ -> __IMPOSSIBLE__
(DefP o q ps, v) -> do
let f (Def q' vs) | q == q' = Just (Def q, vs)
f _ = Nothing
fallback' f ps v
where
fallback c ps v = do
isMatchable <- isMatchable'
let f (Con c' ci' vs) | c == c' = Just (Con c' ci',vs)
f _ = Nothing
fallback' f ps v
isMatchable' = do
mhcomp <- getName' builtinHComp
return $ \ r ->
case ignoreBlocking r of
t@Con{} -> Just t
t@(Def q [l,a,phi,u,u0]) | Just q == mhcomp
-> Just t
_ -> Nothing
fallback' mtc ps (Arg info v) = do
isMatchable <- isMatchable'
w <- reduceB' v
w <- traverse constructorForm =<< case w of
NotBlocked r u -> unfoldCorecursion u
_ -> return w
let v = ignoreBlocking w
arg = Arg info v
case w of
b | Just t <- isMatchable b ->
case mtc t of
Just (bld, vs) -> do
(m, vs1) <- yesSimplification <$> matchPatterns ps (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs)
return (m, Arg info $ bld (mergeElims vs vs1))
Nothing
-> 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
matchPatternP :: DeBruijnPattern
-> Arg DeBruijnPattern
-> ReduceM (Match DeBruijnPattern)
matchPatternP p (Arg info (DotP _ v)) = do
(m, arg) <- matchPattern p (Arg info v)
return $ fmap (DotP defaultPatternInfo) m
matchPatternP p arg@(Arg info q) = do
let varMatch x = return $ Yes NoSimplification $ singleton (dbPatVarIndex x, arg)
termMatch = do
(m, arg) <- matchPattern p (fmap patternToTerm arg)
return $ fmap (DotP defaultPatternInfo) m
case p of
ProjP{} -> __IMPOSSIBLE__
IApplyP _ _ _ x -> varMatch x
VarP _ x -> varMatch x
DotP _ _ -> return $ Yes NoSimplification empty
LitP{} -> termMatch
DefP{} -> termMatch
ConP c cpi ps ->
case q of
ConP c' _ qs | c == c' -> matchPatternsP ps ((map . fmap) namedThing qs)
| otherwise -> return No
LitP{} -> fmap toLitP <$> termMatch
where toLitP (DotP _ (Lit l)) = litP l
toLitP _ = __IMPOSSIBLE__
_ -> termMatch
matchPatternsP :: [NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern]
-> ReduceM (Match DeBruijnPattern)
matchPatternsP ps qs = do
mconcat <$> zipWithM matchPatternP (map namedArg ps) qs