[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