[Git][ghc/ghc][wip/romes/eqsat-pmc] Improve a little bit the mixing of Ids and ClassIds
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Sun Jul 2 17:45:57 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
aebda191 by Rodrigo Mesquita at 2023-07-02T18:45:45+01:00
Improve a little bit the mixing of Ids and ClassIds
- - - - -
8 changed files:
- 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
Changes:
=====================================
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,10 @@ 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))
+ let (varid, cr_uncov') = representId var (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 ReportPatBind ctxt [varid] result0{cr_uncov = cr_uncov'}
pmcPatBind _ _ _ = pure ()
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -165,18 +168,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 +345,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 +353,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 +392,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 +433,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,9 @@ 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
+ let (args, inc) = representIds args0 inc1
!div <- if isPmAltConMatchStrict con
then addPhiCtNablas inc (PhiBotCt x)
else pure mempty
@@ -181,7 +185,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
=====================================
@@ -328,6 +328,11 @@ desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
-- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
--
-- Returns a desugared guard tree of guard expressions.
+--
+-- 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,5 +1,6 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
@@ -105,8 +106,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 +570,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]
+ | 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 +673,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 (PhiCoreCt x e) = addCoreCt nabla x e
addPhiTmCt nabla (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
-- 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
@@ -900,6 +893,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 +918,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 +954,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 +1473,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 +1496,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 +1558,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 +1580,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 +1608,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 +2027,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 +2042,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 +2145,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,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)
+import Data.Bifunctor (second, bimap)
-- import GHC.Driver.Ppr
@@ -318,7 +318,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 +833,15 @@ type TmEGraph = EGraph VarInfo (DeBruijnF CoreExprF)
instance Show VarInfo where
show = showPprUnsafe . ppr
-representId :: Id -> Nabla -> (ClassId, Nabla)
+representId :: Id -> Nablas -> (ClassId, Nablas)
-- 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 x (MkNablas nbs) = bimap (fromJust . headMaybe) MkNablas $ unzipBag $ mapBag go nbs 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 nablas = swap $ mapAccumL (\acc x -> swap $ representId x acc) nablas xs
-- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
-- There ought to be a better way.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/aebda191e9aa022eaabfde2ea6e18b7a524c7c2d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/aebda191e9aa022eaabfde2ea6e18b7a524c7c2d
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/20230702/95351034/attachment-0001.html>
More information about the ghc-commits
mailing list