[Git][ghc/ghc][wip/romes/eqsat-pmc] 3 commits: IWP
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Wed Jun 14 16:11:09 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
c545c607 by Rodrigo Mesquita at 2023-06-13T19:19:47+01:00
IWP
- - - - -
f3bbd6c0 by Rodrigo Mesquita at 2023-06-14T00:56:52+01:00
WIP
- - - - -
6dec19d1 by Rodrigo Mesquita at 2023-06-14T17:10:56+01:00
WIP
- - - - -
6 changed files:
- + compiler/GHC/Core/Functor.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- compiler/ghc.cabal.in
- libraries/hegg
Changes:
=====================================
compiler/GHC/Core/Functor.hs
=====================================
@@ -0,0 +1,118 @@
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+module GHC.Core.Functor where
+
+import GHC.Generics
+import GHC.Prelude
+
+import Data.Bool
+import Data.Eq
+import Data.Ord
+import Data.Functor
+import Data.Functor.Classes
+import Data.Foldable
+import Data.Traversable
+
+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 Data.Equality.Utils (Fix(..))
+
+-- 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)
+
+data BindF b a
+ = NonRecF b a
+ | RecF [(b, a)]
+ deriving (Functor, Foldable, Traversable)
+
+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 (Eq a, Eq b) => Eq (AltF b a) where
+-- (==) (AltF c as a) (AltF c' as' a') = c == c' && as == as' && a == a'
+
+-- instance Eq b => Eq1 (AltF b) where
+-- liftEq eq (AltF c as a) (AltF c' as' a') = c == c' && as == as' && eq a a'
+
+-- instance (Eq a, Eq b) => Eq (BindF b a) where
+-- (==) (RecF as) (RecF as') = as == as'
+-- (==) (NonRecF a b) (NonRecF a' b') = a == a' && b == b'
+-- (==) _ _ = False
+
+-- instance Eq b => Eq1 (BindF b) where
+-- liftEq eq (RecF as) (RecF as') = liftEq (\(x,y) (x',y') -> x == x' && eq y y') as as'
+-- liftEq eq (NonRecF a b) (NonRecF a' b') = a == a' && eq b b'
+-- liftEq _ _ _ = False
+
+-- instance (Eq a, Eq b) => Eq (ExprF b a) where
+-- (==) (VarF a) (VarF b) = a == b
+-- (==) (LitF a) (LitF b) = a == b
+-- (==) (AppF a a') (AppF b b') = a == b && a' == b'
+-- (==) (LamF a a') (LamF b b') = a == b && a' == b'
+-- (==) (LetF a a') (LetF b b') = a == b && a' == b'
+ -- (==) (CaseF a a' t as) (CaseF b b' v bs) = a == b && a' == b'
+ -- && eqDeBruijnType t v
+ -- && as == bs
+ -- (==) (CastF a c) (CastF b c') = a == b && eqDeBruijnType (coercionType c) (coercionType c')
+ -- ROMES:TODO: THE REST OF IT!!
+ -- (==) _ _ = False
+
+instance Eq a => Eq (DeBruijnF CoreExprF a) where
+ (==) _ _ = error "TODO"
+
+instance Eq1 (DeBruijnF CoreExprF) where
+ liftEq eq = error "TODO"
+
+instance Ord a => Ord (DeBruijnF CoreExprF a) where
+ compare _ _ = error "TODO"
+
+instance Ord1 (DeBruijnF CoreExprF) where
+ liftCompare cmp _ _ = error "TODO"
+
+instance Functor (DeBruijnF CoreExprF)
+instance Foldable (DeBruijnF CoreExprF)
+instance Traversable (DeBruijnF CoreExprF)
+
+
+-- | 'unsafeCoerce' mostly because I'm too lazy to write the boilerplate.
+fromCoreExpr :: CoreExpr -> Fix CoreExprF
+fromCoreExpr = unsafeCoerce
+
+fromDBCoreExpr :: DeBruijn CoreExpr -> Fix (DeBruijnF CoreExprF)
+fromDBCoreExpr = unsafeCoerce
+
+toCoreExpr :: CoreExpr -> Fix CoreExprF
+toCoreExpr = unsafeCoerce
+
=====================================
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
@@ -21,7 +22,7 @@ module GHC.Core.Map.Type (
-- * Utilities for use by friends only
TypeMapG, CoercionMapG,
- DeBruijn(..), deBruijnize, eqDeBruijnType, eqDeBruijnVar,
+ DeBruijn(..), DeBruijnF(..), deBruijnize, deBruijnizeF, eqDeBruijnType, eqDeBruijnVar,
BndrMap, xtBndr, lkBndr,
VarMap, xtVar, lkVar, lkDFreeVar, xtDFreeVar,
@@ -34,6 +35,7 @@ module GHC.Core.Map.Type (
-- between GHC.Core.Unify (which depends on this module) and GHC.Core
import GHC.Prelude
+import Data.Functor.Classes
import GHC.Core.Type
import GHC.Core.Coercion
@@ -513,12 +515,18 @@ lookupCME (CME { cme_env = env }) v = lookupVarEnv env v
-- needing it.
data DeBruijn a = D CmEnv a
+newtype DeBruijnF f a = DeBruijnF (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
-- isn't already a 'CmEnv' in scope.
deBruijnize :: a -> DeBruijn a
deBruijnize = D emptyCME
+-- | Like 'deBruijnize' but synthesizes a @DeBruijnF f a@ from an @f a@
+deBruijnizeF :: f a -> DeBruijnF f a
+deBruijnizeF = DeBruijnF . deBruijnize
+
instance Eq (DeBruijn a) => Eq (DeBruijn [a]) where
D _ [] == D _ [] = True
D env (x:xs) == D env' (x':xs') = D env x == D env' x' &&
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -59,7 +59,8 @@ 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,9 +100,13 @@ import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
import Data.Functor.Const
-import Data.Equality.Graph (EGraph)
+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)
+import Data.Function ((&))
+import qualified Data.IntSet as IS
--
-- * Main exports
@@ -689,38 +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 (xid, env') = EG.represent (Fix $ Const x) env
- env'' <- EG.adjustF go xid env'
+-- 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 :: VarInfo -> MaybeT DsM VarInfo
- go vi at VI { vi_bot = bot }
+ 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 vi -- There already is x ~ ⊥. Nothing left to do
+ 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 vi{ vi_bot = IsBot }
+ 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 (xid, env') = EG.represent (Fix $ Const x) env
- -- ROMES:TODO: This could be all be a function passed to adjust
- let (y, vi at VI { vi_bot = bot }, TmSt{ts_facts=env''}) = lookupVarInfoNT (ts{ts_facts=env'}) x -- ROMES:TODO: this will represent x again (quite cheap still), but whatever for now
- case bot of
- IsBot -> mzero -- There was x ~ ⊥. Contradiction!
- IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do (ROMES:TODO missing env')
- 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 = EG.adjust (const vi') xid env''} }
+ 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
@@ -729,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))
@@ -758,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
@@ -779,10 +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 (xid, env') = EG.represent (Fix $ Const x) env
- -- ROMES:TODO: Omssions of updates on ts_facts on nabla are fine, but not perfect. Get it consistent
+ let (xid, env') = representId x env
-- ROMES:TODO: Also looks like a function on varinfo (adjust)
- let (vi@(VI _ pos neg bot _), TmSt{ts_facts=env''}) = lookupVarInfo (ts{ts_facts=env'}) x
+ 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
@@ -801,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 = EG.adjust (const (vi{vi_pos = pos', vi_bot = bot'})) xid env''} }
+ 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 ->
@@ -835,8 +850,9 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- 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
- (vi_x, env') -> do
+ (Just vi_x, env') -> do
let nabla_equated = nabla{ nabla_tm_st = ts{ts_facts = env'} }
-- and then gradually merge every positive fact we have on x into y
let add_pos nabla (PACA cl tvs args) = addConCt nabla y cl tvs args
@@ -855,12 +871,12 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- >>> 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 :: EGraph VarInfo (Const Id) -> Id -> Id -> (VarInfo, EGraph VarInfo (Const Id))
+ equate :: TmEGraph -> Id -> Id -> (Maybe VarInfo, TmEGraph)
equate eg x y = do
- let (xid, eg') = EG.represent (Fix $ Const x) eg
- (yid, eg'') = EG.represent (Fix $ Const y) eg'
+ let (xid, eg') = representId x eg
+ (yid, eg'') = representId y eg'
(_, eg''') = EG.merge xid yid eg''
- in (EG.lookup xid eg', eg''')
+ in (eg' ^. _class xid ._data, eg''')
-- Note: lookup in eg', because it's before the merge.
@@ -929,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
@@ -987,25 +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
--- ROMES:TODO: Represent
- | 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}}) $ EG.represent (fromDBCoreExpr (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
@@ -1094,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]
@@ -1306,24 +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
- let (vi, TmSt{ts_facts=env'}) = lookupVarInfo ts x
- vi' <- f vi -- todo: lookupvar should really return the xid
- let (xid,env'') = EG.represent (Fix $ Const x) env' -- ROMES:TODO: really, a helper functoin for representing Ids
- go xs (EG.adjust (const vi') xid env'')
+ 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' <- EG.traverseAnalysisData 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
@@ -1345,18 +1357,19 @@ 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 cid 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
@@ -1364,15 +1377,15 @@ inhabitationTest fuel old_ty_st nabla at MkNabla{ nabla_tm_st = ts } = {-# SCC "in
-- | 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)
@@ -1400,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
@@ -1433,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 (fst $ 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)
@@ -1462,7 +1476,7 @@ instCompleteSet fuel nabla x cs
| otherwise
= {-# SCC "instCompleteSet" #-} go nabla (sorted_candidates cs)
where
- (vi, _env') = lookupVarInfo (nabla_tm_st nabla) x
+ vi = fromMaybe (emptyVarInfo x) $ lookupVarInfo (nabla_tm_st nabla) x
sorted_candidates :: CompleteMatch -> [ConLike]
sorted_candidates cm
@@ -1949,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 _ _, _env') = 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):
@@ -1988,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, _env) = 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)
@@ -2122,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?
\ No newline at end of file
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,5 +1,6 @@
-{-# OPTIONS_GHC -Wno-orphans #-} -- Oh god, ROMES:TODO
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
@@ -13,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,
@@ -48,6 +49,7 @@ import GHC.Types.Id
import GHC.Types.Var.Set
import GHC.Types.Unique.DSet
import GHC.Types.Name
+import GHC.Core.Functor
import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Utils.Outputable
@@ -61,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
@@ -78,10 +81,16 @@ 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)
+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
@@ -139,29 +148,24 @@ 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 :: !(EGraph VarInfo (Const Id)) -- ROMES:TODO: The Id here is because we don't merge yet ts_reps into the e-graph; so we simply have Ids as E-nodes
- -- ^ Facts about term variables. Deterministic env, so that we generate
- -- deterministic error messages.
--- ROMES:TODO: ts_reps perhaps too as well... but a first iteration should map CoreMap to ClassId, and replace just ts_facts.
- , 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.
--- 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 :: !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@).
}
-instance EG.Language (Const Id)
+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 (:)".
@@ -174,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
@@ -181,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.
@@ -219,10 +225,10 @@ data VarInfo
-- There ought to be a better way.
instance Eq VarInfo where
(==) _ _ = False
-instance Analysis VarInfo (Const Id) where
+instance Analysis (Maybe VarInfo) (DeBruijnF CoreExprF) where
{-# INLINE makeA #-}
{-# INLINE joinA #-}
- makeA (Const id) = emptyVarInfo id
+ 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
@@ -252,7 +258,7 @@ instance Outputable BotInfo where
-- | Not user-facing.
instance Outputable TmState where
- ppr (TmSt _state reps dirty) = text "<e-graph>" $$ ppr reps $$ ppr dirty
+ ppr (TmSt _ dirty) = text "<e-graph>" $$ ppr dirty
-- | Not user-facing.
instance Outputable VarInfo where
@@ -273,7 +279,7 @@ instance Outputable VarInfo where
-- | Initial state of the term oracle.
initTmState :: TmState
-initTmState = TmSt EG.emptyEGraph 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
@@ -326,16 +332,12 @@ emptyVarInfo x
}
-- | @lookupVarInfo tms x@ tells what we know about 'x'
---- romes: TODO: lookupVarInfo should also return the ClassId the Id was represented in..., that'd make things better
-lookupVarInfo :: TmState -> Id -> (VarInfo, TmState)
-lookupVarInfo tm@(TmSt env _ _) x
- -- = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
- -- ROMES:TODO Kind of an issue here, we could have a lookup operation on e-graphs but it'd be good to make it faster
- -- We will want to assume every Id is mapped to VarInfo, with emptyVarInfo as the default rather than Maybe
- -- I'm just unsure if the Id always exists or not.
- -- Then again this shouldn't be Id, but rather ClassId§
- = let (i,env') = EG.represent (Fix $ Const x) env
- in (EG.lookup i env', tm{ts_facts=env'})
+--- 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
@@ -347,38 +349,35 @@ lookupVarInfo tm@(TmSt env _ _) x
-- modulo type normalisation!
--
-- See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
-lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo, TmState)
+lookupVarInfoNT :: TmState -> Id -> (Id, Maybe VarInfo)
lookupVarInfoNT ts x = case lookupVarInfo ts x of
- (VI{ vi_pos = as_newtype -> Just y },ts')
- -> lookupVarInfoNT ts' y
- (res,ts')
- -> (x, res, ts')
+ 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
--- ROMES:TODO: What does this do, how to update?
-trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
-trvVarInfo f nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts = _env} } x
- -- ROMES:TODO: adjust on the EG, instead of fetching? the (a,) bit is not trivial
- = let (vi, ts'@TmSt{ts_facts = env'}) = lookupVarInfo ts x
- set_vi (a, vi') =
- (a, nabla{ nabla_tm_st = ts'{ ts_facts = let (i,env'') = EG.represent (Fix $ Const $ vi_id vi') env' in EG.adjust (const vi') i env'' } })
- in set_vi <$> f vi
- where
+-- 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
+ = 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 =
- -- bimap (pmAltConSetElems . vi_neg) (\ts' -> nabla{nabla_tm_st=ts'}) $ lookupVarInfo ts x
- -- ROMES:TODO: It's a bit unfortunate we forget the representation of $x$, but OK
- pmAltConSetElems $ vi_neg $ fst $ lookupVarInfo ts x
+ maybe [] (pmAltConSetElems . vi_neg) $ lookupVarInfo ts x
isDataConSolution :: PmAltConApp -> Bool
isDataConSolution PACA{paca_con = PmAltConLike (RealDataCon _)} = True
@@ -387,8 +386,9 @@ 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 $ fst $ lookupVarInfo (nabla_tm_st nabla) x of
- -- ROMES:TODO: It's a bit unfortunate we forget the representation of $x$, but OK
+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
@@ -506,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
@@ -838,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.cabal.in
=====================================
@@ -300,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
=====================================
libraries/hegg
=====================================
@@ -1 +1 @@
-Subproject commit 67453e7735fdfc9e6212c607ba3ed855d525d349
+Subproject commit 94339b984e48bd6ce009b4e70c9374e8ac4981cd
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d0575935ff754d76fd358ba6229e7fc6c798801b...6dec19d1bcfc25d4c3d79c795d5fba865c1b2876
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d0575935ff754d76fd358ba6229e7fc6c798801b...6dec19d1bcfc25d4c3d79c795d5fba865c1b2876
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/20230614/9c150b8b/attachment-0001.html>
More information about the ghc-commits
mailing list