{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Coverage.Match where
import Control.Monad.State
import Prelude hiding ( null )
import qualified Data.List as List
import Data.Maybe (mapMaybe, isJust, fromMaybe)
import Data.Monoid ( Monoid, mempty, mappend, mconcat )
import Data.Semigroup ( Semigroup, (<>), Any(..) )
import Data.Traversable (traverse)
import Agda.Syntax.Abstract (IsProjP(..))
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern ()
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty ( PrettyTCM(..) )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( Pretty(..), text, (<+>), cat , prettyList_ )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.List
import Agda.Utils.Monad
#include "undefined.h"
import Agda.Utils.Impossible
match :: [Clause] -> [NamedArg SplitPattern] -> Match (Nat,[SplitPattern])
match cs ps = foldr choice No $ zipWith matchIt [0..] cs
where
matchIt i c = (i,) <$> matchClause ps c
data SplitPatVar = SplitPatVar
{ splitPatVarName :: PatVarName
, splitPatVarIndex :: Int
, splitExcludedLits :: [Literal]
} deriving (Show)
instance Pretty SplitPatVar where
prettyPrec _ x =
(text $ patVarNameToString (splitPatVarName x)) P.<>
(text $ "@" ++ show (splitPatVarIndex x)) P.<>
(ifNull (splitExcludedLits x) empty $ \lits ->
text "\\{" P.<> prettyList_ lits P.<> text "}")
instance PrettyTCM SplitPatVar where
prettyTCM = prettyTCM . var . splitPatVarIndex
type SplitPattern = Pattern' SplitPatVar
toSplitVar :: DBPatVar -> SplitPatVar
toSplitVar x = SplitPatVar (dbPatVarName x) (dbPatVarIndex x) []
fromSplitVar :: SplitPatVar -> DBPatVar
fromSplitVar x = DBPatVar (splitPatVarName x) (splitPatVarIndex x)
toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns = (fmap . fmap . fmap . fmap) toSplitVar
fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns = (fmap . fmap . fmap . fmap) fromSplitVar
instance DeBruijn SplitPattern where
debruijnNamedVar n i = varP $ SplitPatVar n i []
deBruijnView _ = Nothing
type SplitPSubstitution = Substitution' SplitPattern
toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
toSplitPSubst = (fmap . fmap) toSplitVar
fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst = (fmap . fmap) fromSplitVar
applySplitPSubst :: (Subst Term a) => SplitPSubstitution -> a -> a
applySplitPSubst = applyPatSubst . fromSplitPSubst
instance Subst SplitPattern SplitPattern where
applySubst IdS p = p
applySubst rho p = case p of
VarP o x ->
usePatOrigin o $
useName (splitPatVarName x) $
useExcludedLits (splitExcludedLits x) $
lookupS rho $ splitPatVarIndex x
DotP o u -> DotP o $ applySplitPSubst rho u
ConP c ci ps -> ConP c ci $ applySubst rho ps
LitP x -> p
ProjP{} -> p
where
useName :: PatVarName -> SplitPattern -> SplitPattern
useName n (VarP o x)
| isUnderscore (splitPatVarName x)
= VarP o $ x { splitPatVarName = n }
useName _ x = x
useExcludedLits :: [Literal] -> SplitPattern -> SplitPattern
useExcludedLits lits = \case
(VarP o x) -> VarP o $ x
{ splitExcludedLits = lits ++ splitExcludedLits x }
p -> p
isTrivialPattern :: (HasConstInfo m) => Pattern' a -> m Bool
isTrivialPattern p = case p of
VarP{} -> return True
DotP{} -> return True
ConP c i ps -> andM $ (isEtaCon $ conName c)
: (map (isTrivialPattern . namedArg) ps)
LitP{} -> return False
ProjP{} -> return False
type MatchResult = Match [SplitPattern]
data Match a
= Yes a
| No
| Block
{ blockedOnResult :: Bool
, blockedOnVars :: BlockingVars
}
deriving (Functor)
data BlockingVar = BlockingVar
{ blockingVarNo :: Nat
, blockingVarCons :: [ConHead]
, blockingVarLits :: [Literal]
, blockingVarOverlap :: Bool
} deriving (Show)
instance Pretty BlockingVar where
pretty (BlockingVar i cs ls o) = cat
[ text ("variable " ++ show i)
, if null cs then empty else text " blocked on constructors" <+> pretty cs
, if null ls then empty else text " blocked on literals" <+> pretty ls
, if o then text " (overlapping)" else empty
]
type BlockingVars = [BlockingVar]
blockedOnConstructor :: Nat -> ConHead -> Match a
blockedOnConstructor i c = Block False [BlockingVar i [c] [] False]
blockedOnLiteral :: Nat -> Literal -> Match a
blockedOnLiteral i l = Block False [BlockingVar i [] [l] False]
blockedOnProjection :: Match a
blockedOnProjection = Block True []
mapBlockingVarCons :: ([ConHead] -> [ConHead]) -> BlockingVar -> BlockingVar
mapBlockingVarCons f b = b { blockingVarCons = f (blockingVarCons b) }
mapBlockingVarLits :: ([Literal] -> [Literal]) -> BlockingVar -> BlockingVar
mapBlockingVarLits f b = b { blockingVarLits = f (blockingVarLits b) }
setBlockingVarOverlap :: BlockingVar -> BlockingVar
setBlockingVarOverlap = \x -> x { blockingVarOverlap = True }
overlapping :: BlockingVars -> BlockingVars
overlapping = map setBlockingVarOverlap
zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
zipBlockingVars xs ys = map upd xs
where
upd (BlockingVar x cons lits o) = case List.find ((x ==) . blockingVarNo) ys of
Just (BlockingVar _ cons' lits' o') -> BlockingVar x (cons ++ cons') (lits ++ lits') (o || o')
Nothing -> BlockingVar x cons lits True
choice :: Match a -> Match a -> Match a
choice (Yes a) _ = Yes a
choice (Block r xs) (Block s ys) = Block (r && s) $ zipBlockingVars xs ys
choice (Block r xs) (Yes _) = Block r $ overlapping xs
choice m@Block{} No = m
choice No m = m
matchClause
:: [NamedArg SplitPattern]
-> Clause
-> MatchResult
matchClause qs c = matchPats (namedClausePats c) qs
matchPats
:: [NamedArg (Pattern' a)]
-> [NamedArg SplitPattern]
-> MatchResult
matchPats ps qs = mconcat $ [ projPatternsLeftInSplitClause ] ++
zipWith matchPat (map namedArg ps) (map namedArg qs) ++
[ projPatternsLeftInMatchedClause ]
where
qsrest = drop (length ps) qs
projPatternsLeftInSplitClause =
case mapMaybe isProjP qsrest of
[] -> mempty
_ -> No
psrest = drop (length qs) ps
projPatternsLeftInMatchedClause =
case mapMaybe isProjP psrest of
[] -> mempty
ds -> blockedOnProjection
instance Semigroup a => Semigroup (Match a) where
Yes a <> Yes b = Yes (a <> b)
Yes _ <> m = m
No <> _ = No
Block{} <> No = No
Block r xs <> Block s ys = Block (r || s) (xs ++ ys)
m@Block{} <> Yes{} = m
instance (Semigroup a, Monoid a) => Monoid (Match a) where
mempty = Yes mempty
mappend = (<>)
matchPat
:: Pattern' a
-> SplitPattern
-> MatchResult
matchPat VarP{} q = Yes [q]
matchPat DotP{} q = mempty
matchPat p@(LitP l) q = case q of
VarP _ x -> if l `elem` splitExcludedLits x
then No
else blockedOnLiteral (splitPatVarIndex x) l
ConP{} -> No
DotP{} -> No
LitP l' -> if l == l' then Yes [] else No
ProjP{} -> __IMPOSSIBLE__
matchPat (ProjP _ d) (ProjP _ d') = if d == d' then mempty else No
matchPat ProjP{} _ = __IMPOSSIBLE__
matchPat p@(ConP c _ ps) q = case q of
VarP _ x -> blockedOnConstructor (splitPatVarIndex x) c
ConP c' i qs
| c == c' -> matchPats ps qs
| otherwise -> No
DotP o t -> No
LitP _ -> No
ProjP{} -> __IMPOSSIBLE__