[Git][ghc/ghc][wip/romes/eqsat-pmc] WIP
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Mon Jun 19 21:57:58 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
761d3d3b by Rodrigo Mesquita at 2023-06-19T22:57:23+01:00
WIP
- - - - -
3 changed files:
- compiler/GHC/Core/Functor.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
Changes:
=====================================
compiler/GHC/Core/Functor.hs
=====================================
@@ -1,7 +1,10 @@
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
+-- ROMES:TODO: Rename to Core.Equality or something
module GHC.Core.Functor where
import GHC.Prelude
@@ -15,6 +18,10 @@ import GHC.Types.Literal
import GHC.Types.Tickish
import Unsafe.Coerce (unsafeCoerce)
+import Control.Monad.Trans.State.Strict (state)
+import Data.Equality.Graph as EG
+import Data.Equality.Analysis
+import qualified Data.Equality.Graph.Monad as EGM
import Data.Equality.Utils (Fix(..))
import GHC.Utils.Misc (all2, equalLength)
@@ -63,7 +70,7 @@ instance Eq a => Eq (DeBruijnF CoreExprF a) where
-- of Id binders. Now, ignoring DeBruijn indices, we'll simply get this compile
-- to get a rougher estimate of performance?
eqDeBruijnExprF :: forall a. Eq a => DeBruijnF CoreExprF a -> DeBruijnF CoreExprF a -> Bool
-eqDeBruijnExprF (DeBruijnF (D env1 e1)) (DeBruijnF (D env2 e2)) = go e1 e2 where
+eqDeBruijnExprF (DF (D env1 e1)) (DF (D env2 e2)) = go e1 e2 where
go :: CoreExprF a -> CoreExprF a -> Bool
go (VarF v1) (VarF v2) = eqDeBruijnVar (D env1 v1) (D env2 v2)
go (LitF lit1) (LitF lit2) = lit1 == lit2
@@ -86,18 +93,16 @@ eqDeBruijnExprF (DeBruijnF (D env1 e1)) (DeBruijnF (D env2 e2)) = go e1 e2 where
&& e1 == e2
go (LetF (RecF ps1) e1) (LetF (RecF ps2) e2)
- = equalLength ps1 ps2
+ =
-- See Note [Alpha-equality for let-bindings]
- && all2 (\b1 b2 -> eqDeBruijnType (D env1 (varType b1))
- (D env2 (varType b2)))
- bs1 bs2
+ all2 (\b1 b2 -> eqDeBruijnType (D env1 (varType b1))
+ (D env2 (varType b2)))
+ bs1 bs2
&& rs1 == rs2
&& e1 == e2
where
(bs1,rs1) = unzip ps1
(bs2,rs2) = unzip ps2
- env1' = extendCMEs env1 bs1
- env2' = extendCMEs env2 bs2
go (CaseF e1 b1 t1 a1) (CaseF e2 b2 t2 a2)
| null a1 -- See Note [Empty case alternatives]
@@ -107,10 +112,9 @@ eqDeBruijnExprF (DeBruijnF (D env1 e1)) (DeBruijnF (D env2 e2)) = go e1 e2 where
go _ _ = False
--- With Ints as binders we can have almost trivial eq instances
-
instance Ord a => Ord (DeBruijnF CoreExprF a) where
compare a b = if a == b then EQ else LT
+-- deriving instance Ord a => Ord (DeBruijnF CoreExprF a)
deriving instance Functor (DeBruijnF CoreExprF)
deriving instance Foldable (DeBruijnF CoreExprF)
@@ -120,9 +124,56 @@ deriving instance Traversable (DeBruijnF CoreExprF)
fromCoreExpr :: CoreExpr -> Fix CoreExprF
fromCoreExpr = unsafeCoerce
-fromDBCoreExpr :: DeBruijn CoreExpr -> Fix (DeBruijnF CoreExprF)
-fromDBCoreExpr = unsafeCoerce
-
toCoreExpr :: CoreExpr -> Fix CoreExprF
toCoreExpr = unsafeCoerce
+-- | Represents a DeBruijn CoreExpr being careful to correctly debruijnizie the expression as it is represented
+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''
+ Let (Rec (unzip -> (bs,rs))) e ->
+ let cmenv' = extendCMEs cmenv bs
+ (bsids, eg') = EGM.runEGraphM eg $
+ 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' $
+ 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'
+
+
+-- ROMES:TODO: Instead of DeBruijnF CoreExprF we should have (ExprF (Int,Id))
+-- * A represent function that makes up the debruijn indices as it is representing the expressions
+-- * An Eq and Ord instance which ignore the Id and rather look at the DeBruijn index.
+--
+-- TODO
+-- * For types, can we use eqDeBruijnType ? I think not, because Lambdas and Lets can bind type variables
+--
+-- TODO: The Best Alternative:
+--
+-- Each expression keeps its DeBruijnF CmEnv environment, but the represent
+-- function must correctly prepare the debruijn indices, so that each e-node
+-- has the debruijn indice it would have in its recursive descent in the Eq instance?
+--
+-- TODO: We could even probably have Compose DeBruijn CoreExprF in that case!
+--
+
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -515,7 +515,7 @@ lookupCME (CME { cme_env = env }) v = lookupVarEnv env v
data DeBruijn a = D CmEnv a
deriving (Functor,Foldable,Traversable) -- romes:TODO: For internal use only!
-newtype DeBruijnF f a = DeBruijnF (DeBruijn (f a))
+newtype DeBruijnF f a = DF (DeBruijn (f a))
-- | Synthesizes a @DeBruijn a@ from an @a@, by assuming that there are no
-- bound binders (an empty 'CmEnv'). This is usually what you want if there
@@ -525,7 +525,7 @@ deBruijnize = D emptyCME
-- | Like 'deBruijnize' but synthesizes a @DeBruijnF f a@ from an @f a@
deBruijnizeF :: Functor f => f a -> DeBruijnF f a
-deBruijnizeF = DeBruijnF . deBruijnize
+deBruijnizeF = DF . deBruijnize
instance Eq (DeBruijn a) => Eq (DeBruijn [a]) where
D _ [] == D _ [] = True
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -53,7 +53,6 @@ import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Var (EvVar)
import GHC.Types.Var.Env
-import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
import GHC.Core
@@ -99,9 +98,7 @@ import Data.List (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
-import Data.Functor.Const
import Data.Equality.Graph (EGraph, ClassId)
-import Data.Equality.Utils (Fix(..))
import Data.Equality.Graph.Lens
import qualified Data.Equality.Graph as EG
import Data.Bifunctor (second)
@@ -720,7 +717,7 @@ addBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x = do
addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla
addNotBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts=env} } x = do
let (xid, env') = representId x env
- (y, mvi) = lookupVarInfoNT (ts{ts_facts=env'}) x
+ (_y, mvi) = lookupVarInfoNT (ts{ts_facts=env'}) x
(yid, env'') = representId x env'
case mvi of
Just vi at VI { vi_bot = bot } ->
@@ -755,7 +752,7 @@ addNotConCt nabla at MkNabla{nabla_tm_st=ts at TmSt{ts_facts=env}} x nalt = do
-- where `x'` is the representative of `x`.
go :: Maybe VarInfo -> MaybeT DsM (Bool, Maybe VarInfo)
go Nothing = pure (False, Just (emptyVarInfo x){vi_bot = IsNotBot, vi_neg = emptyPmAltConSet `extendPmAltConSet` nalt}) -- romes:TODO: Do I need to mark dirty the new thing?
- go (Just vi@(VI x' pos neg _ rcm)) = do
+ go (Just vi@(VI _x' pos neg _ rcm)) = do
-- 1. Bail out quickly when nalt contradicts a solution
let contradicts nalt sol = eqPmAltCon (paca_con sol) nalt == Equal
guard (not (any (contradicts nalt) pos))
@@ -1007,7 +1004,7 @@ modifyT f = StateT $ fmap ((,) ()) . f
-- there weren't any such constraints.
representCoreExpr :: Nabla -> CoreExpr -> (ClassId, Nabla)
representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = egraph } } e =
- second (\g -> nabla{nabla_tm_st = ts{ts_facts = g}}) $ EG.represent (fromDBCoreExpr (deBruijnize (makeDictsCoherent e))) egraph
+ second (\g -> nabla{nabla_tm_st = ts{ts_facts = g}}) $ representDBCoreExpr (deBruijnize (makeDictsCoherent e)) egraph
-- Use a key in which dictionaries for the same type become equal.
-- See Note [Unique dictionaries in the TmOracle CoreMap]
@@ -1361,7 +1358,7 @@ inhabitationTest fuel old_ty_st nabla at MkNabla{ nabla_tm_st = ts } = {-# SCC "in
where
nabla_not_dirty = nabla{ nabla_tm_st = ts{ts_dirty=IS.empty} }
test_one :: ClassId -> Maybe VarInfo -> MaybeT DsM (Maybe VarInfo)
- test_one cid Nothing = pure Nothing
+ test_one _ Nothing = pure Nothing
test_one cid (Just vi) =
lift (varNeedsTesting old_ty_st nabla cid vi) >>= \case
True -> do
@@ -2142,4 +2139,4 @@ updateVarInfo :: Functor f => ClassId -> (a -> f a) -> EGraph a l -> f (EGraph a
-- Update the data at class @xid@ using lenses and the monadic action @go@
updateVarInfo xid = _class xid . _data
--- ROMES:TODO: When exactly to rebuild?
\ No newline at end of file
+-- ROMES:TODO: When exactly to rebuild?
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/761d3d3b61cb674a9033fb74054372a2f7af7f50
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/761d3d3b61cb674a9033fb74054372a2f7af7f50
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/20230619/f671a934/attachment-0001.html>
More information about the ghc-commits
mailing list