[Git][ghc/ghc][wip/romes/eqsat-pmc] 2 commits: Improvement to repId attempt

Rodrigo Mesquita (@alt-romes) gitlab at gitlab.haskell.org
Thu Jul 6 20:28:10 UTC 2023



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


Commits:
25f926d1 by Rodrigo Mesquita at 2023-07-06T21:27:53+01:00
Improvement to repId attempt

submodule hegg update for no reason

- - - - -
7539a46a by Rodrigo Mesquita at 2023-07-06T21:28:01+01:00
Add TODO

- - - - -


4 changed files:

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


Changes:

=====================================
TODO
=====================================
@@ -0,0 +1,12 @@
+Oh, we'll really need a "universal" Id that maps to each class-id on each nabla.
+
+* It still feels like the right thing to do is have PhiCt receive ClassIds
+instead of Ids
+    * especially because of mkPmMatchId, which generates new match-ids without requiring them to be Ids.
+    * but the complication is having one representative across all Nabla(s) in Nablas
+
+Do one improvement at a time, and benchmark accordingly.
+Ideas:
+VarId -> Maybe VarId
+Better representation than DeBruijnF, seems wasteful, we only care about
+debruijnization for lambdas in view patterns, which don't happen that often.


=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -105,8 +105,6 @@ import qualified Data.Equality.Graph as EG
 import Data.Bifunctor (second)
 import Data.Function ((&))
 import qualified Data.IntSet as IS
-import Data.Tuple (swap)
-import Data.Traversable (mapAccumL)
 
 --
 -- * Main exports
@@ -845,7 +843,7 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
   -- equate should also update e-graph, basically re-implement "equateUSDFM" in terms of the e-graph, or inline it or so
   case equate env x y of
     -- Add the constraints we had for x to y
-    -- See Note [Joining e-classes PMC] todo mention from joinA
+    -- See Note (TODO) [Joining e-classes PMC] todo mention from joinA
     -- Now, here's a really tricky bit (TODO Write note, is it the one above?)
     -- Bc the joinA operation is unlawful, and because the makeA operation for
     -- expressions is also unlawful (sets the type to ()::(), mostly out of
@@ -960,10 +958,9 @@ addCoreCt nabla x e = do
 
     bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) ClassId
     bind_expr e = do
-      x <- lift (lift (mkPmId (exprType e)))
-      xid <- StateT $ \nabla -> pure $ representId x nabla
-      core_expr xid e
-      pure xid
+      x <- StateT $ \nabla -> lift (mkPmMatchId (exprType e) nabla)
+      core_expr x e
+      pure x
 
     -- Look at @let x = K taus theta es@ and generate the following
     -- constraints (assuming universals were dropped from @taus@ before):
@@ -1588,8 +1585,9 @@ instCon fuel nabla at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} Ma
       let gammas = substTheta sigma_ex (eqSpecPreds eq_spec ++ thetas)
       -- (4) Instantiate fresh term variables as arguments to the constructor
       let field_tys' = substTys sigma_ex $ map scaledThing field_tys
