[Git][ghc/ghc][wip/pmcheck-refuts] TmOracle: Replace negative term equalities by refutable PmAltCons
Sebastian Graf
gitlab at gitlab.haskell.org
Sat Jun 1 10:29:36 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-refuts at Glasgow Haskell Compiler / GHC
Commits:
f9758aaf by Sebastian Graf at 2019-06-01T10:29:23Z
TmOracle: Replace negative term equalities by refutable PmAltCons
The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".
This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5". We encode this knowledge in a
`PmRefutEnv`, mapping a set of newly introduced `PmAltCon`s (which are
just `PmLit`s at the moment) to each variable denoting above
inequalities.
So, say we have `x ≁ 42 ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ 42`. The entry in the refutable
environment will immediately lead to a contradiction.
This machinery renders the whole `PmExprEq` and `ComplexEq` business
unnecessary, getting rid of a lot of (mostly dead) code.
See the Note [Refutable shapes] in TmOracle for a place to start.
- - - - -
9 changed files:
- compiler/basicTypes/NameEnv.hs
- compiler/deSugar/Check.hs
- compiler/deSugar/DsMonad.hs
- compiler/deSugar/PmExpr.hs
- + compiler/deSugar/PmPpr.hs
- compiler/deSugar/TmOracle.hs
- compiler/ghc.cabal.in
- compiler/typecheck/TcRnTypes.hs
- compiler/utils/ListSetOps.hs
Changes:
=====================================
compiler/basicTypes/NameEnv.hs
=====================================
@@ -25,6 +25,7 @@ module NameEnv (
emptyDNameEnv,
lookupDNameEnv,
+ delFromDNameEnv,
mapDNameEnv,
alterDNameEnv,
-- ** Dependency analysis
@@ -147,6 +148,9 @@ emptyDNameEnv = emptyUDFM
lookupDNameEnv :: DNameEnv a -> Name -> Maybe a
lookupDNameEnv = lookupUDFM
+delFromDNameEnv :: DNameEnv a -> Name -> DNameEnv a
+delFromDNameEnv = delFromUDFM
+
mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
mapDNameEnv = mapUDFM
=====================================
compiler/deSugar/Check.hs
=====================================
@@ -25,6 +25,7 @@ module Check (
import GhcPrelude
import TmOracle
+import PmPpr
import Unify( tcMatchTy )
import DynFlags
import HsSyn
@@ -578,7 +579,7 @@ pmTopNormaliseType_maybe env ty_cs typ
pmInitialTmTyCs :: PmM Delta
pmInitialTmTyCs = do
ty_cs <- liftD getDictsDs
- tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
+ tm_cs <- bagToList <$> liftD getTmCsDs
sat_ty <- tyOracle ty_cs
let initTyCs = if sat_ty then ty_cs else emptyBag
initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
@@ -626,7 +627,7 @@ that we expect.
pmIsSatisfiable
:: Delta -- ^ The ambient term and type constraints
-- (known to be satisfiable).
- -> ComplexEq -- ^ The new term constraint.
+ -> TmEq -- ^ The new term constraint.
-> Bag EvVar -- ^ The new type constraints.
-> [Type] -- ^ The strict argument types.
-> PmM (Maybe Delta)
@@ -652,7 +653,7 @@ pmIsSatisfiable amb_cs new_tm_c new_ty_cs strict_arg_tys = do
tmTyCsAreSatisfiable
:: Delta -- ^ The ambient term and type constraints
-- (known to be satisfiable).
- -> ComplexEq -- ^ The new term constraint.
+ -> TmEq -- ^ The new term constraint.
-> Bag EvVar -- ^ The new type constraints.
-> PmM (Maybe Delta)
-- ^ @'Just' delta@ if the constraints (@delta@) are
@@ -1457,7 +1458,7 @@ pmPatType PmFake = pmPatType truePattern
data InhabitationCandidate =
InhabitationCandidate
{ ic_val_abs :: ValAbs
- , ic_tm_ct :: ComplexEq
+ , ic_tm_ct :: TmEq
, ic_ty_cs :: Bag EvVar
, ic_strict_arg_tys :: [Type]
}
@@ -1654,7 +1655,7 @@ mkOneConFull x con = do
strict_arg_tys = filterByList arg_is_banged arg_tys'
return $ InhabitationCandidate
{ ic_val_abs = con_abs
- , ic_tm_ct = (PmExprVar (idName x), vaToPmExpr con_abs)
+ , ic_tm_ct = (x, vaToPmExpr con_abs)
, ic_ty_cs = listToBag evvars
, ic_strict_arg_tys = strict_arg_tys
}
@@ -1672,21 +1673,15 @@ mkGuard pv e = do
| PmExprOther {} <- expr -> pure PmFake
| otherwise -> pure (PmGrd pv expr)
--- | 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)
+mkPosEq :: Id -> PmLit -> TmEq
+mkPosEq x l = (x, PmExprLit l)
{-# INLINE mkPosEq #-}
-- | Create a term equality of the form: `(x ~ x)`
-- (always discharged by the term oracle)
-mkIdEq :: Id -> ComplexEq
-mkIdEq x = (PmExprVar name, PmExprVar name)
- where name = idName x
+mkIdEq :: Id -> TmEq
+mkIdEq x = (x, PmExprVar (idName x))
{-# INLINE mkIdEq #-}
-- | Generate a variable pattern of a given type
@@ -2053,8 +2048,7 @@ pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
-- Var
pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
- | Just tm_state <- solveOneEq (delta_tm_cs delta)
- (PmExprVar (idName x), vaToPmExpr va)
+ | Just tm_state <- solveOneEq (delta_tm_cs delta) (x, vaToPmExpr va)
= ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
| otherwise = return mempty
@@ -2116,7 +2110,8 @@ pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
ValVec vva (delta {delta_tm_cs = tm_state})
Nothing -> return mempty
where
- us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+ -- See Note [Refutable shapes] in TmOracle
+ us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
= [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
| otherwise = []
@@ -2136,7 +2131,8 @@ pmcheckHd (p@(PmLit l)) ps guards
(ValVec vva (delta { delta_tm_cs = tm_state }))
| otherwise = return non_matched
where
- us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+ -- See Note [Refutable shapes] in TmOracle
+ us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
= [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
| otherwise = []
@@ -2401,7 +2397,7 @@ these constraints.
genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee
-> [Pat GhcTc] -- LHS (should have length 1)
-> [Id] -- MatchVars (should have length 1)
- -> DsM (Bag SimpleEq)
+ -> DsM (Bag TmEq)
genCaseTmCs2 Nothing _ _ = return emptyBag
genCaseTmCs2 (Just scr) [p] [var] = do
fam_insts <- dsGetFamInstEnvs
@@ -2414,7 +2410,7 @@ genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
-- case x of { matches }
-- When checking matches we record that (x ~ y) where y is the initial
-- uncovered. All matches will have to satisfy this equality.
-genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag SimpleEq
+genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag TmEq
genCaseTmCs1 Nothing _ = emptyBag
genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
@@ -2478,21 +2474,15 @@ isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
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)
+ = let (subst, refuts) = wrapUpTmState (delta_tm_cs delta)
+ vector = substInValAbs subst vva
+ in pprUncovered (vector, refuts)
-- | 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
@@ -2532,10 +2522,11 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
maxPatterns = maxUncoveredPatterns dflags
-- Print a single clause (for redundant/with-inaccessible-rhs)
- pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q
+ pprEqn q txt = pprContext True ctx (text txt) $ \f ->
+ f (pprPats kind (map unLoc q))
-- Print several clauses (for uncovered clauses)
- pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ ->
+ pprEqns qs = pprContext False ctx (text "are non-exhaustive") $ \_ ->
case qs of -- See #11245
[ValVec [] _]
-> text "Guards do not cover entire pattern space"
@@ -2546,7 +2537,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
-- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
-- which we only know the type and have no inhabitants at hand)
- warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ ->
+ warnEmptyCase ty = pprContext False ctx (text "are non-exhaustive") $ \_ ->
hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
{- Note [Inaccessible warnings for record updates]
@@ -2618,8 +2609,8 @@ exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete pat
-- incomplete
-- True <==> singular
-pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
-pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
+pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
+pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
= vcat [text txt <+> msg,
sep [ text "In" <+> ppr_match <> char ':'
, nest 4 (rest_of_msg_fun pref)]]
@@ -2633,87 +2624,10 @@ pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
-> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
_ -> (pprMatchContext kind, \ pp -> pp)
-ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
-ppr_pats kind pats
+pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
+pprPats kind pats
= sep [sep (map ppr pats), matchSeparator kind, text "..."]
-ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
-ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
-
-ppr_constraint :: (SDoc,[PmLit]) -> SDoc
-ppr_constraint (var, lits) = var <+> text "is not one of"
- <+> braces (pprWithCommas ppr lits)
-
-ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
-ppr_uncovered (expr_vec, complex)
- | null cs = fsep vec -- there are no literal constraints
- | otherwise = hang (fsep vec) 4 $
- text "where" <+> vcat (map ppr_constraint cs)
- where
- sdoc_vec = mapM pprPmExprWithParens expr_vec
- (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
-
-{- Note [Representation of Term Equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In the paper, term constraints always take the form (x ~ e). Of course, a more
-general constraint of the form (e1 ~ e1) can always be transformed to an
-equivalent set of the former constraints, by introducing a fresh, intermediate
-variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
-to #11160 (incredibly bad performance for literal pattern matching). Two are
-the main sources of this problem (the actual problem is how these two interact
-with each other):
-
-1. Pattern matching on literals generates twice as many constraints as needed.
- Consider the following (tests/ghci/should_run/ghcirun004):
-
- foo :: Int -> Int
- foo 1 = 0
- ...
- foo 5000 = 4999
-
- The covered and uncovered set *should* look like:
- U0 = { x |> {} }
-
- C1 = { 1 |> { x ~ 1 } }
- U1 = { x |> { False ~ (x ~ 1) } }
- ...
- C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
- U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
- ...
-
- If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
- we get twice as many constraints. Also note that half of them are just the
- substitution [x |-> False].
-
-2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
- (x ~ e) as substitutions [x |-> e]. More specifically, function
- `extendSubstAndSolve` applies such substitutions in the residual constraints
- and partitions them in the affected and non-affected ones, which are the new
- worklist. Essentially, this gives quadradic behaviour on the number of the
- residual constraints. (This would not be the case if the term oracle used
- mutable variables but, since we use it to handle disjunctions on value set
- abstractions (`Union` case), we chose a pure, incremental interface).
-
-Now the problem becomes apparent (e.g. for clause 300):
- * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
- constraints that we know that will not reduce (stay in the worklist).
- * To check for consistency, we apply the substituting constraints ONE BY ONE
- (since `tmOracle` is called incrementally, it does not have all of them
- available at once). Hence, we go through the (non-progressing) constraints
- over and over, achieving over-quadradic behaviour.
-
-If instead we allow constraints of the form (e ~ e),
- * All uncovered sets Ui contain no substituting constraints and i
- non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
- behaves linearly.
- * All covered sets Ci contain exactly (i-1) non-progressing constraints and
- a single substituting constraint. So the term oracle goes through the
- constraints only once.
-
-The performance improvement becomes even more important when more arguments are
-involved.
--}
-
-- Debugging Infrastructre
tracePm :: String -> SDoc -> PmM ()
=====================================
compiler/deSugar/DsMonad.hs
=====================================
@@ -396,11 +396,11 @@ addDictsDs ev_vars
= updLclEnv (\env -> env { dsl_dicts = unionBags ev_vars (dsl_dicts env) })
-- | Get in-scope term constraints (pm check)
-getTmCsDs :: DsM (Bag SimpleEq)
+getTmCsDs :: DsM (Bag TmEq)
getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) }
-- | Add in-scope term constraints (pm check)
-addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a
+addTmCsDs :: Bag TmEq -> DsM a -> DsM a
addTmCsDs tm_cs
= updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) })
=====================================
compiler/deSugar/PmExpr.hs
=====================================
@@ -6,12 +6,11 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module PmExpr (
- PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit,
- truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
- lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
- pprPmExprWithParens, runPmPprM
+ PmExpr(..), PmLit(..), PmAltCon(..), TmEq,
+ eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr
) where
#include "HsVersions.h"
@@ -23,19 +22,13 @@ import FastString (FastString, unpackFS)
import HsSyn
import Id
import Name
-import NameSet
import DataCon
import ConLike
import TcType (isStringTy)
import TysWiredIn
import Outputable
-import Util
import SrcLoc
-import Data.Maybe (mapMaybe)
-import Data.List (groupBy, sortBy, nubBy)
-import Control.Monad.Trans.State.Lazy
-
{-
%************************************************************************
%* *
@@ -61,7 +54,6 @@ refer to variables that are otherwise substituted away.
data PmExpr = PmExprVar Name
| PmExprCon ConLike [PmExpr]
| PmExprLit PmLit
- | PmExprEq PmExpr PmExpr -- Syntactic equality
| PmExprOther (HsExpr GhcTc) -- Note [PmExprOther in PmExpr]
@@ -79,6 +71,16 @@ eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
-- See Note [Undecidable Equality for Overloaded Literals]
eqPmLit _ _ = False
+-- | Represents a match against a literal. We mostly use it to to encode shapes
+-- for a variable that immediately lead to a refutation.
+--
+-- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'.
+newtype PmAltCon = PmAltLit PmLit
+ deriving Outputable
+
+instance Eq PmAltCon where
+ PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
+
{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
@@ -145,24 +147,8 @@ impact of this is the following:
appearance of the warnings and is, in practice safe.
-}
-nubPmLit :: [PmLit] -> [PmLit]
-nubPmLit = nubBy eqPmLit
-
-- | Term equalities
-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 = mkPmExprData trueDataCon []
-
--- | Expression `False'
-falsePmExpr :: PmExpr
-falsePmExpr = mkPmExprData falseDataCon []
+type TmEq = (Id, PmExpr)
-- ----------------------------------------------------------------------------
-- ** Predicates on PmExpr
@@ -172,66 +158,6 @@ isNotPmExprOther :: PmExpr -> Bool
isNotPmExprOther (PmExprOther _) = False
isNotPmExprOther _expr = True
--- | Check whether a literal is negated
-isNegatedPmLit :: PmLit -> Bool
-isNegatedPmLit (PmOLit b _) = b
-isNegatedPmLit _other_lit = False
-
--- | Check whether a PmExpr is syntactically equal to term `True'.
-isTruePmExpr :: PmExpr -> Bool
-isTruePmExpr (PmExprCon c []) = c == RealDataCon trueDataCon
-isTruePmExpr _other_expr = False
-
--- | Check whether a PmExpr is syntactically equal to term `False'.
-isFalsePmExpr :: PmExpr -> Bool
-isFalsePmExpr (PmExprCon c []) = c == RealDataCon falseDataCon
-isFalsePmExpr _other_expr = False
-
--- | Check whether a PmExpr is syntactically e
-isNilPmExpr :: PmExpr -> Bool
-isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon
-isNilPmExpr _other_expr = False
-
--- | Check whether a PmExpr is syntactically equal to (x == y).
--- Since (==) is overloaded and can have an arbitrary implementation, we use
--- the PmExprEq constructor to represent only equalities with non-overloaded
--- literals where it coincides with a syntactic equality check.
-isPmExprEq :: PmExpr -> Maybe (PmExpr, PmExpr)
-isPmExprEq (PmExprEq e1 e2) = Just (e1,e2)
-isPmExprEq _other_expr = Nothing
-
--- | Check if a DataCon is (:).
-isConsDataCon :: DataCon -> Bool
-isConsDataCon con = consDataCon == con
-
--- ----------------------------------------------------------------------------
--- ** Substitution in PmExpr
-
--- | We return a boolean along with the expression. Hence, if substitution was
--- a no-op, we know that the expression still cannot progress.
-substPmExpr :: Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
-substPmExpr x e1 e =
- case e of
- PmExprVar z | x == z -> (e1, True)
- | otherwise -> (e, False)
- PmExprCon c ps -> let (ps', bs) = mapAndUnzip (substPmExpr x e1) ps
- in (PmExprCon c ps', or bs)
- PmExprEq ex ey -> let (ex', bx) = substPmExpr x e1 ex
- (ey', by) = substPmExpr x e1 ey
- in (PmExprEq ex' ey', bx || by)
- _other_expr -> (e, False) -- The rest are terminals (We silently ignore
- -- Other). See Note [PmExprOther in PmExpr]
-
--- | Substitute in a complex equality. We return (Left eq) if the substitution
--- affected the equality or (Right eq) if nothing happened.
-substComplexEq :: Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
-substComplexEq x e (ex, ey)
- | bx || by = Left (ex', ey')
- | otherwise = Right (ex', ey')
- where
- (ex', bx) = substPmExpr x e ex
- (ey', by) = substPmExpr x e ey
-
-- -----------------------------------------------------------------------
-- ** Lift source expressions (HsExpr Id) to PmExpr
@@ -312,155 +238,23 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s))
%************************************************************************
-}
-{- 1. Literals
-~~~~~~~~~~~~~~
-Starting with a function definition like:
-
- f :: Int -> Bool
- f 5 = True
- f 6 = True
-
-The uncovered set looks like:
- { var |> False == (var == 5), False == (var == 6) }
-
-Yet, we would like to print this nicely as follows:
- x , where x not one of {5,6}
-
-Function `filterComplex' takes the set of residual constraints and packs
-together the negative constraints that refer to the same variable so we can do
-just this. Since these variables will be shown to the programmer, we also give
-them better names (t1, t2, ..), hence the SDoc in PmNegLitCt.
-
-2. Residual Constraints
-~~~~~~~~~~~~~~~~~~~~~~~
-Unhandled constraints that refer to HsExpr are typically ignored by the solver
-(it does not even substitute in HsExpr so they are even printed as wildcards).
-Additionally, the oracle returns a substitution if it succeeds so we apply this
-substitution to the vectors before printing them out (see function `pprOne' in
-Check.hs) to be more precice.
--}
-
--- -----------------------------------------------------------------------------
--- ** Transform residual constraints in appropriate form for pretty printing
-
-type PmNegLitCt = (Name, (SDoc, [PmLit]))
-
-filterComplex :: [ComplexEq] -> [PmNegLitCt]
-filterComplex = zipWith rename nameList . map mkGroup
- . groupBy name . sortBy order . mapMaybe isNegLitCs
- where
- order x y = compare (fst x) (fst y)
- name x y = fst x == fst y
- mkGroup l = (fst (head l), nubPmLit $ map snd l)
- rename new (old, lits) = (old, (new, lits))
-
- isNegLitCs (e1,e2)
- | isFalsePmExpr e1, Just (x,y) <- isPmExprEq e2 = isNegLitCs' x y
- | isFalsePmExpr e2, Just (x,y) <- isPmExprEq e1 = isNegLitCs' x y
- | otherwise = Nothing
-
- isNegLitCs' (PmExprVar x) (PmExprLit l) = Just (x, l)
- isNegLitCs' (PmExprLit l) (PmExprVar x) = Just (x, l)
- isNegLitCs' _ _ = Nothing
-
- -- Try nice names p,q,r,s,t before using the (ugly) t_i
- nameList :: [SDoc]
- nameList = map text ["p","q","r","s","t"] ++
- [ text ('t':show u) | u <- [(0 :: Int)..] ]
-
--- ----------------------------------------------------------------------------
-
-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, emptyNameSet)
-
- is_used (x,(name, lits))
- | elemNameSet x used = Just (name, lits)
- | otherwise = Nothing
-
-type PmPprM a = State ([PmNegLitCt], NameSet) a
--- (the first part of the state is read only. make it a reader?)
-
-addUsed :: Name -> PmPprM ()
-addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x))
-
-checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated
-checkNegation x = do
- negated <- gets fst
- return $ case lookup x negated of
- Just (new, _) -> Just new
- Nothing -> Nothing
-
--- | Pretty print a pmexpr, but remember to prettify the names of the variables
--- that refer to neg-literals. The ones that cannot be shown are printed as
--- underscores.
-pprPmExpr :: PmExpr -> PmPprM SDoc
-pprPmExpr (PmExprVar x) = do
- mb_name <- checkNegation x
- case mb_name of
- Just name -> addUsed x >> return name
- Nothing -> return underscore
-
-pprPmExpr (PmExprCon con args) = pprPmExprCon con args
-pprPmExpr (PmExprLit l) = return (ppr l)
-pprPmExpr (PmExprEq _ _) = return underscore -- don't show
-pprPmExpr (PmExprOther _) = return underscore -- don't show
-
-needsParens :: PmExpr -> Bool
-needsParens (PmExprVar {}) = False
-needsParens (PmExprLit l) = isNegatedPmLit l
-needsParens (PmExprEq {}) = False -- will become a wildcard
-needsParens (PmExprOther {}) = False -- will become a wildcard
-needsParens (PmExprCon (RealDataCon c) es)
- | isTupleDataCon c
- || isConsDataCon c || null es = False
- | otherwise = True
-needsParens (PmExprCon (PatSynCon _) es) = not (null es)
-
-pprPmExprWithParens :: PmExpr -> PmPprM SDoc
-pprPmExprWithParens expr
- | needsParens expr = parens <$> pprPmExpr expr
- | otherwise = pprPmExpr expr
-
-pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
-pprPmExprCon (RealDataCon con) args
- | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args
- | isConsDataCon con = pretty_list
- where
- mkTuple :: [SDoc] -> SDoc
- mkTuple = parens . fsep . punctuate comma
-
- -- lazily, to be used in the list case only
- pretty_list :: PmPprM SDoc
- pretty_list = case isNilPmExpr (last list) of
- True -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list)
- False -> parens . hcat . punctuate colon <$> mapM pprPmExpr list
-
- list = list_elements args
-
- list_elements [x,y]
- | PmExprCon c es <- y, RealDataCon nilDataCon == c
- = ASSERT(null es) [x,y]
- | PmExprCon c es <- y, RealDataCon consDataCon == c
- = x : list_elements es
- | otherwise = [x,y]
- list_elements list = pprPanic "list_elements:" (ppr list)
-pprPmExprCon cl args
- | conLikeIsInfix cl = case args of
- [x, y] -> do x' <- pprPmExprWithParens x
- y' <- pprPmExprWithParens y
- return (x' <+> ppr cl <+> y')
- -- can it be infix but have more than two arguments?
- list -> pprPanic "pprPmExprCon:" (ppr list)
- | null args = return (ppr cl)
- | otherwise = do args' <- mapM pprPmExprWithParens args
- return (fsep (ppr cl : args'))
-
instance Outputable PmLit where
ppr (PmSLit l) = pmPprHsLit l
ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
--- not really useful for pmexprs per se
instance Outputable PmExpr where
- ppr e = fst $ runPmPprM (pprPmExpr e) []
+ ppr = go (0 :: Int)
+ where
+ go _ (PmExprLit l) = ppr l
+ go _ (PmExprVar v) = ppr v
+ go _ (PmExprOther e) = angleBrackets (ppr e)
+ go _ (PmExprCon (RealDataCon dc) args)
+ | isTupleDataCon dc = parens $ comma_sep $ map ppr args
+ | dc == consDataCon = brackets $ comma_sep $ map ppr (list_cells args)
+ where
+ comma_sep = fsep . punctuate comma
+ list_cells (hd:tl) = hd : list_cells tl
+ list_cells _ = []
+ go prec (PmExprCon cl args)
+ = cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args))
+
=====================================
compiler/deSugar/PmPpr.hs
=====================================
@@ -0,0 +1,191 @@
+{-# LANGUAGE CPP #-}
+
+-- | Provides factilities for pretty-printing 'PmExpr's in a way approriate for
+-- user facing pattern match warnings.
+module PmPpr (
+ pprUncovered
+ ) where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import Name
+import NameEnv
+import NameSet
+import UniqDFM
+import UniqSet
+import ConLike
+import DataCon
+import TysWiredIn
+import Outputable
+import Control.Monad.Trans.State.Strict
+import Maybes
+import Util
+
+import TmOracle
+
+-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
+-- components and refutable shapes associated to any mentioned variables.
+--
+-- Example for @([Just p, q], [p :-> [3,4], q :-> [0,5]]):
+--
+-- @
+-- (Just p) q
+-- where p is not one of {3, 4}
+-- q is not one of {0, 5}
+-- @
+pprUncovered :: ([PmExpr], PmRefutEnv) -> SDoc
+pprUncovered (expr_vec, refuts)
+ | null cs = fsep vec -- there are no literal constraints
+ | otherwise = hang (fsep vec) 4 $
+ text "where" <+> vcat (map pprRefutableShapes cs)
+ where
+ sdoc_vec = mapM pprPmExprWithParens expr_vec
+ (vec,cs) = runPmPpr sdoc_vec (prettifyRefuts refuts)
+
+-- | Output refutable shapes of a variable in the form of @var is not one of {2,
+-- Nothing, 3}@.
+pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
+pprRefutableShapes (var, alts)
+ = var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts)
+ where
+ ppr_alt (PmAltLit lit) = ppr lit
+
+{- 1. Literals
+~~~~~~~~~~~~~~
+Starting with a function definition like:
+
+ f :: Int -> Bool
+ f 5 = True
+ f 6 = True
+
+The uncovered set looks like:
+ { var |> var /= 5, var /= 6 }
+
+Yet, we would like to print this nicely as follows:
+ x , where x not one of {5,6}
+
+Since these variables will be shown to the programmer, we give them better names
+(t1, t2, ..) in 'prettifyRefuts', hence the SDoc in 'PrettyPmRefutEnv'.
+
+2. Residual Constraints
+~~~~~~~~~~~~~~~~~~~~~~~
+Unhandled constraints that refer to HsExpr are typically ignored by the solver
+(it does not even substitute in HsExpr so they are even printed as wildcards).
+Additionally, the oracle returns a substitution if it succeeds so we apply this
+substitution to the vectors before printing them out (see function `pprOne' in
+Check.hs) to be more precise.
+-}
+
+-- | A 'PmRefutEnv' with pretty names for the occuring variables.
+type PrettyPmRefutEnv = DNameEnv (SDoc, [PmAltCon])
+
+-- | Assigns pretty names to constraint variables in the domain of the given
+-- 'PmRefutEnv'.
+prettifyRefuts :: PmRefutEnv -> PrettyPmRefutEnv
+prettifyRefuts = listToUDFM . zipWith rename nameList . udfmToList
+ where
+ rename new (old, lits) = (old, (new, lits))
+ -- Try nice names p,q,r,s,t before using the (ugly) t_i
+ nameList :: [SDoc]
+ nameList = map text ["p","q","r","s","t"] ++
+ [ text ('t':show u) | u <- [(0 :: Int)..] ]
+
+type PmPprM a = State (PrettyPmRefutEnv, NameSet) a
+-- (the first part of the state is read only. make it a reader?)
+
+runPmPpr :: PmPprM a -> PrettyPmRefutEnv -> (a, [(SDoc,[PmAltCon])])
+runPmPpr m lit_env = (result, mapMaybe is_used (udfmToList lit_env))
+ where
+ (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet)
+
+ is_used (k,v)
+ | elemUniqSet_Directly k used = Just v
+ | otherwise = Nothing
+
+addUsed :: Name -> PmPprM ()
+addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x))
+
+checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated
+checkNegation x = do
+ negated <- gets fst
+ return $ case lookupDNameEnv negated x of
+ Just (new, _) -> Just new
+ Nothing -> Nothing
+
+-- | Pretty print a pmexpr, but remember to prettify the names of the variables
+-- that refer to neg-literals. The ones that cannot be shown are printed as
+-- underscores.
+pprPmExpr :: PmExpr -> PmPprM SDoc
+pprPmExpr (PmExprVar x) = do
+ mb_name <- checkNegation x
+ case mb_name of
+ Just name -> addUsed x >> return name
+ Nothing -> return underscore
+pprPmExpr (PmExprCon con args) = pprPmExprCon con args
+pprPmExpr (PmExprLit l) = return (ppr l)
+pprPmExpr (PmExprOther _) = return underscore -- don't show
+
+needsParens :: PmExpr -> Bool
+needsParens (PmExprVar {}) = False
+needsParens (PmExprLit l) = isNegatedPmLit l
+needsParens (PmExprOther {}) = False -- will become a wildcard
+needsParens (PmExprCon (RealDataCon c) es)
+ | isTupleDataCon c
+ || isConsDataCon c || null es = False
+ | otherwise = True
+needsParens (PmExprCon (PatSynCon _) es) = not (null es)
+
+pprPmExprWithParens :: PmExpr -> PmPprM SDoc
+pprPmExprWithParens expr
+ | needsParens expr = parens <$> pprPmExpr expr
+ | otherwise = pprPmExpr expr
+
+pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
+pprPmExprCon (RealDataCon con) args
+ | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args
+ | isConsDataCon con = pretty_list
+ where
+ mkTuple :: [SDoc] -> SDoc
+ mkTuple = parens . fsep . punctuate comma
+
+ -- lazily, to be used in the list case only
+ pretty_list :: PmPprM SDoc
+ pretty_list = case isNilPmExpr (last list) of
+ True -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list)
+ False -> parens . hcat . punctuate colon <$> mapM pprPmExpr list
+
+ list = list_elements args
+
+ list_elements [x,y]
+ | PmExprCon c es <- y, RealDataCon nilDataCon == c
+ = ASSERT(null es) [x,y]
+ | PmExprCon c es <- y, RealDataCon consDataCon == c
+ = x : list_elements es
+ | otherwise = [x,y]
+ list_elements list = pprPanic "list_elements:" (ppr list)
+pprPmExprCon cl args
+ | conLikeIsInfix cl = case args of
+ [x, y] -> do x' <- pprPmExprWithParens x
+ y' <- pprPmExprWithParens y
+ return (x' <+> ppr cl <+> y')
+ -- can it be infix but have more than two arguments?
+ list -> pprPanic "pprPmExprCon:" (ppr list)
+ | null args = return (ppr cl)
+ | otherwise = do args' <- mapM pprPmExprWithParens args
+ return (fsep (ppr cl : args'))
+
+-- | Check whether a literal is negated
+isNegatedPmLit :: PmLit -> Bool
+isNegatedPmLit (PmOLit b _) = b
+isNegatedPmLit _other_lit = False
+
+-- | Check whether a PmExpr is syntactically e
+isNilPmExpr :: PmExpr -> Bool
+isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon
+isNilPmExpr _other_expr = False
+
+-- | Check if a DataCon is (:).
+isConsDataCon :: DataCon -> Bool
+isConsDataCon con = consDataCon == con
=====================================
compiler/deSugar/TmOracle.hs
=====================================
@@ -1,23 +1,27 @@
{-
Author: George Karachalias <george.karachalias at cs.kuleuven.be>
-
-The term equality oracle. The main export of the module is function `tmOracle'.
-}
{-# LANGUAGE CPP, MultiWayIf #-}
+-- | The term equality oracle. The main export of the module are the functions
+-- 'tmOracle', 'solveOneEq' and 'addSolveRefutableAltCon'.
+--
+-- If you are looking for an oracle that can solve type-level constraints, look
+-- at 'TcSimplify.tcCheckSatisfiability'.
module TmOracle (
-- re-exported from PmExpr
- PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
- eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr,
- hsExprToPmExpr, pprPmExprWithParens,
+ PmExpr(..), PmLit(..), PmAltCon(..), TmEq, PmVarEnv,
+ PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
-- the term oracle
- tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,
+ tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq,
+ extendSubst, canDiverge,
+ addSolveRefutableAltCon, lookupRefutableAltCons,
-- misc.
- toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
+ exprDeepLookup, pmLitType
) where
#include "HsVersions.h"
@@ -32,7 +36,8 @@ import Type
import HsLit
import TcHsSyn
import MonadUtils
-import Util
+import ListSetOps (insertNoDup, unionLists)
+import Maybes
import Outputable
import NameEnv
@@ -48,199 +53,219 @@ import NameEnv
-- | The type of substitutions.
type PmVarEnv = NameEnv PmExpr
--- | The environment of the oracle contains
--- 1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
--- 2. A substitution we extend with every step and return as a result.
-type TmOracleEnv = (Bool, PmVarEnv)
+-- | An environment assigning shapes to variables that immediately lead to a
+-- refutation. So, if this maps @x :-> [Just]@, then trying to solve a
+-- 'TmEq' like @x ~ Just False@ immediately leads to a contradiction.
+-- Determinism is important since we use this for warning messages in
+-- 'PmPpr.pprUncovered'. We don't do the same for 'PmVarEnv', so that is a plain
+-- 'NameEnv'.
+--
+-- See also Note [Refutable shapes] in TmOracle.
+type PmRefutEnv = DNameEnv [PmAltCon]
+
+-- | The state of the term oracle. Tracks all term-level facts of the form "x is
+-- @True@" ('tm_pos') and "x is not @5@" ('tm_neg').
+--
+-- Subject to Note [The Pos/Neg invariant].
+data TmState = TmS
+ { tm_pos :: !PmVarEnv
+ -- ^ A substitution with solutions we extend with every step and return as a
+ -- result. The substitution is in /triangular form/: It might map @x@ to @y@
+ -- where @y@ itself occurs in the domain of 'tm_pos', rendering lookup
+ -- non-idempotent. This means that 'varDeepLookup' potentially has to walk
+ -- along a chain of var-to-var mappings until we find the solution but has the
+ -- advantage that when we update the solution for @y@ above, we automatically
+ -- update the solution for @x@ in a union-find-like fashion.
+ , tm_neg :: !PmRefutEnv
+ -- ^ Maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely
+ -- cannot match. Example, @x :-> [3, 4]@ means that @x@ cannot match a literal
+ -- 3 or 4. Should we later solve @x@ to a variable @y@
+ -- ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into those of
+ -- @y at . See also Note [The Pos/Neg invariant].
+ }
+
+{- Note [The Pos/Neg invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Invariant: In any 'TmState', The domains of 'tm_pos' and 'tm_neg' are disjoint.
+
+For example, it would make no sense to say both
+ tm_pos = [...x :-> 3 ...]
+ tm_neg = [...x :-> [3,42]... ]
+The positive information is strictly more informative than the negative.
+
+Suppose we are adding the (positive) fact @x :-> e@ to 'tm_pos'. Then we must
+delete any binding for @x@ from 'tm_neg', to uphold the invariant.
+
+But there is more! Suppose we are adding @x :-> y@ to 'tm_pos', and 'tm_neg'
+contains @x :-> cs, y :-> ds at . Then we want to update 'tm_neg' to
+ at y :-> (cs ++ ds)@, to make use of the negative information we have about @x at .
+-}
+
+-- | Initial state of the oracle.
+initialTmState :: TmState
+initialTmState = TmS emptyNameEnv emptyDNameEnv
+
+-- | Wrap up the term oracle's state once solving is complete. Return the
+-- flattened 'tm_pos' and 'tm_neg'.
+wrapUpTmState :: TmState -> (PmVarEnv, PmRefutEnv)
+wrapUpTmState solver_state
+ = (flattenPmVarEnv (tm_pos solver_state), tm_neg solver_state)
+
+-- | Flatten the triangular subsitution.
+flattenPmVarEnv :: PmVarEnv -> PmVarEnv
+flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
-- | Check whether a constraint (x ~ BOT) can succeed,
-- given the resulting state of the term oracle.
canDiverge :: Name -> TmState -> Bool
-canDiverge x (standby, (_unhandled, env))
+canDiverge x TmS{ tm_pos = pos, tm_neg = neg }
-- If the variable seems not evaluated, there is a possibility for
- -- constraint x ~ BOT to be satisfiable.
- | PmExprVar y <- varDeepLookup env x -- seems not forced
- -- If it is involved (directly or indirectly) in any equality in the
- -- worklist, we can assume that it is already indirectly evaluated,
- -- as a side-effect of equality checking. If not, then we can assume
- -- that the constraint is satisfiable.
- = not $ any (isForcedByEq x) standby || any (isForcedByEq y) standby
- -- Variable x is already in WHNF so the constraint is non-satisfiable
+ -- constraint x ~ BOT to be satisfiable. That's the case when we haven't found
+ -- a solution (i.e. some equivalent literal or constructor) for it yet.
+ | (_, PmExprVar y) <- varDeepLookup pos x -- seems not forced
+ -- Even if we don't have a solution yet, it might be involved in a negative
+ -- constraint, in which case we must already have evaluated it earlier.
+ , Nothing <- lookupDNameEnv neg y
+ = True
+ -- Variable x is already in WHNF or we know some refutable shape, so the
+ -- constraint is non-satisfiable
| otherwise = False
- where
- 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 :: Name -> PmExpr -> Bool
-varIn x e = case e of
- PmExprVar y -> x == y
- PmExprCon _ es -> any (x `varIn`) es
- PmExprLit _ -> False
- PmExprEq e1 e2 -> (x `varIn` e1) || (x `varIn` e2)
- PmExprOther _ -> False
-
--- | Flatten the DAG (Could be improved in terms of performance.).
-flattenPmVarEnv :: PmVarEnv -> PmVarEnv
-flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
-
--- | The state of the term oracle (includes complex constraints that cannot
--- progress unless we get more information).
-type TmState = ([ComplexEq], TmOracleEnv)
-
--- | Initial state of the oracle.
-initialTmState :: TmState
-initialTmState = ([], (False, emptyNameEnv))
-
--- | Solve a complex equality (top-level).
-solveOneEq :: TmState -> ComplexEq -> Maybe TmState
-solveOneEq solver_env@(_,(_,env)) complex
- = solveComplexEq solver_env -- do the actual *merging* with existing state
- $ simplifyComplexEq -- simplify as much as you can
- $ applySubstComplexEq env complex -- replace everything we already know
-
--- | Solve a complex equality.
--- Nothing => definitely unsatisfiable
--- Just tms => I have added the complex equality and added
--- it to the tmstate; the result may or may not be
--- satisfiable
-solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
-solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
+-- | Check whether the equality @x ~ e@ leads to a refutation. Make sure that
+-- @x@ and @e@ are completely substituted before!
+isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool
+isRefutable x e env
+ = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x
+
+-- | Solve an equality (top-level).
+solveOneEq :: TmState -> TmEq -> Maybe TmState
+solveOneEq solver_env (x, e) = unify solver_env (PmExprVar (idName x), e)
+
+exprToAlt :: PmExpr -> Maybe PmAltCon
+exprToAlt (PmExprLit l) = Just (PmAltLit l)
+exprToAlt _ = Nothing
+
+-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
+-- 'TmState' and return @Nothing@ if that leads to a contradiction.
+addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
+addSolveRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
+ = case exprToAlt e of
+ -- We have to take care to preserve Note [The Pos/Neg invariant]
+ Nothing -> Just extended -- Not solved yet
+ Just alt -- We have a solution
+ | alt == nalt -> Nothing -- ... which is contradictory
+ | otherwise -> Just original -- ... which is compatible, rendering the
+ where -- refutation redundant
+ (y, e) = varDeepLookup pos (idName x)
+ extended = original { tm_neg = neg' }
+ neg' = alterDNameEnv (delNulls (insertNoDup nalt)) neg y
+
+-- | When updating 'tm_neg', we want to delete any 'null' entries. This adapter
+-- intends to provide a suitable interface for 'alterDNameEnv'.
+delNulls :: ([a] -> [a]) -> Maybe [a] -> Maybe [a]
+delNulls f mb_entry
+ | ret@(_:_) <- f (fromMaybe [] mb_entry) = Just ret
+ | otherwise = Nothing
+
+-- | Return all 'PmAltCon' shapes that are impossible for 'Id' to take, i.e.
+-- would immediately lead to a refutation by the term oracle.
+lookupRefutableAltCons :: Id -> TmState -> [PmAltCon]
+lookupRefutableAltCons x TmS { tm_neg = neg }
+ = fromMaybe [] (lookupDNameEnv neg (idName x))
+
+-- | Is the given variable /rigid/ (i.e., we have a solution for it) or
+-- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A
+-- semantically helpful alias for 'lookupNameEnv'.
+isRigid :: TmState -> Name -> Maybe PmExpr
+isRigid TmS{ tm_pos = pos } x = lookupNameEnv pos x
+
+-- | Try to unify two 'PmExpr's and record the gained knowledge in the
+-- 'TmState'.
+--
+-- Returns @Nothing@ when there's a contradiction. Returns @Just tms@
+-- when the constraint was compatible with prior facts, in which case @tms@ has
+-- integrated the knowledge from the equality constraint.
+unify :: TmState -> (PmExpr, PmExpr) -> Maybe TmState
+unify tms eq@(e1, e2) = case eq of
-- We cannot do a thing about these cases
- (PmExprOther _,_) -> Just (standby, (True, env))
- (_,PmExprOther _) -> Just (standby, (True, env))
+ (PmExprOther _,_) -> boring
+ (_,PmExprOther _) -> symmetric
(PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-- See Note [Undecidable Equality for Overloaded Literals]
- True -> Just solver_state
- False -> Nothing
+ True -> boring
+ False -> unsat
(PmExprCon c1 ts1, PmExprCon c2 ts2)
- | c1 == c2 -> foldlM solveComplexEq solver_state (zip ts1 ts2)
- | otherwise -> Nothing
- (PmExprCon _ [], PmExprEq t1 t2)
- | isTruePmExpr e1 -> solveComplexEq solver_state (t1, t2)
- | isFalsePmExpr e1 -> Just (eq:standby, (unhandled, env))
- (PmExprEq t1 t2, PmExprCon _ [])
- | isTruePmExpr e2 -> solveComplexEq solver_state (t1, t2)
- | isFalsePmExpr e2 -> Just (eq:standby, (unhandled, env))
+ | c1 == c2 -> foldlM unify tms (zip ts1 ts2)
+ | otherwise -> unsat
(PmExprVar x, PmExprVar y)
- | x == y -> Just solver_state
- | otherwise -> extendSubstAndSolve x e2 solver_state
+ | x == y -> boring
- (PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
- (_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
+ (PmExprVar x, _)
+ | Just e1' <- isRigid tms x -> unify tms (e1', e2)
+ | otherwise -> extendSubstAndSolve x e2 tms
+ (_, PmExprVar{}) -> symmetric
- (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
-
- _ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
- Just (standby, (True, env)) -- I HATE CATCH-ALLS
+ _ -> WARN( True, text "unify: Catch all" <+> ppr eq)
+ boring -- I HATE CATCH-ALLS
+ where
+ boring = Just tms
+ unsat = Nothing
+ symmetric = unify tms (e2, e1)
--- | Extend the substitution and solve the (possibly updated) constraints.
+-- | Extend the substitution if compatible with refutable shapes, reject
+-- (@Nothing@) otherwise.
extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
-extendSubstAndSolve x e (standby, (unhandled, env))
- = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
+extendSubstAndSolve x e TmS{ tm_pos = pos, tm_neg = neg }
+ | isRefutable x e' neg -- NB: e', the flattened solution for @x@
+ = Nothing
+ | otherwise
+ = Just (TmS new_pos new_neg)
where
- -- Apply the substitution to the worklist and partition them to the ones
- -- that had some progress and the rest. Then, recurse over the ones that
- -- had some progress. Careful about performance:
- -- See Note [Representation of Term Equalities] in deSugar/Check.hs
- (changed, unchanged) = partitionWith (substComplexEq x e) standby
- new_incr_state = (unchanged, (unhandled, extendNameEnv env x e))
+ new_pos = extendNameEnv pos x e
+ (y, e') = varDeepLookup new_pos x
+ -- Be careful to uphold Note [The Pos/Neg invariant] by adjusting 'tm_neg'
+ neg' | x == y = neg
+ | otherwise = case lookupDNameEnv neg x of
+ Nothing -> neg
+ Just nalts ->
+ alterDNameEnv (delNulls (unionLists nalts)) neg y
+ new_neg = delFromDNameEnv neg' x
-- | 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@ simply extends the substitution, unlike what
+-- 'extendSubstAndSolve' does.
extendSubst :: Id -> PmExpr -> TmState -> TmState
-extendSubst y e (standby, (unhandled, env))
+extendSubst y e solver_state at TmS{ tm_pos = pos }
| isNotPmExprOther simpl_e
- = (standby, (unhandled, extendNameEnv env x simpl_e))
- | otherwise = (standby, (True, env))
+ = solver_state { tm_pos = extendNameEnv pos x simpl_e }
+ | otherwise = solver_state
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)
-
--- | Simplify an expression. The boolean indicates if there has been any
--- simplification or if the operation was a no-op.
-simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyPmExpr e = case e of
- PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
- (ts', bs) -> (PmExprCon c ts', or bs)
- PmExprEq t1 t2 -> simplifyEqExpr t1 t2
- _other_expr -> (e, False) -- the others are terminals
-
--- | Simplify an equality expression. The equality is given in parts.
-simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyEqExpr e1 e2 = case (e1, e2) of
- -- Varables
- (PmExprVar x, PmExprVar y)
- | x == y -> (truePmExpr, True)
-
- -- Literals
- (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
- -- See Note [Undecidable Equality for Overloaded Literals]
- True -> (truePmExpr, True)
- False -> (falsePmExpr, True)
-
- -- Can potentially be simplified
- (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
- ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
- ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
- ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
- (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
- ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
- ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
- ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
-
- -- Constructors
- (PmExprCon c1 ts1, PmExprCon c2 ts2)
- | c1 == c2 ->
- let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
- (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
- (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
- worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
- in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
- | all isTruePmExpr tss -> (truePmExpr, True)
- | any isFalsePmExpr tss -> (falsePmExpr, True)
- | otherwise -> (worst_case, False)
- | otherwise -> (falsePmExpr, True)
-
- -- We cannot do anything about the rest..
- _other_equality -> (original, False)
-
- where
- original = PmExprEq e1 e2 -- reconstruct equality
-
--- | Apply an (un-flattened) substitution to a simple equality.
-applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
-applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
-
--- | Apply an (un-flattened) substitution to a variable.
-varDeepLookup :: PmVarEnv -> Name -> PmExpr
-varDeepLookup env x
- | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper
- | otherwise = PmExprVar x -- terminal
+ simpl_e = exprDeepLookup pos e
+
+-- | Apply an (un-flattened) substitution to a variable and return its
+-- representative in the triangular substitution @env@ and the completely
+-- substituted expression. The latter may just be the representative wrapped
+-- with 'PmExprVar' if we haven't found a solution for it yet.
+varDeepLookup :: PmVarEnv -> Name -> (Name, PmExpr)
+varDeepLookup env x = case lookupNameEnv env x of
+ Just (PmExprVar y) -> varDeepLookup env y
+ Just e -> (x, exprDeepLookup env e) -- go deeper
+ Nothing -> (x, PmExprVar x) -- terminal
{-# INLINE varDeepLookup #-}
-- | Apply an (un-flattened) substitution to an expression.
exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
-exprDeepLookup env (PmExprVar x) = varDeepLookup env x
+exprDeepLookup env (PmExprVar x) = snd (varDeepLookup env x)
exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
-exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
- (exprDeepLookup env e2)
exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
-- | External interface to the term oracle.
-tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
+tmOracle :: TmState -> [TmEq] -> Maybe TmState
tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
-- | Type of a PmLit
@@ -248,18 +273,49 @@ pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
pmLitType (PmSLit lit) = hsLitType lit
pmLitType (PmOLit _ lit) = overLitType lit
-{- Note [Deep equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Solving nested equalities is the most difficult part. The general strategy
-is the following:
+{- Note [Refutable shapes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider a pattern match like
+
+ foo x
+ | 0 <- x = 42
+ | 0 <- x = 43
+ | 1 <- x = 44
+ | otherwise = 45
+
+This will result in the following initial matching problem:
+
+ PatVec: x (0 <- x)
+ ValVec: $tm_y
+
+Where the first line is the pattern vector and the second line is the value
+vector abstraction. When we handle the first pattern guard in Check, it will be
+desugared to a match of the form
+
+ PatVec: x 0
+ ValVec: $tm_y x
+
+In LitVar, this will split the value vector abstraction for `x` into a positive
+`PmLit 0` and a negative `PmLit x [0]` value abstraction. While the former is
+immediately matched against the pattern vector, the latter (vector value
+abstraction `~[0] $tm_y`) is completely uncovered by the clause.
+
+`pmcheck` proceeds by *discarding* the the value vector abstraction involving
+the guard to accomodate for the desugaring. But this also discards the valuable
+information that `x` certainly is not the literal 0! Consequently, we wouldn't
+be able to report the second clause as redundant.
- * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
- (e1 ~ e2) and then treated recursively.
+That's a typical example of why we need the term oracle, and in this specific
+case, the ability to encode that `x` certainly is not the literal 0. Now the
+term oracle can immediately refute the constraint `x ~ 0` generated by the
+second clause and report the clause as redundant. After the third clause, the
+set of such *refutable* literals is again extended to `[0, 1]`.
- * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
- we know more about the inner equality (e1 ~ e2). That's exactly what
- `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
- truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
- that it is not e but rather e', since it may perform some
- simplifications deeper.
+In general, we want to store a set of refutable shapes (`PmAltCon`) for each
+variable. That's the purpose of the `PmRefutEnv`. `addSolveRefutableAltCon` will
+add such a refutable mapping to the `PmRefutEnv` in the term oracles state and
+check if causes any immediate contradiction. Whenever we record a solution in
+the substitution via `extendSubstAndSolve`, the refutable environment is checked
+for any matching refutable `PmAltCon`.
-}
=====================================
compiler/ghc.cabal.in
=====================================
@@ -324,6 +324,7 @@ Library
MkCore
PprCore
PmExpr
+ PmPpr
TmOracle
Check
Coverage
=====================================
compiler/typecheck/TcRnTypes.hs
=====================================
@@ -391,7 +391,7 @@ data DsLclEnv = DsLclEnv {
-- These two fields are augmented as we walk inwards,
-- through each patttern match in turn
dsl_dicts :: Bag EvVar, -- Constraints from GADT pattern-matching
- dsl_tm_cs :: Bag SimpleEq, -- Constraints form term-level pattern matching
+ dsl_tm_cs :: Bag TmEq, -- Constraints form term-level pattern matching
dsl_pm_iter :: IORef Int -- Number of iterations for pmcheck so far
-- We fail if this gets too big
@@ -1020,7 +1020,7 @@ splice. In particular it is not set when the splice is renamed or typechecked.
'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert
the finalizer (see Note [Delaying modFinalizers in untyped splices]), and
'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to
-set 'RunSplice' when renaming or typechecking the splice, where 'Splice',
+set 'RunSplice' when renaming or typechecking the splice, where 'Splice',
'Brack' or 'Comp' are used instead.
-}
=====================================
compiler/utils/ListSetOps.hs
=====================================
@@ -14,7 +14,7 @@ module ListSetOps (
Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing,
-- Duplicate handling
- hasNoDups, removeDups, findDupsEq,
+ hasNoDups, removeDups, findDupsEq, insertNoDup,
equivClasses,
-- Indexing
@@ -169,3 +169,10 @@ findDupsEq _ [] = []
findDupsEq eq (x:xs) | null eq_xs = findDupsEq eq xs
| otherwise = (x :| eq_xs) : findDupsEq eq neq_xs
where (eq_xs, neq_xs) = partition (eq x) xs
+
+-- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only
+-- when an equal element couldn't be found in @xs at .
+insertNoDup :: (Eq a) => a -> [a] -> [a]
+insertNoDup x set
+ | Nothing <- find (== x) set = x:set
+ | otherwise = set
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/f9758aaf530556f4b9bc5d63005f654c552a599c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/f9758aaf530556f4b9bc5d63005f654c552a599c
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20190601/a54fca8b/attachment-0001.html>
More information about the ghc-commits
mailing list