[Git][ghc/ghc][wip/romes/eqsat-pmc] 3 commits: Add e-graphs submodule (hegg)
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Sun Jun 25 17:35:21 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
a97ab784 by Rodrigo Mesquita at 2023-06-25T17:56:17+01:00
Add e-graphs submodule (hegg)
- - - - -
e821aed9 by Rodrigo Mesquita at 2023-06-25T17:56:17+01:00
Compiler working with e-graph
IWP
WIP
WIP
WIP
WIP
Use numbers when threading e-graph to fix a bug
- - - - -
fb48c348 by Rodrigo Mesquita at 2023-06-25T18:12:53+01:00
IPW
- - - - -
13 changed files:
- .gitmodules
- + compiler/GHC/Core/Functor.hs
- compiler/GHC/Core/Map/Expr.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- compiler/GHC/Types/Unique/SDFM.hs
- compiler/ghc.cabal.in
- hadrian/src/Packages.hs
- hadrian/src/Rules/ToolArgs.hs
- hadrian/src/Settings/Default.hs
- + libraries/hegg
- packages
Changes:
=====================================
.gitmodules
=====================================
@@ -117,3 +117,6 @@
[submodule "utils/hpc"]
path = utils/hpc
url = https://gitlab.haskell.org/hpc/hpc-bin.git
+[submodule "libraries/hegg"]
+ path = libraries/hegg
+ url = https://github.com/alt-romes/hegg.git
=====================================
compiler/GHC/Core/Functor.hs
=====================================
@@ -0,0 +1,165 @@
+{-# 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
+
+import GHC.Core
+import GHC.Core.TyCo.Rep
+import GHC.Core.Map.Type
+import GHC.Core.Map.Expr
+import GHC.Types.Var
+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)
+
+import Data.Functor.Compose
+
+import Data.Coerce
+
+type DeBruijnF = Compose DeBruijn
+
+-- Important to note the binders are also represented by $a$
+-- This is because in the e-graph we will represent binders with the
+-- equivalence class id of things equivalent to it.
+--
+-- Unfortunately type binders are still not correctly accounted for.
+-- Perhaps it'd really be better to make DeBruijn work over these types
+
+-- ROMES:TODO: Rename module to specify this is for egraphs
+
+data AltF b a
+ = AltF AltCon [b] a
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
+
+data BindF b a
+ = NonRecF b a
+ | RecF [(b, a)]
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
+
+data ExprF b a
+ = VarF Id
+ | LitF Literal
+ | AppF a a
+ | LamF b a
+ | LetF (BindF b a) a
+ | CaseF a b Type [AltF b a]
+
+ | CastF a CoercionR
+ | TickF CoreTickish a
+ | TypeF Type
+ | CoercionF Coercion
+ deriving (Functor, Foldable, Traversable)
+
+type CoreExprF
+ = ExprF CoreBndr
+
+instance {-# OVERLAPS #-} Eq a => Eq (DeBruijnF CoreExprF a) where
+ (==) = eqDeBruijnExprF
+
+-- ROMES:TODO: This instance is plain wrong. This DeBruijn scheme won't
+-- particularly work for our situation, we'll likely have to have ints instead
+-- 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 (Compose (D env1 e1)) (Compose (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
+ go (TypeF t1) (TypeF t2) = eqDeBruijnType (D env1 t1) (D env2 t2)
+ -- See Note [Alpha-equality for Coercion arguments]
+ go (CoercionF {}) (CoercionF {}) = True
+ go (CastF e1 co1) (CastF e2 co2) = D env1 co1 == D env2 co2 && e1 == e2
+ go (AppF f1 a1) (AppF f2 a2) = f1 == f2 && a1 == a2
+ go (TickF n1 e1) (TickF n2 e2)
+ = eqDeBruijnTickish (D env1 n1) (D env2 n2)
+ && e1 == e2
+
+ go (LamF b1 e1) (LamF b2 e2)
+ = eqDeBruijnType (D env1 (varType b1)) (D env2 (varType b2))
+ && D env1 (varMultMaybe b1) == D env2 (varMultMaybe b2)
+ && e1 == e2
+
+ go (LetF (NonRecF v1 r1) e1) (LetF (NonRecF v2 r2) e2)
+ = r1 == r2 -- See Note [Alpha-equality for let-bindings]
+ && e1 == e2
+
+ go (LetF (RecF ps1) e1) (LetF (RecF ps2) e2)
+ =
+ -- See Note [Alpha-equality for let-bindings]
+ 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
+
+ go (CaseF e1 b1 t1 a1) (CaseF e2 b2 t2 a2)
+ | null a1 -- See Note [Empty case alternatives]
+ = null a2 && e1 == e2 && D env1 t1 == D env2 t2
+ | otherwise
+ = e1 == e2 && a1 == a2
+
+ go _ _ = False
+
+-- 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)
+
+-- | 'unsafeCoerce' mostly because I'm too lazy to write the boilerplate.
+fromCoreExpr :: CoreExpr -> Fix CoreExprF
+fromCoreExpr = unsafeCoerce
+
+toCoreExpr :: CoreExpr -> Fix CoreExprF
+toCoreExpr = unsafeCoerce
+
+-- | Represents a DeBruijn CoreExpr being careful to correctly debruijnizie the expression as it is represented
+--
+-- 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) eg0 = case expr of
+ Var v -> add (Node $ Compose (D cmenv (VarF v))) eg0
+ Lit lit -> add (Node $ Compose (D cmenv (LitF lit))) eg0
+ Type t -> add (Node $ Compose (D cmenv (TypeF t))) eg0
+ Coercion c -> add (Node $ Compose (D cmenv (CoercionF c))) eg0
+ Cast e co -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
+ in add (Node $ Compose (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 $ Compose (D cmenv (AppF fid aid))) eg2
+ Tick n e -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
+ in add (Node $ Compose (D cmenv (TickF n eid))) eg1
+ Lam b e -> let (eid,eg1) = representDBCoreExpr (D (extendCME cmenv b) e) eg0
+ in add (Node $ Compose (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 $ Compose (D cmenv (LetF (NonRecF v rid) eid))) eg2
+ Let (Rec (unzip -> (bs,rs))) e ->
+ let cmenv' = extendCMEs cmenv bs
+ (bsids, eg1) = EGM.runEGraphM eg0 $
+ traverse (\r -> state $ representDBCoreExpr (D cmenv' r)) rs
+ (eid, eg2) = representDBCoreExpr (D cmenv' e) eg1
+ in add (Node $ Compose (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 $ Compose (D cmenv (CaseF eid b t as'))) eg2
+
=====================================
compiler/GHC/Core/Map/Expr.hs
=====================================
@@ -18,6 +18,8 @@ module GHC.Core.Map.Expr (
CoreMap, emptyCoreMap, extendCoreMap, lookupCoreMap, foldCoreMap,
-- * Alpha equality
eqDeBruijnExpr, eqCoreExpr,
+ -- ** Exports for CoreExprF instances
+ eqDeBruijnTickish, eqDeBruijnVar,
-- * 'TrieMap' class reexports
TrieMap(..), insertTM, deleteTM,
lkDFreeVar, xtDFreeVar,
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -6,6 +6,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DeriveTraversable #-}
module GHC.Core.Map.Type (
-- * Re-export generic interface
@@ -512,6 +513,7 @@ lookupCME (CME { cme_env = env }) v = lookupVarEnv env v
-- export the constructor. Make a helper function if you find yourself
-- needing it.
data DeBruijn a = D CmEnv a
+ deriving (Functor, Foldable, Traversable) -- romes:TODO: for internal use only!
-- | 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
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -49,18 +49,17 @@ import GHC.Data.Bag
import GHC.Types.CompleteMatch
import GHC.Types.Unique.Set
import GHC.Types.Unique.DSet
-import GHC.Types.Unique.SDFM
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
import GHC.Core.FVs (exprFreeVars)
import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Map.Expr
+import GHC.Core.Map.Type
+import GHC.Core.Functor
import GHC.Core.Predicate (typeDeterminesValue)
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils (exprType)
@@ -99,6 +98,13 @@ import Data.List (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
+import Data.Equality.Graph (EGraph, ClassId)
+import Data.Equality.Graph.Lens
+import qualified Data.Equality.Graph as EG
+import Data.Bifunctor (second)
+import Data.Function ((&))
+import qualified Data.IntSet as IS
+
--
-- * Main exports
--
@@ -556,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".
@@ -685,32 +694,47 @@ filterUnliftedFields con args =
-- ⊥.
addBotCt :: Nabla -> Id -> MaybeT DsM Nabla
addBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x = do
- let (y, vi at VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x
- case bot of
- IsNotBot -> mzero -- There was x ≁ ⊥. Contradiction!
- IsBot -> pure nabla -- There already is x ~ ⊥. Nothing left to do
- MaybeBot -- We add x ~ ⊥
- | definitelyUnliftedType (idType x)
- -- Case (3) in Note [Strict fields and variables of unlifted type]
- -> mzero -- unlifted vars can never be ⊥
- | otherwise
- -> do
- let vi' = vi{ vi_bot = IsBot }
- pure nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env y vi' } }
+-- ROMES:TODO: bit of a hack to represent binders with `Var`, which is likely wrong (lambda bound vars might get equivalent to global ones?). Will need to justify this well
+-- Perhaps I can get a new e-class everytime I have a new binder, and use the e-class Id as the true identifier.
+-- (would just require adding a primitive to create empty e-classes. easy.)
+ let (xid, env') = representId x env
+ env'' <- updateVarInfo xid go env'
+ pure nabla{nabla_tm_st = ts{ts_facts = env''}}
+ where
+ go :: Maybe VarInfo -> MaybeT DsM (Maybe VarInfo)
+ go Nothing = pure (Just (emptyVarInfo x){vi_bot = IsBot})
+ go (Just vi at VI { vi_bot = bot })
+ = case bot of
+ IsNotBot -> mzero -- There was x ≁ ⊥. Contradiction!
+ IsBot -> pure (Just vi) -- There already is x ~ ⊥. Nothing left to do
+ MaybeBot -- We add x ~ ⊥
+ | definitelyUnliftedType (idType x)
+ -- Case (3) in Note [Strict fields and variables of unlifted type]
+ -> mzero -- unlifted vars can never be ⊥
+ | otherwise
+ -> do
+ pure (Just vi{ vi_bot = IsBot })
-- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt',
-- but only cares for the ⊥ "constructor".
addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla
addNotBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts=env} } x = do
- let (y, vi at VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x
- case bot of
- IsBot -> mzero -- There was x ~ ⊥. Contradiction!
- IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do
- MaybeBot -> do -- We add x ≁ ⊥ and test if x is still inhabited
- -- Mark dirty for a delayed inhabitation test
- let vi' = vi{ vi_bot = IsNotBot}
- pure $ markDirty y
- $ nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env y vi' } }
+ let (xid, env') = representId x env
+ (_y, mvi) = lookupVarInfoNT (ts{ts_facts=env'}) x
+ (yid, env'') = representId x env'
+ case mvi of
+ Just vi at VI { vi_bot = bot } ->
+ case bot of
+ IsBot -> mzero -- There was x ~ ⊥. Contradiction!
+ IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do
+ MaybeBot -> do -- We add x ≁ ⊥ and test if x is still inhabited
+ -- Mark dirty for a delayed inhabitation test
+ let vi' = vi{ vi_bot = IsNotBot}
+ pure $ markDirty yid
+ $ nabla{nabla_tm_st = ts{ ts_facts = env'' & _class xid . _data .~ Just vi'}}
+ Nothing ->
+ pure $ markDirty yid -- as above
+ $ nabla{nabla_tm_st = ts{ ts_facts = env'' & _class xid . _data .~ Just ((emptyVarInfo x){vi_bot = IsNotBot})}}
-- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't
-- take the shape of a 'PmAltCon' @K@ in the 'Nabla' and return @Nothing@ if
@@ -719,17 +743,19 @@ addNotBotCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts=env} } x = do
addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
addNotConCt _ _ (PmAltConLike (RealDataCon dc))
| isNewDataCon dc = mzero -- (3) in Note [Coverage checking Newtype matches]
-addNotConCt nabla x nalt = do
- (mb_mark_dirty, nabla') <- trvVarInfo go nabla x
+addNotConCt nabla at MkNabla{nabla_tm_st=ts at TmSt{ts_facts=env}} x nalt = do
+ let (xid, env') = representId x env
+ (mb_mark_dirty, nabla') <- trvVarInfo go nabla{nabla_tm_st=ts{ts_facts=env'}} xid
pure $ case mb_mark_dirty of
- Just x -> markDirty x nabla'
- Nothing -> nabla'
+ True -> markDirty xid nabla'
+ False -> nabla'
where
-- Update `x`'s 'VarInfo' entry. Fail ('MaybeT') if contradiction,
-- otherwise return updated entry and `Just x'` if `x` should be marked dirty,
-- where `x'` is the representative of `x`.
- go :: VarInfo -> MaybeT DsM (Maybe Id, VarInfo)
- go vi@(VI x' pos neg _ rcm) = do
+ 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
-- 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))
@@ -748,12 +774,12 @@ addNotConCt nabla x nalt = do
pure $ case mb_rcm' of
-- If nalt could be removed from a COMPLETE set, we'll get back Just and
-- have to mark x dirty, by returning Just x'.
- Just rcm' -> (Just x', vi'{ vi_rcm = rcm' })
+ Just rcm' -> (True, Just vi'{ vi_rcm = rcm' })
-- Otherwise, nalt didn't occur in any residual COMPLETE set and we
-- don't have to mark it dirty. So we return Nothing, which in the case
-- above would have compromised precision.
-- See Note [Shortcutting the inhabitation test], grep for T17836.
- Nothing -> (Nothing, vi')
+ Nothing -> (False, Just vi')
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike cl) = notNull req_theta
@@ -769,7 +795,9 @@ hasRequiredTheta _ = False
-- See Note [TmState invariants].
addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla
addConCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x alt tvs args = do
- let vi@(VI _ pos neg bot _) = lookupVarInfo ts x
+ let (xid, env') = representId x env
+ -- ROMES:TODO: Also looks like a function on varinfo (adjust)
+ let vi@(VI _ pos neg bot _) = fromMaybe (emptyVarInfo x) $ lookupVarInfo (ts{ts_facts=env'}) x
-- First try to refute with a negative fact
guard (not (elemPmAltConSet alt neg))
-- Then see if any of the other solutions (remember: each of them is an
@@ -788,7 +816,7 @@ addConCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x alt tvs args =
Nothing -> do
let pos' = PACA alt tvs args : pos
let nabla_with bot' =
- nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
+ nabla{nabla_tm_st = ts{ts_facts = env' & _class xid ._data .~ (Just vi{vi_pos = pos', vi_bot = bot'})}}
-- Do (2) in Note [Coverage checking Newtype matches]
case (alt, args) of
(PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
@@ -817,9 +845,12 @@ equateTys ts us =
--
-- See Note [TmState invariants].
addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
+-- This is where equality-graphs really come into play.
addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
- case equateUSDFM env x y of
- (Nothing, env') -> pure (nabla{ nabla_tm_st = ts{ ts_facts = env' } })
+ -- ROMES:TODO: equate auxiliary var that finds both vars, and lookups up the domain associated. However, I think we no longer should have Just/Nothing but rather always store emptyVarInfo for new e-nodes
+ -- 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
+ (Nothing, env') -> pure $ nabla{nabla_tm_st=ts{ts_facts=env'}} -- We keep the VarInfo as Nothing
-- Add the constraints we had for x to y
(Just vi_x, env') -> do
let nabla_equated = nabla{ nabla_tm_st = ts{ts_facts = env'} }
@@ -829,6 +860,25 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- Do the same for negative info
let add_neg nabla nalt = addNotConCt nabla y nalt
foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x))
+ where
+ -- @equate env x y@ makes @x@ and @y@ point to the same entry,
+ -- thereby merging @x@'s class with @y@'s.
+ -- If both @x@ and @y@ are in the domain of the map, then @y@'s entry will be
+ -- chosen as the new entry and @x@'s old entry will be returned.
+ --
+ -- Examples in terms of the model (see 'UniqSDFM'):
+ -- >>> equate [] u1 u2 == (Nothing, [({u1,u2}, Nothing)])
+ -- >>> equate [({u1,u3}, Just ele1)] u3 u4 == (Nothing, [({u1,u3,u4}, Just ele1)])
+ -- >>> equate [({u1,u3}, Just ele1)] u4 u3 == (Nothing, [({u1,u3,u4}, Just ele1)])
+ -- >>> equate [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 u2 == (Just ele1, [({u2,u1,u3}, Just ele2)])
+ equate :: TmEGraph -> Id -> Id -> (Maybe VarInfo, TmEGraph)
+ equate eg x y = do
+ let (xid, eg') = representId x eg
+ (yid, eg'') = representId y eg'
+ (_, eg''') = EG.merge xid yid eg''
+ in (eg' ^. _class xid ._data, eg''')
+ -- Note: lookup in eg', because it's before the merge.
+
-- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
-- on the shape of the 'CoreExpr' @e at . Examples:
@@ -895,10 +945,12 @@ addCoreCt nabla x e = do
-- semantically equivalent to @e@, in which case we may add the constraint
-- @x ~ y at .
equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
- equate_with_similar_expr x e = do
- rep <- StateT $ \nabla -> lift (representCoreExpr nabla e)
+ equate_with_similar_expr _x e = do
+ _ <- StateT $ \nabla -> pure (representCoreExpr nabla e)
+ pure ()
-- Note that @rep == x@ if we encountered @e@ for the first time.
- modifyT (\nabla -> addVarCt nabla x rep)
+ -- ROMES:TODO: I don't think we need to do this anymore
+ -- modifyT (\nabla -> addVarCt nabla x rep)
bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id
bind_expr e = do
@@ -953,24 +1005,18 @@ modifyT f = StateT $ fmap ((,) ()) . f
-- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
-- equivalent to @e'@) we encountered earlier, or a fresh identifier if
-- there weren't any such constraints.
-representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
-representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_reps = reps } } e
- | Just rep <- lookupCoreMap reps key = pure (rep, nabla)
- | otherwise = do
- rep <- mkPmId (exprType e)
- let reps' = extendCoreMap reps key rep
- let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
- pure (rep, nabla')
- where
- key = makeDictsCoherent e
- -- Use a key in which dictionaries for the same type become equal.
- -- See Note [Unique dictionaries in the TmOracle CoreMap]
+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}}) $ 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]
-- | Change out 'Id's which are uniquely determined by their type to a
-- common value, so that different names for dictionaries of the same type
-- are considered equal when building a 'CoreMap'.
--
-- See Note [Unique dictionaries in the TmOracle CoreMap]
+-- ROMES:TODO: I suppose this should be taken into account by the Eq instance of DeBruijnF CoreExprF -- if we do that there then we're sure that EG.represent takes that into account.
makeDictsCoherent :: CoreExpr -> CoreExpr
makeDictsCoherent var@(Var v)
| let ty = idType v
@@ -1059,6 +1105,7 @@ In the end, replacing dictionaries with an error value in the pattern-match
checker was the most self-contained, although we might want to revisit once
we implement a more robust approach to computing equality in the pattern-match
checker (see #19272).
+ROMES:TODO: I don't think e-graphs avoid this situation, because the names of the binders will still differ (although the Eq instance could take this into account?)
-}
{- Note [The Pos/Neg invariant]
@@ -1271,22 +1318,24 @@ tyStateRefined :: TyState -> TyState -> Bool
-- refinement of b or vice versa!
tyStateRefined a b = ty_st_n a /= ty_st_n b
-markDirty :: Id -> Nabla -> Nabla
+markDirty :: ClassId -> Nabla -> Nabla
markDirty x nabla at MkNabla{nabla_tm_st = ts at TmSt{ts_dirty = dirty} } =
- nabla{ nabla_tm_st = ts{ ts_dirty = extendDVarSet dirty x } }
+ nabla{nabla_tm_st = ts{ ts_dirty = IS.insert x dirty }}
-traverseDirty :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
+traverseDirty :: Monad m => (ClassId -> Maybe VarInfo -> m (Maybe VarInfo)) -> TmState -> m TmState
traverseDirty f ts at TmSt{ts_facts = env, ts_dirty = dirty} =
- go (uniqDSetToList dirty) env
+
+ go (IS.elems dirty) env
where
go [] env = pure ts{ts_facts=env}
- go (x:xs) !env = do
- vi' <- f (lookupVarInfo ts x)
- go xs (addToUSDFM env x vi')
+ go (x:xs) !_env = do
+ let vi = env ^._class x._data
+ vi' <- f x vi
+ go xs (env & _class x._data .~ vi') -- Use 'over' or so instead?
-traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
+traverseAll :: Monad m => (ClassId -> Maybe VarInfo -> m (Maybe VarInfo)) -> TmState -> m TmState
traverseAll f ts at TmSt{ts_facts = env} = do
- env' <- traverseUSDFM f env
+ env' <- (_iclasses.(\fab (i,cl) -> let mvi = fab (i,cl^._data) in (cl &) . (_data .~) <$> mvi)) (uncurry f) env
pure ts{ts_facts = env'}
-- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate
@@ -1308,31 +1357,35 @@ inhabitationTest fuel old_ty_st nabla at MkNabla{ nabla_tm_st = ts } = {-# SCC "in
ts' <- if tyStateRefined old_ty_st (nabla_ty_st nabla)
then traverseAll test_one ts
else traverseDirty test_one ts
- pure nabla{ nabla_tm_st = ts'{ts_dirty=emptyDVarSet}}
+ pure nabla{ nabla_tm_st = ts'{ts_dirty=IS.empty}}
where
- nabla_not_dirty = nabla{ nabla_tm_st = ts{ts_dirty=emptyDVarSet} }
- test_one :: VarInfo -> MaybeT DsM VarInfo
- test_one vi =
- lift (varNeedsTesting old_ty_st nabla vi) >>= \case
+ nabla_not_dirty = nabla{ nabla_tm_st = ts{ts_dirty=IS.empty} }
+ test_one :: ClassId -> Maybe VarInfo -> MaybeT DsM (Maybe VarInfo)
+ test_one _ Nothing = pure Nothing
+ test_one cid (Just vi) =
+ lift (varNeedsTesting old_ty_st nabla cid vi) >>= \case
True -> do
-- lift $ tracePm "test_one" (ppr vi)
-- No solution yet and needs testing
-- We have to test with a Nabla where all dirty bits are cleared
- instantiate (fuel-1) nabla_not_dirty vi
- _ -> pure vi
+ Just <$> instantiate (fuel-1) nabla_not_dirty vi
+ _ -> pure (Just vi)
+
+-- ROMES:TODO: The dirty shortcutting bit seems like the bookeeping on nodes to
+-- upward merge, perhaps we can rid of it too
-- | Checks whether the given 'VarInfo' needs to be tested for inhabitants.
-- Returns `False` when we can skip the inhabitation test, presuming it would
-- say "yes" anyway. See Note [Shortcutting the inhabitation test].
-varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
-varNeedsTesting _ MkNabla{nabla_tm_st=tm_st} vi
- | elemDVarSet (vi_id vi) (ts_dirty tm_st) = pure True
-varNeedsTesting _ _ vi
+varNeedsTesting :: TyState -> Nabla -> ClassId -> VarInfo -> DsM Bool
+varNeedsTesting _ MkNabla{nabla_tm_st=tm_st} cid _
+ | IS.member cid (ts_dirty tm_st) = pure True
+varNeedsTesting _ _ _ vi
| notNull (vi_pos vi) = pure False
-varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _
+varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _ _
-- Same type state => still inhabited
| not (tyStateRefined old_ty_st new_ty_st) = pure False
-varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = do
+varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _ vi = do
-- These normalisations are relatively expensive, but still better than having
-- to perform a full inhabitation test
(_, _, old_norm_ty) <- tntrGuts <$> pmTopNormaliseType old_ty_st (idType $ vi_id vi)
@@ -1360,19 +1413,20 @@ instBot _fuel nabla vi = {-# SCC "instBot" #-} do
pure vi
addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
-addNormalisedTypeMatches nabla at MkNabla{ nabla_ty_st = ty_st } x
- = trvVarInfo add_matches nabla x
+addNormalisedTypeMatches nabla at MkNabla{ nabla_ty_st = ty_st, nabla_tm_st = ts at TmSt{ts_facts=env} } x
+ | (xid,env') <- representId x env
+ = trvVarInfo (add_matches . fromMaybe (emptyVarInfo x)) nabla{nabla_tm_st=ts{ts_facts=env'}} xid
where
add_matches vi at VI{ vi_rcm = rcm }
-- important common case, shaving down allocations of PmSeriesG by -5%
- | isRcmInitialised rcm = pure (rcm, vi)
+ | isRcmInitialised rcm = pure (rcm, Just vi)
add_matches vi at VI{ vi_rcm = rcm } = do
norm_res_ty <- normaliseSourceTypeWHNF ty_st (idType x)
env <- dsGetFamInstEnvs
rcm' <- case splitReprTyConApp_maybe env norm_res_ty of
Just (rep_tc, _args, _co) -> addTyConMatches rep_tc rcm
Nothing -> addCompleteMatches rcm
- pure (rcm', vi{ vi_rcm = rcm' })
+ pure (rcm', Just vi{ vi_rcm = rcm' })
-- | Does a 'splitTyConApp_maybe' and then tries to look through a data family
-- application to find the representation TyCon, to which the data constructors
@@ -1393,7 +1447,7 @@ instCompleteSets fuel nabla vi = {-# SCC "instCompleteSets" #-} do
let x = vi_id vi
(rcm, nabla) <- lift (addNormalisedTypeMatches nabla x)
nabla <- foldM (\nabla cls -> instCompleteSet fuel nabla x cls) nabla (getRcm rcm)
- pure (lookupVarInfo (nabla_tm_st nabla) x)
+ pure (fromMaybe (emptyVarInfo x) (lookupVarInfo (nabla_tm_st nabla) x))
anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution p = any (go . paca_con)
@@ -1422,7 +1476,7 @@ instCompleteSet fuel nabla x cs
| otherwise
= {-# SCC "instCompleteSet" #-} go nabla (sorted_candidates cs)
where
- vi = lookupVarInfo (nabla_tm_st nabla) x
+ vi = fromMaybe (emptyVarInfo x) $ lookupVarInfo (nabla_tm_st nabla) x
sorted_candidates :: CompleteMatch -> [ConLike]
sorted_candidates cm
@@ -1909,9 +1963,9 @@ generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [Id] -> Int -> N
-- See Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
generateInhabitingPatterns _ _ 0 _ = pure []
generateInhabitingPatterns _ [] _ nabla = pure [nabla]
-generateInhabitingPatterns mode (x:xs) n nabla = do
+generateInhabitingPatterns mode (x:xs) n nabla at MkNabla{nabla_tm_st=ts} = do
tracePm "generateInhabitingPatterns" (ppr mode <+> ppr n <+> ppr (x:xs) $$ ppr nabla)
- let VI _ pos neg _ _ = lookupVarInfo (nabla_tm_st nabla) x
+ let (VI _ pos neg _ _) = fromMaybe (emptyVarInfo x) $ lookupVarInfo ts x
case pos of
_:_ -> do
-- Example for multiple solutions (must involve a PatSyn):
@@ -1948,8 +2002,8 @@ generateInhabitingPatterns mode (x:xs) n nabla = do
mb_stuff <- runMaybeT $ instantiate_newtype_chain x nabla dcs
case mb_stuff of
Nothing -> pure []
- Just (y, newty_nabla) -> do
- let vi = lookupVarInfo (nabla_tm_st newty_nabla) y
+ Just (y, newty_nabla at MkNabla{nabla_tm_st=ts}) -> do
+ let vi = fromMaybe (emptyVarInfo y) $ lookupVarInfo ts y
env <- dsGetFamInstEnvs
rcm <- case splitReprTyConApp_maybe env rep_ty of
Just (tc, _, _) -> addTyConMatches tc (vi_rcm vi)
@@ -2082,3 +2136,10 @@ Note that for -XEmptyCase, we don't want to emit a minimal cover. We arrange
that by passing 'CaseSplitTopLevel' to 'generateInhabitingPatterns'. We detect
the -XEmptyCase case in 'reportWarnings' by looking for 'ReportEmptyCase'.
-}
+
+-- | Update the value of the analysis data of some e-class by its id.
+updateVarInfo :: Functor f => ClassId -> (a -> f a) -> EGraph a l -> f (EGraph a l)
+-- Update the data at class @xid@ using lenses and the monadic action @go@
+updateVarInfo xid = _class xid . _data
+
+-- ROMES:TODO: When exactly to rebuild?
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,3 +1,7 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
@@ -10,12 +14,12 @@
module GHC.HsToCore.Pmc.Solver.Types (
-- * Normalised refinement types
- BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
+ BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TmEGraph, TyState(..),
Nabla(..), Nablas(..), initNablas,
lookupRefuts, lookupSolution,
-- ** Looking up 'VarInfo'
- lookupVarInfo, lookupVarInfoNT, trvVarInfo,
+ lookupVarInfo, lookupVarInfoNT, trvVarInfo, emptyVarInfo, representId,
-- ** Caching residual COMPLETE sets
CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
@@ -44,8 +48,8 @@ import GHC.Data.FastString
import GHC.Types.Id
import GHC.Types.Var.Set
import GHC.Types.Unique.DSet
-import GHC.Types.Unique.SDFM
import GHC.Types.Name
+import GHC.Core.Functor
import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Utils.Outputable
@@ -59,6 +63,7 @@ import GHC.Types.Literal
import GHC.Core
import GHC.Core.TyCo.Compare( eqType )
import GHC.Core.Map.Expr
+import GHC.Core.Map.Type
import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
@@ -75,6 +80,18 @@ import Data.Ratio
import GHC.Real (Ratio(..))
import qualified Data.Semigroup as Semi
+import Data.Functor.Const
+import Data.Functor.Compose
+import Data.Function ((&))
+import Data.Equality.Analysis (Analysis(..))
+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.IntSet (IntSet)
+import qualified Data.IntSet as IS (empty)
+import Data.Bifunctor (second)
+
-- import GHC.Driver.Ppr
--
@@ -131,25 +148,25 @@ instance Outputable TyState where
initTyState :: TyState
initTyState = TySt 0 emptyInert
--- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
--- entries are possibly shared when we figure out that two variables must be
--- equal, thus represent the same set of values.
+-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's and
+-- 'CoreExpr's. These entries are possibly shared when we figure out that two
+-- variables must be equal, thus represent the same set of values.
--
-- See Note [TmState invariants] in "GHC.HsToCore.Pmc.Solver".
data TmState
= TmSt
- { ts_facts :: !(UniqSDFM Id VarInfo)
- -- ^ Facts about term variables. Deterministic env, so that we generate
- -- deterministic error messages.
- , ts_reps :: !(CoreMap Id)
- -- ^ An environment for looking up whether we already encountered semantically
- -- equivalent expressions that we want to represent by the same 'Id'
- -- representative.
- , ts_dirty :: !DIdSet
+ { ts_facts :: !TmEGraph
+ -- ^ Facts about terms.
+
+ -- 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.
+ , ts_dirty :: !IntSet
-- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
-- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
}
+type TmEGraph = EGraph (Maybe VarInfo) (DeBruijnF CoreExprF)
+
-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
-- and negative ('vi_neg') facts, like "x is not (:)".
-- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
@@ -161,6 +178,8 @@ data VarInfo
{ vi_id :: !Id
-- ^ The 'Id' in question. Important for adding new constraints relative to
-- this 'VarInfo' when we don't easily have the 'Id' available.
+ -- ROMES:TODO: What is the Id in question when we might have multiple Ids in the same equivalence class?
+ -- It seems currenlty this is the representative of the e-class, so we could probably drop it, in favour of Type or so (since sometimes we need to know the type, and that's also reasonable data for the e-class to have)
, vi_pos :: ![PmAltConApp]
-- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
@@ -168,7 +187,7 @@ data VarInfo
-- pattern matches involving pattern synonym
-- case x of { Just y -> case x of PatSyn z -> ... }
-- However, no more than one RealDataCon in the list, otherwise contradiction
- -- because of generativity.
+ -- because of generativity (which would violate Invariant 1 from the paper).
, vi_neg :: !PmAltConSet
-- ^ Negative info: A list of 'PmAltCon's that it cannot match.
@@ -202,6 +221,18 @@ data VarInfo
-- to recognise completion of a COMPLETE set efficiently for large enums.
}
+-- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
+-- There ought to be a better way.
+instance Eq VarInfo where
+ (==) _ _ = False
+instance Analysis (Maybe VarInfo) (DeBruijnF CoreExprF) where
+ {-# INLINE makeA #-}
+ {-# INLINE joinA #-}
+ makeA _ = Nothing
+ -- romes: so currently, variables are joined in 'addVarCt' manually by getting the old value of $x$ and assuming the value of $y$ was chosen.
+ -- That's obviously bad now, it'd be much more clearer to do it here. It's just the nabla threading that's more trouble
+ joinA _a b = b
+
data PmAltConApp
= PACA
{ paca_con :: !PmAltCon
@@ -227,7 +258,7 @@ instance Outputable BotInfo where
-- | Not user-facing.
instance Outputable TmState where
- ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
+ ppr (TmSt _ dirty) = text "<e-graph>" $$ ppr dirty
-- | Not user-facing.
instance Outputable VarInfo where
@@ -248,7 +279,7 @@ instance Outputable VarInfo where
-- | Initial state of the term oracle.
initTmState :: TmState
-initTmState = TmSt emptyUSDFM emptyCoreMap emptyDVarSet
+initTmState = TmSt EG.emptyEGraph 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
@@ -300,9 +331,13 @@ emptyVarInfo x
, vi_rcm = emptyRCM
}
-lookupVarInfo :: TmState -> Id -> VarInfo
--- (lookupVarInfo tms x) tells what we know about 'x'
-lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
+-- | @lookupVarInfo tms x@ tells what we know about 'x'
+--- romes:TODO: This will have a different type. I don't know what yet.
+-- 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 -> Id -> Maybe VarInfo
+lookupVarInfo (TmSt eg _) x
+ = let (xid, eg') = representId x eg in eg' ^._class xid._data
-- | Like @lookupVarInfo ts x@, but @lookupVarInfo ts x = (y, vi)@ also looks
-- through newtype constructors. We have @x ~ N1 (... (Nk y))@ such that the
@@ -314,31 +349,35 @@ lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
-- modulo type normalisation!
--
-- See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
-lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
+lookupVarInfoNT :: TmState -> Id -> (Id, Maybe VarInfo)
lookupVarInfoNT ts x = case lookupVarInfo ts x of
- VI{ vi_pos = as_newtype -> Just y } -> lookupVarInfoNT ts y
- res -> (x, res)
+ Just VI{ vi_pos = as_newtype -> Just y } -> lookupVarInfoNT ts y
+ res -> (x, res)
where
as_newtype = listToMaybe . mapMaybe go
go PACA{paca_con = PmAltConLike (RealDataCon dc), paca_ids = [y]}
| isNewDataCon dc = Just y
go _ = Nothing
-trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
+-- romes: We could probably inline this
+trvVarInfo :: forall f a. Functor f => (Maybe VarInfo -> f (a,Maybe VarInfo)) -> Nabla -> ClassId -> f (a,Nabla)
trvVarInfo f nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts = env} } x
- = set_vi <$> f (lookupVarInfo ts x)
- where
- set_vi (a, vi') =
- (a, nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env (vi_id vi') vi' } })
+ = second (\g -> nabla{nabla_tm_st = ts{ts_facts=g}}) <$> updateAccum (_class x._data) f env
+ where
+ updateAccum :: forall f a s c. Functor f => Lens' s a -> (a -> f (c,a)) -> s -> f (c,s)
+ updateAccum lens g = getCompose . lens @(Compose f ((,) c)) (Compose . g)
------------------------------------------------
-- * Exported utility functions querying 'Nabla'
+-- ROMES:TODO: Document
+-- | Lookup the refutable patterns, i.e. the pattern alt cons that certainly can't happen??
+-- ROMES:TODO: ClassId?
lookupRefuts :: Nabla -> Id -> [PmAltCon]
-- Unfortunately we need the extra bit of polymorphism and the unfortunate
-- duplication of lookupVarInfo here.
lookupRefuts MkNabla{ nabla_tm_st = ts } x =
- pmAltConSetElems $ vi_neg $ lookupVarInfo ts x
+ maybe [] (pmAltConSetElems . vi_neg) $ lookupVarInfo ts x
isDataConSolution :: PmAltConApp -> Bool
isDataConSolution PACA{paca_con = PmAltConLike (RealDataCon _)} = True
@@ -347,11 +386,13 @@ isDataConSolution _ = False
-- @lookupSolution nabla x@ picks a single solution ('vi_pos') of @x@ from
-- possibly many, preferring 'RealDataCon' solutions whenever possible.
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
-lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of
- [] -> Nothing
- pos@(x:_)
- | Just sol <- find isDataConSolution pos -> Just sol
- | otherwise -> Just x
+lookupSolution nabla x = do
+ varinfo <- lookupVarInfo (nabla_tm_st nabla) x
+ case vi_pos varinfo of
+ [] -> Nothing
+ pos@(x:_)
+ | Just sol <- find isDataConSolution pos -> Just sol
+ | otherwise -> Just x
--------------------------------------------------------------------------------
-- The rest is just providing an IR for (overloaded!) literals and AltCons that
@@ -465,6 +506,7 @@ extendPmAltConSet (PACS cls lits) (PmAltConLike cl)
extendPmAltConSet (PACS cls lits) (PmAltLit lit)
= PACS cls (unionLists lits [lit])
+-- | The elements of a 'PmAltConSet'
pmAltConSetElems :: PmAltConSet -> [PmAltCon]
pmAltConSetElems (PACS cls lits)
= map PmAltConLike (uniqDSetToList cls) ++ map PmAltLit lits
@@ -797,3 +839,8 @@ instance Outputable PmAltCon where
instance Outputable PmEquality where
ppr = text . show
+
+
+representId :: Id -> TmEGraph -> (ClassId, TmEGraph)
+-- ROMES:TODO: bit of a hack to represent binders with `Var`, which is likely wrong (lambda bound vars might get equivalent to global ones?). Will need to justify this well
+representId x = EG.add (EG.Node (deBruijnizeF (VarF x))) -- debruijn things are compared correctly wrt binders, but we can still have a debruijn var w name with no prob
=====================================
compiler/GHC/Types/Unique/SDFM.hs
=====================================
@@ -82,6 +82,7 @@ lookupUSDFM usdfm x = snd (lookupReprAndEntryUSDFM usdfm x)
-- >>> equateUSDFM [({u1,u3}, Just ele1)] u3 u4 == (Nothing, [({u1,u3,u4}, Just ele1)])
-- >>> equateUSDFM [({u1,u3}, Just ele1)] u4 u3 == (Nothing, [({u1,u3,u4}, Just ele1)])
-- >>> equateUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 u2 == (Just ele1, [({u2,u1,u3}, Just ele2)])
+-- ROMES:TODO: Are all USDFM functions just for the PMC Nabla TM?
equateUSDFM
:: Uniquable key => UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele)
equateUSDFM usdfm@(USDFM env) x y =
=====================================
compiler/ghc.cabal.in
=====================================
@@ -88,6 +88,7 @@ Library
array >= 0.1 && < 0.6,
filepath >= 1 && < 1.5,
template-haskell == 2.20.*,
+ hegg,
hpc == 0.6.*,
transformers >= 0.5 && < 0.7,
exceptions == 0.10.*,
@@ -299,6 +300,7 @@ Library
GHC.Core.ConLike
GHC.Core.DataCon
GHC.Core.FamInstEnv
+ GHC.Core.Functor
GHC.Core.FVs
GHC.Core.InstEnv
GHC.Core.Lint
=====================================
hadrian/src/Packages.hs
=====================================
@@ -6,7 +6,7 @@ module Packages (
compareSizes, compiler, containers, deepseq, deriveConstants, directory,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh,
ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline,
- hsc2hs, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy,
+ hegg, hsc2hs, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy,
libffi, mtl, parsec, pretty, primitive, process, remoteIserv, rts,
runGhc, semaphoreCompat, stm, templateHaskell, terminfo, text, time, timeout, touchy,
transformers, unlit, unix, win32, xhtml,
@@ -37,8 +37,8 @@ ghcPackages =
[ array, base, binary, bytestring, cabalSyntax, cabal, checkPpr, checkExact, countDeps
, compareSizes, compiler, containers, deepseq, deriveConstants, directory
, exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh
- , ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline, hsc2hs
- , hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, libffi, mtl
+ , ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline
+ , hegg, hsc2hs, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, libffi, mtl
, parsec, pretty, process, rts, runGhc, stm, semaphoreCompat, templateHaskell
, terminfo, text, time, touchy, transformers, unlit, unix, win32, xhtml
, timeout
@@ -53,7 +53,7 @@ isGhcPackage = (`elem` ghcPackages)
array, base, binary, bytestring, cabalSyntax, cabal, checkPpr, checkExact, countDeps,
compareSizes, compiler, containers, deepseq, deriveConstants, directory,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh,
- ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline, hsc2hs,
+ ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline, hegg, hsc2hs,
hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy, remoteIserv, libffi, mtl,
parsec, pretty, primitive, process, rts, runGhc, semaphoreCompat, stm, templateHaskell,
terminfo, text, time, touchy, transformers, unlit, unix, win32, xhtml,
@@ -93,6 +93,7 @@ ghcPkg = util "ghc-pkg"
ghcPrim = lib "ghc-prim"
haddock = util "haddock"
haskeline = lib "haskeline"
+hegg = lib "hegg"
hsc2hs = util "hsc2hs"
hp2ps = util "hp2ps"
hpc = lib "hpc"
=====================================
hadrian/src/Rules/ToolArgs.hs
=====================================
@@ -162,6 +162,7 @@ toolTargets = [ binary
, ghci
, ghcPkg -- # executable
-- , haddock -- # depends on ghc library
+ , hegg
, hsc2hs -- # executable
, hpc
, hpcBin -- # executable
=====================================
hadrian/src/Settings/Default.hs
=====================================
@@ -89,6 +89,7 @@ stage0Packages = do
, ghci
, ghcPkg
, haddock
+ , hegg
, hsc2hs
, hpc
, hpcBin
@@ -137,6 +138,7 @@ stage1Packages = do
, ghcPkg
, ghcPrim
, haskeline
+ , hegg
, hp2ps
, hsc2hs
, integerGmp
=====================================
libraries/hegg
=====================================
@@ -0,0 +1 @@
+Subproject commit d2862ab93d0420841aae3b8436f27301814d61a0
=====================================
packages
=====================================
@@ -51,6 +51,7 @@ libraries/deepseq - - ssh://g
libraries/directory - - ssh://git@github.com/haskell/directory.git
libraries/filepath - - ssh://git@github.com/haskell/filepath.git
libraries/haskeline - - https://github.com/judah/haskeline.git
+libraries/hegg - - https://github.com/alt-romes/hegg.git
libraries/hpc - - -
libraries/mtl - - https://github.com/haskell/mtl.git
libraries/parsec - - https://github.com/haskell/parsec.git
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/deb79e164b8c1af182123e4e66ccf12eaa9b848b...fb48c3487bc588e22b16838ebee9654719caf4bb
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/deb79e164b8c1af182123e4e66ccf12eaa9b848b...fb48c3487bc588e22b16838ebee9654719caf4bb
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/21e3e685/attachment-0001.html>
More information about the ghc-commits
mailing list