{-# 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.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__
matchCopatterns :: [NamedArg DeBruijnPattern]
-> [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 :: 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
matchPatterns :: [NamedArg DeBruijnPattern]
-> [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 :: DeBruijnPattern
-> Arg Term
-> ReduceM (Match Term, Arg Term)
matchPattern p u = case (p, u) of
(ProjP{}, _ ) -> __IMPOSSIBLE__
(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 else do
isEtaRecordCon (conName c) >>= \case
Nothing -> fallback
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__
fallback = do
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
NotBlocked _ (Con c' ci vs)
| c == c' -> do
(m, vs) <- yesSimplification <$> matchPatterns ps (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs)
return (m, Arg info $ Con c' ci (map Apply 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