[Git][ghc/ghc][wip/romes/eqsat-pmc] Paper over

Rodrigo Mesquita (@alt-romes) gitlab at gitlab.haskell.org
Thu Jul 6 12:40:04 UTC 2023



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


Commits:
8a397ff9 by Rodrigo Mesquita at 2023-07-06T13:39:53+01:00
Paper over

- - - - -


4 changed files:

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


Changes:

=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -76,6 +76,7 @@ import qualified Data.List.NonEmpty as NE
 import Data.Coerce
 
 import Data.Equality.Graph (ClassId)
+import Data.Maybe (maybeToList)
 
 --
 -- * Exported entry points to the checker
@@ -119,7 +120,7 @@ pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
   -- empty-eclasses, the representId on the next line wouldn't match the match
   -- ids we defined in checkPatBind.
   let (varid, cr_uncov') = representId var (cr_uncov result0)
-  formatReportWarnings ReportPatBind ctxt [varid] result0{cr_uncov = cr_uncov'}
+  formatReportWarnings ReportPatBind ctxt (maybeToList varid) result0{cr_uncov = cr_uncov'}
 pmcPatBind _ _ _ = pure ()
 
 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -189,7 +190,10 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
       result0 <- {-# SCC "checkMatchGroup" #-}
                  unCA (checkMatchGroup matches) 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
+      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 variable already "represented"
+      -- in the e-graph
       {-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt varids result0{cr_uncov=cr_uncov'}
       return (NE.toList (ldiMatchGroup (cr_ret result0)))
 
@@ -445,8 +449,10 @@ addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a
 addCoreScrutTmCs []         _      k = k
 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))
+    let (mvarid, nablas) = representId x0 nablas0
+     in case mvarid of
+          Nothing -> return nablas0 -- return the empty nablas unchanged
+          Just x  -> 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
=====================================
@@ -106,27 +106,32 @@ checkGrd :: PmGrd -> CheckAction RedSets
 checkGrd grd = CA $ \inc0 -> case grd of
   -- let x = e: Refine with x ~ e
   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)
-    tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
-    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
-                     , cr_uncov = mempty
-                     , cr_approx = Precise }
+    -- It'd be better to do this earlier even, maybe
+    let (mx, inc) = representId x0 inc0
+    case mx of
+      Nothing -> emptyCheckResult
+      Just x -> do
+        matched <- addPhiCtNablas inc (PhiCoreCt x e)
+        tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
+        pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
+                         , cr_uncov = mempty
+                         , cr_approx = Precise }
   -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
   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]
-    -- mb_info = Just info <==> PmBang originates from bang pattern in source
-    let bangs | Just info <- mb_info = unitOL (div, info)
-              | otherwise            = NilOL
-    tracePm "check:Bang" (ppr x <+> ppr div)
-    pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
-                     , cr_uncov = mempty
-                     , cr_approx = Precise }
+    let (mx, inc) = representId x0 inc0
+    case mx of
+      Nothing -> emptyCheckResult
+      Just x -> do
+        div <- addPhiCtNablas inc (PhiBotCt x)
+        matched <- addPhiCtNablas inc (PhiNotBotCt x)
+        -- See Note [Dead bang patterns]
+        -- mb_info = Just info <==> PmBang originates from bang pattern in source
+        let bangs | Just info <- mb_info = unitOL (div, info)
+                  | otherwise            = NilOL
+        tracePm "check:Bang" (ppr x <+> ppr div)
+        pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
+                         , cr_uncov = mempty
+                         , cr_approx = Precise }
   -- See point (3) of Note [considerAccessible]
   PmCon x (PmAltConLike con) _ _ _
     | x `hasKey` considerAccessibleIdKey
@@ -136,24 +141,32 @@ checkGrd grd = CA $ \inc0 -> case grd of
                         , cr_approx = Precise }
   -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
   PmCon x0 con tvs dicts args0 -> do
-    let (x, inc1) = representId x0 inc0
+    let (mx, inc1) = representId x0 inc0
         (args, inc) = representIds args0 inc1
