{-# LANGUAGE CPP, PatternGuards, DeriveFunctor #-} module Agda.TypeChecking.Coverage.Match where import Control.Applicative import Control.Monad.State import Data.Map (Map) import qualified Data.Map as Map import Data.Monoid import Data.Traversable (traverse) import Data.Function import Agda.Syntax.Common import Agda.Syntax.Internal import Agda.Syntax.Internal.Pattern import Agda.Syntax.Literal import Agda.Utils.Permutation import Agda.Utils.Size import Agda.Utils.List #include "../../undefined.h" import Agda.Utils.Impossible {-| Given 1. the function clauses @cs@ 2. the patterns @ps@ and permutation @perm@ of a split clause we want to compute a variable index of the split clause to split on next. First, we find the set @cs'@ of all the clauses that are instances (via substitutions @rhos@) of the split clause. In these substitutions, we look for a column that has only constructor patterns. We try to split on this column first. -} {- nonOverlappingCompleteMatches :: [Clause] -> [Arg Pattern] -> Permutation -> Match Nat nonOverlappingCompleteMatches cs ps perm -} -- | Match the given patterns against a list of clauses match :: [Clause] -> [Arg Pattern] -> Permutation -> Match Nat match cs ps perm = foldr choice No $ zipWith matchIt [0..] cs where mps = buildMPatterns perm ps -- If liberal matching on literals fails or blocks we go with that. -- If it succeeds we use the result from conservative literal matching. -- This is to make sure that we split enough when literals are involved. -- For instance, -- f ('x' :: 'y' :: _) = ... -- f (c :: s) = ... -- would never split the tail of the list if we only used conservative -- literal matching. matchIt i c = matchClause yesMatchLit mps i c +++ matchClause noMatchLit mps i c Yes _ +++ m = m No +++ _ = No Block x +++ _ = Block x -- | We use a special representation of the patterns we're trying to match -- against a clause. In particular we want to keep track of which variables -- are blocking a match. data MPat = VarMP Nat | ConMP QName [Arg MPat] | LitMP Literal | WildMP buildMPatterns :: Permutation -> [Arg Pattern] -> [Arg MPat] buildMPatterns perm ps = evalState (mapM (traverse build) ps) xs where xs = permute (invertP perm) $ downFrom (size perm) -- reverse [0 .. size perm - 1] tick = do x : xs <- get; put xs; return x build (VarP _) = VarMP <$> tick build (ConP con _ ps) = ConMP con <$> mapM (traverse build) ps build (DotP t) = tick *> buildT t build (LitP l) = return $ LitMP l buildT (Con c args) = ConMP c <$> mapM (traverse buildT) args buildT (Var i []) = return (VarMP i) buildT _ = return WildMP -- | If matching is inconclusive (@Block@) we want to know which -- variables are blocking the match. data Match a = Yes a -- ^ Matches unconditionally. | No -- ^ Definitely does not match. | Block BlockingVars -- ^ Could match if non-empty list of blocking variables -- is instantiated properly. deriving (Functor) -- | @Nothing@ means there is an overlapping match for this variable. -- @Just cons@ means that it is an non-overlapping match and -- @cons@ are the encountered constructors. type BlockingVar = (Nat, (Maybe [QName])) type BlockingVars = [BlockingVar] overlapping :: BlockingVars -> BlockingVars overlapping = map $ \ (x, _) -> (x, Nothing) -- | Left dominant merge of blocking vars. zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars zipBlockingVars xs ys = map upd xs where upd (x, Just cons) | Just (Just cons') <- lookup x ys = (x, Just $ cons ++ cons') upd (x, _) = (x, Nothing) -- | @choice m m'@ combines the match results @m@ of a function clause -- with the (already combined) match results $m'$ of the later clauses. -- It is for skipping clauses that definitely do not match ('No'). -- It is left-strict, to be used with @foldr@. -- If one clause unconditionally matches ('Yes') we do not look further. choice :: Match a -> Match a -> Match a choice (Yes a) _ = Yes a choice (Block x) (Block y) = Block (zipBlockingVars x y) choice (Block x) (Yes _) = Block $ overlapping x choice (Block x) No = Block x choice No m = m type MatchLit = Literal -> MPat -> Match () noMatchLit :: MatchLit noMatchLit _ _ = No yesMatchLit :: MatchLit yesMatchLit _ VarMP{} = Yes () yesMatchLit _ WildMP{} = Yes () yesMatchLit _ _ = No -- | Check if a clause could match given generously chosen literals matchLits :: Clause -> [Arg Pattern] -> Permutation -> Bool matchLits c ps perm = case matchClause yesMatchLit (buildMPatterns perm ps) 0 c of Yes _ -> True _ -> False -- | @matchClause mlist qs i c@ checks whther clause @c@ number @i@ -- covers a split clause with patterns @qs@. matchClause :: MatchLit -> [Arg MPat] -> Nat -> Clause -> Match Nat matchClause mlit qs i c = fmap (const i) $ matchPats mlit (clausePats c) qs -- | @matchPats mlist ps qs@ checks whether a function clause with patterns -- @ps@ covers a split clause with patterns @qs@ matchPats :: MatchLit -> [Arg Pattern] -> [Arg MPat] -> Match () matchPats mlit ps qs = mconcat $ zipWith (matchPat mlit) (map unArg ps) (map unArg qs) -- | Combine results of checking whether function clause patterns -- covers split clause patterns. -- -- 'No' is dominant: if one function clause pattern is disjoint to -- the corresponding split clause pattern, then -- the whole clauses are disjoint. -- -- 'Yes' is neutral: for a match, all patterns have to match. -- -- 'Block' accumulates variables of the split clause -- that have to be instantiated -- to make the split clause an instance of the function clause. instance Monoid a => Monoid (Match a) where mempty = Yes mempty Yes a `mappend` Yes b = Yes $ mappend a b Yes _ `mappend` No = No Yes _ `mappend` Block x = Block x No `mappend` _ = No Block x `mappend` Yes b = Block x Block x `mappend` No = No Block x `mappend` Block y = Block $ mappend x y -- | @matchPat mlit p q@ checks whether a function clause pattern @p@ -- covers a split clause pattern @q@. There are three results: -- @Yes ()@ means it covers, because @p@ is a variable -- pattern or @q@ is a wildcard. -- @No@ means it does not cover. -- @Block [x]@ means @p@ is a proper instance of @q@ and could become -- a cover if @q@ was split on variable @x@. matchPat :: MatchLit -> Pattern -> MPat -> Match () matchPat _ (VarP _) _ = Yes () matchPat _ (DotP _) _ = Yes () matchPat mlit (LitP l) q = mlit l q -- matchPat mlit (ConP c (Just _) ps) q | recordPattern ps = Yes () -- Andreas, 2012-07-25 record patterns always match! matchPat mlit (ConP c _ ps) q = case q of VarMP x -> Block [(x, Just [c])] WildMP -> Yes () ConMP c' qs | c == c' -> matchPats mlit ps qs | otherwise -> No LitMP _ -> __IMPOSSIBLE__ {- UNUSED class RecordPattern a where recordPattern :: a -> Bool instance RecordPattern Pattern where recordPattern VarP{} = True recordPattern DotP{} = False recordPattern LitP{} = False recordPattern (ConP _ Nothing _) = False recordPattern (ConP _ (Just _) ps) = recordPattern ps instance RecordPattern a => RecordPattern [a] where recordPattern = all recordPattern instance RecordPattern a => RecordPattern (Arg a) where recordPattern = recordPattern . unArg -}