[Git][ghc/ghc][wip/romes/eqsat-pmc] 5 commits: Drop SDFM module
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Thu Jul 6 11:17:36 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
37279f53 by Rodrigo Mesquita at 2023-07-03T10:00:29+01:00
Drop SDFM module
- - - - -
7e4cebee by Rodrigo Mesquita at 2023-07-03T10:00:29+01:00
Improve a little bit the mixing of Ids and ClassIds
tWeaks
Don't use EG.rebuild as a view pattern
- - - - -
00b4cbd2 by Rodrigo Mesquita at 2023-07-03T10:16:23+01:00
Debuggging
- - - - -
2f2f1867 by Rodrigo Mesquita at 2023-07-03T19:39:10+01:00
Touches
- - - - -
e779a752 by Rodrigo Mesquita at 2023-07-06T12:17:17+01:00
Fix to representId over multiple (different) nablas
- - - - -
14 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/Desugar.hs
- compiler/GHC/HsToCore/Pmc/Ppr.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- − compiler/GHC/Types/Unique/SDFM.hs
- compiler/ghc.cabal.in
- libraries/hegg
- testsuite/tests/count-deps/CountDepsAst.stdout
- testsuite/tests/count-deps/CountDepsParser.stdout
Changes:
=====================================
compiler/GHC/Core/Equality.hs
=====================================
@@ -7,6 +7,11 @@
module GHC.Core.Equality where
+-- ROMES:TODO:
+-- I think, for the particular usages of Core e-graphs, we can do much better
+-- than this for equality.
+-- E.g. representation could transform the CoreExpr to an actual debruijnized one (with Ints for Vars)
+
import GHC.Exts (dataToTag#, tagToEnum#, (>#), (<#))
import GHC.Prelude
=====================================
compiler/GHC/HsToCore/Errors/Ppr.hs
=====================================
@@ -72,7 +72,8 @@ instance Diagnostic DsMessage where
case vars of -- See #11245
[] -> text "Guards do not cover entire pattern space"
_ -> let us = map (\nabla -> pprUncovered nabla vars) nablas
- pp_tys = pprQuotedList $ map idType vars
+ -- pp_tys = pprQuotedList $ map idType vars
+ pp_tys = empty
in hang
(text "Patterns of type" <+> pp_tys <+> text "not matched:")
4
=====================================
compiler/GHC/HsToCore/Errors/Types.hs
=====================================
@@ -20,6 +20,8 @@ import GHC.Types.Id
import GHC.Types.Name (Name)
import qualified GHC.LanguageExtensions as LangExt
+import Data.Equality.Graph (ClassId)
+
import GHC.Generics (Generic)
newtype MinBound = MinBound Integer
@@ -99,7 +101,7 @@ data DsMessage
| DsNonExhaustivePatterns !(HsMatchContext GhcRn)
!ExhaustivityCheckType
!MaxUncoveredPatterns
- [Id]
+ [ClassId]
[Nabla]
| DsTopLevelBindsNotAllowed !BindsType !(HsBindLR GhcTc GhcTc)
=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -75,6 +75,8 @@ import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Data.Coerce
+import Data.Equality.Graph (ClassId)
+
--
-- * Exported entry points to the checker
--
@@ -104,9 +106,20 @@ pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
!missing <- getLdiNablas
pat_bind <- noCheckDs $ desugarPatBind loc var p
tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
- result <- unCA (checkPatBind pat_bind) missing
- tracePm "}: " (ppr (cr_uncov result))
- formatReportWarnings ReportPatBind ctxt [var] result
+ 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'}
pmcPatBind _ _ _ = pure ()
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -165,18 +178,20 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
-- This must be an -XEmptyCase. See Note [Checking EmptyCase]
let var = only vars
empty_case <- noCheckDs $ desugarEmptyCase var
- result <- unCA (checkEmptyCase empty_case) missing
- tracePm "}: " (ppr (cr_uncov result))
- formatReportWarnings ReportEmptyCase ctxt vars result
+ 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'}
return []
Just matches -> do
matches <- {-# SCC "desugarMatches" #-}
noCheckDs $ desugarMatches vars matches
- result <- {-# SCC "checkMatchGroup" #-}
+ result0 <- {-# 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)))
+ 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)))
{- Note [pmcPatBind only checks PatBindRhs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -340,7 +355,7 @@ collectInMode ReportEmptyCase = cirbsEmptyCase
-- | Given a 'FormatReportWarningsMode', this function will emit warnings
-- for a 'CheckResult'.
-formatReportWarnings :: FormatReportWarningsMode ann -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
+formatReportWarnings :: FormatReportWarningsMode ann -> DsMatchContext -> [ClassId] -> CheckResult ann -> DsM ()
formatReportWarnings report_mode ctx vars cr at CheckResult { cr_ret = ann } = do
cov_info <- collectInMode report_mode ann
dflags <- getDynFlags
@@ -348,7 +363,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 -> [Id] -> CheckResult CIRB -> DsM ()
+reportWarnings :: DynFlags -> FormatReportWarningsMode ann -> DsMatchContext -> [ClassId] -> CheckResult CIRB -> DsM ()
reportWarnings dflags report_mode (DsMatchContext kind loc) vars
CheckResult { cr_ret = CIRB { cirb_inacc = inaccessible_rhss
, cirb_red = redundant_rhss
@@ -387,14 +402,13 @@ reportWarnings dflags report_mode (DsMatchContext kind loc) vars
maxPatterns = maxUncoveredPatterns dflags
-getNFirstUncovered :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nablas -> DsM [Nabla]
+getNFirstUncovered :: GenerateInhabitingPatternsMode -> [ClassId] -> 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
- let (vars', nabla') = representIds vars nabla -- they're already there, we're just getting the e-class ids back
- front <- generateInhabitingPatterns mode vars' n nabla'
+ front <- generateInhabitingPatterns mode vars n nabla
back <- go (n - length front) nablas
pure (front ++ back)
@@ -429,9 +443,10 @@ addTyCs origin ev_vars m = do
-- to be added for multiple scrutinees rather than just one.
addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs [] _ k = k
-addCoreScrutTmCs (scr:scrs) (x:xs) k =
- flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas ->
- addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
+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))
addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: numbers of scrutinees and match ids differ"
-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.
=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -103,9 +103,10 @@ emptyRedSets :: RedSets
emptyRedSets = RedSets mempty mempty mempty
checkGrd :: PmGrd -> CheckAction RedSets
-checkGrd grd = CA $ \inc -> case grd of
+checkGrd grd = CA $ \inc0 -> case grd of
-- let x = e: Refine with x ~ e
- PmLet x e -> do
+ 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)
@@ -114,7 +115,8 @@ checkGrd grd = CA $ \inc -> case grd of
, cr_uncov = mempty
, cr_approx = Precise }
-- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
- PmBang x mb_info -> do
+ PmBang x0 mb_info -> do
+ let (x, inc) = representId x0 inc0
div <- addPhiCtNablas inc (PhiBotCt x)
matched <- addPhiCtNablas inc (PhiNotBotCt x)
-- See Note [Dead bang patterns]
@@ -133,7 +135,10 @@ checkGrd grd = CA $ \inc -> 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 x con tvs dicts args -> do
+ PmCon x0 con tvs dicts args0 -> do
+ let (x, inc1) = representId x0 inc0
+ (args, inc) = representIds args0 inc1
+ pprTraceM "PmCon" (ppr inc $$ text "args:" <+> ppr args)
!div <- if isPmAltConMatchStrict con
then addPhiCtNablas inc (PhiBotCt x)
else pure mempty
@@ -181,7 +186,8 @@ 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
- unc <- addPhiCtNablas inc (PhiNotBotCt var)
+ let (varid, inc') = representId var inc
+ unc <- addPhiCtNablas inc' (PhiNotBotCt varid)
pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
=====================================
compiler/GHC/HsToCore/Pmc/Desugar.hs
=====================================
@@ -327,7 +327,14 @@ desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
-- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
--
--- Returns a desugared guard tree of guard expressions.
+-- TODO: Would this be a good design?
+-- Returns a desugared guard tree of guard expressions /and/ an e-graph e-graph
+-- per tree branch.
+--
+-- These e-graphs have an equivalence class for each match-id in the guard
+-- expression, and are required in the subsequent passes of the PMC
+--
+-- Furthermore, the match-ids in the PmGrd expressions are e-class ids from said e-graph
desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
-> DsM (PmMatchGroup Pre)
desugarMatches vars matches =
=====================================
compiler/GHC/HsToCore/Pmc/Ppr.hs
=====================================
@@ -12,7 +12,6 @@ import GHC.Prelude
import GHC.Data.List.Infinite (Infinite (..))
import qualified GHC.Data.List.Infinite as Inf
import GHC.Types.Basic
-import GHC.Types.Id
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Builtin.Types
@@ -42,7 +41,7 @@ import qualified Data.IntMap as IM
--
-- When the set of refutable shapes contains more than 3 elements, the
-- additional elements are indicated by "...".
-pprUncovered :: Nabla -> [Id] -> SDoc
+pprUncovered :: Nabla -> [ClassId] -> SDoc
pprUncovered nabla vas
| IM.null refuts = fsep vec -- there are no refutations
| otherwise = hang (fsep vec) 4 $
@@ -53,10 +52,9 @@ pprUncovered nabla vas
-- precedence
| [_] <- vas = topPrec
| otherwise = appPrec
- (vas',nabla') = representIds vas nabla
- ppr_action = mapM (pprPmVar init_prec) vas'
- (vec, renamings) = runPmPpr nabla' ppr_action
- refuts = prettifyRefuts nabla' renamings
+ ppr_action = mapM (pprPmVar init_prec) vas
+ (vec, renamings) = runPmPpr nabla ppr_action
+ refuts = prettifyRefuts nabla renamings
-- | Output refutable shapes of a variable in the form of @var is not one of {2,
-- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -1,7 +1,9 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RankNTypes, GADTs #-}
{-
Authors: George Karachalias <george.karachalias at cs.kuleuven.be>
@@ -105,8 +107,6 @@ import qualified Data.Equality.Graph as EG
import Data.Bifunctor (second)
import Data.Function ((&))
import qualified Data.IntSet as IS
-import Data.Tuple (swap)
-import Data.Traversable (mapAccumL)
--
-- * Main exports
@@ -571,20 +571,20 @@ where you can find the solution in a perhaps more digestible format.
data PhiCt
= PhiTyCt !PredType
-- ^ A type constraint "T ~ U".
- | PhiCoreCt !Id !CoreExpr
+ | PhiCoreCt !ClassId !CoreExpr
-- ^ @PhiCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e at .
- | PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id]
+ | HasCallStack => PhiConCt !ClassId !PmAltCon ![TyVar] ![PredType] ![ClassId]
-- ^ @PhiConCt x K tvs dicts ys@ encodes @K \@tvs dicts ys <- x@, matching @x@
-- against the 'PmAltCon' application @K \@tvs dicts ys@, binding @tvs@,
-- @dicts@ and possibly unlifted fields @ys@ in the process.
-- See Note [Strict fields and variables of unlifted type].
- | PhiNotConCt !Id !PmAltCon
+ | PhiNotConCt !ClassId !PmAltCon
-- ^ @PhiNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed
-- by @K at .
- | PhiBotCt !Id
+ | PhiBotCt !ClassId
-- ^ @PhiBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
-- by @K at .
- | PhiNotBotCt !Id
+ | PhiNotBotCt !ClassId
-- ^ @PhiNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥.
instance Outputable PhiCt where
@@ -674,31 +674,25 @@ nameTyCt pred_ty = do
-- 'addTyCts' before, through 'addPhiCts'.
addPhiTmCt :: Nabla -> PhiCt -> MaybeT DsM Nabla
addPhiTmCt _ (PhiTyCt ct) = pprPanic "addPhiCt:TyCt" (ppr ct) -- See the precondition
-addPhiTmCt nabla (PhiCoreCt x e) = let (xid, nabla') = representId x nabla
- in addCoreCt nabla' xid e
-addPhiTmCt nabla (PhiConCt x con tvs dicts args) = do
+addPhiTmCt nabla (PhiCoreCt x e) = addCoreCt nabla x e
+addPhiTmCt nabla0 (PhiConCt x con tvs dicts args) = do
-- Case (1) of Note [Strict fields and variables of unlifted type]
-- PhiConCt correspond to the higher-level φ constraints from the paper with
-- bindings semantics. It disperses into lower-level δ constraints that the
-- 'add*Ct' functions correspond to.
- nabla1 <- addTyCts nabla (listToBag dicts)
- let (xid, nabla2) = representId x nabla1
- let (args_ids, nabla3) = representIds args nabla2
+ nabla1 <- addTyCts nabla0 (listToBag dicts)
-- romes: here we could have something like (merge (add K arg_ids) x)
-- or actually that should be done by addConCt?
- nabla4 <- addConCt nabla3 xid con tvs args_ids
- foldlM addNotBotCt nabla4 (filterUnliftedFields con (zip args_ids args))
-addPhiTmCt nabla (PhiNotConCt x con) = let (xid, nabla') = representId x nabla
- in addNotConCt nabla' xid con
-addPhiTmCt nabla (PhiBotCt x) = let (xid, nabla') = representId x nabla
- in addBotCt nabla' xid
-addPhiTmCt nabla (PhiNotBotCt x) = let (xid, nabla') = representId x nabla
- in addNotBotCt nabla' xid
-
-filterUnliftedFields :: PmAltCon -> [(ClassId,Id)] -> [ClassId]
-filterUnliftedFields con args =
- [ arg_id | ((arg_id,arg), bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con)
- , isBanged bang || definitelyUnliftedType (idType arg) ]
+ nabla2 <- addConCt nabla1 x con tvs args
+ foldlM addNotBotCt nabla2 (filterUnliftedFields nabla2 con args)
+addPhiTmCt nabla (PhiNotConCt x con) = addNotConCt nabla x con
+addPhiTmCt nabla (PhiBotCt x) = addBotCt nabla x
+addPhiTmCt nabla (PhiNotBotCt x) = addNotBotCt nabla x
+
+filterUnliftedFields :: Nabla -> PmAltCon -> [ClassId] -> [ClassId]
+filterUnliftedFields nabla con args =
+ [ arg_id | (arg_id, bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con)
+ , isBanged bang || definitelyUnliftedType (eclassType arg_id nabla) ]
-- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@
-- surely diverges. Quite similar to 'addConCt', only that it only cares about
@@ -788,7 +782,7 @@ hasRequiredTheta _ = False
-- have on @x@, reject (@Nothing@) otherwise.
--
-- See Note [TmState invariants].
-addConCt :: Nabla -> ClassId -> PmAltCon -> [TyVar] -> [ClassId] -> MaybeT DsM Nabla
+addConCt :: HasCallStack => Nabla -> ClassId -> PmAltCon -> [TyVar] -> [ClassId] -> MaybeT DsM Nabla
addConCt nabla at MkNabla{ nabla_tm_st = ts } x alt tvs args = do
-- ROMES:TODO: Also looks like a function on varinfo (adjust)
let vi@(VI _ pos neg bot _) = lookupVarInfo ts x
@@ -838,14 +832,14 @@ equateTys ts us =
-- @nabla@ has integrated the knowledge from the equality constraint.
--
-- See Note [TmState invariants].
-addVarCt :: Nabla -> ClassId -> ClassId -> MaybeT DsM Nabla
+addVarCt :: HasCallStack => Nabla -> ClassId -> ClassId -> MaybeT DsM Nabla
-- This is where equality-graphs really come into play.
addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- ROMES:TODO: equate auxiliary var that finds both vars, and lookups up the domain associated. However, I think we no longer should have Just/Nothing but rather always store emptyVarInfo for new e-nodes
-- equate should also update e-graph, basically re-implement "equateUSDFM" in terms of the e-graph, or inline it or so
case equate env x y of
-- Add the constraints we had for x to y
- -- See Note [Joining e-classes PMC] todo mention from joinA
+ -- See Note (TODO) Joining e-classes PMC] todo mention from joinA
-- Now, here's a really tricky bit (TODO Write note, is it the one above?)
-- Bc the joinA operation is unlawful, and because the makeA operation for
-- expressions is also unlawful (sets the type to ()::(), mostly out of
@@ -854,7 +848,7 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- We *also update the type* (WTF1).
-- This is because every e-class should always have a match-var first, which will always have a type, and it should appear on "the left"
-- We also rebuild here, we did just merge two things. TODO: Where and when exactly should we merge?
- (vi_x, EG.rebuild -> env') -> do
+ (vi_x, env') -> do
let nabla_equated = nabla{ nabla_tm_st = ts{ts_facts = env'} }
-- and then gradually merge every positive fact we have on x into y
let add_pos nabla (PACA cl tvs args) = addConCt nabla y cl tvs args
@@ -875,7 +869,7 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- >>> equate [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 u2 == (Just ele1, [({u2,u1,u3}, Just ele2)])
equate :: TmEGraph -> ClassId -> ClassId -> (VarInfo, TmEGraph)
equate eg x y = let (_, eg') = EG.merge x y eg
- in (eg ^. _class x ._data, eg')
+ in (eg ^. _class x ._data, EG.rebuild eg')
-- Note: lookup in @eg@, not @eg'@, because we want to return x's data before the merge.
@@ -900,6 +894,7 @@ addCoreCt nabla x e = do
where
-- Takes apart a 'CoreExpr' and tries to extract as much information about
-- literals and constructor applications as possible.
+ -- ROMES:TODO: Consider CoreExprF instead of CoreExpr already here?
core_expr :: ClassId -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
-- TODO: Handle newtypes properly, by wrapping the expression in a DataCon
-- RM: Could this be done better with e-graphs? The whole newtype stuff
@@ -924,18 +919,18 @@ addCoreCt nabla x e = do
<- exprIsConApp_maybe in_scope_env e
= data_con_app x in_scope dc args
| otherwise
- = do
- nabla' <- get
- if
+ = equate_with_similar_expr x e
+ -- nabla' <- get
+ -- if
-- See Note [Detecting pattern synonym applications in expressions]
- | Var y <- e, Nothing <- isDataConId_maybe (eclassMatchId x nabla')
+ -- ROMES:TODO: Can we fix this more easily with e-graphs?
+ -- x| Var y <- e, Nothing <- isDataConId_maybe (eclassMatchId x nabla')
-- We don't consider DataCons flexible variables
- -> modifyT (\nabla -> let (yid, nabla') = representId y nabla
- in addVarCt nabla' x yid)
- | otherwise
+ -- -> modifyT (\nabla -> addVarCt nabla' x y)
+ -- x| otherwise
-- Any other expression. Try to find other uses of a semantically
-- equivalent expression and represent them by the same variable!
- -> equate_with_similar_expr x e
+ -- -> equate_with_similar_expr x e
where
expr_ty = exprType e
expr_in_scope = mkInScopeSet (exprFreeVars e)
@@ -960,10 +955,9 @@ addCoreCt nabla x e = do
bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) ClassId
bind_expr e = do
- x <- lift (lift (mkPmId (exprType e)))
- xid <- StateT $ \nabla -> pure $ representId x nabla
- core_expr xid e
- pure xid
+ x <- StateT $ \nabla -> lift (mkPmMatchId (exprType e) nabla)
+ core_expr x e
+ pure x
-- Look at @let x = K taus theta es@ and generate the following
-- constraints (assuming universals were dropped from @taus@ before):
@@ -1480,7 +1474,6 @@ instCompleteSet fuel nabla xid cs
= {-# SCC "instCompleteSet" #-} go nabla (sorted_candidates cs)
where
vi = lookupVarInfo (nabla_tm_st nabla) xid
- x = vi_id vi
sorted_candidates :: CompleteMatch -> [ConLike]
sorted_candidates cm
@@ -1504,8 +1497,8 @@ instCompleteSet fuel nabla xid cs
let recur_not_con = do
nabla' <- addNotConCt nabla xid (PmAltConLike con)
go nabla' cons
- (nabla <$ instCon fuel nabla x con) -- return the original nabla, not the
- -- refined one!
+ (nabla <$ instCon fuel nabla xid con) -- return the original nabla, not the
+ -- refined one!
<|> recur_not_con -- Assume that x can't be con. Encode that fact
-- with addNotConCt and recur.
@@ -1566,11 +1559,11 @@ compareConLikeTestability (RealDataCon a) (RealDataCon b) = mconcat
-- adding the proper constructor constraint.
--
-- See Note [Instantiating a ConLike].
-instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla
-instCon fuel nabla at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} MaybeT $ do
+instCon :: Int -> Nabla -> ClassId -> ConLike -> MaybeT DsM Nabla
+instCon fuel nabla0 at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} MaybeT $ do
let hdr what = "instCon " ++ show fuel ++ " " ++ what
env <- dsGetFamInstEnvs
- let match_ty = idType x
+ let match_ty = eclassType x nabla0
tracePm (hdr "{") $
ppr con <+> text "... <-" <+> ppr x <+> dcolon <+> ppr match_ty
norm_match_ty <- normaliseSourceTypeWHNF ty_st match_ty
@@ -1588,24 +1581,23 @@ instCon fuel nabla at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} Ma
let gammas = substTheta sigma_ex (eqSpecPreds eq_spec ++ thetas)
-- (4) Instantiate fresh term variables as arguments to the constructor
let field_tys' = substTys sigma_ex $ map scaledThing field_tys
- arg_ids <- mapM mkPmId field_tys'
- let (nabla', arg_class_ids) = mapAccumL (\nab id -> swap $ representId id nab) nabla arg_ids
+ (arg_ids, nabla1) <- runStateT (mapM (StateT @Nabla . mkPmMatchId) field_tys') nabla0
tracePm (hdr "(cts)") $ vcat
[ ppr x <+> dcolon <+> ppr match_ty
, text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
, ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
, ppr (map (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs)
, ppr gammas
- , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids)
+ , ppr (map (\x -> ppr x <+> dcolon <+> ppr (eclassType x nabla1)) arg_ids)
]
-- (5) Finally add the new constructor constraint
runMaybeT $ do
-- Case (2) of Note [Strict fields and variables of unlifted type]
let alt = PmAltConLike con
- let branching_factor = length $ filterUnliftedFields alt (zip arg_class_ids arg_ids)
+ let branching_factor = length $ filterUnliftedFields nabla1 alt arg_ids
let ct = PhiConCt x alt ex_tvs gammas arg_ids
- nabla1 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $
- addPhiTmCt nabla' ct
+ nabla2 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $
+ addPhiTmCt nabla1 ct
-- See Note [Fuel for the inhabitation test]
let new_fuel
| branching_factor <= 1 = fuel
@@ -1617,17 +1609,17 @@ instCon fuel nabla at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} Ma
, ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
, ppr (map (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs)
, ppr gammas
- , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids)
+ , ppr (map (\x -> ppr x <+> dcolon <+> ppr (eclassType x nabla1)) arg_ids)
, ppr branching_factor
, ppr new_fuel
]
- nabla2 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla1) $
- inhabitationTest new_fuel (nabla_ty_st nabla') nabla1
- lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla2)
- pure nabla2
+ nabla3 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla2) $
+ inhabitationTest new_fuel (nabla_ty_st nabla1) nabla2
+ lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla3)
+ pure nabla3
Nothing -> do
tracePm (hdr "(match_ty not instance of res_ty) }") empty
- pure (Just nabla) -- Matching against match_ty failed. Inhabited!
+ pure (Just nabla0) -- Matching against match_ty failed. Inhabited!
-- See Note [Instantiating a ConLike].
-- | @matchConLikeResTy _ _ ty K@ tries to match @ty@ against the result
@@ -2036,12 +2028,11 @@ generateInhabitingPatterns mode (x:xs) n nabla at MkNabla{nabla_tm_st=ts} = do
instantiate_newtype_chain :: ClassId -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (ClassId, Nabla)
instantiate_newtype_chain x nabla [] = pure (x, nabla)
instantiate_newtype_chain x nabla ((_ty, dc, arg_ty):dcs) = do
- y <- lift $ mkPmId arg_ty
- let (yid,nabla') = representId y nabla
+ (y,nabla') <- lift $ mkPmMatchId arg_ty nabla
-- Newtypes don't have existentials (yet?!), so passing an empty
-- list as ex_tvs.
- nabla'' <- addConCt nabla' x (PmAltConLike (RealDataCon dc)) [] [yid]
- instantiate_newtype_chain yid nabla'' dcs
+ nabla'' <- addConCt nabla' x (PmAltConLike (RealDataCon dc)) [] [y]
+ instantiate_newtype_chain y nabla'' dcs
instantiate_cons :: ClassId -> Type -> [ClassId] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
instantiate_cons _ _ _ _ _ [] = pure []
@@ -2052,7 +2043,7 @@ generateInhabitingPatterns mode (x:xs) n nabla at MkNabla{nabla_tm_st=ts} = do
= generateInhabitingPatterns mode xs n nabla
instantiate_cons x ty xs n nabla (cl:cls) = do
-- The following line is where we call out to the inhabitationTest!
- mb_nabla <- runMaybeT $ instCon 4 nabla (eclassMatchId x nabla) cl
+ mb_nabla <- runMaybeT $ instCon 4 nabla x cl
tracePm "instantiate_cons" (vcat [ ppr x <+> dcolon <+> ppr (eclassType x nabla)
, ppr ty
, ppr cl
@@ -2155,5 +2146,13 @@ eclassMatchId cid = vi_id . (^. _class cid . _data) . (ts_facts . nabla_tm_st)
eclassType :: ClassId -> Nabla -> Type
eclassType cid = idType . eclassMatchId cid
-
-- ROMES:TODO: When exactly to rebuild?
+
+-- | Generate a fresh class for matching, returning the class-id as the match-id
+mkPmMatchId :: Type -> Nabla -> DsM (ClassId, Nabla)
+mkPmMatchId ty (MkNabla tyst ts at TmSt{ts_facts = egr}) = do
+ x <- mkPmId ty -- romes:Todo: for now, we still use mkPmId to get an Id for emptyVarInfo, but we want to get rid of this too
+ let (xid, egr') = EG.newEClass (emptyVarInfo x) egr
+ return (xid, MkNabla tyst ts{ts_facts=egr'})
+{-# NOINLINE mkPmMatchId #-} -- We'll CPR deeply, that should be enough
+
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -88,7 +88,10 @@ 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)
+import Data.Bifunctor (second, bimap)
+import Control.Monad.Trans.State (runState, state)
+import Data.List (sortOn)
+import Data.Ord (Down(..))
-- import GHC.Driver.Ppr
@@ -318,7 +321,6 @@ emptyVarInfo x
-- | @lookupVarInfo tms x@ tells what we know about 'x'
--- romes:TODO: This will have a different type. I don't know what yet.
-- romes:TODO I don't think this is what we want any longer, more like represent Id and see if it was previously represented by some data or not?
--- romes:TodO should return VarInfo rather than Maybe VarInfo
lookupVarInfo :: TmState -> ClassId -> VarInfo
lookupVarInfo (TmSt eg _) x
-- RM: Yea, I don't like the fact that currently all e-classes are created by Ids and have an Empty Var info, yet we must call "fromMaybe" here. Not good.
@@ -834,14 +836,27 @@ type TmEGraph = EGraph VarInfo (DeBruijnF CoreExprF)
instance Show VarInfo where
show = showPprUnsafe . ppr
-representId :: Id -> Nabla -> (ClassId, Nabla)
--- Will need to justify this well
-representId x (MkNabla tyst tmst at TmSt{ts_facts=eg0})
- = case EG.add (EG.Node (DF (deBruijnize (VarF x)))) eg0 of
- (xid, eg1) -> (xid, MkNabla tyst tmst{ts_facts=eg1})
+representId :: Id -> Nablas -> (ClassId, Nablas)
+-- TODO:TOMORROW: pick the highest Id, and use newPointerToClassId on the Nablas on which the represented Id got a lower clsas Id
+--
+-- I suppose that if we do it earlier, we can make all the nablas share the exact same match-ids and avoid this complexity.
+representId x (MkNablas nbs)
+ = case unzip $ map go (bagToList nbs) of
+ (ids,nablas) ->
+ case sortOn Down ids of
+ [] -> panic "representId: impossible, there's at least one nabla"
+ (max_i:_) ->
+ let go_zip i nabla@(MkNabla tyst tmst at TmSt{ts_facts=eg0}) = if max_i > i
+ then MkNabla tyst tmst{ts_facts=EG.newPointerToClassId max_i i eg0}
+ else nabla
+ in (max_i, MkNablas $ listToBag $ zipWith go_zip ids nablas)
+ where
+ go (MkNabla tyst tmst at TmSt{ts_facts=eg0})
+ = case EG.add (EG.Node (DF (deBruijnize (VarF x)))) eg0 of
+ (xid, eg1) -> (xid, MkNabla tyst tmst{ts_facts=eg1})
-representIds :: [Id] -> Nabla -> ([ClassId], Nabla)
-representIds xs nabla = swap $ mapAccumL (\acc x -> swap $ representId x acc) nabla xs
+representIds :: [Id] -> Nablas -> ([ClassId], Nablas)
+representIds xs = runState (mapM (state . representId) xs)
-- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
-- There ought to be a better way.
=====================================
compiler/GHC/Types/Unique/SDFM.hs deleted
=====================================
@@ -1,122 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ApplicativeDo #-}
-{-# OPTIONS_GHC -Wall #-}
-
--- | Like a 'UniqDFM', but maintains equivalence classes of keys sharing the
--- same entry. See 'UniqSDFM'.
-module GHC.Types.Unique.SDFM (
- -- * Unique-keyed, /shared/, deterministic mappings
- UniqSDFM,
-
- emptyUSDFM,
- lookupUSDFM,
- equateUSDFM, addToUSDFM,
- traverseUSDFM
- ) where
-
-import GHC.Prelude
-
-import GHC.Types.Unique
-import GHC.Types.Unique.DFM
-import GHC.Utils.Outputable
-
--- | Either @Indirect x@, meaning the value is represented by that of @x@, or
--- an @Entry@ containing containing the actual value it represents.
-data Shared key ele
- = Indirect !key
- | Entry !ele
-
--- | A 'UniqDFM' whose domain is /sets/ of 'Unique's, each of which share a
--- common value of type @ele at .
--- Every such set (\"equivalence class\") has a distinct representative
--- 'Unique'. Supports merging the entries of multiple such sets in a union-find
--- like fashion.
---
--- An accurate model is that of @[(Set key, Maybe ele)]@: A finite mapping from
--- sets of @key at s to possibly absent entries @ele@, where the sets don't overlap.
--- Example:
--- @
--- m = [({u1,u3}, Just ele1), ({u2}, Just ele2), ({u4,u7}, Nothing)]
--- @
--- On this model we support the following main operations:
---
--- * @'lookupUSDFM' m u3 == Just ele1@, @'lookupUSDFM' m u4 == Nothing@,
--- @'lookupUSDFM' m u5 == Nothing at .
--- * @'equateUSDFM' m u1 u3@ is a no-op, but
--- @'equateUSDFM' m u1 u2@ merges @{u1,u3}@ and @{u2}@ to point to
--- @Just ele2@ and returns the old entry of @{u1,u3}@, @Just ele1 at .
--- * @'addToUSDFM' m u3 ele4@ sets the entry of @{u1,u3}@ to @Just ele4 at .
---
--- As well as a few means for traversal/conversion to list.
-newtype UniqSDFM key ele
- = USDFM { unUSDFM :: UniqDFM key (Shared key ele) }
-
-emptyUSDFM :: UniqSDFM key ele
-emptyUSDFM = USDFM emptyUDFM
-
-lookupReprAndEntryUSDFM :: Uniquable key => UniqSDFM key ele -> key -> (key, Maybe ele)
-lookupReprAndEntryUSDFM (USDFM env) = go
- where
- go x = case lookupUDFM env x of
- Nothing -> (x, Nothing)
- Just (Indirect y) -> go y
- Just (Entry ele) -> (x, Just ele)
-
--- | @lookupSUDFM env x@ looks up an entry for @x@, looking through all
--- 'Indirect's until it finds a shared 'Entry'.
---
--- Examples in terms of the model (see 'UniqSDFM'):
--- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 == Just ele1
--- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u4 == Nothing
--- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Nothing)] u2 == Nothing
-lookupUSDFM :: Uniquable key => UniqSDFM key ele -> key -> Maybe ele
-lookupUSDFM usdfm x = snd (lookupReprAndEntryUSDFM usdfm x)
-
--- | @equateUSDFM env x y@ makes @x@ and @y@ point to the same entry,
--- thereby merging @x@'s class with @y@'s.
--- If both @x@ and @y@ are in the domain of the map, then @y@'s entry will be
--- chosen as the new entry and @x@'s old entry will be returned.
---
--- Examples in terms of the model (see 'UniqSDFM'):
--- >>> equateUSDFM [] u1 u2 == (Nothing, [({u1,u2}, Nothing)])
--- >>> equateUSDFM [({u1,u3}, Just ele1)] u3 u4 == (Nothing, [({u1,u3,u4}, Just ele1)])
--- >>> equateUSDFM [({u1,u3}, Just ele1)] u4 u3 == (Nothing, [({u1,u3,u4}, Just ele1)])
--- >>> equateUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 u2 == (Just ele1, [({u2,u1,u3}, Just ele2)])
--- ROMES:TODO: Are all USDFM functions just for the PMC Nabla TM?
-equateUSDFM
- :: Uniquable key => UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele)
-equateUSDFM usdfm@(USDFM env) x y =
- case (lu x, lu y) of
- ((x', _) , (y', _))
- | getUnique x' == getUnique y' -> (Nothing, usdfm) -- nothing to do
- ((x', _) , (y', Nothing)) -> (Nothing, set_indirect y' x')
- ((x', mb_ex), (y', _)) -> (mb_ex, set_indirect x' y')
- where
- lu = lookupReprAndEntryUSDFM usdfm
- set_indirect a b = USDFM $ addToUDFM env a (Indirect b)
-
--- | @addToUSDFM env x a@ sets the entry @x@ is associated with to @a@,
--- thereby modifying its whole equivalence class.
---
--- Examples in terms of the model (see 'UniqSDFM'):
--- >>> addToUSDFM [] u1 ele1 == [({u1}, Just ele1)]
--- >>> addToUSDFM [({u1,u3}, Just ele1)] u3 ele2 == [({u1,u3}, Just ele2)]
-addToUSDFM :: Uniquable key => UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
-addToUSDFM usdfm@(USDFM env) x v =
- USDFM $ addToUDFM env (fst (lookupReprAndEntryUSDFM usdfm x)) (Entry v)
-
-traverseUSDFM :: forall key a b f. Applicative f => (a -> f b) -> UniqSDFM key a -> f (UniqSDFM key b)
-traverseUSDFM f = fmap (USDFM . listToUDFM_Directly) . traverse g . udfmToList . unUSDFM
- where
- g :: (Unique, Shared key a) -> f (Unique, Shared key b)
- g (u, Indirect y) = pure (u,Indirect y)
- g (u, Entry a) = do
- a' <- f a
- pure (u,Entry a')
-
-instance (Outputable key, Outputable ele) => Outputable (Shared key ele) where
- ppr (Indirect x) = ppr x
- ppr (Entry a) = ppr a
-
-instance (Outputable key, Outputable ele) => Outputable (UniqSDFM key ele) where
- ppr (USDFM env) = ppr env
=====================================
compiler/ghc.cabal.in
=====================================
@@ -818,7 +818,6 @@ Library
GHC.Types.Unique.FM
GHC.Types.Unique.Map
GHC.Types.Unique.MemoFun
- GHC.Types.Unique.SDFM
GHC.Types.Unique.Set
GHC.Types.Unique.Supply
GHC.Types.Var
=====================================
libraries/hegg
=====================================
@@ -1 +1 @@
-Subproject commit 238557096a773b8cbe70d141ed63aef302918a62
+Subproject commit f2cb5d7671f9135340fd2bd782f08614c34bceeb
=====================================
testsuite/tests/count-deps/CountDepsAst.stdout
=====================================
@@ -248,7 +248,6 @@ GHC.Types.Unique.DFM
GHC.Types.Unique.DSet
GHC.Types.Unique.FM
GHC.Types.Unique.Map
-GHC.Types.Unique.SDFM
GHC.Types.Unique.Set
GHC.Types.Unique.Supply
GHC.Types.Var
=====================================
testsuite/tests/count-deps/CountDepsParser.stdout
=====================================
@@ -255,7 +255,6 @@ GHC.Types.Unique.DFM
GHC.Types.Unique.DSet
GHC.Types.Unique.FM
GHC.Types.Unique.Map
-GHC.Types.Unique.SDFM
GHC.Types.Unique.Set
GHC.Types.Unique.Supply
GHC.Types.Var
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9d2039eecbf8e8ca071c63803640a3e32c05ee01...e779a75246e3f6dc4ecbdf79eec77fd803a1e57d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9d2039eecbf8e8ca071c63803640a3e32c05ee01...e779a75246e3f6dc4ecbdf79eec77fd803a1e57d
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/20230706/03e35cc5/attachment-0001.html>
More information about the ghc-commits
mailing list