Commit 28f951ed authored by Georgios Karachalias's avatar Georgios Karachalias Committed by Ben Gamari

Overhaul the Overhauled Pattern Match Checker

Overhaul the Overhauled Pattern Match Checker

* 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). Hence, an example written with pattern
guards is 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:
Trac #11195, #11276, #11303, #11374, #11162

Test Plan: validate

Reviewers: goldfire, bgamari, hvr, austin

Subscribers: simonpj, thomie

Differential Revision: https://phabricator.haskell.org/D1795
parent db121b2e
......@@ -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,38 +637,11 @@ 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
......@@ -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)