-      arg_ids <- mapM mkPmId field_tys'
-      let (nabla', arg_class_ids) = mapAccumL (\nab id -> swap $ representId id nab) nabla arg_ids
+      arg_ids <- mapM mkPmId field_tys' -- unfortunate, if PhiConCt received ClassIds instead of Ids we wouldn't need this. ROMES:TODO Explore
+      -- (arg_ids, nabla') <- runStateT (mapM (StateT @Nabla . mkPmMatchId) field_tys') nabla
+      let (arg_class_ids, nabla') = representIds arg_ids nabla
       tracePm (hdr "(cts)") $ vcat
         [ ppr x <+> dcolon <+> ppr match_ty
         , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
@@ -2036,12 +2034,11 @@ generateInhabitingPatterns mode (x:xs) n nabla at MkNabla{nabla_tm_st=ts} = do
     instantiate_newtype_chain :: ClassId -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (ClassId, Nabla)
     instantiate_newtype_chain x nabla []                      = pure (x, nabla)
     instantiate_newtype_chain x nabla ((_ty, dc, arg_ty):dcs) = do
-      y <- lift $ mkPmId arg_ty
-      let (yid,nabla') = representId y nabla
+      (y, nabla') <- lift $ mkPmMatchId arg_ty nabla
       -- Newtypes don't have existentials (yet?!), so passing an empty
       -- list as ex_tvs.
-      nabla'' <- addConCt nabla' x (PmAltConLike (RealDataCon dc)) [] [yid]
-      instantiate_newtype_chain yid nabla'' dcs
+      nabla'' <- addConCt nabla' x (PmAltConLike (RealDataCon dc)) [] [y]
+      instantiate_newtype_chain y nabla'' dcs
 
     instantiate_cons :: ClassId -> Type -> [ClassId] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
     instantiate_cons _ _  _  _ _     []       = pure []
@@ -2149,7 +2146,7 @@ updateVarInfo :: Functor f => ClassId -> (VarInfo -> f VarInfo) -> Nabla -> f Na
 -- Update the data at class @xid@ using lenses and the monadic action @go@
 updateVarInfo xid f nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=eg } } = (\eg' -> nabla{ nabla_tm_st = ts{ts_facts = eg'} }) <$> (_class xid . _data) f eg
 
-eclassMatchId :: HasCallStack => ClassId -> Nabla -> Id
+eclassMatchId :: ClassId -> Nabla -> Id
 eclassMatchId cid = vi_id . (^. _class cid . _data) . (ts_facts . nabla_tm_st)
 
 eclassType :: ClassId -> Nabla -> Type
@@ -2157,3 +2154,11 @@ eclassType cid = idType . eclassMatchId cid
 
 
 -- ROMES:TODO: When exactly to rebuild?
+
+-- | Generate a fresh class for matching, returning the class-id as the match-id
+mkPmMatchId :: Type -> Nabla -> DsM (ClassId, Nabla)
+mkPmMatchId ty (MkNabla tyst ts at TmSt{ts_facts = egr}) = do
+  x <- mkPmId ty -- romes:Todo: for now, we still use mkPmId to get an Id for emptyVarInfo, but we want to get rid of this too
+  let (xid, egr') = EG.newEClass (emptyVarInfo x) egr
+  return (xid, MkNabla tyst ts{ts_facts=egr'})
+{-# NOINLINE mkPmMatchId #-} -- We'll CPR deeply, that should be enough


=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -47,6 +47,7 @@ import GHC.Prelude
 import GHC.Data.Bag
 import GHC.Data.FastString
 import GHC.Types.Id
+import GHC.Types.Var.Env
 import GHC.Types.Unique.DSet
 import GHC.Types.Name
 import GHC.Core.Equality
@@ -155,6 +156,8 @@ data TmState
   = TmSt
   { ts_facts :: !TmEGraph
   -- ^ Facts about terms.
+  , ts_reps :: !(IdEnv ClassId)
+  -- ^ A mapping from match-id Ids to the class-id representing that match-id
 
   -- ROMES:TODO: ts_dirty looks a bit to me like the bookeeping needed to know
   -- which nodes to upward merge, perhaps we can get rid of it too.
@@ -242,7 +245,7 @@ instance Outputable BotInfo where
 
 -- | Not user-facing.
 instance Outputable TmState where
-  ppr (TmSt eg dirty) = text (show eg) $$ ppr dirty
+  ppr (TmSt eg idmp dirty) = text (show eg) $$ ppr idmp $$ ppr dirty
 
 -- | Not user-facing.
 instance Outputable VarInfo where
@@ -263,7 +266,7 @@ instance Outputable VarInfo where
 
 -- | Initial state of the term oracle.
 initTmState :: TmState
-initTmState = TmSt EG.emptyEGraph IS.empty
+initTmState = TmSt EG.emptyEGraph mempty IS.empty
 
 -- | A data type that caches for the 'VarInfo' of @x@ the results of querying
 -- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
@@ -320,7 +323,7 @@ emptyVarInfo x
 -- romes:TODO I don't think this is what we want any longer, more like represent Id and see if it was previously represented by some data or not?
 -- romes:TodO should return VarInfo rather than Maybe VarInfo
 lookupVarInfo :: TmState -> ClassId -> VarInfo
-lookupVarInfo (TmSt eg _) x
+lookupVarInfo (TmSt eg _ _) x
 -- RM: Yea, I don't like the fact that currently all e-classes are created by Ids and have an Empty Var info, yet we must call "fromMaybe" here. Not good.
   = eg ^._class x._data
 
@@ -836,9 +839,11 @@ instance Show VarInfo where
 
 representId :: Id -> Nabla -> (ClassId, Nabla)
 -- Will need to justify this well
-representId x (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})
+representId x (MkNabla tyst tmst at TmSt{ts_facts=eg0, ts_reps=idmp})
+  = case lookupVarEnv idmp x of
+      Nothing -> case EG.newEClass (emptyVarInfo x) eg0 of
+        (xid, eg1) -> (xid, MkNabla tyst tmst{ts_facts=eg1, ts_reps=extendVarEnv idmp x xid})
+      Just xid -> (xid, MkNabla tyst tmst)
 
 representIds :: [Id] -> Nabla -> ([ClassId], Nabla)
 representIds xs nabla = swap $ mapAccumL (\acc x -> swap $ representId x acc) nabla xs


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



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/40552c651cc38f8db397171f0b5b573e3c9f178f...7539a46aa34f431fe019507a19b345e96fceeb7f

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/40552c651cc38f8db397171f0b5b573e3c9f178f...7539a46aa34f431fe019507a19b345e96fceeb7f
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/3350816a/attachment-0001.html>


More information about the ghc-commits mailing list