[Git][ghc/ghc][wip/pmcheck-refuts] TmOracle: Replace negative term equalities by refutable PmAltCons
Sebastian Graf
gitlab at gitlab.haskell.org
Fri May 31 16:12:51 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-refuts at Glasgow Haskell Compiler / GHC
Commits:
5ccfbb40 by Sebastian Graf at 2019-05-31T16:06:15Z
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` business unnecessary,
getting rid of a lot of (mostly dead) code.
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,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
@@ -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
=====================================
@@ -6,12 +6,12 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE GeneralisedNewtypeDeriving #-}
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,7 +23,6 @@ import FastString (FastString, unpackFS)
import HsSyn
import Id
import Name
-import NameSet
import DataCon
import ConLike
import TcType (isStringTy)
@@ -32,10 +31,6 @@ import Outputable
import Util
import SrcLoc
-import Data.Maybe (mapMaybe)
-import Data.List (groupBy, sortBy, nubBy)
-import Control.Monad.Trans.State.Lazy
-
{-
%************************************************************************
%* *
@@ -61,7 +56,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 +73,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,9 +149,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 +157,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 +165,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 +177,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 +270,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(..), 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
+ toComplex, exprDeepLookup, pmLitType
) where
#include "HsVersions.h"
@@ -32,7 +36,9 @@ import Type
import HsLit
import TcHsSyn
import MonadUtils
+import ListSetOps (insertNoDup, unionLists)
import Util
+import Maybes
import Outputable
import NameEnv
@@ -48,26 +54,93 @@ 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').
+--
+-- Subject to Note [The Pos/Neg invariant].
+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, @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. 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
-
where
isForcedByEq :: Name -> ComplexEq -> Bool
isForcedByEq y (e1, e2) = varIn y e1 || varIn y e2
@@ -78,27 +151,51 @@ 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
+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))
-- | Solve a complex equality.
-- Nothing => definitely unsatisfiable
@@ -106,10 +203,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 +216,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 +224,66 @@ 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
+
+ -- Be careful to uphold Note [The Pos/Neg invariant] by adjusting 'tm_neg'
+ (y, e') = varDeepLookup new_pos x
+ 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
+ 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@ 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 +295,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]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
- * 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`. `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`.
+-}
\ 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
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/5ccfbb4069ee9e9bb35bf7b81a3de0f2c09eaf9d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/5ccfbb4069ee9e9bb35bf7b81a3de0f2c09eaf9d
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/20190531/13dca501/attachment-0001.html>
More information about the ghc-commits
mailing list