-    pprTraceM "PmCon" (ppr inc $$ text "args:" <+> ppr args)
-    !div <- if isPmAltConMatchStrict con
-      then addPhiCtNablas inc (PhiBotCt x)
-      else pure mempty
-    !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
-    !uncov   <- addPhiCtNablas inc (PhiNotConCt x con)
-    tracePm "check:Con" $ vcat
-      [ ppr grd
-      , ppr inc
-      , hang (text "div") 2 (ppr div)
-      , hang (text "matched") 2 (ppr matched)
-      , hang (text "uncov") 2 (ppr uncov)
-      ]
-    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
-                     , cr_uncov = uncov
-                     , cr_approx = Precise }
+    case mx of
+      Nothing -> emptyCheckResult
+      Just x -> do
+        pprTraceM "PmCon" (ppr inc $$ text "args:" <+> ppr args)
+        !div <- if isPmAltConMatchStrict con
+          then addPhiCtNablas inc (PhiBotCt x)
+          else pure mempty
+        !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
+        !uncov   <- addPhiCtNablas inc (PhiNotConCt x con)
+        tracePm "check:Con" $ vcat
+          [ ppr grd
+          , ppr inc
+          , hang (text "div") 2 (ppr div)
+          , hang (text "matched") 2 (ppr matched)
+          , hang (text "uncov") 2 (ppr uncov)
+          ]
+        pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
+                         , cr_uncov = uncov
+                         , cr_approx = Precise }
+  where
+    -- We return this when we know the nablas are empty
+    emptyCheckResult = pure CheckResult { cr_ret = emptyRedSets
+                                        , cr_uncov = mempty
+                                        , cr_approx = Precise }
 
 checkGrds :: [PmGrd] -> CheckAction RedSets
 checkGrds [] = CA $ \inc ->
@@ -186,9 +199,12 @@ 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
-  let (varid, inc') = representId var inc
-  unc <- addPhiCtNablas inc' (PhiNotBotCt varid)
-  pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
+  let (mvarid, inc') = representId var inc
+  case mvarid of
+    Nothing -> pure (CheckResult pe mempty Precise)
+    Just varid -> do
+      unc <- addPhiCtNablas inc' (PhiNotBotCt varid)
+      pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
 
 checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
 checkPatBind = coerce checkGRHS


=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE MagicHash           #-}
 {-# LANGUAGE RankNTypes   #-}
 {-# LANGUAGE TypeApplications   #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -84,12 +85,15 @@ import Data.Equality.Analysis (Analysis(..))
 import Data.Equality.Graph (EGraph, ClassId)
 import Data.Equality.Graph.Lens
 import qualified Data.Equality.Graph as EG
+import qualified Data.Equality.Graph.Internal as EG
+import qualified Data.Equality.Graph.ReprUnionFind as EG
 import Data.IntSet (IntSet)
 import qualified Data.IntSet as IS (empty)
 import Data.Bifunctor (second)
 import Control.Monad.Trans.State (runState, state)
 import Data.List (sortOn)
 import Data.Ord (Down(..))
+import GHC.Int (Int(..))
 
 -- import GHC.Driver.Ppr
 
@@ -834,27 +838,35 @@ type TmEGraph = EGraph VarInfo (DeBruijnF CoreExprF)
 instance Show VarInfo where
   show = showPprUnsafe . ppr
 
-representId :: Id -> Nablas -> (ClassId, Nablas)
+
+-- I think the right thing to do here is have representId always return a ClassId, or panic
+-- and have an additional method which is called by representIds...
+--
+-- | Represents a match-id in 'Nablas' and returns the match-id in terms of the e-graph
+--
+-- It returns Nothing if the Nablas is empty, and hence there's no returned
+-- match-id in terms of e-graphs (there are none in which we can represent that Id)
+representId :: Id -> Nablas -> (Maybe ClassId, Nablas)
 -- 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
-          [] -> MkNablas emptyBag
-          (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)
+  = case unzip3 $ map go (bagToList nbs) of
+      (counters,ids,nablas) ->
+        case sortOn Down counters of
+          [] -> (Nothing, MkNablas nbs)
+          (max_counter:_) ->
+            let go_zip i (MkNabla tyst tmst at TmSt{ts_facts=eg0})
+                  -- The max counter + 1 will be never be an id already in these e-graphs
+                  = MkNabla tyst tmst{ts_facts=EG.newPointerToClassId (max_counter+1) i eg0}
+             in (Just max_counter, 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})
+          (xid, eg1) -> (case EG.unionFind eg0 of EG.RUF _ size# -> I# size#, xid, MkNabla tyst tmst{ts_facts=eg1})
 
 representIds :: [Id] -> Nablas -> ([ClassId], Nablas)
-representIds xs = runState (mapM (state . representId) xs)
+representIds xs = runState (catMaybes <$> mapM (state . representId) xs)
 
 -- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
 -- There ought to be a better way.


=====================================
libraries/hegg
=====================================
@@ -1 +1 @@
-Subproject commit f2cb5d7671f9135340fd2bd782f08614c34bceeb
+Subproject commit ff5fa306092c6539866d5ebffde9a3041d83444f



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8a397ff99c0be4413490954e36fe0d9ee80ebb7b

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8a397ff99c0be4413490954e36fe0d9ee80ebb7b
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/10fb3ee8/attachment-0001.html>


More information about the ghc-commits mailing list