{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Patterns.Match where
import Prelude hiding (null)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
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
import Agda.TypeChecking.Monad.Builtin (getName',builtinHComp)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Datatypes
import Agda.Utils.Empty
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
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
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
let vs1 = v' : vs
case r' of
Yes s' us' -> return (No , vs1)
No -> return (No , vs1)
DontKnow m -> return (DontKnow m , vs1)
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 `mappend` us'), vs1)
No -> return (No , vs1)
DontKnow m -> return (DontKnow m , vs1)
_ -> __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 isNothing $ 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 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