[Git][ghc/ghc][wip/romes/eqsat-pmc] Retrying from the working stage.
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Thu Jul 13 23:45:47 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
ebacbf5c by Rodrigo Mesquita at 2023-07-14T00:45:30+01:00
Retrying from the working stage.
- - - - -
7 changed files:
- compiler/GHC/Core/Equality.hs
- compiler/GHC/HsToCore/Errors/Ppr.hs
- compiler/GHC/HsToCore/Errors/Types.hs
- compiler/GHC/HsToCore/Pmc.hs
- compiler/GHC/HsToCore/Pmc/Check.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
Changes:
=====================================
compiler/GHC/Core/Equality.hs
=====================================
@@ -338,7 +338,7 @@ instance Ord a => Ord (DeBruijn (CoreAltF a)) where
cmpDeBruijnTickish :: DeBruijn CoreTickish -> DeBruijn CoreTickish -> Ordering
cmpDeBruijnTickish (D env1 t1) (D env2 t2) = go t1 t2 where
- go (Breakpoint lext lid lids) (Breakpoint rext rid rids)
+ go (Breakpoint lext lid lids _) (Breakpoint rext rid rids _)
= case compare lid rid of
LT -> LT
EQ -> case compare (D env1 lids) (D env2 rids) of
=====================================
compiler/GHC/HsToCore/Errors/Ppr.hs
=====================================
@@ -22,6 +22,8 @@ import GHC.Utils.Misc
import GHC.Utils.Outputable
import qualified GHC.LanguageExtensions as LangExt
import GHC.HsToCore.Pmc.Ppr
+import GHC.HsToCore.Pmc.Solver.Types (lookupMatchIdMap)
+import Data.Maybe (fromJust)
instance Diagnostic DsMessage where
@@ -71,7 +73,8 @@ instance Diagnostic DsMessage where
pprContext False kind (text "are non-exhaustive") $ \_ ->
case vars of -- See #11245
[] -> text "Guards do not cover entire pattern space"
- _ -> let us = map (\nabla -> pprUncovered nabla vars) nablas
+ -- See Note (TODO) [The MatchIds for error reporting] (and possibly factor this map lookupMatchIdMap outside)
+ _ -> let us = map (\nabla -> pprUncovered nabla (map (fromJust . (`lookupMatchIdMap` nabla)) vars)) nablas
-- pp_tys = pprQuotedList $ map idType vars
pp_tys = empty
in hang
=====================================
compiler/GHC/HsToCore/Errors/Types.hs
=====================================
@@ -101,7 +101,7 @@ data DsMessage
| DsNonExhaustivePatterns !(HsMatchContext GhcRn)
!ExhaustivityCheckType
!MaxUncoveredPatterns
- [ClassId]
+ [Id] -- ^ The MatchIds, see Note (TODO) [The MatchIds for error reporting]
[Nabla]
| DsTopLevelBindsNotAllowed !BindsType !(HsBindLR GhcTc GhcTc)
=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -75,7 +75,7 @@ import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Data.Coerce
-import Data.Equality.Graph (ClassId)
+import Data.Maybe (fromJust)
--
-- * Exported entry points to the checker
@@ -104,22 +104,15 @@ pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
-- See Note [pmcPatBind only checks PatBindRhs]
pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
!missing <- getLdiNablas
+
+ -- See Note (TODO) [Represent the MatchIds before the CheckAction]
+ let missing' = representIdNablas var missing
+
pat_bind <- noCheckDs $ desugarPatBind loc var p
tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
- result0 <- unCA (checkPatBind pat_bind) missing
- tracePm "}: " (ppr (cr_uncov result0))
- -- romes:todo: this seems redundant, hints that the right thing might be for desugar to return already the match variables already "represented" in the e-graph
- -- doing this, however, wouuld require for desugar pat binds to care about/thread through nablas
- -- DESIGN:TODO: However, if we represent the variables while desugaring, we
- -- would no longer need representId to represent VarF in the e-class, and can
- -- instead do newEClass. This would further reduce allocations.
- -- The reason why we can't do that currently is that on checkPatBind we'll
- -- representIds, and when we represent them again in the next line, we want
- -- them to match the ones we represented during checkPatBind. If we made
- -- empty-eclasses, the representId on the next line wouldn't match the match
- -- ids we defined in checkPatBind.
- let (varid, cr_uncov') = representId var (cr_uncov result0)
- formatReportWarnings ReportPatBind ctxt [varid] result0{cr_uncov = cr_uncov'}
+ result <- unCA (checkPatBind pat_bind) missing'
+ tracePm "}: " (ppr (cr_uncov result))
+ formatReportWarnings ReportPatBind ctxt [var] result
pmcPatBind _ _ _ = pure ()
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -173,28 +166,27 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
2
(vcat (map ppr matches) $$ ppr missing)
+
+ -- See Note (TODO) [Represent the MatchIds before the CheckAction]
+ let missing' = representIdsNablas vars missing
+
case NE.nonEmpty matches of
Nothing -> do
-- This must be an -XEmptyCase. See Note [Checking EmptyCase]
let var = only vars
empty_case <- noCheckDs $ desugarEmptyCase var
- result0 <- unCA (checkEmptyCase empty_case) missing
- tracePm "}: " (ppr (cr_uncov result0))
- let (varids, cr_uncov') = representIds vars (cr_uncov result0) -- romes:todo: this seems redundant, hints that the right thing might be for desugar to return already the match variables already "represented" in the e-graph
- formatReportWarnings ReportEmptyCase ctxt varids result0{cr_uncov=cr_uncov'}
+ result <- unCA (checkEmptyCase empty_case) missing'
+ tracePm "}: " (ppr (cr_uncov result))
+ formatReportWarnings ReportEmptyCase ctxt vars result
return []
Just matches -> do
matches <- {-# SCC "desugarMatches" #-}
noCheckDs $ desugarMatches vars matches
- result0 <- {-# SCC "checkMatchGroup" #-}
- unCA (checkMatchGroup matches) missing
- tracePm "}: " (ppr (cr_uncov result0))
- let (varids, cr_uncov') = representIds vars (cr_uncov result0)
- -- romes:todo: this seems redundant, hints that the right thing might be
- -- for desugar to return already the match variables already "represented"
- -- in the e-graph
- {-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt varids result0{cr_uncov=cr_uncov'}
- return (NE.toList (ldiMatchGroup (cr_ret result0)))
+ result <- {-# SCC "checkMatchGroup" #-}
+ unCA (checkMatchGroup matches) missing'
+ tracePm "}: " (ppr (cr_uncov result))
+ {-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt vars result
+ return (NE.toList (ldiMatchGroup (cr_ret result)))
{- Note [pmcPatBind only checks PatBindRhs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -358,7 +350,11 @@ collectInMode ReportEmptyCase = cirbsEmptyCase
-- | Given a 'FormatReportWarningsMode', this function will emit warnings
-- for a 'CheckResult'.
-formatReportWarnings :: FormatReportWarningsMode ann -> DsMatchContext -> [ClassId] -> CheckResult ann -> DsM ()
+formatReportWarnings :: FormatReportWarningsMode ann
+ -> DsMatchContext
+ -> [Id] -- ^ The MatchIds, see Note (TODO) [The MatchIds for error reporting]
+ -> CheckResult ann
+ -> DsM ()
formatReportWarnings report_mode ctx vars cr at CheckResult { cr_ret = ann } = do
cov_info <- collectInMode report_mode ann
dflags <- getDynFlags
@@ -366,7 +362,7 @@ formatReportWarnings report_mode ctx vars cr at CheckResult { cr_ret = ann } = do
-- | Issue all the warnings
-- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
-reportWarnings :: DynFlags -> FormatReportWarningsMode ann -> DsMatchContext -> [ClassId] -> CheckResult CIRB -> DsM ()
+reportWarnings :: DynFlags -> FormatReportWarningsMode ann -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
reportWarnings dflags report_mode (DsMatchContext kind loc) vars
CheckResult { cr_ret = CIRB { cirb_inacc = inaccessible_rhss
, cirb_red = redundant_rhss
@@ -405,13 +401,16 @@ reportWarnings dflags report_mode (DsMatchContext kind loc) vars
maxPatterns = maxUncoveredPatterns dflags
-getNFirstUncovered :: GenerateInhabitingPatternsMode -> [ClassId] -> Int -> Nablas -> DsM [Nabla]
+getNFirstUncovered :: GenerateInhabitingPatternsMode
+ -> [Id] -- ^ The MatchIds, see Note (TODO) [The MatchIds for error reporting]
+ -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered mode vars n (MkNablas nablas) = go n (bagToList nablas)
where
go 0 _ = pure []
go _ [] = pure []
go n (nabla:nablas) = do
- front <- generateInhabitingPatterns mode vars n nabla
+ -- See Note (TODO) [The MatchIds for error reporting] (and possibly factor this map lookupMatchIdMap to an independent function since its used twice, here and in the call of pprUncovered)
+ front <- generateInhabitingPatterns mode (map (fromJust . (`lookupMatchIdMap` nabla)) vars) n nabla
back <- go (n - length front) nablas
pure (front ++ back)
@@ -448,8 +447,9 @@ addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs [] _ k = k
addCoreScrutTmCs (scr:scrs) (x0:xs) k =
flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas0 ->
- let (x, nablas) = representId x0 nablas0
- in addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
+ liftNablasM (\d ->
+ let (x, d') = representId x0 d
+ in addPhiCts d' (unitBag (PhiCoreCt x scr))) nablas0
addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: numbers of scrutinees and match ids differ"
-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.
@@ -500,4 +500,18 @@ unreachable.
We make sure to always start from an inhabited 'Nablas' by calling
'getLdiNablas', which falls back to the trivially inhabited 'Nablas' if the
long-distance info returned by 'GHC.HsToCore.Monad.getPmNablas' is empty.
+
+Note [The MatchId for error reporting]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Something sometihng, when we're talking about MatchIds that might occur in
+Nablas (rather than just in a Nabla), we have to refer to them by Id, rather
+than by e-class-id.
+
+This is because e-class-ids will vary between Nabla, but each Nabla maps Ids to e-class-ids.
+So an Id is the only identifier that identifies the same match-id across Nablas.
+
+We can safely query each Nabla for the MatchIds because we make sure to
+represent the MatchIds in the Nablas as soon as possible (in pmcMatches and
+friends)
+
-}
=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -1,4 +1,5 @@
+{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
@@ -103,22 +104,18 @@ emptyRedSets :: RedSets
emptyRedSets = RedSets mempty mempty mempty
checkGrd :: PmGrd -> CheckAction RedSets
-checkGrd grd = CA $ \inc0 -> case grd of
+checkGrd grd = CA $ \inc -> case grd of
-- let x = e: Refine with x ~ e
- PmLet x0 e -> do
- let (x, inc) = representId x0 inc0
- -- romes: we could potentially do update the trees to use e-class ids here,
- -- or in pmcMatches
- matched <- addPhiCtNablas inc (PhiCoreCt x e)
+ PmLet x e -> do
+ matched <- addPhiCtNablasWithRep inc x (`PhiCoreCt` e)
tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
, cr_uncov = mempty
, cr_approx = Precise }
-- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
- PmBang x0 mb_info -> do
- let (x, inc) = representId x0 inc0
- div <- addPhiCtNablas inc (PhiBotCt x)
- matched <- addPhiCtNablas inc (PhiNotBotCt x)
+ PmBang x mb_info -> do
+ div <- addPhiCtNablasWithRep inc x PhiBotCt
+ matched <- addPhiCtNablasWithRep inc x PhiNotBotCt -- it will do a redundant lookup to represent x again... we would like @inc@ to have the rep already for both
-- See Note [Dead bang patterns]
-- mb_info = Just info <==> PmBang originates from bang pattern in source
let bangs | Just info <- mb_info = unitOL (div, info)
@@ -135,14 +132,13 @@ checkGrd grd = CA $ \inc0 -> case grd of
, cr_uncov = mempty
, cr_approx = Precise }
-- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
- PmCon x0 con tvs dicts args0 -> do
- let (x, inc1) = representId x0 inc0
- (args, inc) = representIds args0 inc1
+ PmCon x con tvs dicts args -> do
+ -- romes: for now we do the redundant representation of vars, but whatever
!div <- if isPmAltConMatchStrict con
- then addPhiCtNablas inc (PhiBotCt x)
+ then addPhiCtNablasWithRep inc x PhiBotCt
else pure mempty
- !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
- !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
+ !matched <- addPhiCtNablasWithReps inc (x:args) (\case (xi:argsi) -> PhiConCt xi con tvs (map evVarPred dicts) argsi; _ -> error "impossible")
+ !uncov <- addPhiCtNablasWithRep inc x (`PhiNotConCt` con)
tracePm "check:Con" $ vcat
[ ppr grd
, ppr inc
@@ -185,8 +181,7 @@ checkGRHS (PmGRHS { pg_grds = GrdVec grds, pg_rhs = rhs_info }) =
checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
-- See Note [Checking EmptyCase]
checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
- let (varid, inc') = representId var inc
- unc <- addPhiCtNablas inc' (PhiNotBotCt varid)
+ unc <- addPhiCtNablasWithRep inc var PhiNotBotCt
pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -29,6 +29,9 @@ module GHC.HsToCore.Pmc.Solver (
PhiCt(..), PhiCts,
addPhiCtNablas,
addPhiCtsNablas,
+ addPhiCtNablasWithRep, addPhiCtNablasWithReps,
+ liftNablasM,
+ addPhiCts,
isInhabited,
generateInhabitingPatterns, GenerateInhabitingPatternsMode(..)
@@ -121,6 +124,16 @@ addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
+-- | 'addPmCtsNablas' for a single 'PmCt', but first represent the Id in each Nabla.
+addPhiCtNablasWithRep :: Nablas -> Id -> (ClassId -> PhiCt) -> DsM Nablas
+addPhiCtNablasWithRep nablas x ctf
+ = liftNablasM (\d -> let (xi, d') = representId x d in addPhiCts d' (unitBag (ctf xi))) nablas
+
+-- | Represent all Id in each Nabla.
+addPhiCtNablasWithReps :: Nablas -> [Id] -> ([ClassId] -> PhiCt) -> DsM Nablas
+addPhiCtNablasWithReps nablas xs ctf
+ = liftNablasM (\d -> let (xsi, d') = representIds xs d in addPhiCts d' (unitBag (ctf xsi))) nablas
+
liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds)
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,3 +1,4 @@
+{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}
@@ -21,7 +22,10 @@ module GHC.HsToCore.Pmc.Solver.Types (
lookupRefuts, lookupSolution,
-- ** Looking up 'VarInfo'
- lookupVarInfo, lookupVarInfoNT, trvVarInfo, emptyVarInfo, representId, representIds, representIdNablas, representIdsNablas,
+ lookupVarInfo, lookupVarInfoNT, trvVarInfo, emptyVarInfo,
+
+ representId, representIds, representIdNablas, representIdsNablas,
+ lookupMatchIdMap,
-- ** Caching residual COMPLETE sets
CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
@@ -88,7 +92,7 @@ import Data.Equality.Graph.Lens
import qualified Data.Equality.Graph as EG
import Data.IntSet (IntSet)
import qualified Data.IntSet as IS (empty)
-import Data.Bifunctor (second, bimap, first)
+import Data.Bifunctor (second)
import Control.Monad.Trans.State (runState, state, execState)
-- import GHC.Driver.Ppr
@@ -166,6 +170,9 @@ data TmState
-- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
}
+lookupMatchIdMap :: Id -> Nabla -> Maybe ClassId
+lookupMatchIdMap id (MkNabla _ TmSt{ts_reps}) = lookupVarEnv ts_reps id
+
-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
-- and negative ('vi_neg') facts, like "x is not (:)".
-- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
@@ -243,6 +250,9 @@ instance Outputable BotInfo where
ppr IsBot = text "~⊥"
ppr IsNotBot = text "≁⊥"
+instance Outputable IntSet where
+ ppr = text . show
+
-- | Not user-facing.
instance Outputable TmState where
ppr (TmSt eg idmp dirty) = text (show eg) $$ ppr idmp $$ ppr dirty
@@ -843,6 +853,7 @@ representIdNablas x (MkNablas nbs) = MkNablas $ mapBag (snd . representId x) nbs
representIdsNablas :: [Id] -> Nablas -> Nablas
representIdsNablas xs = execState (mapM (\x -> state (((),) . representIdNablas x)) xs)
+-- Are these even used? don't we always use the ones above?
-- | Like 'representId' but for a single Nabla
representId :: Id -> Nabla -> (ClassId, Nabla)
representId x (MkNabla tyst tmst at TmSt{ts_facts=eg0, ts_reps=idmp})
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ebacbf5c1bfb47ba4dcf222626cb1b2c41867edc
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ebacbf5c1bfb47ba4dcf222626cb1b2c41867edc
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/20230713/15fe7df3/attachment-0001.html>
More information about the ghc-commits
mailing list