[Git][ghc/ghc][wip/romes/eqsat-pmc] More comments
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Fri Oct 20 10:09:39 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
e175adb7 by Rodrigo Mesquita at 2023-10-20T12:09:31+02:00
More comments
- - - - -
2 changed files:
- compiler/GHC/Core/Equality.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
Changes:
=====================================
compiler/GHC/Core/Equality.hs
=====================================
@@ -136,28 +136,30 @@ representCoreExprEgr expr egr = EGM.runEGraphMT egr (runReaderT (go expr) emptyC
addE :: Analysis m a CoreExprF => CoreExprF ClassId -> ReaderT CmEnv (EGM.EGraphMT a CoreExprF m) ClassId
addE e = lift $ EGM.addM $ Node e
+{-# INLINEABLE representCoreExprEgr #-}
type CoreExprF = ExprF
type CoreAltF = AltF
type CoreBindF = BindF
-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 _)
- = case compare lid rid of
- LT -> LT
- EQ -> case compare (D env1 lids) (D env2 rids) of
- LT -> LT
- EQ -> compare lext rext
- GT -> GT
- GT -> GT
- go l r = compare l r
+-- 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 _)
+-- = case compare lid rid of
+-- LT -> LT
+-- EQ -> case compare (D env1 lids) (D env2 rids) of
+-- LT -> LT
+-- EQ -> compare lext rext
+-- GT -> GT
+-- GT -> GT
+-- go l r = compare l r
cmpDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Ordering
cmpDeBruijnType d1@(D _ t1) d2@(D _ t2)
= if eqDeBruijnType d1 d2
then EQ
-- ROMES:TODO: This definitely does not look OK.
+ -- ROMES:TODO: This hurts performance a lot (50% of regression is basically this)
else compare (showPprUnsafe t1) (showPprUnsafe t2)
cmpDeBruijnCoercion :: DeBruijn Coercion -> DeBruijn Coercion -> Ordering
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -586,6 +586,18 @@ where you can find the solution in a perhaps more digestible format.
-- | A high-level pattern-match constraint. Corresponds to φ from Figure 3 of
-- the LYG paper.
-- Additionally, we use class-ids instead of ids (note... TODO)
+-- ROMES:TODO:
+-- Actually, I now think that we should only use e-class Ids within this module? and PhiCt should used Ids.
+-- The reasoning is that we only represent Ids and merge them to their RHS
+-- That sounds like the cleanest design, and we might even be able to rid other
+-- modules of thinking about e-class Ids and just use them for our
+-- representation of normalised refinement types
+-- Even though other modules are aware of Nablas, which means somehow they will
+-- have to know a bit about ClassIds, but we could also just refactor what we
+-- used to have (in terms of lookupId) to lookup the id through representing
+-- it, which is probably not that expensive. Eventually, if it is in fact
+-- expensive, we can try again talking about ClassIds more often. But I dislike
+-- how that breaks the illusion now.
data PhiCt
= PhiTyCt !PredType
-- ^ A type constraint "T ~ U".
@@ -707,6 +719,7 @@ addPhiTmCt nabla (PhiNotConCt x con) = addNotConCt nabla x con
addPhiTmCt nabla (PhiBotCt x) = addBotCt nabla x
addPhiTmCt nabla (PhiNotBotCt x) = addNotBotCt nabla x
+-- ROMES:TODO: For example this one would be trivial if we still had Ids at this level...
filterUnliftedFields :: Nabla -> PmAltCon -> [ClassId] -> [ClassId]
filterUnliftedFields nabla con args =
[ arg_id | (arg_id, bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con)
@@ -739,7 +752,7 @@ mergeBotCt vi at VI { vi_bot = bot }
addNotBotCt :: Nabla -> ClassId -> MaybeT DsM Nabla
addNotBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts=env} } x = do
-- This means we only add not-bottom constraints to the true match-id of newtype constructors (ie skipping NT classes)
- -- This is the only occurrence of lookupVarInfoNT.
+ -- This is the only occurrence of lookupVarInfoNT.(nope)
let (yid, vi at VI { vi_bot = bot }) = lookupVarInfoNT ts x
case bot of
IsBot -> mzero -- There was x ~ ⊥. Contradiction!
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e175adb789ce41806083731b1d6cd7f4affa06a2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e175adb789ce41806083731b1d6cd7f4affa06a2
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/20231020/8ca495b0/attachment-0001.html>
More information about the ghc-commits
mailing list