[Git][ghc/ghc][wip/romes/eqsat-pmc] Use numbers when threading e-graph to fix a bug

[Rodrigo Mesquita (@alt-romes)]

Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC


Commits:
1f78dd7d by Rodrigo Mesquita at 2023-06-25T17:32:46+01:00
Use numbers when threading e-graph to fix a bug

- - - - -


2 changed files:

- compiler/GHC/Core/Functor.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs


Changes:

=====================================
compiler/GHC/Core/Functor.hs
=====================================
@@ -128,37 +128,39 @@ toCoreExpr :: CoreExpr -> Fix CoreExprF
 toCoreExpr = unsafeCoerce
 
 -- | Represents a DeBruijn CoreExpr being careful to correctly debruijnizie the expression as it is represented
+-- TODO: Use `Compose DeBruijn CoreExprF` instead
+-- Always represent Ids, at least for now. We're seemingly using inexistent ids
 representDBCoreExpr :: Analysis a (DeBruijnF CoreExprF)
                     => DeBruijn CoreExpr
                     -> EGraph a (DeBruijnF CoreExprF)
                     -> (ClassId, EGraph a (DeBruijnF CoreExprF))
-representDBCoreExpr (D cmenv expr) eg = case expr of
-  Var v   -> add (Node $ DF (D cmenv (VarF v)))   eg
-  Lit lit -> add (Node $ DF (D cmenv (LitF lit))) eg
-  Type t  -> add (Node $ DF (D cmenv (TypeF t)))  eg
-  Coercion c -> add (Node $ DF (D cmenv (CoercionF c))) eg
-  Cast e co  -> let (eid,eg') = representDBCoreExpr (D cmenv e) eg
-                 in add (Node $ DF (D cmenv (CastF eid co))) eg'
-  App f a -> let (fid,eg')  = representDBCoreExpr (D cmenv f) eg
-                 (aid,eg'') = representDBCoreExpr (D cmenv a) eg'
-              in add (Node $ DF (D cmenv (AppF fid aid))) eg''
-  Tick n e -> let (eid,eg') = representDBCoreExpr (D cmenv e) eg
-               in add (Node $ DF (D cmenv (TickF n eid))) eg'
-  Lam b e  -> let (eid,eg') = representDBCoreExpr (D (extendCME cmenv b) e) eg
-               in add (Node $ DF (D cmenv (LamF b eid))) eg'
-  Let (NonRec v r) e -> let (rid,eg')  = representDBCoreExpr (D cmenv r) eg
-                            (eid,eg'') = representDBCoreExpr (D (extendCME cmenv v) e) eg'
-                         in add (Node $ DF (D cmenv (LetF (NonRecF v rid) eid))) eg''
+representDBCoreExpr (D cmenv expr) eg0 = case expr of
+  Var v   -> add (Node $ DF (D cmenv (VarF v)))   eg0
+  Lit lit -> add (Node $ DF (D cmenv (LitF lit))) eg0
+  Type t  -> add (Node $ DF (D cmenv (TypeF t)))  eg0
+  Coercion c -> add (Node $ DF (D cmenv (CoercionF c))) eg0
+  Cast e co  -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
+                 in add (Node $ DF (D cmenv (CastF eid co))) eg1
+  App f a -> let (fid,eg1) = representDBCoreExpr (D cmenv f) eg0
+                 (aid,eg2) = representDBCoreExpr (D cmenv a) eg1
+              in add (Node $ DF (D cmenv (AppF fid aid))) eg2
+  Tick n e -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
+               in add (Node $ DF (D cmenv (TickF n eid))) eg1
+  Lam b e  -> let (eid,eg1) = representDBCoreExpr (D (extendCME cmenv b) e) eg0
+               in add (Node $ DF (D cmenv (LamF b eid))) eg1
+  Let (NonRec v r) e -> let (rid,eg1) = representDBCoreExpr (D cmenv r) eg0
+                            (eid,eg2) = representDBCoreExpr (D (extendCME cmenv v) e) eg1
+                         in add (Node $ DF (D cmenv (LetF (NonRecF v rid) eid))) eg2
   Let (Rec (unzip -> (bs,rs))) e ->
     let cmenv' = extendCMEs cmenv bs
-        (bsids, eg') = EGM.runEGraphM eg $
+        (bsids, eg1) = EGM.runEGraphM eg0 $
                          traverse (\r -> state $ representDBCoreExpr (D cmenv' r)) rs
-        (eid, eg'')  = representDBCoreExpr (D cmenv' e) eg'
-     in add (Node $ DF (D cmenv (LetF (RecF (zip bs bsids)) eid))) eg''
-  Case e b t as -> let (eid, eg')  = representDBCoreExpr (D cmenv e) eg
-                       (as', eg'') = EGM.runEGraphM eg' $
+        (eid, eg2)  = representDBCoreExpr (D cmenv' e) eg1
+     in add (Node $ DF (D cmenv (LetF (RecF (zip bs bsids)) eid))) eg2
+  Case e b t as -> let (eid, eg1)  = representDBCoreExpr (D cmenv e) eg0
+                       (as', eg2) = EGM.runEGraphM eg1 $
                          traverse (\(Alt cons bs a) -> state $ \s -> let (aid, g) = representDBCoreExpr (D (extendCME cmenv b) a) s in (AltF cons bs aid, g)) as
-                    in add (Node $ DF (D cmenv (CaseF eid b t as'))) eg'
+                    in add (Node $ DF (D cmenv (CaseF eid b t as'))) eg2
 
 
 -- ROMES:TODO: Instead of DeBruijnF CoreExprF we should have (ExprF (Int,Id))


=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -562,6 +562,9 @@ 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.
+-- ROMES:TODO: Ultimately, all these Ids could be replaced by e-class ids which
+-- are generated during desugaring, but there are some details to it
+-- (propagating the e-graphs in which these e-classes were created)
 data PhiCt
   = PhiTyCt !PredType
   -- ^ A type constraint "T ~ U".



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1f78dd7d207db07ffeca18e53635324f54b366c1

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1f78dd7d207db07ffeca18e53635324f54b366c1
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/20230625/f64956a6/attachment-0001.html>