diff options
| author | George Karachalias <george.karachalias@gmail.com> | 2016-02-01 11:43:12 +0100 |
|---|---|---|
| committer | George Karachalias <george.karachalias@gmail.com> | 2016-02-01 11:43:12 +0100 |
| commit | b5df2cc6cf2af4508a4f34a718320a6d79f9adca (patch) | |
| tree | 525e975eaf60e0200555e7f269fd79b7eaeb227d | |
| parent | a883c1b7b08657102a2081b55c8fe68714d8bf73 (diff) | |
| download | haskell-wip/gadtpm.tar.gz | |
Overhaul the Overhauled Pattern Match Checkerwip/gadtpm
* Changed the representation of Value Set Abstractions. Instead
of using a prefix tree, we now use a list of Value Vector
Abstractions. The set of constraints Delta for every Value
Vector Abstraction is the oracle state so that we solve
everything only once.
* Instead of doing everything lazily, we prune at once (and in
general everything is much stricter). A case writtern with
pattern guards is not checked in almost the same time as the
equivalent with pattern matching.
* Do not store the covered and the divergent sets at all. Since
what we only need is a yes/no (does this clause cover anything?
Does it force any thunk?) We just keep a boolean for each.
* Removed flags `-Wtoo-many-guards` and `-ffull-guard-reasoning`.
Replaced with `fmax-pmcheck-iterations=n`. Still debatable what
should the default `n` be.
* When a guard is for sure not going to contribute anything, we
treat it as such: The oracle is not called and cases `CGuard`,
`UGuard` and `DGuard` from the paper are not happening at all
(the generation of a fresh variable, the unfolding of the
pattern list etc.). his combined with the above seems to be
enough to drop the memory increase for test T783 down to 18.7%.
* Do not export function `dsPmWarn` (it is now called directly
from within `checkSingle` and `checkMatches`).
* Make `PmExprVar` hold a `Name` instead of an `Id`. The term
oracle does not handle type information so using `Id` was a
waste of time/space.
* Added testcases T11195, T11303b (data families) and T11374
The patch addresses at least the following:
#11195, #11276, #11303, #11374, #11162
23 files changed, 911 insertions, 850 deletions
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index 043b4f2a04..a28e39edb1 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -7,14 +7,8 @@ Pattern Matching Coverage Checking. {-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-} module Check ( - -- Actual check and pretty printing - checkSingle, checkMatches, dsPmWarn, - - -- Check for exponential explosion due to guards - computeNoGuards, - isAnyPmCheckEnabled, - warnManyGuards, - maximum_failing_guards, + -- Checking and printing + checkSingle, checkMatches, isAnyPmCheckEnabled, -- See Note [Type and Term Equality Propagation] genCaseTmCs1, genCaseTmCs2 @@ -55,6 +49,7 @@ import Data.Maybe -- isNothing, isJust, fromJust import Control.Monad -- liftM3, forM import Coercion import TcEvidence +import IOEnv {- This module checks pattern matches for: @@ -64,7 +59,7 @@ This module checks pattern matches for: \item Exhaustiveness \end{enumerate} -The algorithm used is described in the paper: +The algorithm is based on the paper: "GADTs Meet Their Match: Pattern-matching Warnings That Account for GADTs, Guards, and Laziness" @@ -80,11 +75,6 @@ The algorithm used is described in the paper: type PmM a = DsM a -data PmConstraint = TmConstraint PmExpr PmExpr -- ^ Term equalities: e ~ e - -- See Note [Representation of Term Equalities] - | TyConstraint [EvVar] -- ^ Type equalities - | BtConstraint Id -- ^ Strictness constraints: x ~ _|_ - data PatTy = PAT | VA -- Used only as a kind, to index PmPat -- The *arity* of a PatVec [p1,..,pn] is @@ -99,10 +89,10 @@ data PmPat :: PatTy -> * where -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs PmVar :: { pm_var_id :: Id } -> PmPat t PmLit :: { pm_lit_lit :: PmLit } -> PmPat t -- See Note [Literals in PmPat] - PmNLit :: { pm_lit_id :: Id - , pm_lit_not :: [PmLit] } -> PmPat 'VA + PmNLit :: { pm_lit_id :: Id + , pm_lit_not :: [PmLit] } -> PmPat 'VA PmGrd :: { pm_grd_pv :: PatVec - , pm_grd_expr :: PmExpr } -> PmPat 'PAT + , pm_grd_expr :: PmExpr } -> PmPat 'PAT -- data T a where -- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p] @@ -111,31 +101,36 @@ data PmPat :: PatTy -> * where type Pattern = PmPat 'PAT -- ^ Patterns type ValAbs = PmPat 'VA -- ^ Value Abstractions -type PatVec = [Pattern] -- Pattern Vectors -type ValVecAbs = [ValAbs] -- Value Vector Abstractions - -data ValSetAbs -- Reprsents a set of value vector abstractions - -- Notionally each value vector abstraction is a triple: - -- (Gamma |- us |> Delta) - -- where 'us' is a ValueVec - -- 'Delta' is a constraint - -- INVARIANT VsaInvariant: an empty ValSetAbs is always represented by Empty - -- INVARIANT VsaArity: the number of Cons's in any path to a leaf is the same - -- The *arity* of a ValSetAbs is the number of Cons's in any path to a leaf - = Empty -- ^ {} - | Union ValSetAbs ValSetAbs -- ^ S1 u S2 - | Singleton -- ^ { |- empty |> empty } - | Constraint [PmConstraint] ValSetAbs -- ^ Extend Delta - | Cons ValAbs ValSetAbs -- ^ map (ucon u) vs +type PatVec = [Pattern] -- ^ Pattern Vectors +data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions + +-- | Term and type constraints to accompany each value vector abstraction. +-- For efficiency, we store the term oracle state instead of the term +-- constraints. TODO: Do the same for the type constraints? +data Delta = MkDelta { delta_ty_cs :: Bag EvVar + , delta_tm_cs :: TmState } + +type ValSetAbs = [ValVec] -- ^ Value Set Abstractions +type Uncovered = ValSetAbs + +-- Instead of keeping the whole sets in memory, we keep a boolean for both the +-- covered and the divergent set (we store the uncovered set though, since we +-- want to print it). For both the covered and the divergent we have: +-- +-- True <=> The set is non-empty +-- +-- hence: +-- C = True ==> Useful clause (no warning) +-- C = False, D = True ==> Clause with inaccessible RHS +-- C = False, D = False ==> Redundant clause +type Triple = (Bool, Uncovered, Bool) -- | Pattern check result -- --- * redundant clauses --- * clauses with inaccessible RHS --- * missing -type PmResult = ( [[LPat Id]] - , [[LPat Id]] - , [([PmExpr], [ComplexEq])] ) +-- * Redundant clauses +-- * Not-covered clauses +-- * Clauses with inaccessible RHS +type PmResult = ([[LPat Id]], Uncovered, [[LPat Id]]) {- %************************************************************************ @@ -146,78 +141,56 @@ type PmResult = ( [[LPat Id]] -} -- | Check a single pattern binding (let) -checkSingle :: Id -> Pat Id -> DsM PmResult -checkSingle var p = do - let lp = [noLoc p] +checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat Id -> DsM () +checkSingle dflags ctxt var p = do + mb_pm_res <- tryM (checkSingle' var p) + case mb_pm_res of + Left _ -> warnPmIters dflags ctxt + Right res -> dsPmWarn dflags ctxt res + +-- | Check a single pattern binding (let) +checkSingle' :: Id -> Pat Id -> DsM PmResult +checkSingle' var p = do + resetPmIterDs -- set the iter-no to zero fam_insts <- dsGetFamInstEnvs - vec <- liftUs (translatePat fam_insts p) - vsa <- initial_uncovered [var] - (c,d,us') <- patVectProc False (vec,[]) vsa -- no guards - us <- pruneVSA us' - return $ case (c,d) of - (True, _) -> ([], [], us) - (False, True) -> ([], [lp], us) - (False, False) -> ([lp], [], us) + clause <- translatePat fam_insts p + missing <- mkInitialUncovered [var] + (cs,us,ds) <- runMany (pmcheckI clause []) missing -- no guards + return $ case (cs,ds) of + (True, _ ) -> ([], us, []) -- useful + (False, False) -> ( m, us, []) -- redundant + (False, True ) -> ([], us, m) -- inaccessible rhs + where m = [[noLoc p]] -- | Check a matchgroup (case, functions, etc.) -checkMatches :: Bool -> [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult -checkMatches oversimplify vars matches - | null matches = return ([],[],[]) - | otherwise = do - missing <- initial_uncovered vars - (rs,is,us) <- go matches missing - return (map hsLMatchPats rs, map hsLMatchPats is, us) - where - go [] missing = do - missing' <- pruneVSA missing - return ([], [], missing') - - go (m:ms) missing = do - fam_insts <- dsGetFamInstEnvs - clause <- liftUs (translateMatch fam_insts m) - (c, d, us ) <- patVectProc oversimplify clause missing - (rs, is, us') <- go ms us - return $ case (c,d) of - (True, _) -> ( rs, is, us') - (False, True) -> ( rs, m:is, us') - (False, False) -> (m:rs, is, us') - --- | Generate the initial uncovered set. It initializes the --- delta with all term and type constraints in scope. -initial_uncovered :: [Id] -> DsM ValSetAbs -initial_uncovered vars = do - cs <- getCsPmM - let vsa = foldr Cons Singleton (map PmVar vars) - return $ if null cs then vsa - else mkConstraint cs vsa - --- | Collect all term and type constraints from the local environment -getCsPmM :: DsM [PmConstraint] -getCsPmM = do - ty_cs <- bagToList <$> getDictsDs - tm_cs <- map simpleToTmCs . bagToList <$> getTmCsDs - return $ if null ty_cs - then tm_cs - else TyConstraint ty_cs : tm_cs - where - simpleToTmCs :: (Id, PmExpr) -> PmConstraint - simpleToTmCs (x,e) = TmConstraint (PmExprVar x) e +checkMatches :: DynFlags -> DsMatchContext + -> [Id] -> [LMatch Id (LHsExpr Id)] -> DsM () +checkMatches dflags ctxt vars matches = do + mb_pm_res <- tryM (checkMatches' vars matches) + case mb_pm_res of + Left _ -> warnPmIters dflags ctxt + Right res -> dsPmWarn dflags ctxt res --- | Total number of guards in a translated match that could fail. -noFailingGuards :: [(PatVec,[PatVec])] -> Int -noFailingGuards clauses = sum [ countPatVecs gvs | (_, gvs) <- clauses ] +-- | Check a matchgroup (case, functions, etc.) +checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult +checkMatches' vars matches + | null matches = return ([], [], []) + | otherwise = do + resetPmIterDs -- set the iter-no to zero + missing <- mkInitialUncovered vars + (rs,us,ds) <- go matches missing + return (map hsLMatchPats rs, us, map hsLMatchPats ds) where - countPatVec gv = length [ () | p <- gv, not (cantFailPattern p) ] - countPatVecs gvs = sum [ countPatVec gv | gv <- gvs ] - -computeNoGuards :: [LMatch Id (LHsExpr Id)] -> PmM Int -computeNoGuards matches = do - fam_insts <- dsGetFamInstEnvs - matches' <- mapM (liftUs . translateMatch fam_insts) matches - return (noFailingGuards matches') - -maximum_failing_guards :: Int -maximum_failing_guards = 20 -- Find a better number + go [] missing = return ([], missing, []) + go (m:ms) missing = do + fam_insts <- dsGetFamInstEnvs + (clause, guards) <- translateMatch fam_insts m + (cs, missing', ds) <- runMany (pmcheckI clause guards) missing + (rs, final_u, is) <- go ms missing' + return $ case (cs, ds) of + (True, _ ) -> ( rs, final_u, is) -- useful + (False, False) -> (m:rs, final_u, is) -- redundant + (False, True ) -> ( rs, final_u, m:is) -- inaccessible {- %************************************************************************ @@ -235,45 +208,67 @@ nullaryConPattern :: DataCon -> Pattern nullaryConPattern con = PmCon { pm_con_con = con, pm_con_arg_tys = [] , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] } +{-# INLINE nullaryConPattern #-} truePattern :: Pattern truePattern = nullaryConPattern trueDataCon +{-# INLINE truePattern #-} -- | A fake guard pattern (True <- _) used to represent cases we cannot handle fake_pat :: Pattern fake_pat = PmGrd { pm_grd_pv = [truePattern] , pm_grd_expr = PmExprOther EWildPat } +{-# INLINE fake_pat #-} + +-- | Check whether a guard pattern is generated by the checker (unhandled) +isFakeGuard :: [Pattern] -> PmExpr -> Bool +isFakeGuard [PmCon { pm_con_con = c }] (PmExprOther EWildPat) + | c == trueDataCon = True + | otherwise = False +isFakeGuard _pats _e = False + +-- | Generate a `canFail` pattern vector of a specific type +mkCanFailPmPat :: Type -> PmM PatVec +mkCanFailPmPat ty = do + var <- mkPmVar ty + return [var, fake_pat] vanillaConPattern :: DataCon -> [Type] -> PatVec -> Pattern -- ADT constructor pattern => no existentials, no local constraints vanillaConPattern con arg_tys args = PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args } +{-# INLINE vanillaConPattern #-} +-- | Create an empty list pattern of a given type nilPattern :: Type -> Pattern nilPattern ty = PmCon { pm_con_con = nilDataCon, pm_con_arg_tys = [ty] , pm_con_tvs = [], pm_con_dicts = [] , pm_con_args = [] } +{-# INLINE nilPattern #-} mkListPatVec :: Type -> PatVec -> PatVec -> PatVec mkListPatVec ty xs ys = [PmCon { pm_con_con = consDataCon , pm_con_arg_tys = [ty] , pm_con_tvs = [], pm_con_dicts = [] , pm_con_args = xs++ys }] +{-# INLINE mkListPatVec #-} +-- | Create a (non-overloaded) literal pattern mkLitPattern :: HsLit -> Pattern mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit } +{-# INLINE mkLitPattern #-} -- ----------------------------------------------------------------------- -- * Transform (Pat Id) into of (PmPat Id) -translatePat :: FamInstEnvs -> Pat Id -> UniqSM PatVec +translatePat :: FamInstEnvs -> Pat Id -> PmM PatVec translatePat fam_insts pat = case pat of - WildPat ty -> mkPmVarsSM [ty] + WildPat ty -> mkPmVars [ty] VarPat id -> return [PmVar (unLoc id)] ParPat p -> translatePat fam_insts (unLoc p) - LazyPat _ -> mkPmVarsSM [hsPatType pat] -- like a variable + LazyPat _ -> mkPmVars [hsPatType pat] -- like a variable -- ignore strictness annotations for now BangPat p -> translatePat fam_insts (unLoc p) @@ -281,7 +276,7 @@ translatePat fam_insts pat = case pat of AsPat lid p -> do -- Note [Translating As Patterns] ps <- translatePat fam_insts (unLoc p) - let [e] = map valAbsToPmExpr (coercePatVec ps) + let [e] = map vaToPmExpr (coercePatVec ps) g = PmGrd [PmVar (unLoc lid)] e return (ps ++ [g]) @@ -293,18 +288,12 @@ translatePat fam_insts pat = case pat of | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts p | otherwise -> do ps <- translatePat fam_insts p - (xp,xe) <- mkPmId2FormsSM ty + (xp,xe) <- mkPmId2Forms ty let g = mkGuard ps (HsWrap wrapper (unLoc xe)) return [xp,g] -- (n + k) ===> x (True <- x >= k) (n <- x-k) - NPlusKPat (L _ n) k1 k2 ge minus ty -> do - (xp, xe) <- mkPmId2FormsSM ty - let ke1 = L (getLoc k1) (HsOverLit (unLoc k1)) - ke2 = L (getLoc k1) (HsOverLit k2) - g1 = mkGuard [truePattern] (unLoc $ nlHsSyntaxApps ge [xe, ke1]) - g2 = mkGuard [PmVar n] (unLoc $ nlHsSyntaxApps minus [xe, ke2]) - return [xp, g1, g2] + NPlusKPat (L _ _n) _k1 _k2 _ge _minus ty -> mkCanFailPmPat ty -- (fun -> pat) ===> x (pat <- fun x) ViewPat lexpr lpat arg_ty -> do @@ -312,41 +301,38 @@ translatePat fam_insts pat = case pat of -- See Note [Guards and Approximation] case all cantFailPattern ps of True -> do - (xp,xe) <- mkPmId2FormsSM arg_ty + (xp,xe) <- mkPmId2Forms arg_ty let g = mkGuard ps (HsApp lexpr xe) return [xp,g] - False -> do - var <- mkPmVarSM arg_ty - return [var, fake_pat] + False -> mkCanFailPmPat arg_ty -- list ListPat ps ty Nothing -> do - foldr (mkListPatVec ty) [nilPattern ty] <$> translatePatVec fam_insts (map unLoc ps) + foldr (mkListPatVec ty) [nilPattern ty] + <$> translatePatVec fam_insts (map unLoc ps) -- overloaded list ListPat lpats elem_ty (Just (pat_ty, _to_list)) | Just e_ty <- splitListTyConApp_maybe pat_ty , (_, norm_elem_ty) <- normaliseType fam_insts Nominal elem_ty - -- elem_ty is frequently something like `Item [Int]`, but we prefer `Int` + -- elem_ty is frequently something like + -- `Item [Int]`, but we prefer `Int` , norm_elem_ty `eqType` e_ty -> -- We have to ensure that the element types are exactly the same. -- Otherwise, one may give an instance IsList [Int] (more specific than -- the default IsList [a]) with a different implementation for `toList' translatePat fam_insts (ListPat lpats e_ty Nothing) - | otherwise -> do - -- See Note [Guards and Approximation] - var <- mkPmVarSM pat_ty - return [var, fake_pat] + -- See Note [Guards and Approximation] + | otherwise -> mkCanFailPmPat pat_ty - ConPatOut { pat_con = L _ (PatSynCon _) } -> do + ConPatOut { pat_con = L _ (PatSynCon _) } -> -- Pattern synonyms have a "matcher" -- (see Note [Pattern synonym representation] in PatSyn.hs -- We should be able to transform (P x y) -- to v (Just (x, y) <- matchP v (\x y -> Just (x,y)) Nothing -- That is, a combination of a variable pattern and a guard -- But there are complications with GADTs etc, and this isn't done yet - var <- mkPmVarSM (hsPatType pat) - return [var,fake_pat] + mkCanFailPmPat (hsPatType pat) ConPatOut { pat_con = L _ (RealDataCon con) , pat_arg_tys = arg_tys @@ -387,7 +373,7 @@ translatePat fam_insts pat = case pat of -- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs) translateNPat :: FamInstEnvs - -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> Type -> UniqSM PatVec + -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> Type -> PmM PatVec translateNPat fam_insts (OverLit val False _ ty) mb_neg outer_ty | not type_change, isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg = translatePat fam_insts (LitPat (HsString src s)) @@ -405,22 +391,23 @@ translateNPat _ ol mb_neg _ -- | Translate a list of patterns (Note: each pattern is translated -- to a pattern vector but we do not concatenate the results). -translatePatVec :: FamInstEnvs -> [Pat Id] -> UniqSM [PatVec] +translatePatVec :: FamInstEnvs -> [Pat Id] -> PmM [PatVec] translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats +-- | Translate a constructor pattern translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar] - -> DataCon -> HsConPatDetails Id -> UniqSM PatVec + -> DataCon -> HsConPatDetails Id -> PmM PatVec translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps) = concat <$> translatePatVec fam_insts (map unLoc ps) translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2) = concat <$> translatePatVec fam_insts (map unLoc [p1,p2]) translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _)) -- Nothing matched. Make up some fresh term variables - | null fs = mkPmVarsSM arg_tys + | null fs = mkPmVars arg_tys -- The data constructor was not defined using record syntax. For the -- pattern to be in record syntax it should be empty (e.g. Just {}). -- So just like the previous case. - | null orig_lbls = ASSERT(null matched_lbls) mkPmVarsSM arg_tys + | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys -- Some of the fields appear, in the original order (there may be holes). -- Generate a simple constructor pattern and make up fresh variables for -- the rest of the fields @@ -428,20 +415,20 @@ translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _)) = ASSERT(length orig_lbls == length arg_tys) let translateOne (lbl, ty) = case lookup lbl matched_pats of Just p -> translatePat fam_insts p - Nothing -> mkPmVarsSM [ty] + Nothing -> mkPmVars [ty] in concatMapM translateOne (zip orig_lbls arg_tys) -- The fields that appear are not in the correct order. Make up fresh -- variables for all fields and add guards after matching, to force the -- evaluation in the correct order. | otherwise = do - arg_var_pats <- mkPmVarsSM arg_tys + arg_var_pats <- mkPmVars arg_tys translated_pats <- forM matched_pats $ \(x,pat) -> do pvec <- translatePat fam_insts pat return (x, pvec) let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ] guards = map (\(name,pvec) -> case lookup name zipped of - Just x -> PmGrd pvec (PmExprVar x) + Just x -> PmGrd pvec (PmExprVar (idName x)) Nothing -> panic "translateConPatVec: lookup") translated_pats @@ -463,7 +450,8 @@ translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _)) | x == y = subsetOf xs ys | otherwise = subsetOf (x:xs) ys -translateMatch :: FamInstEnvs -> LMatch Id (LHsExpr Id) -> UniqSM (PatVec,[PatVec]) +-- Translate a single match +translateMatch :: FamInstEnvs -> LMatch Id (LHsExpr Id) -> PmM (PatVec,[PatVec]) translateMatch fam_insts (L _ (Match _ lpats _ grhss)) = do pats' <- concat <$> translatePatVec fam_insts pats guards' <- mapM (translateGuards fam_insts) guards @@ -479,11 +467,11 @@ translateMatch fam_insts (L _ (Match _ lpats _ grhss)) = do -- * Transform source guards (GuardStmt Id) to PmPats (Pattern) -- | Translate a list of guard statements to a pattern vector -translateGuards :: FamInstEnvs -> [GuardStmt Id] -> UniqSM PatVec +translateGuards :: FamInstEnvs -> [GuardStmt Id] -> PmM PatVec translateGuards fam_insts guards = do all_guards <- concat <$> mapM (translateGuard fam_insts) guards return (replace_unhandled all_guards) - -- It should have been (return $ all_guards) but it is too expressive. + -- It should have been (return all_guards) but it is too expressive. -- Since the term oracle does not handle all constraints we generate, -- we (hackily) replace all constraints the oracle cannot handle with a -- single one (we need to know if there is a possibility of falure). @@ -519,28 +507,29 @@ cantFailPattern (PmGrd pv _e) cantFailPattern _ = False -- | Translate a guard statement to Pattern -translateGuard :: FamInstEnvs -> GuardStmt Id -> UniqSM PatVec -translateGuard _ (BodyStmt e _ _ _) = translateBoolGuard e -translateGuard _ (LetStmt binds) = translateLet (unLoc binds) -translateGuard fam_insts (BindStmt p e _ _ _) = translateBind fam_insts p e -translateGuard _ (LastStmt {}) = panic "translateGuard LastStmt" -translateGuard _ (ParStmt {}) = panic "translateGuard ParStmt" -translateGuard _ (TransStmt {}) = panic "translateGuard TransStmt" -translateGuard _ (RecStmt {}) = panic "translateGuard RecStmt" -translateGuard _ (ApplicativeStmt {}) = panic "translateGuard ApplicativeLastStmt" +translateGuard :: FamInstEnvs -> GuardStmt Id -> PmM PatVec +translateGuard fam_insts guard = case guard of + BodyStmt e _ _ _ -> translateBoolGuard e + LetStmt binds -> translateLet (unLoc binds) + BindStmt p e _ _ _ -> translateBind fam_insts p e + LastStmt {} -> panic "translateGuard LastStmt" + ParStmt {} -> panic "translateGuard ParStmt" + TransStmt {} -> panic "translateGuard TransStmt" + RecStmt {} -> panic "translateGuard RecStmt" + ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt" -- | Translate let-bindings -translateLet :: HsLocalBinds Id -> UniqSM PatVec +translateLet :: HsLocalBinds Id -> PmM PatVec translateLet _binds = return [] -- | Translate a pattern guard -translateBind :: FamInstEnvs -> LPat Id -> LHsExpr Id -> UniqSM PatVec +translateBind :: FamInstEnvs -> LPat Id -> LHsExpr Id -> PmM PatVec translateBind fam_insts (L _ p) e = do ps <- translatePat fam_insts p return [mkGuard ps (unLoc e)] -- | Translate a boolean guard -translateBoolGuard :: LHsExpr Id -> UniqSM PatVec +translateBoolGuard :: LHsExpr Id -> PmM PatVec translateBoolGuard e | isJust (isTrueLHsExpr e) = return [] -- The formal thing to do would be to generate (True <- True) @@ -599,7 +588,7 @@ below is the *right thing to do*: ListPat lpats elem_ty (Just (pat_ty, to_list)) otherwise -> do - (xp, xe) <- mkPmId2FormsSM pat_ty + (xp, xe) <- mkPmId2Forms pat_ty ps <- translatePatVec (map unLoc lpats) let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps g = mkGuard pats (HsApp (noLoc to_list) xe) @@ -648,39 +637,12 @@ families is not really efficient. %************************************************************************ %* * - Main Pattern Matching Check + Utilities for Pattern Match Checking %* * %************************************************************************ -} -- ---------------------------------------------------------------------------- --- * Process a vector - --- Covered, Uncovered, Divergent -process_guards :: UniqSupply -> Bool -> [PatVec] - -> (ValSetAbs, ValSetAbs, ValSetAbs) -process_guards _us _oversimplify [] = (Singleton, Empty, Empty) -- No guard -process_guards us oversimplify gs - -- If we have a list of guards but one of them is empty (True by default) - -- then we know that it is exhaustive (just a shortcut) - | any null gs = (Singleton, Empty, Singleton) - -- If the user wants the same behaviour (almost no expressivity about guards) - | oversimplify = go us Singleton [[fake_pat]] -- to signal failure - -- If the user want the full reasoning (may be non-performant) - | otherwise = go us Singleton gs - where - go _usupply missing [] = (Empty, missing, Empty) - go usupply missing (gv:gvs) = (mkUnion cs css, uss, mkUnion ds dss) - where - (us1, us2, us3, us4) = splitUniqSupply4 usupply - - cs = covered us1 Singleton gv missing - us = uncovered us2 Empty gv missing - ds = divergent us3 Empty gv missing - - (css, uss, dss) = go us4 us gvs - --- ---------------------------------------------------------------------------- -- * Basic utilities -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type @@ -695,7 +657,9 @@ pmPatType (PmGrd { pm_grd_pv = pv }) = ASSERT(patVecArity pv == 1) (pmPatType p) where Just p = find ((==1) . patternArity) pv -mkOneConFull :: Id -> UniqSupply -> DataCon -> (ValAbs, [PmConstraint]) +-- | Generate a value abstraction for a given constructor (generate +-- fresh variables of the appropriate type for arguments) +mkOneConFull :: Id -> DataCon -> PmM (ValAbs, ComplexEq, Bag EvVar) -- * x :: T tys, where T is an algebraic data type -- NB: in the case of a data familiy, T is the *representation* TyCon -- e.g. data instance T (a,b) = T1 a b @@ -709,142 +673,98 @@ mkOneConFull :: Id -> UniqSupply -> DataCon -> (ValAbs, [PmConstraint]) -- K tys :: forall bs. Q => s1 .. sn -> T tys -- -- Results: ValAbs: K (y1::s1) .. (yn::sn) --- [PmConstraint]: Q, x ~ K y1..yn - -mkOneConFull x usupply con = (con_abs, constraints) - where - - (usupply1, usupply2, usupply3) = splitUniqSupply3 usupply - - res_ty = idType x -- res_ty == TyConApp (dataConTyCon cabs_con) cabs_arg_tys - (univ_tvs, ex_tvs, eq_spec, thetas, arg_tys, _) = dataConFullSig con - data_tc = dataConTyCon con -- The representation TyCon - tc_args = case splitTyConApp_maybe res_ty of - Just (tc, tys) -> ASSERT( tc == data_tc ) tys - Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty) - - subst1 = zipTvSubst univ_tvs tc_args - - (subst, ex_tvs') = cloneTyVarBndrs subst1 ex_tvs usupply1 - - -- Fresh term variables (VAs) as arguments to the constructor - arguments = mkConVars usupply2 (substTys subst arg_tys) - -- All constraints bound by the constructor (alpha-renamed) - theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas) - evvars = zipWith (nameType "pm") (listSplitUniqSupply usupply3) theta_cs - con_abs = PmCon { pm_con_con = con +-- ComplexEq: x ~ K y1..yn +-- [EvVar]: Q +mkOneConFull x con = do + let -- res_ty == TyConApp (dataConTyCon cabs_con) cabs_arg_tys + res_ty = idType x + (univ_tvs, ex_tvs, eq_spec, thetas, arg_tys, _) = dataConFullSig con + data_tc = dataConTyCon con -- The representation TyCon + tc_args = case splitTyConApp_maybe res_ty of + Just (tc, tys) -> ASSERT( tc == data_tc ) tys + Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty) + subst1 = zipTvSubst univ_tvs tc_args + + (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM + + -- Fresh term variables (VAs) as arguments to the constructor + arguments <- mapM mkPmVar (substTys subst arg_tys) + -- All constraints bound by the constructor (alpha-renamed) + let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas) + evvars <- mapM (nameType "pm") theta_cs + let con_abs = PmCon { pm_con_con = con , pm_con_arg_tys = tc_args , pm_con_tvs = ex_tvs' , pm_con_dicts = evvars , pm_con_args = arguments } - - constraints -- term and type constraints - | null evvars = [ TmConstraint (PmExprVar x) (valAbsToPmExpr con_abs) ] - | otherwise = [ TmConstraint (PmExprVar x) (valAbsToPmExpr con_abs) - , TyConstraint evvars ] - -mkConVars :: UniqSupply -> [Type] -> [ValAbs] -- ys, fresh with the given type -mkConVars us tys = zipWith mkPmVar (listSplitUniqSupply us) tys - -tailVSA :: ValSetAbs -> ValSetAbs -tailVSA Empty = Empty -tailVSA Singleton = panic "tailVSA: Singleton" -tailVSA (Union vsa1 vsa2) = tailVSA vsa1 `mkUnion` tailVSA vsa2 -tailVSA (Constraint cs vsa) = cs `mkConstraint` tailVSA vsa -tailVSA (Cons _ vsa) = vsa -- actual work - -wrapK :: DataCon -> [Type] -> [TyVar] -> [EvVar] -> ValSetAbs -> ValSetAbs -wrapK con arg_tys ex_tvs dicts = go (dataConSourceArity con) emptylist - where - go :: Int -> DList ValAbs -> ValSetAbs -> ValSetAbs - go _ _ Empty = Empty - go 0 args vsa = PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys - , pm_con_tvs = ex_tvs, pm_con_dicts = dicts - , pm_con_args = toList args } `mkCons` vsa - go _ _ Singleton = panic "wrapK: Singleton" - go n args (Cons vs vsa) = go (n-1) (args `snoc` vs) vsa - go n args (Constraint cs vsa) = cs `mkConstraint` go n args vsa - go n args (Union vsa1 vsa2) = go n args vsa1 `mkUnion` go n args vsa2 - -newtype DList a = DL { unDL :: [a] -> [a] } - -toList :: DList a -> [a] -toList = ($[]) . unDL -{-# INLINE toList #-} - -emptylist :: DList a -emptylist = DL id -{-# INLINE emptylist #-} - -infixl `snoc` -snoc :: DList a -> a -> DList a -snoc xs x = DL (unDL xs . (x:)) -{-# INLINE snoc #-} - --- ---------------------------------------------------------------------------- --- * Smart Value Set Abstraction Constructors --- (NB: An empty value set can only be represented as `Empty') - --- | The smart constructor for Constraint (maintains VsaInvariant) -mkConstraint :: [PmConstraint] -> ValSetAbs -> ValSetAbs -mkConstraint _cs Empty = Empty -mkConstraint cs1 (Constraint cs2 vsa) = Constraint (cs1++cs2) vsa -mkConstraint cs other_vsa = Constraint cs other_vsa - --- | The smart constructor for Union (maintains VsaInvariant) -mkUnion :: ValSetAbs -> ValSetAbs -> ValSetAbs -mkUnion Empty vsa = vsa -mkUnion vsa Empty = vsa -mkUnion vsa1 vsa2 = Union vsa1 vsa2 - --- | The smart constructor for Cons (maintains VsaInvariant) -mkCons :: ValAbs -> ValSetAbs -> ValSetAbs -mkCons _ Empty = Empty -mkCons va vsa = Cons va vsa + return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars) -- ---------------------------------------------------------------------------- -- * More smart constructors and fresh variable generation +-- | Create a guard pattern mkGuard :: PatVec -> HsExpr Id -> Pattern -mkGuard pv e = PmGrd pv (hsExprToPmExpr e) - -mkPmVar :: UniqSupply -> Type -> PmPat p -mkPmVar usupply ty = PmVar (mkPmId usupply ty) - -mkPmVarSM :: Type -> UniqSM Pattern -mkPmVarSM ty = flip mkPmVar ty <$> getUniqueSupplyM - -mkPmVarsSM :: [Type] -> UniqSM PatVec -mkPmVarsSM tys = mapM mkPmVarSM tys - -mkPmId :: UniqSupply -> Type -> Id -mkPmId usupply ty = mkLocalId name ty +mkGuard pv e + | all cantFailPattern pv = PmGrd pv expr + | PmExprOther {} <- expr = fake_pat + | otherwise = PmGrd pv expr where - unique = uniqFromSupply usupply - occname = mkVarOccFS (fsLit (show unique)) - name = mkInternalName unique occname noSrcSpan - -mkPmId2FormsSM :: Type -> UniqSM (Pattern, LHsExpr Id) -mkPmId2FormsSM ty = do - us <- getUniqueSupplyM - let x = mkPmId us ty + expr = hsExprToPmExpr e + +-- | Create a term equality of the form: `(False ~ (x ~ lit))` +mkNegEq :: Id -> PmLit -> ComplexEq +mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l) +{-# INLINE mkNegEq #-} + +-- | Create a term equality of the form: `(x ~ lit)` +mkPosEq :: Id -> PmLit -> ComplexEq +mkPosEq x l = (PmExprVar (idName x), PmExprLit l) +{-# INLINE mkPosEq #-} + +-- | Generate a variable pattern of a given type +mkPmVar :: Type -> PmM (PmPat p) +mkPmVar ty = PmVar <$> mkPmId ty +{-# INLINE mkPmVar #-} + +-- | Generate many variable patterns, given a list of types +mkPmVars :: [Type] -> PmM PatVec +mkPmVars tys = mapM mkPmVar tys +{-# INLINE mkPmVars #-} + +-- | Generate a fresh `Id` of a given type +mkPmId :: Type -> PmM Id +mkPmId ty = getUniqueM >>= \unique -> + let occname = mkVarOccFS (fsLit (show unique)) + name = mkInternalName unique occname noSrcSpan + in return (mkLocalId name ty) + +-- | Generate a fresh term variable of a given and return it in two forms: +-- * A variable pattern +-- * A variable expression +mkPmId2Forms :: Type -> PmM (Pattern, LHsExpr Id) +mkPmId2Forms ty = do + x <- mkPmId ty return (PmVar x, noLoc (HsVar (noLoc x))) -- ---------------------------------------------------------------------------- -- * Converting between Value Abstractions, Patterns and PmExpr -valAbsToPmExpr :: ValAbs -> PmExpr -valAbsToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps }) - = PmExprCon c (map valAbsToPmExpr ps) -valAbsToPmExpr (PmVar { pm_var_id = x }) = PmExprVar x -valAbsToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l -valAbsToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar x - --- Convert a pattern vector to a value list abstraction by dropping the guards --- recursively (See Note [Translating As Patterns]) -coercePatVec :: PatVec -> ValVecAbs +-- | Convert a value abstraction an expression +vaToPmExpr :: ValAbs -> PmExpr +vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps }) + = PmExprCon c (map vaToPmExpr ps) +vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x) +vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l +vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x) + +-- | Convert a pattern vector to a list of value abstractions by dropping the +-- guards (See Note [Translating As Patterns]) +coercePatVec :: PatVec -> [ValAbs] coercePatVec pv = concatMap coercePmPat pv +-- | Convert a pattern to a list of value abstractions (will be either an empty +-- list if the pattern is a guard pattern, or a singleton list in all other +-- cases) by dropping the guards (See Note [Translating As Patterns]) coercePmPat :: Pattern -> [ValAbs] coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }] coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }] @@ -856,7 +776,7 @@ coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys , pm_con_args = coercePatVec args }] coercePmPat (PmGrd {}) = [] -- drop the guards --- Get all constructors in the family (including given) +-- | Get all constructors in the family (including given) allConstructors :: DataCon -> [DataCon] allConstructors = tyConDataCons . dataConTyCon @@ -866,108 +786,21 @@ allConstructors = tyConDataCons . dataConTyCon newEvVar :: Name -> Type -> EvVar newEvVar name ty = mkLocalId name (toTcType ty) -nameType :: String -> UniqSupply -> Type -> EvVar -nameType name usupply ty = newEvVar idname ty - where - unique = uniqFromSupply usupply - occname = mkVarOccFS (fsLit (name++"_"++show unique)) - idname = mkInternalName unique occname noSrcSpan - --- | Partition the constraints to type cs, term cs and forced variables -splitConstraints :: [PmConstraint] -> ([EvVar], [(PmExpr, PmExpr)], Maybe Id) -splitConstraints [] = ([],[],Nothing) -splitConstraints (c : rest) - = case c of - TyConstraint cs -> (cs ++ ty_cs, tm_cs, bot_cs) - TmConstraint e1 e2 -> (ty_cs, (e1,e2):tm_cs, bot_cs) - BtConstraint cs -> ASSERT(isNothing bot_cs) -- NB: Only one x ~ _|_ - (ty_cs, tm_cs, Just cs) - where - (ty_cs, tm_cs, bot_cs) = splitConstraints rest +nameType :: String -> Type -> PmM EvVar +nameType name ty = do + unique <- getUniqueM + let occname = mkVarOccFS (fsLit (name++"_"++show unique)) + idname = mkInternalName unique occname noSrcSpan + return (newEvVar idname ty) {- %************************************************************************ %* * - The oracles + The type oracle %* * %************************************************************************ -} --- | Check whether at least a path in a value set --- abstraction has satisfiable constraints. -anySatVSA :: ValSetAbs -> PmM Bool -anySatVSA vsa = notNull <$> pruneVSABound 1 vsa - -pruneVSA :: ValSetAbs -> PmM [([PmExpr], [ComplexEq])] --- Prune a Value Set abstraction, keeping only as many as we are going to print --- plus one more. We need the additional one to be able to print "..." when the --- uncovered are too many. -pruneVSA vsa = pruneVSABound (maximum_output+1) vsa - --- | Apply a term substitution to a value vector abstraction. All VAs are --- transformed to PmExpr (used only before pretty printing). -substInValVecAbs :: PmVarEnv -> ValVecAbs -> [PmExpr] -substInValVecAbs subst = map (exprDeepLookup subst . valAbsToPmExpr) - -mergeBotCs :: Maybe Id -> Maybe Id -> Maybe Id -mergeBotCs (Just x) Nothing = Just x -mergeBotCs Nothing (Just y) = Just y -mergeBotCs Nothing Nothing = Nothing -mergeBotCs (Just _) (Just _) = panic "mergeBotCs: two (x ~ _|_) constraints" - --- | Wrap up the term oracle's state once solving is complete. Drop any --- information about unhandled constraints (involving HsExprs) and flatten --- (height 1) the substitution. -wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv) -wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst) - --- | Prune all paths in a value set abstraction with inconsistent constraints. --- Returns only `n' value vector abstractions, when `n' is given as an argument. -pruneVSABound :: Int -> ValSetAbs -> PmM [([PmExpr], [ComplexEq])] -pruneVSABound n v = go n init_cs emptylist v - where - init_cs :: ([EvVar], TmState, Maybe Id) - init_cs = ([], initialTmState, Nothing) - - go :: Int -> ([EvVar], TmState, Maybe Id) -> DList ValAbs - -> ValSetAbs -> PmM [([PmExpr], [ComplexEq])] - go n all_cs@(ty_cs, tm_env, bot_ct) vec in_vsa - | n <= 0 = return [] -- no need to keep going - | otherwise = case in_vsa of - Empty -> return [] - Union vsa1 vsa2 -> do - vecs1 <- go n all_cs vec vsa1 - vecs2 <- go (n - length vecs1) all_cs vec vsa2 - return (vecs1 ++ vecs2) - Singleton -> do - -- TODO: Provide an incremental interface for the type oracle - sat <- tyOracle (listToBag ty_cs) - return $ case sat of - True -> let (residual_eqs, subst) = wrapUpTmState tm_env - vector = substInValVecAbs subst (toList vec) - in [(vector, residual_eqs)] - False -> [] - - Constraint cs vsa -> case splitConstraints cs of - (new_ty_cs, new_tm_cs, new_bot_ct) -> - case tmOracle tm_env new_tm_cs of - Just new_tm_env -> - let bot = mergeBotCs new_bot_ct bot_ct - ans = case bot of - Nothing -> True -- covered - Just b -> canDiverge b new_tm_env -- divergent - in case ans of - True -> go n (new_ty_cs++ty_cs,new_tm_env,bot) vec vsa - False -> return [] - Nothing -> return [] - Cons va vsa -> go n all_cs (vec `snoc` va) vsa - --- | This variable shows the maximum number of lines of output generated for --- warnings. It will limit the number of patterns/equations displayed to --- maximum_output. (TODO: add command-line option?) -maximum_output :: Int -maximum_output = 4 - -- | Check whether a set of type constraints is satisfiable. tyOracle :: Bag EvVar -> PmM Bool tyOracle evs @@ -984,11 +817,15 @@ tyOracle evs %************************************************************************ -} +-- | The arity of a pattern/pattern vector is the +-- number of top-level patterns that are not guards type PmArity = Int +-- | Compute the arity of a pattern vector patVecArity :: PatVec -> PmArity patVecArity = sum . map patternArity +-- | Compute the arity of a pattern patternArity :: Pattern -> PmArity patternArity (PmGrd {}) = 0 patternArity _other_pat = 1 @@ -996,305 +833,270 @@ patternArity _other_pat = 1 {- %************************************************************************ %* * - Heart of the algorithm: Function patVectProc + Heart of the algorithm: Function pmcheck %* * %************************************************************************ --} --- | Process a single vector -patVectProc :: Bool -> (PatVec, [PatVec]) -> ValSetAbs - -> PmM (Bool, Bool, ValSetAbs) -patVectProc oversimplify (vec,gvs) vsa = do - us <- getUniqueSupplyM - let (c_def, u_def, d_def) = process_guards us oversimplify gvs - (usC, usU, usD) <- getUniqueSupplyM3 - mb_c <- anySatVSA (covered usC c_def vec vsa) - mb_d <- anySatVSA (divergent usD d_def vec vsa) - let vsa' = uncovered usU u_def vec vsa - return (mb_c, mb_d, vsa') - --- | Covered, Uncovered, Divergent -covered, uncovered, divergent :: UniqSupply -> ValSetAbs - -> PatVec -> ValSetAbs -> ValSetAbs -covered us gvsa vec vsa = pmTraverse us gvsa cMatcher vec vsa -uncovered us gvsa vec vsa = pmTraverse us gvsa uMatcher vec vsa -divergent us gvsa vec vsa = pmTraverse us gvsa dMatcher vec vsa +Main functions are: --- ---------------------------------------------------------------------------- --- * Generic traversal function --- --- | Because we represent Value Set Abstractions as a different datatype, more --- cases than the ones described in the paper appear. Since they are the same --- for all three functions (covered, uncovered, divergent), function --- `pmTraverse' handles these cases (`pmTraverse' also takes care of the --- Guard-Case since it is common for all). The actual work is done by functions --- `cMatcher', `uMatcher' and `dMatcher' below. - -pmTraverse :: UniqSupply - -> ValSetAbs -- gvsa - -> PmMatcher -- what to do - -> PatVec - -> ValSetAbs - -> ValSetAbs -pmTraverse _us _gvsa _rec _vec Empty = Empty -pmTraverse _us gvsa _rec [] Singleton = gvsa -pmTraverse _us _gvsa _rec [] (Cons _ _) = panic "pmTraverse: cons" -pmTraverse us gvsa rec vec (Union vsa1 vsa2) - = mkUnion (pmTraverse us1 gvsa rec vec vsa1) - (pmTraverse us2 gvsa rec vec vsa2) - where (us1, us2) = splitUniqSupply us -pmTraverse us gvsa rec vec (Constraint cs vsa) - = mkConstraint cs (pmTraverse us gvsa rec vec vsa) -pmTraverse us gvsa rec (p:ps) vsa - | PmGrd pv e <- p - = -- Guard Case - let (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType p) - cs = [TmConstraint (PmExprVar y) e] - in mkConstraint cs $ tailVSA $ - pmTraverse us2 gvsa rec (pv++ps) (PmVar y `mkCons` vsa) - - -- Constructor/Variable/Literal Case - | Cons va vsa <- vsa = rec us gvsa p ps va vsa - -- Impossible: length mismatch for ValSetAbs and PatVec - | otherwise = panic "pmTraverse: singleton" -- can't be anything else - -type PmMatcher = UniqSupply - -> ValSetAbs - -> Pattern -> PatVec -- Vector head and tail - -> ValAbs -> ValSetAbs -- VSA head and tail - -> ValSetAbs - -cMatcher, uMatcher, dMatcher :: PmMatcher - --- cMatcher --- ---------------------------------------------------------------------------- +* mkInitialUncovered :: [Id] -> PmM Uncovered --- CVar -cMatcher us gvsa (PmVar x) ps va vsa - = va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa) - where cs = [TmConstraint (PmExprVar x) (valAbsToPmExpr va)] + Generates the initial uncovered set. Term and type constraints in scope + are checked, if they are inconsistent, the set is empty, otherwise, the + set contains only a vector of variables with the constraints in scope. --- CLitCon -cMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa - = va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa) - where cs = [ TmConstraint (PmExprLit l) (valAbsToPmExpr va) ] +* pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM Triple --- CConLit -cMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa - = cMatcher us3 gvsa p ps con_abs (mkConstraint cs vsa) - where - (us1, us2, us3) = splitUniqSupply3 us - y = mkPmId us1 (pmPatType p) - (con_abs, all_cs) = mkOneConFull y us2 (pm_con_con p) - cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs - --- CConNLit -cMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps - (PmNLit { pm_lit_id = x }) vsa - = cMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa) - where - (us1, us2) = splitUniqSupply us - (con_abs, all_cs) = mkOneConFull x us1 con - --- CConCon -cMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps - (PmCon { pm_con_con = c2, pm_con_args = args2 }) vsa - | c1 /= c2 = Empty - | otherwise = wrapK c1 (pm_con_arg_tys p) - (pm_con_tvs p) - (pm_con_dicts p) - (covered us gvsa (args1 ++ ps) - (foldr mkCons vsa args2)) - --- CLitLit -cMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of - -- See Note [Undecidable Equality for Overloaded Literals] in PmExpr - True -> va `mkCons` covered us gvsa ps vsa -- match - False -> Empty -- mismatch - --- CConVar -cMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa - = cMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa) - where - (us1, us2) = splitUniqSupply us - (con_abs, all_cs) = mkOneConFull x us1 con + Checks redundancy, coverage and inaccessibility, using auxilary functions + `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is + common in all three checks (see paper) and calls `pmcheckGuards` when the + whole clause is checked, or `pmcheckHd` when the pattern vector does not + start with a guard. --- CLitVar -cMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa - = cMatcher us gvsa p ps lit_abs (mkConstraint cs vsa) - where - lit_abs = PmLit l - cs = [TmConstraint (PmExprVar x) (PmExprLit l)] +* pmcheckGuards :: [PatVec] -> ValVec -> PmM Triple --- CLitNLit -cMatcher us gvsa (p@(PmLit l)) ps - (PmNLit { pm_lit_id = x, pm_lit_not = lits }) vsa - | all (not . eqPmLit l) lits - = cMatcher us gvsa p ps lit_abs (mkConstraint cs vsa) - | otherwise = Empty - where - lit_abs = PmLit l - cs = [TmConstraint (PmExprVar x) (PmExprLit l)] + Processes the guards. --- Impossible: handled by pmTraverse -cMatcher _ _ (PmGrd {}) _ _ _ = panic "Check.cMatcher: Guard" +* pmcheckHd :: Pattern -> PatVec -> [PatVec] + -> ValAbs -> ValVec -> PmM Triple --- uMatcher --- ---------------------------------------------------------------------------- - --- UVar -uMatcher us gvsa (PmVar x) ps va vsa - = va `mkCons` (cs `mkConstraint` uncovered us gvsa ps vsa) - where cs = [TmConstraint (PmExprVar x) (valAbsToPmExpr va)] + Worker: This function implements functions `covered`, `uncovered` and + `divergent` from the paper at once. Slightly different from the paper because + it does not even produce the covered and uncovered sets. Since we only care + about whether a clause covers SOMETHING or if it may forces ANY argument, we + only store a boolean in both cases, for efficiency. +-} --- ULitCon -uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa - = uMatcher us2 gvsa (PmVar y) ps va (mkConstraint cs vsa) - where - (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType va) - cs = [TmConstraint (PmExprVar y) (PmExprLit l)] +-- | Lift a pattern matching action from a single value vector abstration to a +-- value set abstraction, but calling it on every vector and the combining the +-- results. +runMany :: (ValVec -> PmM Triple) -> (Uncovered -> PmM Triple) +runMany pm us = mapAndUnzip3M pm us >>= \(css, uss, dss) -> + return (or css, concat uss, or dss) +{-# INLINE runMany #-} --- UConLit -uMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa - = uMatcher us2 gvsa p ps (PmVar y) (mkConstraint cs vsa) - where - (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType p) - cs = [TmConstraint (PmExprVar y) (PmExprLit l)] - --- UConNLit -uMatcher us gvsa (p@(PmCon {})) ps (PmNLit { pm_lit_id = x }) vsa - = uMatcher us gvsa p ps (PmVar x) vsa - --- UConCon -uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps - (va@(PmCon { pm_con_con = c2, pm_con_args = args2 })) vsa - | c1 /= c2 = va `mkCons` vsa - | otherwise = wrapK c1 (pm_con_arg_tys p) - (pm_con_tvs p) - (pm_con_dicts p) - (uncovered us gvsa (args1 ++ ps) - (foldr mkCons vsa args2)) - --- ULitLit -uMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of - -- See Note [Undecidable Equality for Overloaded Literals] in PmExpr - True -> va `mkCons` uncovered us gvsa ps vsa -- match - False -> va `mkCons` vsa -- mismatch - --- UConVar -uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa - = uncovered us2 gvsa (p : ps) inst_vsa - where - (us1, us2) = splitUniqSupply us - - -- Unfold the variable to all possible constructor patterns - cons_cs = zipWith (mkOneConFull x) (listSplitUniqSupply us1) - (allConstructors con) - add_one (va,cs) valset = mkUnion valset (va `mkCons` mkConstraint cs vsa) - inst_vsa = foldr add_one Empty cons_cs -- instantiated vsa [x mapsto K_j ys] - --- ULitVar -uMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa - = mkUnion (uMatcher us gvsa p ps (PmLit l) (mkConstraint match_cs vsa)) - (non_match_cs `mkConstraint` (PmNLit x [l] `mkCons` vsa)) +-- | Generate the initial uncovered set. It initializes the +-- delta with all term and type constraints in scope. +mkInitialUncovered :: [Id] -> PmM Uncovered +mkInitialUncovered vars = do + ty_cs <- getDictsDs + tm_cs <- map toComplex . bagToList <$> getTmCsDs + sat_ty <- tyOracle ty_cs + return $ case (sat_ty, tmOracle initialTmState tm_cs) of + (True, Just tm_state) -> [ValVec patterns (MkDelta ty_cs tm_state)] + -- If any of the term/type constraints are non + -- satisfiable, the initial uncovered set is empty + _non_satisfiable -> [] where - match_cs = [ TmConstraint (PmExprVar x) (PmExprLit l)] - -- See Note [Representation of Term Equalities] - non_match_cs = [ TmConstraint falsePmExpr - (PmExprEq (PmExprVar x) (PmExprLit l)) ] - --- ULitNLit -uMatcher us gvsa (p@(PmLit l)) ps - (va@(PmNLit { pm_lit_id = x, pm_lit_not = lits })) vsa - | all (not . eqPmLit l) lits - = mkUnion (uMatcher us gvsa p ps (PmLit l) (mkConstraint match_cs vsa)) - (non_match_cs `mkConstraint` (PmNLit x (l:lits) `mkCons` vsa)) - | otherwise = va `mkCons` vsa + patterns = map PmVar vars + +-- | Increase the counter for elapsed algorithm iterations, check that the +-- limit is not exceeded and call `pmcheck` +pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM Triple +pmcheckI ps guards vva = incrCheckPmIterDs >> pmcheck ps guards vva +{-# INLINE pmcheckI #-} + +-- | Increase the counter for elapsed algorithm iterations, check that the +-- limit is not exceeded and call `pmcheckGuards` +pmcheckGuardsI :: [PatVec] -> ValVec -> PmM Triple +pmcheckGuardsI gvs vva = incrCheckPmIterDs >> pmcheckGuards gvs vva +{-# INLINE pmcheckGuardsI #-} + +-- | Increase the counter for elapsed algorithm iterations, check that the +-- limit is not exceeded and call `pmcheckHd` +pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec -> PmM Triple +pmcheckHdI p ps guards va vva = incrCheckPmIterDs >> + pmcheckHd p ps guards va vva +{-# INLINE pmcheckHdI #-} + +-- | Matching function: Check simultaneously a clause (takes separately the +-- patterns and the list of guards) for exhaustiveness, redundancy and +-- inaccessibility. +pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM Triple +pmcheck [] guards vva@(ValVec [] _) + | null guards = return (True, [], False) + | otherwise = pmcheckGuardsI guards vva + +-- Guard +pmcheck (p@(PmGrd pv e) : ps) guards vva@(ValVec vas delta) + -- short-circuit if the guard pattern is useless. + -- we just have two possible outcomes: fail here or match and recurse + -- none of the two contains any useful information about the failure + -- though. So just have these two cases but do not do all the boilerplate + | isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva + | otherwise = do + y <- mkPmId (pmPatType p) + let tm_state = extendSubst y e (delta_tm_cs delta) + delta' = delta { delta_tm_cs = tm_state } + utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta') + +pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons" +pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil" + +pmcheck (p:ps) guards (ValVec (va:vva) delta) + = pmcheckHdI p ps guards va (ValVec vva delta) + +-- | Check the list of guards +pmcheckGuards :: [PatVec] -> ValVec -> PmM Triple +pmcheckGuards [] vva = return (False, [vva], False) +pmcheckGuards (gv:gvs) vva = do + (cs, vsa, ds ) <- pmcheckI gv [] vva + (css, vsas, dss) <- runMany (pmcheckGuardsI gvs) vsa + return (cs || css, vsas, ds || dss) + +-- | Worker function: Implements all cases described in the paper for all three +-- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard` +-- cases which are handled by `pmcheck` +pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec -> PmM Triple + +-- Var +pmcheckHd (PmVar x) ps guards va (ValVec vva delta) + | Just tm_state <- solveOneEq (delta_tm_cs delta) + (PmExprVar (idName x), vaToPmExpr va) + = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state})) + | otherwise = return (False, [], False) + +-- ConCon +pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards + (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta) + | c1 /= c2 = return (False, [ValVec (va:vva) delta], False) + | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p) + <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta) + +-- LitLit +pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva = case eqPmLit l1 l2 of + True -> ucon va <$> pmcheckI ps guards vva + False -> return $ ucon va (False, [vva], False) + +-- ConVar +pmcheckHd (p@(PmCon { pm_con_con = con })) ps guards + (PmVar x) (ValVec vva delta) = do + cons_cs <- mapM (mkOneConFull x) (allConstructors con) + inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do + let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state + sat_ty <- if isEmptyBag ty_cs then return True + else tyOracle ty_state + return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of + (True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)] + _ty_or_tm_failed -> [] + + force_if (canDiverge (idName x) (delta_tm_cs delta)) <$> + runMany (pmcheckI (p:ps) guards) inst_vsa + +-- LitVar +pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta) + = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$> + mkUnion non_matched <$> + case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of + Just tm_state -> pmcheckHdI p ps guards (PmLit l) $ + ValVec vva (delta {delta_tm_cs = tm_state}) + Nothing -> return (False, [], False) where - match_cs = [ TmConstraint (PmExprVar x) (PmExprLit l)] - -- See Note [Representation of Term Equalities] - non_match_cs = [ TmConstraint falsePmExpr - (PmExprEq (PmExprVar x) (PmExprLit l)) ] - --- Impossible: handled by pmTraverse -uMatcher _ _ (PmGrd {}) _ _ _ = panic "Check.uMatcher: Guard" - --- dMatcher --- ---------------------------------------------------------------------------- + us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l) + = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })] + | otherwise = [] --- DVar -dMatcher us gvsa (PmVar x) ps va vsa - = va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa) - where cs = [TmConstraint (PmExprVar x) (valAbsToPmExpr va)] + non_matched = (False, us, False) --- DLitCon -dMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa - = va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa) - where cs = [ TmConstraint (PmExprLit l) (valAbsToPmExpr va) ] - --- DConLit -dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmLit l) vsa - = dMatcher us3 gvsa p ps con_abs (mkConstraint cs vsa) - where - (us1, us2, us3) = splitUniqSupply3 us - y = mkPmId us1 (pmPatType p) - (con_abs, all_cs) = mkOneConFull y us2 con - cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs - --- DConNLit -dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps - (PmNLit { pm_lit_id = x }) vsa - = dMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa) - where - (us1, us2) = splitUniqSupply us - (con_abs, all_cs) = mkOneConFull x us1 con - --- DConCon -dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps - (PmCon { pm_con_con = c2, pm_con_args = args2 }) vsa - | c1 /= c2 = Empty - | otherwise = wrapK c1 (pm_con_arg_tys p) - (pm_con_tvs p) - (pm_con_dicts p) - (divergent us gvsa (args1 ++ ps) - (foldr mkCons vsa args2)) - --- DLitLit -dMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of - -- See Note [Undecidable Equality for Overloaded Literals] in PmExpr - True -> va `mkCons` divergent us gvsa ps vsa -- match - False -> Empty -- mismatch - --- DConVar -dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa - = mkUnion (PmVar x `mkCons` mkConstraint [BtConstraint x] vsa) - (dMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa)) +-- LitNLit +pmcheckHd (p@(PmLit l)) ps guards + (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta) + | all (not . eqPmLit l) lits + , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l) + -- Both guards check the same so it would be sufficient to have only + -- the second one. Nevertheless, it is much cheaper to check whether + -- the literal is in the list so we check it first, to avoid calling + -- the term oracle (`solveOneEq`) if possible + = mkUnion non_matched <$> + pmcheckHdI p ps guards (PmLit l) + (ValVec vva (delta { delta_tm_cs = tm_state })) + | otherwise = return non_matched where - (us1, us2) = splitUniqSupply us - (con_abs, all_cs) = mkOneConFull x us1 con + us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l) + = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })] + | otherwise = [] --- DLitVar -dMatcher us gvsa (PmLit l) ps (PmVar x) vsa - = mkUnion (PmVar x `mkCons` mkConstraint [BtConstraint x] vsa) - (dMatcher us gvsa (PmLit l) ps (PmLit l) (mkConstraint cs vsa)) - where - cs = [TmConstraint (PmExprVar x) (PmExprLit l)] + non_matched = (False, us, False) --- DLitNLit -dMatcher us gvsa (p@(PmLit l)) ps - (PmNLit { pm_lit_id = x, pm_lit_not = lits }) vsa - | all (not . eqPmLit l) lits - = dMatcher us gvsa p ps lit_abs (mkConstraint cs vsa) - | otherwise = Empty - where - lit_abs = PmLit l - cs = [TmConstraint (PmExprVar x) (PmExprLit l)] +-- ---------------------------------------------------------------------------- +-- The following three can happen only in cases like #322 where constructors +-- and overloaded literals appear in the same match. The general strategy is +-- to replace the literal (positive/negative) by a variable and recurse. The +-- fact that the variable is equal to the literal is recorded in `delta` so +-- no information is lost + +-- LitCon +pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta) + = do y <- mkPmId (pmPatType va) + let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta) + delta' = delta { delta_tm_cs = tm_state } + pmcheckHdI (PmVar y) ps guards va (ValVec vva delta') + +-- ConLit +pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta) + = do y <- mkPmId (pmPatType p) + let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta) + delta' = delta { delta_tm_cs = tm_state } + pmcheckHdI p ps guards (PmVar y) (ValVec vva delta') + +-- ConNLit +pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva + = pmcheckHdI p ps guards (PmVar x) vva + +-- Impossible: handled by pmcheck +pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard" --- Impossible: handled by pmTraverse -dMatcher _ _ (PmGrd {}) _ _ _ = panic "Check.dMatcher: Guard" +-- ---------------------------------------------------------------------------- +-- * Utilities for main checking + +-- | Take the tail of all value vector abstractions in the uncovered set +utail :: Triple -> Triple +utail (cs, vsa, ds) = (cs, vsa', ds) + where vsa' = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ] + +-- | Prepend a value abstraction to all value vector abstractions in the +-- uncovered set +ucon :: ValAbs -> Triple -> Triple +ucon va (cs, vsa, ds) = (cs, vsa', ds) + where vsa' = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ] + +-- | Given a data constructor of arity `a` and an uncovered set containing +-- value vector abstractions of length `(a+n)`, pass the first `n` value +-- abstractions to the constructor (Hence, the resulting value vector +-- abstractions will have length `n+1`) +kcon :: DataCon -> [Type] -> [TyVar] -> [EvVar] -> Triple -> Triple +kcon con arg_tys ex_tvs dicts (cs, vsa, ds) + = (cs, [ ValVec (va:vva) delta + | ValVec vva' delta <- vsa + , let (args, vva) = splitAt n vva' + , let va = PmCon { pm_con_con = con + , pm_con_arg_tys = arg_tys + , pm_con_tvs = ex_tvs + , pm_con_dicts = dicts + , pm_con_args = args } ] + , ds) + where n = dataConSourceArity con + +-- | Get the union of two covered, uncovered and divergent value set +-- abstractions. Since the covered and divergent sets are represented by a +-- boolean, union means computing the logical or (at least one of the two is +-- non-empty). +mkUnion :: Triple -> Triple -> Triple +mkUnion (cs1, vsa1, ds1) (cs2, vsa2, ds2) + = (cs1 || cs2, vsa1 ++ vsa2, ds1 || ds2) + +-- | Add a value vector abstraction to a value set abstraction (uncovered). +mkCons :: ValVec -> Triple -> Triple +mkCons vva (cs, vsa, ds) = (cs, vva:vsa, ds) + +-- | Set the divergent set to not empty +forces :: Triple -> Triple +forces (cs, us, _) = (cs, us, True) + +-- | Set the divergent set to non-empty if the flag is `True` +force_if :: Bool -> Triple -> Triple +force_if True (cs,us,_) = (cs,us,True) +force_if False triple = triple -- ---------------------------------------------------------------------------- -- * Propagation of term constraints inwards when checking nested matches @@ -1341,10 +1143,9 @@ genCaseTmCs2 :: Maybe (LHsExpr Id) -- Scrutinee genCaseTmCs2 Nothing _ _ = return emptyBag genCaseTmCs2 (Just scr) [p] [var] = do fam_insts <- dsGetFamInstEnvs - liftUs $ do - [e] <- map valAbsToPmExpr . coercePatVec <$> translatePat fam_insts p - let scr_e = lhsExprToPmExpr scr - return $ listToBag [(var, e), (var, scr_e)] + [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p + let scr_e = lhsExprToPmExpr scr + return $ listToBag [(var, e), (var, scr_e)] genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase" -- | Generate a simple equality when checking a case expression: @@ -1395,12 +1196,11 @@ Gives the following with the first translation: If we use the second translation we get an empty set, independently of the oracle. Since the pattern `p' may contain guard patterns though, it cannot be used as an expression. That's why we call `coercePatVec' to drop the guard and -`valAbsToPmExpr' to transform the value abstraction to an expression in the +`vaToPmExpr' to transform the value abstraction to an expression in the guard pattern (value abstractions are a subset of expressions). We keep the guards in the first pattern `p' though. --} -{- + %************************************************************************ %* * Pretty printing of exhaustiveness/redundancy check warnings @@ -1414,24 +1214,27 @@ isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool isAnyPmCheckEnabled dflags (DsMatchContext kind _loc) = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind --- | Issue a warning if the guards are too many and the checker gives up -warnManyGuards :: DsMatchContext -> DsM () -warnManyGuards (DsMatchContext kind loc) - = putSrcSpanDs loc $ warnDs $ vcat - [ sep [ text "Too many guards in" <+> pprMatchContext kind - , text "Guard checking has been over-simplified" ] - , parens (text "Use:" <+> (opt_1 $$ opt_2)) ] - where - opt_1 = hang (text "-Wno-too-many-guards") 2 $ - text "to suppress this warning" - opt_2 = hang (text "-ffull-guard-reasoning") 2 $ vcat - [ text "to run the full checker (may increase" - , text "compilation time and memory consumption)" ] - -dsPmWarn :: DynFlags -> DsMatchContext -> DsM PmResult -> DsM () -dsPmWarn dflags ctx@(DsMatchContext kind loc) mPmResult +instance Outputable ValVec where + ppr (ValVec vva delta) + = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta) + vector = substInValAbs subst vva + in ppr_uncovered (vector, residual_eqs) + +-- | Apply a term substitution to a value vector abstraction. All VAs are +-- transformed to PmExpr (used only before pretty printing). +substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr] +substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr) + +-- | Wrap up the term oracle's state once solving is complete. Drop any +-- information about unhandled constraints (involving HsExprs) and flatten +-- (height 1) the substitution. +wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv) +wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst) + +-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility) +dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM () +dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result = when (flag_i || flag_u) $ do - (redundant, inaccessible, uncovered) <- mPmResult let exists_r = flag_i && notNull redundant exists_i = flag_i && notNull inaccessible exists_u = flag_u && notNull uncovered @@ -1439,26 +1242,47 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) mPmResult when exists_i $ putSrcSpanDs loc (warnDs (pprEqns inaccessible imsg)) when exists_u $ putSrcSpanDs loc (warnDs (pprEqnsU uncovered)) where + (redundant, uncovered, inaccessible) = pm_result + flag_i = wopt Opt_WarnOverlappingPatterns dflags flag_u = exhaustive dflags kind rmsg = "are redundant" imsg = "have inaccessible right hand side" - pprEqns qs text = pp_context ctx (ptext (sLit text)) $ \f -> + pprEqns qs txt = pp_context ctx (text txt) $ \f -> vcat (map (ppr_eqn f kind) (take maximum_output qs)) $$ dots qs pprEqnsU qs = pp_context ctx (text "are non-exhaustive") $ \_ -> case qs of -- See #11245 - [([],_)] -> text "Guards do not cover entire pattern space" - _missing -> let us = map ppr_uncovered qs + [ValVec [] _] + -> text "Guards do not cover entire pattern space" + _missing -> let us = map ppr qs in hang (text "Patterns not matched:") 4 (vcat (take maximum_output us) $$ dots us) +-- | Issue a warning when the predefined number of iterations is exceeded +-- for the pattern match checker +warnPmIters :: DynFlags -> DsMatchContext -> PmM () +warnPmIters dflags (DsMatchContext kind loc) + = when (flag_i || flag_u) $ do + iters <- maxPmCheckIterations <$> getDynFlags + putSrcSpanDs loc (warnDs (msg iters)) + where + ctxt = pprMatchContext kind + msg is = fsep [ text "Pattern match checker exceeded" + , parens (ppr is), text "iterations in", ctxt <> dot + , text "(Use fmax-pmcheck-iterations=n" + , text "to set the maximun number of iterations to n)" ] + + flag_i = wopt Opt_WarnOverlappingPatterns dflags + flag_u = exhaustive dflags kind + dots :: [a] -> SDoc dots qs | qs `lengthExceeds` maximum_output = text "..." | otherwise = empty +-- | Check whether the exhaustiveness checker should run (exhaustiveness only) exhaustive :: DynFlags -> HsMatchContext id -> Bool exhaustive dflags (FunRhs {}) = wopt Opt_WarnIncompletePatterns dflags exhaustive dflags CaseAlt = wopt Opt_WarnIncompletePatterns dflags @@ -1506,6 +1330,12 @@ ppr_uncovered (expr_vec, complex) sdoc_vec = mapM pprPmExprWithParens expr_vec (vec,cs) = runPmPprM sdoc_vec (filterComplex complex) +-- | This variable shows the maximum number of lines of output generated for +-- warnings. It will limit the number of patterns/equations displayed to +-- maximum_output. (TODO: add command-line option?) +maximum_output :: Int +maximum_output = 4 + {- Note [Representation of Term Equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In the paper, term constraints always take the form (x ~ e). Of course, a more diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs index 92bfde0e5d..3d922f6728 100644 --- a/compiler/deSugar/DsMonad.hs +++ b/compiler/deSugar/DsMonad.hs @@ -34,6 +34,9 @@ module DsMonad ( -- Getting and setting EvVars and term constraints in local environment getDictsDs, addDictsDs, getTmCsDs, addTmCsDs, + -- Iterations for pm checking + incrCheckPmIterDs, resetPmIterDs, + -- Warnings DsWarning, warnDs, failWithDs, discardWarningsDs, @@ -146,10 +149,12 @@ initDs :: HscEnv initDs hsc_env mod rdr_env type_env fam_inst_env thing_inside = do { msg_var <- newIORef (emptyBag, emptyBag) ; static_binds_var <- newIORef [] + ; pm_iter_var <- newIORef 0 ; let dflags = hsc_dflags hsc_env (ds_gbl_env, ds_lcl_env) = mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var + pm_iter_var ; either_res <- initTcRnIf 'd' hsc_env ds_gbl_env ds_lcl_env $ loadDAP $ @@ -225,11 +230,12 @@ initDsTc thing_inside ; msg_var <- getErrsVar ; dflags <- getDynFlags ; static_binds_var <- liftIO $ newIORef [] + ; pm_iter_var <- liftIO $ newIORef 0 ; let type_env = tcg_type_env tcg_env rdr_env = tcg_rdr_env tcg_env fam_inst_env = tcg_fam_inst_env tcg_env ds_envs = mkDsEnvs dflags this_mod rdr_env type_env fam_inst_env - msg_var static_binds_var + msg_var static_binds_var pm_iter_var ; setEnvs ds_envs thing_inside } @@ -258,8 +264,8 @@ initTcDsForSolver thing_inside mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv -> IORef Messages -> IORef [(Fingerprint, (Id, CoreExpr))] - -> (DsGblEnv, DsLclEnv) -mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var + -> IORef Int -> (DsGblEnv, DsLclEnv) +mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var pmvar = let if_genv = IfGblEnv { if_rec_types = Just (mod, return type_env) } if_lenv = mkIfLclEnv mod (text "GHC error in desugarer lookup in" <+> ppr mod) real_span = realSrcLocSpan (mkRealSrcLoc (moduleNameFS (moduleName mod)) 1 1) @@ -272,10 +278,11 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var , ds_parr_bi = panic "DsMonad: uninitialised ds_parr_bi" , ds_static_binds = static_binds_var } - lcl_env = DsLclEnv { dsl_meta = emptyNameEnv - , dsl_loc = real_span - , dsl_dicts = emptyBag - , dsl_tm_cs = emptyBag + lcl_env = DsLclEnv { dsl_meta = emptyNameEnv + , dsl_loc = real_span + , dsl_dicts = emptyBag + , dsl_tm_cs = emptyBag + , dsl_pm_iter = pmvar } in (gbl_env, lcl_env) @@ -355,6 +362,24 @@ addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a addTmCsDs tm_cs = updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) }) +-- | Check that we have not done more iterations +-- than we are supposed to and inrease the counter + +-- | Increase the counter for elapsed pattern match check iterations. +-- If the current counter is already over the limit, fail +incrCheckPmIterDs :: DsM () +incrCheckPmIterDs = do + env <- getLclEnv + cnt <- readTcRef (dsl_pm_iter env) + max_iters <- maxPmCheckIterations <$> getDynFlags + if cnt >= max_iters + then failM + else updTcRef (dsl_pm_iter env) (+1) + +-- | Reset the counter for pattern match check iterations to zero +resetPmIterDs :: DsM () +resetPmIterDs = do { env <- getLclEnv; writeTcRef (dsl_pm_iter env) 0 } + getSrcSpanDs :: DsM SrcSpan getSrcSpanDs = do { env <- getLclEnv ; return (RealSrcSpan (dsl_loc env)) } diff --git a/compiler/deSugar/Match.hs b/compiler/deSugar/Match.hs index 0128488d62..be089e6788 100644 --- a/compiler/deSugar/Match.hs +++ b/compiler/deSugar/Match.hs @@ -694,21 +694,9 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches when (isAnyPmCheckEnabled dflags (DsMatchContext ctxt locn)) $ do - -- Count the number of guards that can fail - guards <- computeNoGuards matches - - let simplify = not (gopt Opt_FullGuardReasoning dflags) - && (guards > maximum_failing_guards) - -- See Note [Type and Term Equality Propagation] addTmCsDs (genCaseTmCs1 mb_scr new_vars) $ - dsPmWarn dflags (DsMatchContext ctxt locn) $ - checkMatches simplify new_vars matches - - when (not (gopt Opt_FullGuardReasoning dflags) - && wopt Opt_WarnTooManyGuards dflags - && guards > maximum_failing_guards) - (warnManyGuards (DsMatchContext ctxt locn)) + checkMatches dflags (DsMatchContext ctxt locn) new_vars matches ; result_expr <- handleWarnings $ matchEquations ctxt new_vars eqns_info rhs_ty @@ -777,7 +765,7 @@ matchSinglePat (Var var) ctx pat ty match_result ; locn <- getSrcSpanDs ; let pat' = getMaybeStrictPat dflags pat -- pattern match check warnings - ; dsPmWarn dflags (DsMatchContext ctx locn) (checkSingle var pat') + ; checkSingle dflags (DsMatchContext ctx locn) var pat' ; match [var] ty [EqnInfo { eqn_pats = [pat'], eqn_rhs = match_result }] } diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs index f1f59c1130..48044f912e 100644 --- a/compiler/deSugar/PmExpr.hs +++ b/compiler/deSugar/PmExpr.hs @@ -7,7 +7,7 @@ Haskell expressions (as used by the pattern matching checker) and utilities. {-# LANGUAGE CPP #-} module PmExpr ( - PmExpr(..), PmLit(..), SimpleEq, ComplexEq, eqPmLit, + PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit, truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex, pprPmExprWithParens, runPmPprM @@ -17,12 +17,13 @@ module PmExpr ( import HsSyn import Id +import Name +import NameSet import DataCon import TysWiredIn import Outputable import Util import SrcLoc -import VarSet import Data.Maybe (mapMaybe) import Data.List (groupBy, sortBy, nubBy) @@ -50,7 +51,7 @@ refer to variables that are otherwise substituted away. -- ** Types -- | Lifted expressions for pattern match checking. -data PmExpr = PmExprVar Id +data PmExpr = PmExprVar Name | PmExprCon DataCon [PmExpr] | PmExprLit PmLit | PmExprEq PmExpr PmExpr -- Syntactic equality @@ -140,6 +141,10 @@ nubPmLit = nubBy eqPmLit type SimpleEq = (Id, PmExpr) -- We always use this orientation type ComplexEq = (PmExpr, PmExpr) +-- | Lift a `SimpleEq` to a `ComplexEq` +toComplex :: SimpleEq -> ComplexEq +toComplex (x,e) = (PmExprVar (idName x), e) + -- | Expression `True' truePmExpr :: PmExpr truePmExpr = PmExprCon trueDataCon [] @@ -193,7 +198,7 @@ isConsDataCon con = consDataCon == con -- | We return a boolean along with the expression. Hence, if substitution was -- a no-op, we know that the expression still cannot progress. -substPmExpr :: Id -> PmExpr -> PmExpr -> (PmExpr, Bool) +substPmExpr :: Name -> PmExpr -> PmExpr -> (PmExpr, Bool) substPmExpr x e1 e = case e of PmExprVar z | x == z -> (e1, True) @@ -208,7 +213,7 @@ substPmExpr x e1 e = -- | Substitute in a complex equality. We return (Left eq) if the substitution -- affected the equality or (Right eq) if nothing happened. -substComplexEq :: Id -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq +substComplexEq :: Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq substComplexEq x e (ex, ey) | bx || by = Left (ex', ey') | otherwise = Right (ex', ey') @@ -224,7 +229,7 @@ lhsExprToPmExpr (L _ e) = hsExprToPmExpr e hsExprToPmExpr :: HsExpr Id -> PmExpr -hsExprToPmExpr (HsVar x) = PmExprVar (unLoc x) +hsExprToPmExpr (HsVar x) = PmExprVar (idName (unLoc x)) hsExprToPmExpr (HsOverLit olit) = PmExprLit (PmOLit False olit) hsExprToPmExpr (HsLit lit) = PmExprLit (PmSLit lit) @@ -312,7 +317,7 @@ Check.hs) to be more precice. -- ----------------------------------------------------------------------------- -- ** Transform residual constraints in appropriate form for pretty printing -type PmNegLitCt = (Id, (SDoc, [PmLit])) +type PmNegLitCt = (Name, (SDoc, [PmLit])) filterComplex :: [ComplexEq] -> [PmNegLitCt] filterComplex = zipWith rename nameList . map mkGroup @@ -342,19 +347,19 @@ filterComplex = zipWith rename nameList . map mkGroup runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmLit])]) runPmPprM m lit_env = (result, mapMaybe is_used lit_env) where - (result, (_lit_env, used)) = runState m (lit_env, emptyVarSet) + (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet) is_used (x,(name, lits)) - | elemVarSet x used = Just (name, lits) + | elemNameSet x used = Just (name, lits) | otherwise = Nothing -type PmPprM a = State ([PmNegLitCt], IdSet) a +type PmPprM a = State ([PmNegLitCt], NameSet) a -- (the first part of the state is read only. make it a reader?) -addUsed :: Id -> PmPprM () -addUsed x = modify (\(negated, used) -> (negated, extendVarSet used x)) +addUsed :: Name -> PmPprM () +addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x)) -checkNegation :: Id -> PmPprM (Maybe SDoc) -- the clean name if it is negated +checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated checkNegation x = do negated <- gets fst return $ case lookup x negated of diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs index 5d7a61a460..05966cd858 100644 --- a/compiler/deSugar/TmOracle.hs +++ b/compiler/deSugar/TmOracle.hs @@ -10,14 +10,14 @@ module TmOracle ( -- re-exported from PmExpr PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr, - canDiverge, eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, - pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr, + eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr, + hsExprToPmExpr, pprPmExprWithParens, -- the term oracle - tmOracle, TmState, initialTmState, + tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge, -- misc. - exprDeepLookup, pmLitType, flattenPmVarEnv + toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv ) where #include "HsVersions.h" @@ -25,6 +25,7 @@ module TmOracle ( import PmExpr import Id +import Name import TysWiredIn import Type import HsLit @@ -43,7 +44,7 @@ import qualified Data.Map as Map -} -- | The type of substitutions. -type PmVarEnv = Map.Map Id PmExpr +type PmVarEnv = Map.Map Name PmExpr -- | The environment of the oracle contains -- 1. A Bool (are there any constraints we cannot handle? (PmExprOther)). @@ -52,7 +53,7 @@ type TmOracleEnv = (Bool, PmVarEnv) -- | Check whether a constraint (x ~ BOT) can succeed, -- given the resulting state of the term oracle. -canDiverge :: Id -> TmState -> Bool +canDiverge :: Name -> TmState -> Bool canDiverge x (standby, (_unhandled, env)) -- If the variable seems not evaluated, there is a possibility for -- constraint x ~ BOT to be satisfiable. @@ -66,11 +67,11 @@ canDiverge x (standby, (_unhandled, env)) | otherwise = False where - isForcedByEq :: Id -> ComplexEq -> Bool + isForcedByEq :: Name -> ComplexEq -> Bool isForcedByEq y (e1, e2) = varIn y e1 || varIn y e2 -- | Check whether a variable is in the free variables of an expression -varIn :: Id -> PmExpr -> Bool +varIn :: Name -> PmExpr -> Bool varIn x e = case e of PmExprVar y -> x == y PmExprCon _ es -> any (x `varIn`) es @@ -131,7 +132,7 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of _ -> Just (standby, (True, env)) -- I HATE CATCH-ALLS -- | Extend the substitution and solve the (possibly updated) constraints. -extendSubstAndSolve :: Id -> PmExpr -> TmState -> Maybe TmState +extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState extendSubstAndSolve x e (standby, (unhandled, env)) = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed) where @@ -142,6 +143,19 @@ extendSubstAndSolve x e (standby, (unhandled, env)) (changed, unchanged) = partitionWith (substComplexEq x e) standby new_incr_state = (unchanged, (unhandled, Map.insert x e env)) +-- | When we know that a variable is fresh, we do not actually have to +-- check whether anything changes, we know that nothing does. Hence, +-- `extendSubst` simply extends the substitution, unlike what +-- `extendSubstAndSolve` does. +extendSubst :: Id -> PmExpr -> TmState -> TmState +extendSubst y e (standby, (unhandled, env)) + | isNotPmExprOther simpl_e + = (standby, (unhandled, Map.insert x simpl_e env)) + | otherwise = (standby, (True, env)) + where + x = idName y + simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e + -- | Simplify a complex equality. simplifyComplexEq :: ComplexEq -> ComplexEq simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2) @@ -204,7 +218,7 @@ applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2) -- | Apply an (un-flattened) substitution to a variable. -varDeepLookup :: PmVarEnv -> Id -> PmExpr +varDeepLookup :: PmVarEnv -> Name -> PmExpr varDeepLookup env x | Just e <- Map.lookup x env = exprDeepLookup env e -- go deeper | otherwise = PmExprVar x -- terminal diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 2dca546291..04bf1a13de 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -1,7 +1,4 @@ {-# LANGUAGE CPP, ScopedTypeVariables, MagicHash, UnboxedTuples #-} -#if __GLASGOW_HASKELL__ > 710 -{-# OPTIONS_GHC -ffull-guard-reasoning #-} -#endif ----------------------------------------------------------------------------- -- diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index b86d1a7958..a7aab27e48 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -531,9 +531,6 @@ data GeneralFlag -- safe haskell flags | Opt_DistrustAllPackages | Opt_PackageTrust - - -- pm checking with guards - | Opt_FullGuardReasoning deriving (Eq, Show, Enum) data WarningFlag = @@ -555,7 +552,6 @@ data WarningFlag = | Opt_WarnMissingLocalSigs | Opt_WarnNameShadowing | Opt_WarnOverlappingPatterns - | Opt_WarnTooManyGuards | Opt_WarnTypeDefaults | Opt_WarnMonomorphism | Opt_WarnUnusedTopBinds @@ -642,6 +638,7 @@ data DynFlags = DynFlags { debugLevel :: Int, -- ^ How much debug information to produce simplPhases :: Int, -- ^ Number of simplifier phases maxSimplIterations :: Int, -- ^ Max simplifier iterations + maxPmCheckIterations :: Int, -- ^ Max no iterations for pm checking ruleCheck :: Maybe String, strictnessBefore :: [Int], -- ^ Additional demand analysis @@ -1435,6 +1432,7 @@ defaultDynFlags mySettings = debugLevel = 0, simplPhases = 2, maxSimplIterations = 4, + maxPmCheckIterations = 10000000, ruleCheck = Nothing, maxRelevantBinds = Just 6, simplTickFactor = 100, @@ -2608,6 +2606,8 @@ dynamic_flags = [ (intSuffix (\n d -> d{ simplPhases = n })) , defFlag "fmax-simplifier-iterations" (intSuffix (\n d -> d{ maxSimplIterations = n })) + , defFlag "fmax-pmcheck-iterations" + (intSuffix (\n d -> d{ maxPmCheckIterations = n })) , defFlag "fsimpl-tick-factor" (intSuffix (\n d -> d{ simplTickFactor = n })) , defFlag "fspec-constr-threshold" @@ -2956,7 +2956,6 @@ wWarningFlags = [ flagSpec "orphans" Opt_WarnOrphans, flagSpec "overflowed-literals" Opt_WarnOverflowedLiterals, flagSpec "overlapping-patterns" Opt_WarnOverlappingPatterns, - flagSpec "too-many-guards" Opt_WarnTooManyGuards, flagSpec "missed-specialisations" Opt_WarnMissedSpecs, flagSpec "all-missed-specialisations" Opt_WarnAllMissedSpecs, flagSpec' "safe" Opt_WarnSafe setWarnSafe, @@ -3093,8 +3092,7 @@ fFlags = [ flagSpec "unbox-strict-fields" Opt_UnboxStrictFields, flagSpec "vectorisation-avoidance" Opt_VectorisationAvoidance, flagSpec "vectorise" Opt_Vectorise, - flagSpec "worker-wrapper" Opt_WorkerWrapper, - flagSpec "full-guard-reasoning" Opt_FullGuardReasoning + flagSpec "worker-wrapper" Opt_WorkerWrapper ] -- | These @-f\<blah\>@ flags can all be reversed with @-fno-\<blah\>@ diff --git a/compiler/nativeGen/Dwarf/Constants.hs b/compiler/nativeGen/Dwarf/Constants.hs index 6ba1f8a284..40e4e7d9a8 100644 --- a/compiler/nativeGen/Dwarf/Constants.hs +++ b/compiler/nativeGen/Dwarf/Constants.hs @@ -1,9 +1,5 @@ -- | Constants describing the DWARF format. Most of this simply -- mirrors /usr/include/dwarf.h. -{-# LANGUAGE CPP #-} -#if __GLASGOW_HASKELL__ > 710 -{-# OPTIONS_GHC -ffull-guard-reasoning #-} -#endif module Dwarf.Constants where diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 9ede73d1b1..151e3700bd 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -338,7 +338,8 @@ data DsLclEnv = DsLclEnv { dsl_meta :: DsMetaEnv, -- Template Haskell bindings dsl_loc :: RealSrcSpan, -- To put in pattern-matching error msgs dsl_dicts :: Bag EvVar, -- Constraints from GADT pattern-matching - dsl_tm_cs :: Bag SimpleEq + dsl_tm_cs :: Bag SimpleEq, + dsl_pm_iter :: IORef Int -- no iterations for pmcheck } -- Inside [| |] brackets, the desugarer looks diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs index 2af66f6391..fc6da629ac 100644 --- a/compiler/types/OptCoercion.hs +++ b/compiler/types/OptCoercion.hs @@ -2,9 +2,7 @@ {-# LANGUAGE CPP #-} -- This module used to take 10GB of memory to compile with the new - -- (Nov '15) pattern-match check. In order to be able to compile it, - -- do not enable -ffull-guard-reasoning. Instead, simplify the guards - -- (default behaviour when guards are too many). + -- (Nov '15) pattern-match checker. module OptCoercion ( optCoercion, checkAxInstCo ) where diff --git a/docs/users_guide/8.0.1-notes.rst b/docs/users_guide/8.0.1-notes.rst index 41e6c2b579..771bc99669 100644 --- a/docs/users_guide/8.0.1-notes.rst +++ b/docs/users_guide/8.0.1-notes.rst @@ -291,15 +291,6 @@ Compiler warns in the case of unused term-level patterns. Both flags are implied by :ghc-flag:`-W`. -- Added the :ghc-flag:`-Wtoo-many-guards` flag. When enabled, this will issue a - warning if a pattern match contains too many guards (over 20 at the - moment). Makes a difference only if pattern match checking is also enabled. - -- Added the :ghc-flag:`-ffull-guard-reasoning` flag. When enabled, pattern match - checking tries its best to reason about guards. Since the additional - expressivity may come with a high price in terms of compilation time and - memory consumption, it is turned off by default. - - :ghc-flag:`-this-package-key` has been renamed again (hopefully for the last time!) to :ghc-flag:`-this-unit-id`. The renaming was motivated by the fact that the identifier you pass to GHC here doesn't have much to do with packages: diff --git a/docs/users_guide/bugs.rst b/docs/users_guide/bugs.rst index 8304e25e78..f0c522cf75 100644 --- a/docs/users_guide/bugs.rst +++ b/docs/users_guide/bugs.rst @@ -358,16 +358,6 @@ Bugs in GHC This flag ensures that yield points are inserted at every function entrypoint (at the expense of a bit of performance). -- GHC's updated exhaustiveness and coverage checker (see - :ref:`options-sanity`) is quite expressive but with a rather high - performance cost (in terms of both time and memory consumption), mainly - due to guards. Two flags have been introduced to give more control to - the user over guard reasoning: :ghc-flag:`-Wtoo-many-guards` - and :ghc-flag:`-ffull-guard-reasoning` (see :ref:`options-sanity`). - When :ghc-flag:`-ffull-guard-reasoning` is on, pattern match checking for guards - runs in full power, which may run out of memory/substantially increase - compilation time. - - GHC does not allow you to have a data type with a context that mentions type variables that are not data type parameters. For example: diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst index afcee5b5d7..7fd2019cc6 100644 --- a/docs/users_guide/using-warnings.rst +++ b/docs/users_guide/using-warnings.rst @@ -527,40 +527,6 @@ of ``-W(no-)*``. This option isn't enabled by default because it can be very noisy, and it often doesn't indicate a bug in the program. -.. ghc-flag:: -Wtoo-many-guards - -Wno-too-many-guards - - .. index:: - single: too many guards, warning - - The option :ghc-flag:`-Wtoo-many-guards` warns about places where a - pattern match contains too many guards (over 20 at the moment). - It has an effect only if any form of exhaustivness/overlapping - checking is enabled (one of - :ghc-flag:`-Wincomplete-patterns`, - :ghc-flag:`-Wincomplete-uni-patterns`, - :ghc-flag:`-Wincomplete-record-updates`, - :ghc-flag:`-Woverlapping-patterns`). When enabled, the warning can be - suppressed by enabling either :ghc-flag:`-Wno-too-many-guards`, which just - hides the warning, or :ghc-flag:`-ffull-guard-reasoning` which runs the - full check, independently of the number of guards. - -.. ghc-flag:: -ffull-guard-reasoning - - :implies: :ghc-flag:`-Wno-too-many-guards` - - .. index:: - single: guard reasoning, warning - - The option :ghc-flag:`-ffull-guard-reasoning` forces pattern match checking - to run in full. This gives more precise warnings concerning pattern - guards but in most cases increases memory consumption and - compilation time. Hence, it is off by default. Enabling - :ghc-flag:`-ffull-guard-reasoning` also implies :ghc-flag:`-Wno-too-many-guards`. - Note that (like :ghc-flag:`-Wtoo-many-guards`) :ghc-flag:`-ffull-guard-reasoning` - makes a difference only if pattern match checking is already - enabled. - .. ghc-flag:: -Wmissing-fields .. index:: diff --git a/libraries/base/Foreign/C/Error.hs b/libraries/base/Foreign/C/Error.hs index 4607c37992..761435183e 100644 --- a/libraries/base/Foreign/C/Error.hs +++ b/libraries/base/Foreign/C/Error.hs @@ -1,6 +1,5 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE CPP, NoImplicitPrelude #-} -{-# OPTIONS_GHC -ffull-guard-reasoning #-} ----------------------------------------------------------------------------- -- | diff --git a/testsuite/tests/pmcheck/should_compile/T11195.hs b/testsuite/tests/pmcheck/should_compile/T11195.hs new file mode 100644 index 0000000000..593223f5fc --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T11195.hs @@ -0,0 +1,189 @@ +{-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-} + +module T11195 where + +import TyCoRep +import Coercion +import Type hiding( substTyVarBndr, substTy, extendTCvSubst ) +import TcType ( exactTyCoVarsOfType ) +import CoAxiom +import VarSet +import VarEnv +import Pair +import InstEnv + +type NormalCo = Coercion +type NormalNonIdCo = NormalCo -- Extra invariant: not the identity +type SymFlag = Bool +type ReprFlag = Bool + +chooseRole :: ReprFlag -> Role -> Role +chooseRole = undefined + +wrapRole :: ReprFlag -> Role -> Coercion -> Coercion +wrapRole = undefined + +wrapSym :: SymFlag -> Coercion -> Coercion +wrapSym = undefined + +optForAllCoBndr :: LiftingContext -> Bool + -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion) +optForAllCoBndr = undefined + +opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo +opt_trans = undefined + +opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role + -> Type -> Type -> Coercion +opt_univ = undefined + +opt_co3 :: LiftingContext -> SymFlag -> Maybe Role + -> Role -> Coercion -> NormalCo +opt_co3 = undefined + +opt_co2 :: LiftingContext -> SymFlag -> Role -> Coercion -> NormalCo +opt_co2 = undefined + +compatible_co :: Coercion -> Coercion -> Bool +compatible_co = undefined + +etaTyConAppCo_maybe = undefined +etaAppCo_maybe = undefined +etaForAllCo_maybe = undefined + +matchAxiom = undefined +checkAxInstCo = undefined +isAxiom_maybe = undefined +isCohLeft_maybe = undefined +isCohRight_maybe = undefined + +opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo] +opt_transList is = zipWith (opt_trans is) + +opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo +opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2) + | d1 == d2 + , co1 `compatible_co` co2 = undefined + +opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2) + | d1 == d2 + , co1 `compatible_co` co2 = undefined + +-- Push transitivity inside instantiation +opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2) + | ty1 `eqCoercion` ty2 + , co1 `compatible_co` co2 = undefined + +opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1) + in_co2@(UnivCo p2 r2 _tyl2 tyr2) + | Just prov' <- opt_trans_prov p1 p2 = undefined + where + -- if the provenances are different, opt'ing will be very confusing + opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv + = Just UnsafeCoerceProv + opt_trans_prov (PhantomProv kco1) (PhantomProv kco2) + = Just $ PhantomProv $ opt_trans is kco1 kco2 + opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2) + = Just $ ProofIrrelProv $ opt_trans is kco1 kco2 + opt_trans_prov (PluginProv str1) (PluginProv str2) + | str1 == str2 = Just p1 + opt_trans_prov _ _ = Nothing + +-- Push transitivity down through matching top-level constructors. +opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) + in_co2@(TyConAppCo r2 tc2 cos2) + | tc1 == tc2 = undefined + +opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b) + = undefined + +-- Eta rules +opt_trans_rule is co1@(TyConAppCo r tc cos1) co2 + | Just cos2 <- etaTyConAppCo_maybe tc co2 = undefined + +opt_trans_rule is co1 co2@(TyConAppCo r tc cos2) + | Just cos1 <- etaTyConAppCo_maybe tc co1 = undefined + +opt_trans_rule is co1@(AppCo co1a co1b) co2 + | Just (co2a,co2b) <- etaAppCo_maybe co2 = undefined + +opt_trans_rule is co1 co2@(AppCo co2a co2b) + | Just (co1a,co1b) <- etaAppCo_maybe co1 = undefined + +-- Push transitivity inside forall +opt_trans_rule is co1 co2 + | ForAllCo tv1 eta1 r1 <- co1 + , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2 = undefined + + | ForAllCo tv2 eta2 r2 <- co2 + , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1 = undefined + + where + push_trans tv1 eta1 r1 tv2 eta2 r2 = undefined + +-- Push transitivity inside axioms +opt_trans_rule is co1 co2 + | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe + , True <- sym + , Just cos2 <- matchAxiom sym con ind co2 + , let newAxInst = AxiomInstCo con ind + (opt_transList is (map mkSymCo cos2) cos1) + , Nothing <- checkAxInstCo newAxInst + = undefined + + -- TrPushAxR + | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe + , False <- sym + , Just cos2 <- matchAxiom sym con ind co2 + , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2) + , Nothing <- checkAxInstCo newAxInst + = undefined + + -- TrPushSymAxL + | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe + , True <- sym + , Just cos1 <- matchAxiom (not sym) con ind co1 + , let newAxInst = AxiomInstCo con ind + (opt_transList is cos2 (map mkSymCo cos1)) + , Nothing <- checkAxInstCo newAxInst + = undefined + + -- TrPushAxL + | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe + , False <- sym + , Just cos1 <- matchAxiom (not sym) con ind co1 + , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2) + , Nothing <- checkAxInstCo newAxInst + = undefined + + -- TrPushAxSym/TrPushSymAx + | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe + , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe + , con1 == con2 + , ind1 == ind2 + , sym1 == not sym2 + , let branch = coAxiomNthBranch con1 ind1 + qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch + lhs = coAxNthLHS con1 ind1 + rhs = coAxBranchRHS branch + pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs) + , all (`elemVarSet` pivot_tvs) qtvs + = undefined + where + co1_is_axiom_maybe = isAxiom_maybe co1 + co2_is_axiom_maybe = isAxiom_maybe co2 + role = coercionRole co1 -- should be the same as coercionRole co2! + +opt_trans_rule is co1 co2 + | Just (lco, lh) <- isCohRight_maybe co1 + , Just (rco, rh) <- isCohLeft_maybe co2 + , (coercionType lh) `eqType` (coercionType rh) + = undefined + +opt_trans_rule _ co1 co2 -- Identity rule + | (Pair ty1 _, r) <- coercionKindRole co1 + , Pair _ ty2 <- coercionKind co2 + , ty1 `eqType` ty2 + = undefined + +opt_trans_rule _ _ _ = Nothing diff --git a/testsuite/tests/pmcheck/should_compile/T11303b.hs b/testsuite/tests/pmcheck/should_compile/T11303b.hs new file mode 100644 index 0000000000..f8c4917477 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T11303b.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -Wincomplete-patterns -Woverlapping-patterns #-} + +module T11303b where + +data family Letter a + +data instance Letter a = A | B | C | D | E | F | G | H | I | J + +f :: [Letter a] -> Int +f = foldl go 0 + where + go n letter = n + n' + where + n' = case letter of + A -> 0 + B -> 1 + C -> 2 + D -> 3 + E -> 4 + F -> 5 + G -> 6 + H -> 7 + I -> 8 + J -> 9 diff --git a/testsuite/tests/pmcheck/should_compile/T11374.hs b/testsuite/tests/pmcheck/should_compile/T11374.hs new file mode 100644 index 0000000000..e68fbc88e9 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T11374.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE Haskell2010 #-} +{-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-} + +module T11374 where + +data Type = TCon TCon [Type] + | TUser String [Type] Type + | TRec [(String,Type)] + deriving (Show,Eq,Ord) + +data TCon = TC TC + | TF TFun + deriving (Show,Eq,Ord) + +data TC = TCNum Integer + | TCInf + | TCBit + | TCSeq + | TCFun + | TCTuple Int + deriving (Show,Eq,Ord) + +data TFun = TCAdd + | TCSub + | TCMul + | TCDiv + | TCMod + | TCLg2 + | TCExp + | TCWidth + | TCMin + | TCMax + | TCLenFromThen + | TCLenFromThenTo + deriving (Show, Eq, Ord, Bounded, Enum) + +simpFinTy :: Type -> Maybe [Type] +simpFinTy ty = case ty of + TCon (TC (TCNum _)) _ -> Just [] + + TCon (TF tf) [t1] + | TCLg2 <- tf -> Just [t1] + | TCWidth <- tf -> Just [t1] + + TCon (TF tf) [t1,t2] + | TCAdd <- tf -> Just [t1, t2] + | TCSub <- tf -> Just [t1] + | TCMul <- tf -> Just [t1, t2] + | TCDiv <- tf -> Just [t1] + | TCMod <- tf -> Just [] + | TCExp <- tf -> Just [t1, t2] + | TCMin <- tf -> Nothing + | TCMax <- tf -> Just [t1, t2] + + TCon (TF tf) [_,_,_] + | TCLenFromThen <- tf -> Just [] + | TCLenFromThenTo <- tf -> Just [] + + _ -> Nothing diff --git a/testsuite/tests/pmcheck/should_compile/T2204.stderr b/testsuite/tests/pmcheck/should_compile/T2204.stderr index e6ad7cf9ae..d2e6e0a434 100644 --- a/testsuite/tests/pmcheck/should_compile/T2204.stderr +++ b/testsuite/tests/pmcheck/should_compile/T2204.stderr @@ -2,10 +2,10 @@ T2204.hs:6:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘f’: Patterns not matched: - ('0':'1':_:_) - ('0':p:_) where p is not one of {'1'} - ['0'] + [] (p:_) where p is not one of {'0'} + ['0'] + ('0':p:_) where p is not one of {'1'} ... T2204.hs:9:1: warning: diff --git a/testsuite/tests/pmcheck/should_compile/T9951b.stderr b/testsuite/tests/pmcheck/should_compile/T9951b.stderr index 6a9d0ce112..b998ce225b 100644 --- a/testsuite/tests/pmcheck/should_compile/T9951b.stderr +++ b/testsuite/tests/pmcheck/should_compile/T9951b.stderr @@ -2,8 +2,8 @@ T9951b.hs:7:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘f’: Patterns not matched: - ('a':'b':_:_) - ('a':p:_) where p is not one of {'b'} - ['a'] + [] (p:_) where p is not one of {'a'} + ['a'] + ('a':p:_) where p is not one of {'b'} ... diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T index 521c221e1b..84c2d610f4 100644 --- a/testsuite/tests/pmcheck/should_compile/all.T +++ b/testsuite/tests/pmcheck/should_compile/all.T @@ -24,6 +24,9 @@ test('T9951b',only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-pattern test('T9951', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) test('T11303', normal, compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS']) test('T11276', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS']) +test('T11303b', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS']) +test('T11374', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS']) +test('T11195', compile_timeout_multiplier(0.40), compile, ['-package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS']) # Other tests test('pmc001', only_compiler_types(['ghc']), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) diff --git a/testsuite/tests/pmcheck/should_compile/pmc001.stderr b/testsuite/tests/pmcheck/should_compile/pmc001.stderr index c6145432f0..eb0bd4bc56 100644 --- a/testsuite/tests/pmcheck/should_compile/pmc001.stderr +++ b/testsuite/tests/pmcheck/should_compile/pmc001.stderr @@ -2,16 +2,16 @@ pmc001.hs:14:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘f’: Patterns not matched: - MkT3 (MkT2 _) - MkT3 MkT1 - (MkT2 _) MkT3 MkT1 MkT3 + (MkT2 _) MkT3 + MkT3 MkT1 + MkT3 (MkT2 _) pmc001.hs:19:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘g’: Patterns not matched: - MkT3 (MkT2 _) - MkT3 MkT1 - (MkT2 _) MkT3 MkT1 MkT3 + (MkT2 _) MkT3 + MkT3 MkT1 + MkT3 (MkT2 _) diff --git a/testsuite/tests/pmcheck/should_compile/pmc007.stderr b/testsuite/tests/pmcheck/should_compile/pmc007.stderr index bb011be5aa..291fbdcde2 100644 --- a/testsuite/tests/pmcheck/should_compile/pmc007.stderr +++ b/testsuite/tests/pmcheck/should_compile/pmc007.stderr @@ -7,18 +7,18 @@ pmc007.hs:12:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘g’: Patterns not matched: - ('a':'b':_:_) - ('a':'c':_:_) - ('a':p:_) where p is not one of {'c', 'b'} + [] + (p:_) where p is not one of {'a'} ['a'] + ('a':p:_) where p is not one of {'c', 'b'} ... pmc007.hs:18:11: warning: Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: - ('a':'b':_:_) - ('a':'c':_:_) - ('a':p:_) where p is not one of {'c', 'b'} + [] + (p:_) where p is not one of {'a'} ['a'] + ('a':p:_) where p is not one of {'c', 'b'} ... diff --git a/utils/mkUserGuidePart/Options/Warnings.hs b/utils/mkUserGuidePart/Options/Warnings.hs index 3fa9bf087e..de5e1592ce 100644 --- a/utils/mkUserGuidePart/Options/Warnings.hs +++ b/utils/mkUserGuidePart/Options/Warnings.hs @@ -237,11 +237,6 @@ warningsOptions = , flagType = DynamicFlag , flagReverse = "-Wno-tabs" } - , flag { flagName = "-Wtoo-many-guards" - , flagDescription = "warn when a match has too many guards" - , flagType = DynamicFlag - , flagReverse = "-Wno-too-many-guards" - } , flag { flagName = "-Wtype-defaults" , flagDescription = "warn when defaulting happens" , flagType = DynamicFlag @@ -397,12 +392,4 @@ warningsOptions = , flagType = DynamicFlag , flagReverse = "-Wno-deriving-typeable" } - , flag { flagName = "-ffull-guard-reasoning" - , flagDescription = - "enable the full reasoning of the pattern match checker "++ - "concerning guards, for more precise exhaustiveness/coverage "++ - "warnings" - , flagType = DynamicFlag - , flagReverse = "-fno-full-guard-reasoning" - } ] |