[Git][ghc/ghc][wip/pmcheck-refuts] TmOracle: Replace negative term equalities by refutable PmAltCons
Sebastian Graf
gitlab at gitlab.haskell.org
Fri May 24 21:37:28 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-refuts at Glasgow Haskell Compiler / GHC
Commits:
8c3006e9 by Sebastian Graf at 2019-05-24T21:36:26Z
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
form "x can no longer be the literal 5" or "x can no longer be Just y,
for any y". We encode this knowledge in the form of a `PmRefutEnv`,
storing a set of newly introduced `PmAltCon`s (literals and `ConLike`s)
for each variable denoting equations of the above form.
So, say we have `x ≁ Just ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ Just 5`. The entry in the refutable
environment will immediately lead to a contradiction.
This machinery makes the whole `PmExprEq` business completely
unnecessary, getting rid of a lot of (mostly dead) code.
Note that the PmAltConLike case is currently unnecessary. This is bound
to change in a follow-up patch. If we began to use PmAltConLike, we'd
even profit from nicer error messages as is currently the case for
negative literal equalities.
See the Note [Refutable shapes] in TmOracle for a place to start.
- - - - -
7 changed files:
- compiler/basicTypes/NameEnv.hs
- compiler/deSugar/Check.hs
- compiler/deSugar/PmExpr.hs
- + compiler/deSugar/PmPpr.hs
- compiler/deSugar/TmOracle.hs
- compiler/ghc.cabal.in
- compiler/utils/ListSetOps.hs
Changes:
=====================================
compiler/basicTypes/NameEnv.hs
=====================================
@@ -25,6 +25,7 @@ module NameEnv (
emptyDNameEnv,
lookupDNameEnv,
+ delFromDNameEnv,
mapDNameEnv,
alterDNameEnv,
-- ** Dependency analysis
@@ -147,8 +148,11 @@ 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
alterDNameEnv :: (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
-alterDNameEnv = alterUDFM
+alterDNameEnv = alterUDFM
\ No newline at end of file
=====================================
compiler/deSugar/Check.hs
=====================================
@@ -25,6 +25,7 @@ module Check (
import GhcPrelude
import TmOracle
+import PmPpr
import Unify( tcMatchTy )
import DynFlags
import HsSyn
@@ -1672,11 +1673,6 @@ 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)
@@ -2116,7 +2112,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 +2133,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 = []
@@ -2478,21 +2476,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 +2524,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 +2539,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 +2611,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,26 +2626,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
=====================================
compiler/deSugar/PmExpr.hs
=====================================
@@ -8,10 +8,9 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
{-# LANGUAGE ViewPatterns #-}
module PmExpr (
- PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit,
- truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
- lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
- pprPmExprWithParens, runPmPprM
+ PmExpr(..), PmLit(..), PmAltCon(..), SimpleEq, ComplexEq, toComplex,
+ eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
+ substComplexEq
) where
#include "HsVersions.h"
@@ -23,19 +22,14 @@ import FastString (FastString, unpackFS)
import HsSyn
import Id
import Name
-import NameSet
import DataCon
import ConLike
-import TcType (isStringTy)
+import TcType (Type, 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 +55,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 +72,23 @@ 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 'ConLike' or 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'.
+data PmAltCon = PmAltConLike ConLike [Type]
+ -- ^ The types are the argument types of the 'ConLike' application
+ | PmAltLit PmLit
+
+-- | This instance won't compare the argument types of the 'ConLike', as we
+-- carry them for recovering COMPLETE match groups only. The 'PmRefutEnv' below
+-- should never have different 'PmAltConLike's with the same 'ConLike' for the
+-- same variable. See Note [Refutable shapes] in TmOracle.
+instance Eq PmAltCon where
+ PmAltConLike cl1 _ == PmAltConLike cl2 _ = cl1 == cl2
+ PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
+ _ == _ = False
+
{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
@@ -145,9 +155,6 @@ 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)
@@ -156,14 +163,6 @@ type ComplexEq = (PmExpr, PmExpr)
toComplex :: SimpleEq -> ComplexEq
toComplex (x,e) = (PmExprVar (idName x), e)
--- | Expression `True'
-truePmExpr :: PmExpr
-truePmExpr = mkPmExprData trueDataCon []
-
--- | Expression `False'
-falsePmExpr :: PmExpr
-falsePmExpr = mkPmExprData falseDataCon []
-
-- ----------------------------------------------------------------------------
-- ** Predicates on PmExpr
@@ -172,38 +171,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
@@ -216,9 +183,6 @@ substPmExpr x e1 e =
| 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]
@@ -312,155 +276,26 @@ 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))
+
+instance Outputable PmAltCon where
+ ppr (PmAltConLike cl tys) = ppr cl <+> char '@' <> ppr tys
+ ppr (PmAltLit l) = ppr l
=====================================
compiler/deSugar/PmPpr.hs
=====================================
@@ -0,0 +1,192 @@
+{-# 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
+ ppr_alt (PmAltConLike cl _) = ppr cl
+
+{- 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,20 +1,23 @@
{-
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(..), SimpleEq, ComplexEq, 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
@@ -32,7 +35,9 @@ import Type
import HsLit
import TcHsSyn
import MonadUtils
+import ListSetOps (insertNoDup, unionLists)
import Util
+import Maybes
import Outputable
import NameEnv
@@ -48,23 +53,78 @@ 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
+-- 'ComplexEq' 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 we know,
+-- giving special treatment to constraints of the form "x is @True@" ('tm_pos')
+-- and "x is not @5@" ('tm_neg').
+data TmState = TmS
+ { tm_facts :: ![ComplexEq]
+ -- ^ Complex equalities we may assume to hold. We have not (yet) brought them
+ -- into a form leading to a contradiction or a 'SimpleEq'. Otherwise, we would
+ -- store the 'SimpleEq' as a solution in the 'tm_pos' env, where it could be
+ -- used to simplify other equations. All 'ComplexEq's are fully substituted
+ -- according to (i.e., fixed-points under) 'tm_pos'.
+ , tm_pos :: !PmVarEnv
+ -- ^ A substitution with solutions we extend with every step and return as a
+ -- result. Think of it as any 'ComplexEq' from 'tm_facts' we managed to
+ -- bring into the form of a 'SimpleEq'.
+ -- Contrary to 'tm_facts', 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, assuming
+ --
+ -- @
+ -- data T = Leaf Int | Branch T T | Node Int T
+ -- @
+ --
+ -- then @x :-> [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
+ -- and hence can only match @Branch at . Should we later solve @x@ to a variable
+ -- @y@ ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into
+ -- those of @y at .
+ }
+
+-- | Initial state of the oracle.
+initialTmState :: TmState
+initialTmState = TmS [] emptyNameEnv emptyDNameEnv
+
+-- | Wrap up the term oracle's state once solving is complete. Drop any
+-- information about non-simple constraints and flatten (height 1) the
+-- substitution.
+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_facts = facts }
-- 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
+ -- 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
-- 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
+ = not $ any (isForcedByEq x) facts || any (isForcedByEq y) facts
-- Variable x is already in WHNF so the constraint is non-satisfiable
| otherwise = False
@@ -78,27 +138,54 @@ 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))
+-- | 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 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
+solveOneEq solver_env at TmS{ tm_pos = pos } complex
+ = solveComplexEq solver_env -- do the actual *merging* with existing state
+ $ applySubstComplexEq pos complex -- replace everything we already know
+
+exprToAlt :: PmExpr -> Maybe PmAltCon
+-- Note how this deliberately chooses bogus argument types for PmAltConLike.
+-- This is only safe for doing lookup in a 'PmRefutEnv'!
+exprToAlt (PmExprCon cl _) = Just (PmAltConLike cl [])
+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
+ 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))
-- | Solve a complex equality.
-- Nothing => definitely unsatisfiable
@@ -106,10 +193,10 @@ solveOneEq solver_env@(_,(_,env)) complex
-- 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
+solveComplexEq solver_state 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 _,_) -> Just solver_state
+ (_,PmExprOther _) -> Just solver_state
(PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-- See Note [Undecidable Equality for Overloaded Literals]
@@ -119,12 +206,6 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
(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))
(PmExprVar x, PmExprVar y)
| x == y -> Just solver_state
@@ -133,110 +214,68 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
(PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
(_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
- (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
-
_ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
- Just (standby, (True, env)) -- I HATE CATCH-ALLS
+ Just solver_state -- I HATE CATCH-ALLS
-- | Extend the substitution and solve the (possibly updated) constraints.
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_facts = facts, tm_pos = pos, tm_neg = neg }
+ | isRefutable x e' neg -- NB: e'
+ = Nothing
+ | otherwise
+ = foldlM solveComplexEq new_incr_state changed
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))
+ (changed, unchanged) = partitionWith (substComplexEq x e) facts
+ new_pos = extendNameEnv pos x e
+ -- When e is a @PmExprVar y@, we have to check @y@'s solution for
+ -- refutability instead. Afterwards, we have to merge @x@'s refutable shapes
+ -- to @y@'s. Actually, e == e' because it has been fully substituted before,
+ -- but better be safe.
+ (y, e') = varDeepLookup new_pos x
+ new_neg | x == y = neg
+ | otherwise = case lookupDNameEnv neg x of
+ Nothing -> neg
+ Just nalts ->
+ alterDNameEnv (delNulls (unionLists nalts)) neg y
+ `delFromDNameEnv` x
+ new_incr_state = TmS unchanged new_pos new_neg
-- | 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))
+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
+ simpl_e = exprDeepLookup pos e
-- | 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
+-- | 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.
@@ -248,18 +287,57 @@ 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]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
- * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
- (e1 ~ e2) and then treated recursively.
+Consider a pattern match like
- * 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.
--}
+ 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.
+
+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]`.
+
+In general, we want to store a set of refutable shapes (`PmAltCon`) for each
+variable. That's the purpose of the `PmRefutEnv`. This extends to
+`ConLike`s, where all value arguments are universally quantified implicitly.
+So, if the `PmRefutEnv` contains an entry for `x` with `Just [Bool]`, then this
+corresponds to the fact that `forall y. x ≁ Just @Bool y`.
+
+`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`.
+
+Note that `PmAltConLike` carries a list of type arguments. This purely for the
+purpose of being able to reconstruct all other constructors of the matching
+group the `ConLike` is part of through calling `allCompleteMatches` in Check.
+-}
\ No newline at end of file
=====================================
compiler/ghc.cabal.in
=====================================
@@ -324,6 +324,7 @@ Library
MkCore
PprCore
PmExpr
+ PmPpr
TmOracle
Check
Coverage
=====================================
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
\ No newline at end of file
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/8c3006e9514019ca92ac67b68995361a11c436a5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/8c3006e9514019ca92ac67b68995361a11c436a5
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/20190524/6f99443a/attachment-0001.html>
More information about the ghc-commits
mailing list