[Git][ghc/ghc][wip/pmcheck-ncon] 2 commits: Disentangle refutable altcons into literals and conlikes
Sebastian Graf
gitlab at gitlab.haskell.org
Mon Jun 24 06:51:01 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-ncon at Glasgow Haskell Compiler / GHC
Commits:
f74046b8 by Sebastian Graf at 2019-06-23T14:46:23Z
Disentangle refutable altcons into literals and conlikes
- - - - -
407f6077 by Sebastian Graf at 2019-06-24T06:50:54Z
Equality of PmAltCons is not always decidable
- - - - -
5 changed files:
- compiler/basicTypes/NameEnv.hs
- compiler/deSugar/Check.hs
- compiler/deSugar/PmExpr.hs
- compiler/deSugar/PmPpr.hs
- compiler/deSugar/TmOracle.hs
Changes:
=====================================
compiler/basicTypes/NameEnv.hs
=====================================
@@ -27,7 +27,7 @@ module NameEnv (
lookupDNameEnv,
delFromDNameEnv,
mapDNameEnv,
- alterDNameEnv, extendDNameEnv_C,
+ adjustDNameEnv, alterDNameEnv, extendDNameEnv_C,
-- ** Dependency analysis
depAnal
) where
@@ -154,6 +154,9 @@ delFromDNameEnv = delFromUDFM
mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
mapDNameEnv = mapUDFM
+adjustDNameEnv :: (a -> a) -> DNameEnv a -> Name -> DNameEnv a
+adjustDNameEnv = adjustUDFM
+
alterDNameEnv :: (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
alterDNameEnv = alterUDFM
=====================================
compiler/deSugar/Check.hs
=====================================
@@ -628,11 +628,8 @@ normaliseValAbs delta = runMaybeT . go_va delta
-- @PmCon@ for better readability of warning messages.
case incomplete_grps of
([con]:_) | all (== [con]) incomplete_grps -> do
- -- We don't want to simplify to a @PmCon@ (which won't normalise
- -- any further) when @p@ is just the 'cheapInhabitationTest'.
- -- Thus, we have to assert satisfiability here, even if the
- -- expensive 'isConSatisfiable' already did so. Also, we have to
- -- store the constraints in @delta at .
+ -- mkOneSatisfiableConFull, so that the new constraint x ~ con is
+ -- recorded in delta'
(delta', ic) <- MaybeT $ mkOneSatisfiableConFull delta x con
lift $ tracePm "normaliseValAbs2" (ppr x <+> ppr (idType x) <+> ppr (ic_val_abs ic))
pure (delta', ic_val_abs ic)
=====================================
compiler/deSugar/PmExpr.hs
=====================================
@@ -10,7 +10,8 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
module PmExpr (
PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), isNotPmExprOther,
- lhsExprToPmExpr, hsExprToPmExpr, mkPmExprLit, pmExprAsList
+ lhsExprToPmExpr, hsExprToPmExpr, mkPmExprLit, decEqPmAltCon,
+ injectPmAltCons, pmExprAsList
) where
#include "HsVersions.h"
@@ -63,7 +64,31 @@ data PmExpr = PmExprVar Name
-- See Note [Undecidable Equality for Overloaded Literals]
data PmLit = PmSLit (HsLit GhcTc) -- simple
| PmOLit Bool {- is it negated? -} (HsOverLit GhcTc) -- overloaded
- deriving Eq
+
+-- | Decidable equality for values represented by 'PmLit's.
+-- See Note [Undecidable Equality for Overloaded Literals]
+decEqPmLit :: PmLit -> PmLit -> Maybe Bool
+decEqPmLit (PmSLit l1) (PmSLit l2) = Just (l1 == l2)
+decEqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
+ | b1 == b2, l1 == l2
+ = Just True
+decEqPmLit _ _ = Nothing
+
+-- Syntactic equality.
+instance Eq PmLit where
+ a == b = decEqPmLit a b == Just True
+
+-- | Decidable equality for values represented by 'ConLike's.
+-- 'PatSynCon's aren't enforced to be injective, so two syntactically different
+-- 'PatSynCon's might match the exact same values. Without looking into and
+-- reasoning about the pattern synonym's definition, we can't decide if their
+-- sets of matched values is different.
+decEqConLike :: ConLike -> ConLike -> Maybe Bool
+decEqConLike (RealDataCon dc1) (RealDataCon dc2) = Just (dc1 == dc2)
+decEqConLike (PatSynCon psc1) (PatSynCon psc2)
+ | psc1 == psc2
+ = Just True
+decEqConLike _ _ = Nothing
-- | 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.
@@ -71,7 +96,18 @@ data PmLit = PmSLit (HsLit GhcTc) -- simple
-- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'.
data PmAltCon = PmAltConLike ConLike
| PmAltLit PmLit
- deriving Eq
+
+-- | We can't in general decide whether two 'PmAltCon's match the same set of
+-- values. In addition to the reasons in 'decEqPmLit' and 'decEqConLike', a
+-- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
+decEqPmAltCon :: PmAltCon -> PmAltCon -> Maybe Bool
+decEqPmAltCon (PmAltConLike cl1) (PmAltConLike cl2) = decEqConLike cl1 cl2
+decEqPmAltCon (PmAltLit l1) (PmAltLit l2) = decEqPmLit l1 l2
+decEqPmAltCon _ _ = Nothing
+
+-- Syntactic equality.
+instance Eq PmAltCon where
+ a == b = decEqPmAltCon a b == Just True
mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
mkPmExprData dc args = PmExprCon (PmAltConLike (RealDataCon dc)) args
@@ -79,6 +115,9 @@ mkPmExprData dc args = PmExprCon (PmAltConLike (RealDataCon dc)) args
mkPmExprLit :: PmLit -> PmExpr
mkPmExprLit l = PmExprCon (PmAltLit l) []
+injectPmAltCons :: [PmLit] -> [ConLike] -> [PmAltCon]
+injectPmAltCons lits cls = map PmAltLit lits ++ map PmAltConLike cls
+
{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
=====================================
compiler/deSugar/PmPpr.hs
=====================================
@@ -94,7 +94,7 @@ type PrettyPmRefutEnv = DNameEnv (SDoc, [PmAltCon])
prettifyRefuts :: PmRefutEnv -> PrettyPmRefutEnv
prettifyRefuts = listToUDFM . zipWith rename nameList . udfmToList
where
- rename new (old, (_ty, lits)) = (old, (new, lits))
+ rename new (old, (_ty, nlits, ncls)) = (old, (new, injectPmAltCons nlits ncls))
-- Try nice names p,q,r,s,t before using the (ugly) t_i
nameList :: [SDoc]
nameList = map text ["p","q","r","s","t"] ++
=====================================
compiler/deSugar/TmOracle.hs
=====================================
@@ -14,7 +14,7 @@ module TmOracle (
-- the term oracle
tmOracle, TmVarCtEnv, PmRefutEnv, TmState, initialTmState,
wrapUpTmState, solveOneEq, extendSubst, canDiverge, isRigid,
- tryAddRefutableAltCon, lookupRefutableAltCons,
+ tryAddRefutableAltCon,
-- misc.
exprDeepLookup, pmLitType
@@ -33,6 +33,7 @@ import NameEnv
import UniqFM
import UniqDFM
import Type
+import ConLike
import HsLit
import TcHsSyn
import MonadUtils
@@ -63,7 +64,7 @@ type TmVarCtEnv = NameEnv PmExpr
-- 'NameEnv'.
--
-- See also Note [Refutable shapes] in TmOracle.
-type PmRefutEnv = DNameEnv (Type, [PmAltCon])
+type PmRefutEnv = DNameEnv (Type, [PmLit], [ConLike])
-- | The state of the term oracle. Tracks all term-level facts of the form "x is
-- @True@" ('tm_pos') and "x is not @5@" ('tm_neg').
@@ -117,7 +118,9 @@ instance Outputable TmState where
pos = map pos_eq (nonDetUFMToList (tm_pos state))
neg = map neg_eq (udfmToList (tm_neg state))
pos_eq (l, r) = ppr l <+> char '~' <+> ppr r
- neg_eq (l, r) = ppr l <+> text "/~" <+> ppr r
+ neg_eq (l, (ty, lits, cls)) = hsep [ppr l, dcolon, ppr ty, text "/~", ppr alts]
+ where
+ alts = injectPmAltCons lits cls
-- | Initial state of the oracle.
initialTmState :: TmState
@@ -154,8 +157,10 @@ canDiverge x TmS{ tm_pos = pos, tm_neg = neg }
isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool
isRefutable x e env = fromMaybe False $ do
alt <- exprToAlt e
- (_, nalts) <- lookupDNameEnv env x
- pure (elem alt nalts)
+ (_, nlits, ncls) <- lookupDNameEnv env x
+ case alt of
+ PmAltLit lit -> pure (elem lit nlits)
+ PmAltConLike cl -> pure (elem cl ncls)
-- | Solve an equality (top-level).
solveOneEq :: TmState -> TmVarCt -> Maybe TmState
@@ -172,30 +177,30 @@ tryAddRefutableAltCon 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
+ Just alt -> -- We have a solution
+ case decEqPmAltCon alt nalt of
+ Just True -> Nothing -- ... which is contradictory
+ Just False -> Just original -- ... which is compatible, rendering the
+ -- refutation redundant
+ Nothing -> Just extended -- ... which is incomparable, so might
+ -- refute later
+ where
(y, e) = varDeepLookup pos (idName x)
extended = original { tm_neg = neg' }
- neg' = extendDNameEnv_C combineRefutEntries neg y (idType x, [nalt])
+ entry = case nalt of
+ PmAltLit nlit -> (idType x, [nlit], [])
+ PmAltConLike ncl -> (idType x, [], [ncl])
+ neg' = extendDNameEnv_C combineRefutEntries neg y entry
-- | Combines two entries in a 'PmRefutEnv' by merging the set of refutable
-- 'PmAltCon's.
-combineRefutEntries :: (Type, [PmAltCon]) -> (Type, [PmAltCon]) -> (Type, [PmAltCon])
-combineRefutEntries (old_ty, old_nalts) (new_ty, new_nalts)
- = ASSERT( eqType old_ty new_ty ) (old_ty, unionLists old_nalts new_nalts)
-
--- | Return all 'PmAltCon' shapes that are impossible for 'Id' to take, i.e.
--- would immediately lead to a refutation by the term oracle.
---
--- Note that because of Note [The Pos/Neg invariant], this will return an empty
--- list of alt cons for 'Id's which already have a solution.
-lookupRefutableAltCons :: TmState -> Id -> (Type, [PmAltCon])
-lookupRefutableAltCons _tms at TmS{ tm_pos = pos, tm_neg = neg } x
- = fromMaybe (idType x, []) (lookupDNameEnv neg y)
- where
- (y, _e) = varDeepLookup pos (idName x)
+combineRefutEntries
+ :: (Type, [PmLit], [ConLike])
+ -> (Type, [PmLit], [ConLike])
+ -> (Type, [PmLit], [ConLike])
+combineRefutEntries (old_ty, old_nlits, old_ncls) (new_ty, new_nlits, new_ncls)
+ = ASSERT( eqType old_ty new_ty )
+ (old_ty, unionLists old_nlits new_nlits, unionLists old_ncls new_ncls)
-- | Is the given variable /rigid/ (i.e., we have a solution for it) or
-- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A
@@ -224,17 +229,22 @@ unify tms eq@(e1, e2) = case eq of
(PmExprOther _,_) -> boring
(_,PmExprOther _) -> boring
- (PmExprCon c1 ts1, PmExprCon c2 ts2)
+ (PmExprCon c1 ts1, PmExprCon c2 ts2) -> case decEqPmAltCon c1 c2 of
-- See Note [Undecidable Equality for Overloaded Literals]
- | c1 == c2 -> foldlM unify tms (zip ts1 ts2)
- | otherwise -> unsat
+ Just True -> foldlM unify tms (zip ts1 ts2)
+ Just False -> unsat
+ Nothing -> boring
(PmExprVar x, PmExprVar y)
| x == y -> boring
- -- It's important to handle both rigid cases first, otherwise we get cyclic
- -- substitutions. Cf. 'extendSubstAndSolve' and
+ -- It's important to handle both rigid cases before the flexible ones,
+ -- otherwise we get cyclic substitutions. Cf. 'extendSubstAndSolve' and
-- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs at .
+ (PmExprVar x, _)
+ | isRefutable x e2 (tm_neg tms) -> unsat
+ (_, PmExprVar y)
+ | isRefutable y e1 (tm_neg tms) -> unsat
(PmExprVar x, _)
| Just e1' <- isRigid tms x -> unify tms (e1', e2)
(_, PmExprVar y)
@@ -278,7 +288,12 @@ trySolve x e _tms at TmS{ tm_pos = pos, tm_neg = neg }
isRefutable x e neg
= Nothing
| otherwise
- = Just (TmS (extendNameEnv pos x e) (delFromDNameEnv neg x))
+ = Just (TmS (extendNameEnv pos x e) (adjustDNameEnv del_incompat neg x))
+ where
+ PmExprCon alt _ = e -- always succeeds, bc @e@ is a solution
+ del_incompat (ty, nlits, ncls) = case alt of
+ PmAltConLike _ -> (ty, nlits, [])
+ PmAltLit _ -> (ty, [], ncls)
-- | When we know that a variable is fresh, we do not actually have to
-- check whether anything changes, we know that nothing does. Hence,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/310027eae433147fa7b3de6e6c840c7d28f37c0c...407f6077ed8be976570c134bc747f5c5720f897a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/310027eae433147fa7b3de6e6c840c7d28f37c0c...407f6077ed8be976570c134bc747f5c5720f897a
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/20190624/c9bc7c2a/attachment-0001.html>
More information about the ghc-commits
mailing list