diff options
author | Sebastian Graf <sebastian.graf@kit.edu> | 2020-09-04 10:55:50 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-09-22 05:38:35 -0400 |
commit | 6fe8a0c756f8b12df5cf192ea9b0c33feb150843 (patch) | |
tree | e2da9a25f6ec7a10681bd228f44a3f42aaa2f22e | |
parent | 416bd50e58b23ad70813b18a913ca77a3ab6e936 (diff) | |
download | haskell-6fe8a0c756f8b12df5cf192ea9b0c33feb150843.tar.gz |
PmCheck - Comments only: Replace /~ by ≁
-rw-r--r-- | compiler/GHC/HsToCore/PmCheck.hs | 18 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Oracle.hs | 44 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Types.hs | 4 |
3 files changed, 33 insertions, 33 deletions
diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs index 9b9ce9d700..831509d351 100644 --- a/compiler/GHC/HsToCore/PmCheck.hs +++ b/compiler/GHC/HsToCore/PmCheck.hs @@ -221,7 +221,7 @@ safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning exception into divergence (@f x = f x@). Semantically, unlike every other case expression, -XEmptyCase is strict in its -match var x, which rules out ⊥ as an inhabitant. So we add x /~ ⊥ to the +match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the initial Nabla and check if there are any values left to match on. -} @@ -786,7 +786,7 @@ Note [Strict fields and fields of unlifted type] How do strict fields play into Note [Field match order for RecCon]? Answer: They don't. Desugaring is entirely unconcerned by strict fields; the forcing happens *before* pattern matching. But for each strict (or more generally, -unlifted) field @s@ we have to add @s /~ ⊥@ constraints when we check the PmCon +unlifted) field @s@ we have to add @s ≁ ⊥@ constraints when we check the PmCon guard in 'checkGrd'. Strict fields are devoid of ⊥ by construction, there's nothing that a bang pattern would act on. Example from #18341: @@ -798,7 +798,7 @@ nothing that a bang pattern would act on. Example from #18341: The second clause desugars to @MkT n <- x, !n@. When coverage checked, the 'PmCon' @MkT n <- x@ refines the set of values that reach the bang pattern with -the constraints @x ~ MkT n, n /~ ⊥@ (this list is computed by 'pmConCts'). +the constraints @x ~ MkT n, n ≁ ⊥@ (this list is computed by 'pmConCts'). Checking the 'PmBang' @!n@ will then try to add the constraint @n ~ ⊥@ to this set to get the diverging set, which is found to be empty. Hence the whole clause is detected as redundant, as expected. @@ -942,7 +942,7 @@ throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds) -- These include -- -- * @gammas@: Constraints arising from the bound evidence vars --- * @y /~ ⊥@ constraints for each unlifted field (including strict fields) +-- * @y ≁ ⊥@ constraints for each unlifted field (including strict fields) -- @y@ in @ys@ -- * The constructor constraint itself: @x ~ T as ys@. -- @@ -974,7 +974,7 @@ checkGrd grd = CA $ \inc -> case grd of pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched } , cr_uncov = mempty , cr_approx = Precise } - -- Bang x _: Diverge on x ~ ⊥, refine with x /~ ⊥ + -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥ PmBang x mb_info -> do div <- addPmCtNablas inc (PmBotCt x) matched <- addPmCtNablas inc (PmNotBotCt x) @@ -986,7 +986,7 @@ checkGrd grd = CA $ \inc -> case grd of pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs } , cr_uncov = mempty , cr_approx = Precise } - -- Con: Fall through on x /~ K and refine with x ~ K ys and type info + -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info PmCon x con tvs dicts args -> do !div <- if isPmAltConMatchStrict con then addPmCtNablas inc (PmBotCt x) @@ -1048,7 +1048,7 @@ How do we do that? Consider And imagine we set our limit to 1 for the sake of the example. The first clause will be checked against the initial Nabla, {}. Doing so will produce an -Uncovered set of size 2, containing the models {x/~True} and {x~True,y/~True}. +Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}. Also we find the first clause to cover the model {x~True,y~True}. But the Uncovered set we get out of the match is too huge! We somehow have to @@ -1056,8 +1056,8 @@ ensure not to make things worse as they are already, so we continue checking with a singleton Uncovered set of the initial Nabla {}. Why is this sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts to forgetting that we matched against the first clause. The values represented -by {} are a superset of those represented by its two refinements {x/~True} and -{x~True,y/~True}. +by {} are a superset of those represented by its two refinements {x≁True} and +{x~True,y≁True}. This forgetfulness becomes very apparent in the example above: By continuing with {} we don't detect the second clause as redundant, as it again covers the diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs index e3f4cec57b..492e993f19 100644 --- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs +++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs @@ -628,10 +628,10 @@ Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos', any entry in 'vi_neg' must be incomparable to C (return Nothing) according to 'eqPmAltCons'. Those entries that are comparable either lead to a refutation or are redundant. Examples: -* @x ~ Just y@, @x /~ [Just]@. 'eqPmAltCon' returns @Equal@, so refute. -* @x ~ Nothing@, @x /~ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative +* @x ~ Just y@, @x ≁ [Just]@. 'eqPmAltCon' returns @Equal@, so refute. +* @x ~ Nothing@, @x ≁ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative info is redundant and should be discarded. -* @x ~ I# y@, @x /~ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal. +* @x ~ I# y@, @x ≁ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal. We keep this info in order to be able to refute a redundant match on i.e. 4 later on. @@ -676,19 +676,19 @@ oracle) contradictory. This implies a few invariants: Maintaining these invariants in 'addVarCt' (the core of the term oracle) and 'addNotConCt' is subtle. * Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate'). - - (COMPLETE) If we had @x /~ True@ and @y /~ False@, then we get - @x /~ [True,False]@. This is vacuous by matter of comparing to the built-in + - (COMPLETE) If we had @x ≁ True@ and @y ≁ False@, then we get + @x ≁ [True,False]@. This is vacuous by matter of comparing to the built-in COMPLETE set, so should refute. - - (Pos/Neg) If we had @x /~ True@ and @y ~ True@, we have to refute. + - (Pos/Neg) If we had @x ≁ True@ and @y ~ True@, we have to refute. * Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addConCt') - - (Neg) If we had @x /~ K@, refute. + - (Neg) If we had @x ≁ K@, refute. - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to 'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute. - - (Refine) If we had @x /~ K zs@, unify each y with each z in turn. -* Adding negative information. Example: Add the fact @x /~ Nothing@ (see 'addNotConCt') + - (Refine) If we had @x ≁ K zs@, unify each y with each z in turn. +* Adding negative information. Example: Add the fact @x ≁ Nothing@ (see 'addNotConCt') - (Refut) If we have @x ~ K ys@, refute. - - (COMPLETE) If K=Nothing and we had @x /~ Just@, then we get - @x /~ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in + - (COMPLETE) If K=Nothing and we had @x ≁ Just@, then we get + @x ≁ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in COMPLETE set, so should refute. Note that merging VarInfo in equate can be done by calling out to 'addConCt' and @@ -783,10 +783,10 @@ clause as redundant, which clearly is unsound. The solution: 1. 'isPmAltConMatchStrict' returns False for newtypes, indicating that a newtype match is lazy. 2. When we find @x ~ T2 y@, transfer all constraints on @x@ (which involve @⊥@) - to @y@, similar to what 'equate' does, and don't add a @x /~ ⊥@ constraint. + to @y@, similar to what 'equate' does, and don't add a @x ≁ ⊥@ constraint. This way, the third clause will still be marked as inaccessible RHS instead of redundant. This is ensured by calling 'lookupVarInfoNT'. -3. Immediately reject when we find @x /~ T2@. +3. Immediately reject when we find @x ≁ T2@. Handling of Newtypes is also described in the Appendix of the Lower Your Guards paper, where you can find the solution in a perhaps more digestible format. -} @@ -826,13 +826,13 @@ data TmCt -- ^ @TmConCt x K tvs ys@ encodes "x ~ K @tvs ys", equating @x@ with the 'PmAltCon' -- application @K @tvs ys@. | TmNotConCt !Id !PmAltCon - -- ^ @TmNotConCt x K@ encodes "x /~ K", asserting that @x@ can't be headed + -- ^ @TmNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed -- by @K@. | TmBotCt !Id -- ^ @TmBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥. -- by @K@. | TmNotBotCt !Id - -- ^ @TmNotBotCt x y@ encodes "x /~ ⊥", asserting that @x@ can't be ⊥. + -- ^ @TmNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥. instance Outputable TmCt where ppr (TmVarCt x y) = ppr x <+> char '~' <+> ppr y @@ -841,9 +841,9 @@ instance Outputable TmCt where where pp_tvs = map ((<> char '@') . ppr) tvs pp_args = map ppr args - ppr (TmNotConCt x con) = ppr x <+> text "/~" <+> ppr con + ppr (TmNotConCt x con) = ppr x <+> text "≁" <+> ppr con ppr (TmBotCt x) = ppr x <+> text "~ ⊥" - ppr (TmNotBotCt x) = ppr x <+> text "/~ ⊥" + ppr (TmNotBotCt x) = ppr x <+> text "≁ ⊥" type TyCt = PredType @@ -908,7 +908,7 @@ addBotCt :: Nabla -> Id -> MaybeT DsM Nabla addBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x case bot of - IsNotBot -> mzero -- There was x /~ ⊥. Contradiction! + IsNotBot -> mzero -- There was x ≁ ⊥. Contradiction! IsBot -> pure nabla -- There already is x ~ ⊥. Nothing left to do MaybeBot -> do -- We add x ~ ⊥ let vi' = vi{ vi_bot = IsBot } @@ -1015,8 +1015,8 @@ addNotBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x case bot of IsBot -> mzero -- There was x ~ ⊥. Contradiction! - IsNotBot -> pure nabla -- There already is x /~ ⊥. Nothing left to do - MaybeBot -> do -- We add x /~ ⊥ and test if x is still inhabited + IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do + MaybeBot -> do -- We add x ≁ ⊥ and test if x is still inhabited vi <- ensureInhabited nabla vi{ vi_bot = IsNotBot } pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env y vi) reps} @@ -1776,7 +1776,7 @@ addCoreCt nabla x e = do -- | Look at @let x = K taus theta es@ and generate the following -- constraints (assuming universals were dropped from @taus@ before): - -- 1. @x /~ ⊥@ if 'K' is not a Newtype constructor. + -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor. -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@ -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@ -- 4. @x ~ K as ys@ @@ -1791,7 +1791,7 @@ addCoreCt nabla x e = do uniq_supply <- lift $ lift $ getUniqueSupplyM let (_, ex_tvs) = cloneTyVarBndrs (mkEmptyTCvSubst in_scope) dc_ex_tvs uniq_supply ty_cts = equateTys (map mkTyVarTy ex_tvs) ex_tys - -- 1. @x /~ ⊥@ if 'K' is not a Newtype constructor (#18341) + -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor (#18341) when (not (isNewDataCon dc)) $ modifyT $ \nabla -> addNotBotCt nabla x -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703 diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs index 12bd5f32fb..4602b89611 100644 --- a/compiler/GHC/HsToCore/PmCheck/Types.hs +++ b/compiler/GHC/HsToCore/PmCheck/Types.hs @@ -416,7 +416,7 @@ instance Outputable PmEquality where -- | A data type that caches for the 'VarInfo' of @x@ the results of querying -- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for --- which we already know @x /~ K@ from these sets. +-- which we already know @x ≁ K@ from these sets. -- -- For motivation, see Section 5.3 in Lower Your Guards. -- See also Note [Implementation of COMPLETE pragmas] @@ -552,7 +552,7 @@ data VarInfo -- data T = Leaf Int | Branch T T | Node Int T -- @ -- - -- then @x /~ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@, + -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@, -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos', -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing -- between 'vi_pos' and 'vi_neg'. |