[Git][ghc/ghc][wip/romes/eqsat-pmc] Fix to representId over multiple (different) nablas

[Rodrigo Mesquita (@alt-romes)]

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


Commits:
11153cf5 by Rodrigo Mesquita at 2023-07-06T12:18:45+01:00
Fix to representId over multiple (different) nablas

- - - - -


2 changed files:

- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- libraries/hegg


Changes:

=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -79,8 +79,6 @@ import Data.Ratio
 import GHC.Real (Ratio(..))
 import qualified Data.Semigroup as Semi
 
-import Data.Tuple (swap)
-import Data.Traversable (mapAccumL)
 import Data.Functor.Compose
 import Data.Equality.Analysis (Analysis(..))
 import Data.Equality.Graph (EGraph, ClassId)
@@ -88,8 +86,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, bimap)
+import Data.Bifunctor (second)
 import Control.Monad.Trans.State (runState, state)
+import Data.List (sortOn)
+import Data.Ord (Down(..))
 
 -- import GHC.Driver.Ppr
 
@@ -835,15 +835,23 @@ instance Show VarInfo where
   show = showPprUnsafe . ppr
 
 representId :: Id -> Nablas -> (ClassId, Nablas)
--- Will need to justify this well
--- ROMES:TODO: The headMaybe is wrong, because the nablas are not exactly the
--- same, and the match-id in one might not be the same match-id in the other,
--- weirdly. I suppose that if we do it earlier, we can make all the nablas
--- share the same match-ids.
-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})
+-- 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] -> Nablas -> ([ClassId], Nablas)
 representIds xs = runState (mapM (state . representId) xs)


=====================================
libraries/hegg
=====================================
@@ -1 +1 @@
-Subproject commit 238557096a773b8cbe70d141ed63aef302918a62
+Subproject commit f2cb5d7671f9135340fd2bd782f08614c34bceeb



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/11153cf5f91456df835c87b5fadb4d577751d82a

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/11153cf5f91456df835c87b5fadb4d577751d82a
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/400e79f1/attachment-0001.html>