[Git][ghc/ghc][wip/pmcheck-refuts] TmOracle: Replace negative term equalities by refutable PmAltCons
Sebastian Graf
gitlab at gitlab.haskell.org
Wed May 22 17:20:26 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-refuts at Glasgow Haskell Compiler / GHC
Commits:
13925bff by Sebastian Graf at 2019-05-22T17:20:17Z
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.
- - - - -
3 changed files:
- compiler/deSugar/Check.hs
- compiler/deSugar/PmExpr.hs
- compiler/deSugar/TmOracle.hs
Changes:
=====================================
compiler/deSugar/Check.hs
=====================================
@@ -1672,11 +1672,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 +2111,7 @@ 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)
+ us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
= [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
| otherwise = []
@@ -2136,7 +2131,7 @@ 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)
+ 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,9 +2473,9 @@ 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 (refuts, subst) = wrapUpTmState (delta_tm_cs delta)
+ vector = substInValAbs subst vva
+ in ppr_uncovered (vector, refuts)
-- | Apply a term substitution to a value vector abstraction. All VAs are
-- transformed to PmExpr (used only before pretty printing).
@@ -2490,8 +2485,8 @@ 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)
+wrapUpTmState :: TmState -> (PmRefutEnv, PmVarEnv)
+wrapUpTmState (_, (_, subst, refuts)) = (refuts, flattenPmVarEnv subst)
-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
@@ -2640,18 +2635,21 @@ ppr_pats kind pats
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_constraint :: (SDoc,[PmAltCon]) -> SDoc
+ppr_constraint (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
-ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
-ppr_uncovered (expr_vec, complex)
+ppr_uncovered :: ([PmExpr], PmRefutEnv) -> SDoc
+ppr_uncovered (expr_vec, refuts)
| 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)
+ (vec,cs) = runPmPprM sdoc_vec (prepareRefuts refuts)
{- Note [Representation of Term Equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
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(..), PmRefutEnv, SimpleEq, ComplexEq,
+ toComplex, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
+ substComplexEq, prepareRefuts, pprPmExprWithParens, runPmPprM
) where
#include "HsVersions.h"
@@ -26,14 +25,13 @@ 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 +59,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 +76,31 @@ 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.
+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. We silently assume this in 'TmOracle.isRefutable'.
+instance Eq PmAltCon where
+ PmAltConLike cl1 _ == PmAltConLike cl2 _ = cl1 == cl2
+ PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
+ _ == _ = False
+
+instance Outputable PmAltCon where
+ ppr (PmAltConLike cl tys) = ppr cl <+> char '@' <> ppr tys
+ ppr (PmAltLit l) = ppr l
+
+-- | An environment assigning shapes to variables that immediately lead to a
+-- refutation. So, if @x ≁ Just [Bool] ∈ env@, 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.
+type PmRefutEnv = [(Name, [PmAltCon])]
+
{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
@@ -145,9 +167,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 +175,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
@@ -177,29 +188,11 @@ 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
@@ -216,9 +209,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]
@@ -341,28 +331,15 @@ Check.hs) to be more precice.
-}
-- -----------------------------------------------------------------------------
--- ** Transform residual constraints in appropriate form for pretty printing
+-- ** Transform refutations in appropriate form for pretty printing
-type PmNegLitCt = (Name, (SDoc, [PmLit]))
+type PmNegLitCt = (Name, (SDoc, [PmAltCon]))
-filterComplex :: [ComplexEq] -> [PmNegLitCt]
-filterComplex = zipWith rename nameList . map mkGroup
- . groupBy name . sortBy order . mapMaybe isNegLitCs
+-- | Call this on a list of negative equalities
+prepareRefuts :: PmRefutEnv -> [PmNegLitCt]
+prepareRefuts = zipWith rename nameList
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"] ++
@@ -370,7 +347,7 @@ filterComplex = zipWith rename nameList . map mkGroup
-- ----------------------------------------------------------------------------
-runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmLit])])
+runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmAltCon])])
runPmPprM m lit_env = (result, mapMaybe is_used lit_env)
where
(result, (_lit_env, used)) = runState m (lit_env, emptyNameSet)
@@ -404,13 +381,11 @@ pprPmExpr (PmExprVar x) = do
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
=====================================
compiler/deSugar/TmOracle.hs
=====================================
@@ -9,12 +9,13 @@ The term equality oracle. The main export of the module is function `tmOracle'.
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, prepareRefuts, isNotPmExprOther,
+ runPmPprM, lhsExprToPmExpr, hsExprToPmExpr, pprPmExprWithParens,
-- the term oracle
tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,
+ isRefutable, addSolveRefutableAltCon, lookupRefutableAltCons,
-- misc.
toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
@@ -33,6 +34,7 @@ import HsLit
import TcHsSyn
import MonadUtils
import Util
+import Maybes
import Outputable
import NameEnv
@@ -50,16 +52,20 @@ 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)
+-- 2. A substitution with solutions we extend with every step and return
+-- as a result.
+-- 3. A 'PmRefutEnv' assigning shapes to variables that immediately lead to
+-- a refutation.
+type TmOracleEnv = (Bool, PmVarEnv, PmRefutEnv)
-- | 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 (standby, (_unhandled, env, _refuts))
-- 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 env x -- seems not forced
-- If it is involved (directly or indirectly) in any equality in the
-- worklist, we can assume that it is already indirectly evaluated,
-- as a side-effect of equality checking. If not, then we can assume
@@ -78,9 +84,14 @@ 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
+-- | 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 <*> lookup x env
+
-- | Flatten the DAG (Could be improved in terms of performance.).
flattenPmVarEnv :: PmVarEnv -> PmVarEnv
flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
@@ -91,25 +102,63 @@ type TmState = ([ComplexEq], TmOracleEnv)
-- | Initial state of the oracle.
initialTmState :: TmState
-initialTmState = ([], (False, emptyNameEnv))
+initialTmState = ([], (False, emptyNameEnv, []))
-- | Solve a complex equality (top-level).
solveOneEq :: TmState -> ComplexEq -> Maybe TmState
-solveOneEq solver_env@(_,(_,env)) complex
+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
+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 refute if that leads to a contradiction.
+addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
+addSolveRefutableAltCon original@(standby, (unhandled, env, refuts)) 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
+ -- refutation redundant
+ where
+ (y, e) = varDeepLookup env (idName x)
+ extended = (standby, (unhandled, env, refuts'))
+ refuts' = alterAssoc (Just . (nalt:) . fromMaybe []) y refuts
+
+-- Maybe move this to ListUtils?
+alterAssoc :: Eq a => (Maybe b -> Maybe b) -> a -> [(a, b)] -> [(a, b)]
+alterAssoc f k assocs
+ | Just v <- f mb_entry = (k,v) : assocs'
+ | otherwise = assocs'
+ where
+ (l, r) = break ((== k) . fst) assocs
+ mb_entry = snd <$> listToMaybe r
+ assocs' = l ++ drop 1 r
+
+-- | 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 (_, (_, _, refuts))
+ = fromMaybe [] (lookup (idName x) refuts)
+
-- | Solve a complex equality.
-- Nothing => definitely unsatisfiable
-- Just tms => I have added the complex equality and added
-- it to the tmstate; the result may or may not be
-- satisfiable
solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
-solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
+solveComplexEq solver_state@(standby, (_unhandled, env, refuts)) 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 (standby, (True, env, refuts))
+ (_,PmExprOther _) -> Just (standby, (True, env, refuts))
(PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-- See Note [Undecidable Equality for Overloaded Literals]
@@ -119,12 +168,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,14 +176,15 @@ 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 (standby, (True, env, refuts)) -- 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))
+extendSubstAndSolve x e (standby, (unhandled, env, refuts))
+ | isRefutable x e refuts
+ = Nothing
+ | otherwise
= foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
where
-- Apply the substitution to the worklist and partition them to the ones
@@ -148,17 +192,17 @@ extendSubstAndSolve x e (standby, (unhandled, env))
-- had some progress. Careful about performance:
-- See Note [Representation of Term Equalities] in deSugar/Check.hs
(changed, unchanged) = partitionWith (substComplexEq x e) standby
- new_incr_state = (unchanged, (unhandled, extendNameEnv env x e))
+ new_incr_state = (unchanged, (unhandled, extendNameEnv env x e, refuts))
-- | 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 (standby, (unhandled, env, refuts))
| isNotPmExprOther simpl_e
- = (standby, (unhandled, extendNameEnv env x simpl_e))
- | otherwise = (standby, (True, env))
+ = (standby, (unhandled, extendNameEnv env x simpl_e, refuts))
+ | otherwise = (standby, (True, env, refuts))
where
x = idName y
simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e
@@ -170,73 +214,30 @@ simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
-- | Simplify an expression. The boolean indicates if there has been any
-- simplification or if the operation was a no-op.
simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
simplifyPmExpr e = case e of
PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
(ts', bs) -> (PmExprCon c ts', or bs)
- PmExprEq t1 t2 -> simplifyEqExpr t1 t2
_other_expr -> (e, False) -- the others are terminals
--- | Simplify an equality expression. The equality is given in parts.
-simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyEqExpr e1 e2 = case (e1, e2) of
- -- Varables
- (PmExprVar x, PmExprVar y)
- | x == y -> (truePmExpr, True)
-
- -- Literals
- (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
- -- See Note [Undecidable Equality for Overloaded Literals]
- True -> (truePmExpr, True)
- False -> (falsePmExpr, True)
-
- -- Can potentially be simplified
- (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
- ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
- ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
- ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
- (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
- ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
- ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
- ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
-
- -- Constructors
- (PmExprCon c1 ts1, PmExprCon c2 ts2)
- | c1 == c2 ->
- let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
- (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
- (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
- worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
- in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
- | all isTruePmExpr tss -> (truePmExpr, True)
- | any isFalsePmExpr tss -> (falsePmExpr, True)
- | otherwise -> (worst_case, False)
- | otherwise -> (falsePmExpr, True)
-
- -- We cannot do anything about the rest..
- _other_equality -> (original, False)
-
- where
- original = PmExprEq e1 e2 -- reconstruct equality
-
-- | Apply an (un-flattened) substitution to a simple equality.
applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
--- | Apply an (un-flattened) substitution to a variable.
-varDeepLookup :: PmVarEnv -> Name -> PmExpr
-varDeepLookup env x
- | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper
- | otherwise = PmExprVar x -- terminal
+-- | 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.
@@ -246,20 +247,4 @@ tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
-- | Type of a PmLit
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:
-
- * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
- (e1 ~ e2) and then treated recursively.
-
- * 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.
--}
+pmLitType (PmOLit _ lit) = overLitType lit
\ No newline at end of file
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/13925bff0ee91de0a56addf2baa6d3f7eebbebc5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/13925bff0ee91de0a56addf2baa6d3f7eebbebc5
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/20190522/17ccfd59/attachment-0001.html>
More information about the ghc-commits
mailing list