[Git][ghc/ghc][wip/romes/egraphs-pmc-2] 19 commits: Add e-graphs submodule (hegg)
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Thu May 2 18:13:31 UTC 2024
Rodrigo Mesquita pushed to branch wip/romes/egraphs-pmc-2 at Glasgow Haskell Compiler / GHC
Commits:
7176c8f5 by Rodrigo Mesquita at 2023-10-31T16:56:04+00:00
Add e-graphs submodule (hegg)
- - - - -
1f669af4 by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
Create Core.Equality module
This module defines CoreExprF -- the base functor of CoreExpr, and
equality and ordering operations on the debruijnized CoreExprF.
Furthermore, it provides a function to represent a CoreExpr in an
e-graph.
This is a requirement to represent, reason about equality, and
manipulate CoreExprs in e-graphs. E-graphs are going to be used in the
pattern match checker (#19272), and potentially for type family
rewriting (#TODO) -- amongst other oportunities that are unlocked by
having them available.
- - - - -
8397368f by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
Drop GHC.Types.Unique.SDFM in favour of e-graphs
- - - - -
014285e7 by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
The rest of the owl
- - - - -
b14510a1 by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
Drawing of multiple owls
- - - - -
80946d3c by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
Keep drawing
- - - - -
e7fd39f3 by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
WIP MORE
- - - - -
8fcb5cff by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
WIP ALMOST
- - - - -
b8786444 by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
WIP...
- - - - -
67836a67 by Rodrigo Mesquita at 2023-10-31T16:56:05+00:00
WIP.;
- - - - -
460cf336 by Rodrigo Mesquita at 2023-10-31T16:56:06+00:00
whitsepac
- - - - -
2664f641 by Rodrigo Mesquita at 2023-10-31T16:56:06+00:00
Ww
- - - - -
1fd37591 by Rodrigo Mesquita at 2023-10-31T16:56:06+00:00
Better Outputable instance
- - - - -
86bb09f7 by Rodrigo Mesquita at 2023-10-31T16:56:06+00:00
mergeNotConCt can't use implications only now...?
- - - - -
aba1488f by Rodrigo Mesquita at 2023-10-31T16:56:06+00:00
Sometimes we can omit implied nalts
- - - - -
67027c8d by Rodrigo Mesquita at 2023-10-31T16:56:06+00:00
Fixes + debugging
- - - - -
5b097a0c by Rodrigo Mesquita at 2023-10-31T16:56:06+00:00
STAGE 1 BUILDS WITHOUT FAILURES.
- - - - -
c23d98db by Rodrigo Mesquita at 2023-10-31T16:56:30+00:00
depstest
- - - - -
af60b03e by Rodrigo Mesquita at 2024-05-02T19:12:46+01:00
submodule update
- - - - -
17 changed files:
- .gitmodules
- + TODO
- compiler/GHC/Core.hs
- + compiler/GHC/Core/Equality.hs
- compiler/GHC/Core/Map/Expr.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/HsToCore/Pmc.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
- testsuite/tests/count-deps/CountDepsParser.stdout
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
=====================================
TODO
=====================================
@@ -0,0 +1,9 @@
+The current failures might be because congruence isn't being maintained properly downwards, I think...?
+Instead, we might do this manually for merging positive constructor info in the e-graphs analysis modify function?
+
+If this works, the major todos are
+* Propagating strictness annotations to underlying newtypes (likely modify analysis)
+* Clean up equality
+ * How to do Ord Type?
+* Clean up solver
+ * Merge args of data cons when merging by congruence (likely modify analysis as well)
=====================================
compiler/GHC/Core.hs
=====================================
@@ -294,6 +294,7 @@ data AltCon
-- The instance adheres to the order described in Note [Case expression invariants]
instance Ord AltCon where
compare (DataAlt con1) (DataAlt con2) =
+ -- ROMES:TODO: Couldn't simply do this right by comparing the dataConName of the cons?
assert (dataConTyCon con1 == dataConTyCon con2) $
compare (dataConTag con1) (dataConTag con2)
compare (DataAlt _) _ = GT
=====================================
compiler/GHC/Core/Equality.hs
=====================================
@@ -0,0 +1,188 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DerivingVia #-}
+
+-- TODO: Rename to GHC.HsToCore.CoreEquality or something
+module GHC.Core.Equality where
+
+import GHC.Prelude
+
+-- import GHC.Types.Name (Name)
+import GHC.Core
+import GHC.Core.DataCon
+import GHC.Core.TyCo.Rep
+import GHC.Core.Map.Type
+import GHC.Types.Var
+import GHC.Types.Literal
+
+import Data.Equality.Graph as EG
+import Data.Equality.Analysis.Monadic
+import qualified Data.Equality.Graph.Monad as EGM
+import GHC.Utils.Outputable
+import GHC.Core.Coercion (coercionType)
+
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Reader
+
+-- 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
+
+-- In the pattern match checker, expressions will always be kind of shallow.
+-- In practice, no-one writes gigantic lambda expressions in guards and view patterns
+
+data AltF a
+ = AltF AltCon' [()] a -- [()] tells us the number of constructors..., bad representation TODO
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
+
+data BindF a
+ = NonRecF a
+ | RecF [a]
+ deriving (Functor, Foldable, Traversable, Eq, Ord, Show)
+
+type BoundVar = Int
+-- If we use this datatype specifically for representing HsToCore.Pmc, we may
+-- be able to drop the coercion field, and add a specific one for constructor
+-- application
+data ExprF r
+ = VarF BoundVar
+ -- ROMES:TODO: what about using Names for comparison? Since this is only for equality purposes...
+ -- It makes it possible to use the ConLikeName as the FreeVar Name, since there is conLikeName for PmAltConLike
+ | FreeVarF Id
+ | LitF Literal
+ | AppF r r
+ | LamF r
+ | LetF (BindF r) r
+ | CaseF r [AltF r] -- can we drop the case type for expr equality? we don't need them back, we just need to check equality. (perhaps this specialization makes this more suitable in the Pmc namespace)
+
+ -- | CastF a (DeBruijn CoercionR) -- can we drop this
+ -- | TickF CoreTickish a -- this, when representing expressions for equality?
+ -- but it'll be pretty hard to trigger any bug related to equality matching wrt coercions and casts on view and guard patterns solely
+ | TypeF DBType
+ | CoercionF DBCoercion
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
+
+newtype DBType = DBT (DeBruijn Type) deriving Eq
+instance Ord DBType where
+ compare (DBT dt) (DBT dt') = cmpDeBruijnType dt dt'
+newtype DBCoercion = DBC (DeBruijn Coercion) deriving Eq
+instance Ord DBCoercion where
+ compare (DBC dt) (DBC dt') = cmpDeBruijnCoercion dt dt'
+
+newtype AltCon' = AC' AltCon deriving Eq
+ deriving Outputable via AltCon
+
+instance Ord AltCon' where
+ compare (AC' (DataAlt a)) (AC' (DataAlt b))
+ = case compare (dataConName a) (dataConName b) of
+ LT -> LT
+ EQ -> compare (DataAlt a) (DataAlt b) -- AltCon's Ord instance only works for same datatypes
+ GT -> GT
+ compare (AC' a) (AC' b) = compare a b
+
+-- this makes perfect sense, if we already have to represent this in the e-graph
+-- we might as well make it a better suited representation for the e-graph...
+-- keeping the on-fly debruijn is harder
+representCoreExprEgr :: forall a m
+ . Analysis m a CoreExprF
+ => CoreExpr
+ -> EGraph a CoreExprF
+ -> m (ClassId, EGraph a CoreExprF)
+representCoreExprEgr expr egr = EGM.runEGraphMT egr (runReaderT (go expr) emptyCME) where
+ go :: CoreExpr -> ReaderT CmEnv (EGM.EGraphMT a CoreExprF m) ClassId
+ go = \case
+ Var v -> do
+ env <- ask
+ case lookupCME env v of
+ -- Nothing -> addE (FreeVarF $ varName v)
+ Nothing -> addE (FreeVarF v)
+ Just i -> addE (VarF i)
+ Lit lit -> addE (LitF lit)
+ Type t -> addE (TypeF (DBT $ deBruijnize t))
+ Coercion c -> addE (CoercionF (DBC $ deBruijnize c))
+ Tick _ e -> go e -- bypass ticks!
+ Cast e _ -> go e -- bypass casts! ouch? TODO
+ App f a -> do
+ f' <- go f
+ a' <- go a
+ addE (AppF f' a')
+ Lam b e -> do
+ e' <- local (`extendCME` b) $ go e
+ addE (LamF e')
+ Let (NonRec v r) e -> do
+ r' <- go r
+ e' <- local (`extendCME` v) $ go e
+ addE (LetF (NonRecF r') e')
+ Let (Rec (unzip -> (bs,rs))) e -> do
+ rs' <- traverse (local (`extendCMEs` bs) . go) rs
+ e' <- local (`extendCMEs` bs) $ go e
+ addE (LetF (RecF rs') e')
+ Case e b _t as -> do
+ e' <- go e
+ as' <- traverse (local (`extendCME` b) . goAlt) as
+ addE (CaseF e' as')
+
+ goAlt :: CoreAlt -> ReaderT CmEnv (EGM.EGraphMT a CoreExprF m) (CoreAltF ClassId)
+ goAlt (Alt c bs e) = do
+ e' <- local (`extendCMEs` bs) $ go e
+ return (AltF (AC' c) (map (const ()) bs) e')
+
+ addE :: Analysis m a CoreExprF => CoreExprF ClassId -> ReaderT CmEnv (EGM.EGraphMT a CoreExprF m) ClassId
+ addE e = lift $ EGM.addM $ Node e
+{-# INLINEABLE representCoreExprEgr #-}
+
+type CoreExprF = ExprF
+type CoreAltF = AltF
+type CoreBindF = BindF
+
+instance Outputable (EG.ENode CoreExprF) where
+ ppr (EG.Node n) = text (show n)
+
+-- cmpDeBruijnTickish :: DeBruijn CoreTickish -> DeBruijn CoreTickish -> Ordering
+-- cmpDeBruijnTickish (D env1 t1) (D env2 t2) = go t1 t2 where
+-- go (Breakpoint lext lid lids _) (Breakpoint rext rid rids _)
+-- = case compare lid rid of
+-- LT -> LT
+-- EQ -> case compare (D env1 lids) (D env2 rids) of
+-- LT -> LT
+-- EQ -> compare lext rext
+-- GT -> GT
+-- GT -> GT
+-- go l r = compare l r
+
+cmpDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Ordering
+cmpDeBruijnType d1@(D _ t1) d2@(D _ t2)
+ = if eqDeBruijnType d1 d2
+ then EQ
+ -- ROMES:TODO: This definitely does not look OK.
+ -- ROMES:TODO: This hurts performance a lot (50% of regression is basically this)
+ else compare (showPprUnsafe t1) (showPprUnsafe t2)
+
+cmpDeBruijnCoercion :: DeBruijn Coercion -> DeBruijn Coercion -> Ordering
+cmpDeBruijnCoercion (D env1 co1) (D env2 co2)
+ = cmpDeBruijnType (D env1 (coercionType co1)) (D env2 (coercionType co2))
+
+-- -- instances for debugging purposes
+instance Show a => Show (CoreExprF a) where
+ show (VarF id) = showPprUnsafe $ text "VarF" <+> ppr id
+ show (FreeVarF id) = showPprUnsafe $ ppr id
+ show (LitF lit) = showPprUnsafe $ text "LitF" <+> ppr lit
+ show (AppF a b) = "AppF " ++ show a ++ " " ++ show b
+ show (LamF a) = "LamF " ++ show a
+ show (LetF b a) = "LetF " ++ show b ++ " " ++ show a
+ show (CaseF a alts) = "CaseF " ++ show a ++ show alts
+
+ -- show (CastF _a _cor) = "CastF"
+ -- show (TickF _cotick _a) = "Tick"
+ show (TypeF (DBT (D _ t))) = "TypeF " ++ showPprUnsafe (ppr t)
+ show (CoercionF (DBC (D _ co))) = "CoercionF " ++ showPprUnsafe co
+
+instance Show a => Show (AltF a) where
+ show (AltF alt bs a) = "AltF " ++ showPprUnsafe (ppr alt <+> ppr bs) ++ show a
+
=====================================
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
@@ -22,6 +23,7 @@ module GHC.Core.Map.Type (
TypeMapG, CoercionMapG,
DeBruijn(..), deBruijnize, eqDeBruijnType, eqDeBruijnVar,
+ cmpDeBruijnVar,
BndrMap, xtBndr, lkBndr,
VarMap, xtVar, lkVar, lkDFreeVar, xtDFreeVar,
@@ -282,6 +284,9 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
instance Eq (DeBruijn Var) where
(==) = eqDeBruijnVar
+instance Ord (DeBruijn Var) where
+ compare = cmpDeBruijnVar
+
eqDeBruijnVar :: DeBruijn Var -> DeBruijn Var -> Bool
eqDeBruijnVar (D env1 v1) (D env2 v2) =
case (lookupCME env1 v1, lookupCME env2 v2) of
@@ -289,6 +294,13 @@ eqDeBruijnVar (D env1 v1) (D env2 v2) =
(Nothing, Nothing) -> v1 == v2
_ -> False
+cmpDeBruijnVar :: DeBruijn Var -> DeBruijn Var -> Ordering
+cmpDeBruijnVar (D env1 v1) (D env2 v2) =
+ case (lookupCME env1 v1, lookupCME env2 v2) of
+ (Just b1, Just b2) -> compare b1 b2
+ (Nothing, Nothing) -> compare v1 v2
+ (z,w) -> compare z w -- Compare Maybes on whether they're Just or Nothing
+
instance {-# OVERLAPPING #-}
Outputable a => Outputable (TypeMapG a) where
ppr m = text "TypeMap elts" <+> ppr (foldTM (:) m [])
@@ -512,6 +524,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
@@ -525,6 +538,15 @@ instance Eq (DeBruijn a) => Eq (DeBruijn [a]) where
D env xs == D env' xs'
_ == _ = False
+instance Ord (DeBruijn a) => Ord (DeBruijn [a]) where
+ D _ [] `compare` D _ [] = EQ
+ D env (x:xs) `compare` D env' (x':xs') = case D env x `compare` D env' x' of
+ LT -> LT
+ EQ -> D env xs `compare` D env' xs'
+ GT -> GT
+ D _ [] `compare` D _ (_:_) = LT
+ D _ (_:_) `compare` D _ [] = GT
+
instance Eq (DeBruijn a) => Eq (DeBruijn (Maybe a)) where
D _ Nothing == D _ Nothing = True
D env (Just x) == D env' (Just x') = D env x == D env' x'
=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -278,7 +278,6 @@ pmcRecSel _ _ = return ()
{- Note [pmcPatBind doesn't warn on pattern guards]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@pmcPatBind@'s main purpose is to check vanilla pattern bindings, like
->>>>>>> 8760510af3 (This MR is an implementation of the proposal #516.)
@x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
But its caller is also called for individual pattern guards in a @StmtCtxt at .
For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -1,6 +1,13 @@
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RankNTypes, GADTs #-}
+{-# OPTIONS_GHC -Wno-orphans #-} -- Analysis........
{-
Authors: George Karachalias <george.karachalias at cs.kuleuven.be>
@@ -48,22 +55,22 @@ 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.Equality
import GHC.Core.FVs (exprFreeVars)
import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Map.Expr
+import GHC.Core.Map.Type (deBruijnize)
import GHC.Core.Predicate (typeDeterminesValue)
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils (exprType)
-import GHC.Core.Make (mkListExpr, mkCharExpr, mkImpossibleExpr)
+import GHC.Core.Make (mkListExpr, mkCharExpr, mkImpossibleExpr, mkCoreApp)
+import GHC.Types.Id.Make (unboxedUnitExpr)
import GHC.Data.FastString
import GHC.Types.SrcLoc
@@ -97,6 +104,14 @@ import Data.List (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
+import Data.Equality.Analysis.Monadic
+import Data.Equality.Graph (ClassId)
+import Data.Equality.Graph.Lens
+import qualified Data.Equality.Graph as EG
+import qualified Data.Equality.Graph.Monad as EGM
+import Data.Function ((&))
+import qualified Data.IntSet as IS
+
--
-- * Main exports
--
@@ -602,8 +617,10 @@ addPhiCts :: Nabla -> PhiCts -> DsM (Maybe Nabla)
-- See Note [TmState invariants].
addPhiCts nabla cts = runMaybeT $ do
let (ty_cts, tm_cts) = partitionPhiCts cts
- nabla' <- addTyCts nabla (listToBag ty_cts)
+ nabla' <- addTyCts nabla (listToBag ty_cts)
nabla'' <- foldlM addPhiTmCt nabla' (listToBag tm_cts)
+ lift $ tracePm "addPhiCts, doing inhabitationTest" (ppr nabla'')
+ -- ROMES:TODO: Should the ty_st be nabla' or nabla'' !?
inhabitationTest initFuel (nabla_ty_st nabla) nabla''
partitionPhiCts :: PhiCts -> ([PredType], [PhiCt])
@@ -666,7 +683,7 @@ addPhiTmCt nabla (PhiConCt x con tvs dicts args) = do
-- PhiConCt correspond to the higher-level φ constraints from the paper with
-- bindings semantics. It disperses into lower-level δ constraints that the
-- 'add*Ct' functions correspond to.
- nabla' <- addTyCts nabla (listToBag dicts)
+ nabla' <- addTyCts nabla (listToBag dicts)
nabla'' <- addConCt nabla' x con tvs args
foldlM addNotBotCt nabla'' (filterUnliftedFields con args)
addPhiTmCt nabla (PhiNotConCt x con) = addNotConCt nabla x con
@@ -682,33 +699,68 @@ filterUnliftedFields con args =
-- surely diverges. Quite similar to 'addConCt', only that it only cares about
-- ⊥.
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' } }
+addBotCt nabla0 at MkNabla{nabla_tm_st = ts0} x = do
+ let (y, vi at VI { vi_bot = bot0 }) = lookupVarInfoNT ts0 x
+ -- NOTE FOR REVIEWER:
+ -- we were previously using the idType of |x|, but I think it should rather
+ -- be |y|, since, if y /= x, then x is a newtype and newtypes cannot be
+ -- unlifted
+ bot1 <- mergeBots (idType y) IsBot bot0
+ let vi' = vi{ vi_bot = bot1 }
+
+ (yid, nabla1) <- representId y nabla0
+
+ pure (nabla1 & nabla_egr._class yid._data .~ Just vi')
-- | 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' } }
+addNotBotCt nabla0 at MkNabla{ nabla_tm_st = ts0 } x = do
+ let (y, vi at VI { vi_bot = bot0 }) = lookupVarInfoNT ts0 x
+ bot1 <- mergeBots (idType y) IsNotBot bot0
+ let vi' = vi{ vi_bot = bot1 }
+
+ (yid, nabla1) <- representId y nabla0
+ let
+ marked
+ = case bot0 of
+ -- Mark dirty for a delayed inhabitation test (see comment in 'mergeBots' as well)
+ MaybeBot -> markDirty y
+ _ -> id
+ return $
+ marked
+ (nabla1 & nabla_egr._class yid._data .~ Just vi')
+
+mergeBots :: Type
+ -- ^ The type of the pattern whose 'BotInfo's are being merged
+ -> BotInfo
+ -> BotInfo
+ -> MaybeT DsM BotInfo
+-- There already is x ~ ⊥. Nothing left to do
+mergeBots _ IsBot IsBot = pure IsBot
+-- There was x ≁ ⊥. Contradiction!
+mergeBots _ IsBot IsNotBot = mzero
+-- We add x ~ ⊥
+mergeBots t IsBot MaybeBot
+ | definitelyUnliftedType t
+ -- Case (3) in Note [Strict fields and variables of unlifted type]
+ -- (unlifted vars can never be ⊥)
+ = mzero
+ | otherwise
+ = pure IsBot
+-- There was x ~ ⊥. Contradiction!
+mergeBots _ IsNotBot IsBot = mzero
+-- There already is x ≁ ⊥. Nothing left to do
+mergeBots _ IsNotBot IsNotBot = pure IsNotBot
+-- We add x ≁ ⊥ and will need to test if x is still inhabited (see addNotBotCt)
+-- romes:todo: We don't have the dirty set in the e-graph, so
+-- congruence-fueled merging won't mark anything as dirty... hmm...
+mergeBots _ IsNotBot MaybeBot = pure IsNotBot
+-- Commutativity of 'mergeBots',
+-- and trivially merging MaybeBots
+mergeBots x MaybeBot IsBot = mergeBots x IsBot MaybeBot
+mergeBots x MaybeBot IsNotBot = mergeBots x IsNotBot MaybeBot
+mergeBots _ MaybeBot MaybeBot = pure MaybeBot
-- | 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
@@ -717,41 +769,44 @@ 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 nabla0 x nalt = do
+ (xid, nabla1) <- representId x nabla0
+ (mb_mark_dirty, nabla2) <- trvVarInfo (`mergeNotConCt` nalt) nabla1 (xid, x)
pure $ case mb_mark_dirty of
- Just x -> markDirty x nabla'
- Nothing -> 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
- -- 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))
- -- 2. Only record the new fact when it's not already implied by one of the
- -- solutions
- let implies nalt sol = eqPmAltCon (paca_con sol) nalt == Disjoint
- let neg'
- | any (implies nalt) pos = neg
- -- See Note [Completeness checking with required Thetas]
- | hasRequiredTheta nalt = neg
- | otherwise = extendPmAltConSet neg nalt
- massert (isPmAltConMatchStrict nalt)
- let vi' = vi{ vi_neg = neg', vi_bot = IsNotBot }
- -- 3. Make sure there's at least one other possible constructor
- mb_rcm' <- lift (markMatched nalt rcm)
- 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' })
- -- 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')
+ Just x -> markDirty x nabla2
+ Nothing -> nabla2
+
+-- 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`.
+mergeNotConCt :: VarInfo -> PmAltCon -> MaybeT DsM (Maybe Id, VarInfo)
+mergeNotConCt vi@(VI x' pos neg _ rcm) nalt = do
+ lift $ tracePm "mergeNotConCt vi nalt" (ppr vi <+> ppr nalt)
+ -- 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))
+ -- 2. Only record the new fact when it's not already implied by one of the
+ -- solutions
+ let implies nalt sol = eqPmAltCon (paca_con sol) nalt == Disjoint
+ let neg'
+ | any (implies nalt) pos = neg
+ -- See Note [Completeness checking with required Thetas]
+ | hasRequiredTheta nalt = neg
+ | otherwise = extendPmAltConSet neg nalt
+ massert (isPmAltConMatchStrict nalt)
+ let vi' = vi{ vi_neg = neg', vi_bot = IsNotBot }
+ -- 3. Make sure there's at least one other possible constructor
+ mb_rcm' <- lift (markMatched nalt rcm)
+ lift $ tracePm "mergeNotConCt vi' (no upd. rcm)" (ppr vi')
+ 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' })
+ -- 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')
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike cl) = notNull req_theta
@@ -759,6 +814,10 @@ hasRequiredTheta (PmAltConLike cl) = notNull req_theta
(_,_,_,_,req_theta,_,_) = conLikeFullSig cl
hasRequiredTheta _ = False
+-- | Worth making a lens from Nabla to EGraph, to make changing data operations much easier
+nabla_egr :: Functor f => (TmEGraph -> f TmEGraph) -> (Nabla -> f Nabla)
+nabla_egr f (MkNabla tyst ts at TmSt{ts_facts=egr}) = (\egr' -> MkNabla tyst ts{ts_facts=egr'}) <$> f egr
+
-- | Add a @x ~ K tvs args ts@ constraint.
-- @addConCt x K tvs args ts@ extends the substitution with a solution
-- @x :-> (K, tvs, args)@ if compatible with the negative and positive info we
@@ -766,8 +825,42 @@ 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
+addConCt nabla0 x alt tvs args = do
+ (xid, nabla1) <- representId x nabla0
+ let vi_x = lookupVarInfo (nabla_tm_st nabla1) x
+ (kid, nabla2) <- fromMaybe (xid, nabla1) <$> representPattern vi_x alt tvs args nabla1 -- VarInfo contains K data in pos info
+ let k_vi = (emptyVarInfo x){vi_pos=[PACA alt tvs args]}
+
+ nabla3 <- case (alt, args) of
+ (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc -> do
+ (_yid, nabla3) <- representId y nabla2
+
+ -- A newtype con and the underlying var are in the same e-class
+ -- nabla4 <- mergeVarIds xid yid nabla3
+
+ -- Return the nabla3 and set the k_vi unchanged
+ pure (nabla3 & nabla_egr._class kid._data .~ Just k_vi)
+
+ -- If the merging y and N y thing works, we won't need this.
+ -- (UPDT: It didn't work (looped, i Think. Try uncommenting that line above).
+ -- That means we're not currently moving the strictness information from the NT pattern to the underlying variable.
+ -- We need to.)
+ -- Also, if we do that manually here, that means we won't add strictness
+ -- annotations to underlying NT representatives if merging is done by
+ -- congruence instead of by manually calling 'addConCt'
+ -- case bot of
+ -- MaybeBot -> pure (nabla_with MaybeBot)
+ -- IsBot -> addBotCt (nabla_with IsBot) y
+ -- IsNotBot -> addNotBotCt (nabla_with IsNotBot) y
+
+ _ -> assert (isPmAltConMatchStrict alt)
+ -- Return the nabla2 and set the k_vi with additional IsNotBot info
+ pure (nabla2 & nabla_egr._class kid._data .~ Just k_vi{vi_bot=IsNotBot}) -- strict match ==> not ⊥
+
+ mergeVarIds xid kid nabla3
+
+mergeConCt :: VarInfo -> PmAltConApp -> StateT TyState (MaybeT DsM) VarInfo
+mergeConCt vi@(VI _ pos neg _bot _) paca@(PACA alt tvs _args) = StateT $ \tyst -> do
-- 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
@@ -777,25 +870,19 @@ addConCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x alt tvs args =
-- Now we should be good! Add (alt, tvs, args) as a possible solution, or
-- refine an existing one
case find ((== Equal) . eqPmAltCon alt . paca_con) pos of
- Just (PACA _con other_tvs other_args) -> do
+ Just (PACA _con other_tvs _other_args) -> do
-- We must unify existentially bound ty vars and arguments!
+ --
+ -- The arguments are handled automatically by representing K in
+ -- the e-class...! all equivalent things will be merged.
+ --
+ -- So we treat the ty vars:
let ty_cts = equateTys (map mkTyVarTy tvs) (map mkTyVarTy other_tvs)
- nabla' <- MaybeT $ addPhiCts nabla (listToBag ty_cts)
- let add_var_ct nabla (a, b) = addVarCt nabla a b
- foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args
+ tyst' <- MaybeT (tyOracle tyst (listToBag $ map (\case (PhiTyCt pred) -> pred; _ -> error "impossible") ty_cts))
+ return (vi, tyst') -- All good, and we get no new term information.
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'})} }
- -- Do (2) in Note [Coverage checking Newtype matches]
- case (alt, args) of
- (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
- case bot of
- MaybeBot -> pure (nabla_with MaybeBot)
- IsBot -> addBotCt (nabla_with MaybeBot) y
- IsNotBot -> addNotBotCt (nabla_with MaybeBot) y
- _ -> assert (isPmAltConMatchStrict alt )
- pure (nabla_with IsNotBot) -- strict match ==> not ⊥
+ -- Add new con info
+ return (vi{vi_pos = paca:pos}, tyst)
equateTys :: [Type] -> [Type] -> [PhiCt]
equateTys ts us =
@@ -815,18 +902,22 @@ equateTys ts us =
--
-- See Note [TmState invariants].
addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
-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' } })
- -- 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'} }
- -- 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
- nabla_pos <- foldlM add_pos nabla_equated (vi_pos vi_x)
- -- 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))
+addVarCt nabla0 x y = do
+
+ -- We'd really rather ([xid, yid], nabla1) <- representIds [x,y] nabla0, but that's not exhaustive...
+ ((xid, yid), nabla1)
+ <- runStateT ((,) <$> StateT (representId x) <*> StateT (representId y)) nabla0
+
+ mergeVarIds xid yid nabla1
+
+mergeVarIds :: ClassId -> ClassId -> Nabla -> MaybeT DsM Nabla
+mergeVarIds xid yid (MkNabla tyst0 (TmSt egr0 is)) = do
+
+ -- @merge env x y@ makes @x@ and @y@ point to the same entry,
+ -- thereby merging @x@'s class with @y@'s.
+ (egr1, tyst1) <- runStateT (EG.mergeM xid yid egr0 >>= EG.rebuildM . snd) tyst0
+
+ return (MkNabla tyst1 (TmSt egr1 is))
-- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
-- on the shape of the 'CoreExpr' @e at . Examples:
@@ -894,9 +985,11 @@ addCoreCt nabla x e = do
-- @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)
+ rep <- StateT $ \nabla -> representCoreExpr nabla e
-- Note that @rep == x@ if we encountered @e@ for the first time.
- modifyT (\nabla -> addVarCt nabla x rep)
+ modifyT (\nabla0 -> do
+ (xid, nabla1) <- representId x nabla0
+ mergeVarIds xid rep nabla1)
bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id
bind_expr e = do
@@ -951,14 +1044,13 @@ 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')
+representCoreExpr :: Nabla -> CoreExpr -> MaybeT DsM (ClassId, Nabla)
+representCoreExpr (MkNabla tyst ts at TmSt{ ts_facts = egraph }) e = do
+ ((xid, egr''), tysty') <- (`runStateT` tyst) $ do
+ (xid, egr') <- representCoreExprEgr key egraph
+ egr'' <- EG.rebuildM egr'
+ return (xid, egr'')
+ return (xid, MkNabla tysty' ts{ts_facts = egr''})
where
key = makeDictsCoherent e
-- Use a key in which dictionaries for the same type become equal.
@@ -969,6 +1061,8 @@ representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_reps = reps } } e
-- 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
@@ -1271,21 +1365,30 @@ tyStateRefined a b = ty_st_n a /= ty_st_n b
markDirty :: Id -> 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 } }
+ case lookupId ts x of
+ Nothing -> error "Marking as dirty an Id that is not represented in the Nabla"
+ Just xid ->
+ nabla{ nabla_tm_st = ts{ ts_dirty = IS.insert xid dirty } }
traverseDirty :: Monad m => (VarInfo -> m 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 (xid:xs) !env = do
+ vi' <- f' (env ^._class xid._data)
+ go xs (env & _class xid._data .~ vi')
+
+ f' Nothing = pure Nothing
+ f' (Just x) = Just <$> f x
traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll f ts at TmSt{ts_facts = env} = do
- env' <- traverseUSDFM f env
+ env' <- (_classes._data) f' env
pure ts{ts_facts = env'}
+ where
+ f' Nothing = pure Nothing
+ f' (Just x) = Just <$> f x
-- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate
-- all dirty variables (or all variables when the 'TyState' changed) to concrete
@@ -1296,48 +1399,50 @@ traverseAll f ts at TmSt{ts_facts = env} = do
inhabitationTest :: Int -> TyState -> Nabla -> MaybeT DsM Nabla
inhabitationTest 0 _ nabla = pure nabla
inhabitationTest fuel old_ty_st nabla at MkNabla{ nabla_tm_st = ts } = {-# SCC "inhabitationTest" #-} do
- -- lift $ tracePm "inhabitation test" $ vcat
- -- [ ppr fuel
- -- , ppr old_ty_st
- -- , ppr nabla
- -- , text "tyStateRefined:" <+> ppr (tyStateRefined old_ty_st (nabla_ty_st nabla))
- -- ]
+ lift $ tracePm "inhabitation test" $ vcat
+ [ ppr fuel
+ , ppr old_ty_st
+ , ppr nabla
+ , text "tyStateRefined:" <+> ppr (tyStateRefined old_ty_st (nabla_ty_st nabla))
+ ]
-- When type state didn't change, we only need to traverse dirty VarInfos
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} }
+ nabla_not_dirty = nabla{ nabla_tm_st = ts{ts_dirty=IS.empty} }
test_one :: VarInfo -> MaybeT DsM VarInfo
- test_one vi =
+ test_one vi = do
lift (varNeedsTesting old_ty_st nabla vi) >>= \case
True -> do
- -- lift $ tracePm "test_one" (ppr vi)
+ 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
+ _ -> do
+ lift $ tracePm "test_one needs no testing" (ppr vi)
+ pure vi
-- | 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
- | notNull (vi_pos vi) = pure False
-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
- -- 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)
- (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (idType $ vi_id vi)
- if old_norm_ty `eqType` new_norm_ty
- then pure False
- else pure True
+varNeedsTesting old_ty_st n at MkNabla{nabla_ty_st=new_ty_st,nabla_tm_st=tm_st} vi
+ = do
+ Just (xid, _) <- runMaybeT $ representId (vi_id vi) n
+ if | IS.member xid (IS.map (`EG.find` ts_facts tm_st) $ ts_dirty tm_st) -> pure True
+ | notNull (vi_pos vi) -> pure False
+ -- Same type state => still inhabited
+ | not (tyStateRefined old_ty_st new_ty_st) -> pure False
+ -- These normalisations are relatively expensive, but still better than having
+ -- to perform a full inhabitation test
+ | otherwise -> do
+ (_, _, old_norm_ty) <- tntrGuts <$> pmTopNormaliseType old_ty_st (idType $ vi_id vi)
+ (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (idType $ vi_id vi)
+ if old_norm_ty `eqType` new_norm_ty
+ then pure False
+ else pure True
-- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE
-- set satisfies the oracle
@@ -1358,8 +1463,10 @@ 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 } x
+ = case lookupId ts x of
+ Just xid -> trvVarInfo add_matches nabla (xid, x)
+ Nothing -> error "An Id with a VarInfo (see call site) is not represented in the e-graph..."
where
add_matches vi at VI{ vi_rcm = rcm }
-- important common case, shaving down allocations of PmSeriesG by -5%
@@ -2080,3 +2187,135 @@ 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'.
-}
+
+------------------------------------------------
+-- * E-graphs for pattern match checking
+
+representPattern :: VarInfo
+ -- ^ Var info of e-class in which this pattern is going to be represented...
+ -- The things we are doing with this should rather be done as
+ -- an e-graph analysis modify to "downwards" merge in the e-graph the sub-nodes
+ -- A bit weird that the e-graph doesn't do this, but it seems like it doesn't... (see egraphs zulip discussion)
+ -> PmAltCon -> [TyVar] -> [Id] -> Nabla -> MaybeT DsM (Maybe (ClassId, Nabla))
+-- We don't need to do anything in the case of PmAltLit.
+-- The Constructor information is recorded in the positive info e-class
+-- it is represented in, so when we merge we take care of handling this
+-- equality right.
+-- If we did this even more ideally, we'd just represent PmAltLit in the e-graph and it would fail on merge without having to edit the e-class.
+-- Wait, is it even safe to edit the e-class? Won't that *NOT* trigger the merging??
+-- Here I suppose we're creating the e-class. So we can add information at will. When we eventually merge this class with another one, we can do things.
+-- But we could definitely check whether the information we're adding isn't colliding with the existing one.
+representPattern _ (PmAltLit _) _ _ _ = return Nothing
+ -- We might need represent patterns alongside expressions -- then we can use the "real" equality instances for the patterns (e.g. eqPmLit)
+representPattern (VI _ pos _ _ _) alt@(PmAltConLike conLike) tvs args nab00 = do
+ (args', nab01) <- representIds args nab00
+
+ -- rOMES: It is very akward that this is being done here... perhaps it would be best as a modify method in the analysis
+ -- it certainly won't work for things we learn by congruence...
+ MkNabla tyst0 ts at TmSt{ts_facts=egr0} <-
+ case find ((== Equal) . eqPmAltCon alt . paca_con) pos of
+ Just (PACA _con _other_tvs other_args) -> do
+ let add_var_ct nabla (a, b) = addVarCt nabla a b
+ foldlM add_var_ct nab01 $ zipEqual "addConCt" args other_args
+ Nothing -> pure nab01
+
+ ((cid, egr1), tyst1) <- (`runStateT` tyst0) $ EGM.runEGraphMT egr0 $ do
+ -- We must represent the constructor application in the e-graph to make
+ -- sure the children are recursively merged against other children of
+ -- other constructors represneted in the same e-class.
+ -- We need to represent the constructor correctly to ensure existing
+ -- constructors match or not the new one
+ -- dsHsConLike basically implements the logic we want.
+ -- ROMES:TODO: Nevermind, the dsHsConLike won't work because we want to
+ -- talk about pattern synonyms in their "matching" form, and converting
+ -- them with dsHsConLike assumes they are used as a constructor,
+ -- meaning we will fail for unidirectional patterns
+ desugaredCon <- lift . lift . lift $ ds_hs_con_like_pat conLike -- DsM action to desugar the conlike into the expression we'll represent for this constructor
+ conLikeId <- StateT $ representCoreExprEgr desugaredCon
+ tvs' <- mapM (EGM.addM . EG.Node . TypeF . DBT . deBruijnize . TyVarTy) tvs -- ugh...
+ foldlM (\acc i -> EGM.addM (EG.Node $ AppF acc i)) conLikeId (tvs' ++ args')
+ return (Just (cid, MkNabla tyst1 ts{ts_facts=egr1}))
+ where
+ -- TODO: do something cleaner than the following inlined thing...
+
+ -- We inlined dsHsConLike but use patSynMatcher instead of patSynBuilder
+ ds_hs_con_like_pat :: ConLike -> DsM CoreExpr
+ ds_hs_con_like_pat (RealDataCon dc)
+ = return (varToCoreExpr (dataConWrapId dc))
+ ds_hs_con_like_pat (PatSynCon ps)
+ | (builder_name, _, add_void) <- patSynMatcher ps
+ = do { builder_id <- dsLookupGlobalId builder_name
+ ; return (if add_void
+ then mkCoreApp (text "dsConLike" <+> ppr ps)
+ (Var builder_id) unboxedUnitExpr
+ else Var builder_id) }
+
+representId :: Id -> Nabla -> MaybeT DsM (ClassId, Nabla)
+representId x (MkNabla tyst tmst at TmSt{ts_facts=eg0})
+ = do
+ ((xid, tmst'),tyst') <- (`runStateT` tyst) $ do
+ (xid, eg1) <- EG.addM (EG.Node (FreeVarF x)) eg0
+ eg2 <- EG.rebuildM eg1 -- why do this here? I guess a good place as any, and should be cheap anyway (workload is not something like eqsat)
+ return (xid, tmst{ts_facts=eg2})
+ return (xid, MkNabla tyst' tmst')
+
+representIds :: [Id] -> Nabla -> MaybeT DsM ([ClassId], Nabla)
+representIds xs = runStateT (mapM (StateT . representId) xs)
+
+-- There are too many cycles for this to be in Solver.Types...
+-- We need the TyState to check insoluble constraints while merging VarInfos
+instance Analysis (StateT TyState (MaybeT DsM)) (Maybe VarInfo) ExprF where
+ {-# INLINE makeA #-}
+
+ -- When an e-class is created for a variable, we create an VarInfo from it.
+ -- It doesn't matter if this variable is bound or free, since it's the first
+ -- variable in this e-class (and all others would have to be equivalent to
+ -- it)
+ --
+ -- Also, the Eq instance for DeBruijn Vars will ensure that two free
+ -- variables with the same Id are equal and so they will be represented in
+ -- the same e-class
+ --
+ -- It would be good if we didn't do this always... It might be a bit expensive
+ makeA (FreeVarF x) = pure $ Just $ emptyVarInfo x
+ makeA _ = pure $ Nothing
+
+ joinA Nothing Nothing = pure $ Nothing
+ joinA Nothing (Just b) = pure $ Just b
+ joinA (Just a) Nothing = pure $ Just a
+
+ -- Merge the 'VarInfo's from @x@ and @y@
+ joinA (Just vi_x at VI{ vi_id=_id_x
+ , vi_pos=pos_x
+ , vi_neg=neg_x
+ , vi_bot=bot_x
+ , vi_rcm=_rcm_x
+ })
+ (Just vi_y) = do
+ lift . lift $ tracePm "merging vi_x and vi_y" (ppr vi_x <+> ppr vi_y)
+ -- If we can merge x ~ N y with y too, then we no longer need to worry
+ -- about propagating the bottomness information, since it will always be
+ -- right... though I'm not sure if that would be correct
+
+ -- Gradually merge every positive fact we have on x into y
+ -- The args are merged by congruence, since we represent the
+ -- constructor in the e-graph in addConCt.
+ vi_res1 <- foldlM mergeConCt vi_y pos_x
+
+ -- Do the same for negative info
+ let add_neg vi nalt = lift $ snd <$> mergeNotConCt vi nalt
+ vi_res2 <- foldlM add_neg vi_res1 (pmAltConSetElems neg_x)
+
+ -- We previously were not merging the bottom information, but now we do.
+ -- TODO: We don't need to do it yet if we are only trying to be as good as before, but not better
+ -- Although it might not be so simple if we consider one of the classes is a newtype?
+ -- (No, I think that situation can occur)
+ bot_res <- lift $
+ mergeBots (idType (vi_id vi_res2))
+ bot_x (vi_bot vi_y)
+ let vi_res3 = vi_res2{vi_bot = bot_res}
+
+ lift . lift $ tracePm "result of merging vi_x and vi_y" (ppr vi_res3)
+ return (Just vi_res3)
+
+
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,7 +1,11 @@
{-# LANGUAGE ApplicativeDo #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
-- | Domain types used in "GHC.HsToCore.Pmc.Solver".
-- The ultimate goal is to define 'Nabla', which models normalised refinement
@@ -10,13 +14,16 @@
module GHC.HsToCore.Pmc.Solver.Types (
-- * Normalised refinement types
- BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
- Nabla(..), Nablas(..), initNablas,
+ BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..), TmEGraph,
+ Nabla(..), Nablas(..), initNablas, emptyVarInfo,
lookupRefuts, lookupSolution,
-- ** Looking up 'VarInfo'
lookupVarInfo, lookupVarInfoNT, trvVarInfo,
+ -- *** Looking up 'ClassId'
+ lookupId,
+
-- ** Caching residual COMPLETE sets
CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
@@ -42,9 +49,7 @@ import GHC.Prelude
import GHC.Data.Bag
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.DataCon
import GHC.Core.ConLike
@@ -58,7 +63,6 @@ import GHC.Core.TyCon
import GHC.Types.Literal
import GHC.Core
import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Map.Expr
import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
@@ -75,6 +79,18 @@ import Data.Ratio
import GHC.Real (Ratio(..))
import qualified Data.Semigroup as Semi
+import GHC.Core.Equality
+import Data.Functor.Const
+import Data.Functor.Compose
+import Data.Equality.Graph (EGraph, ClassId)
+import Data.Equality.Graph.Lens
+import qualified Data.Equality.Graph.Nodes as EGN
+import qualified Data.Equality.Graph as EG
+import qualified Data.Equality.Graph.Internal as EGI
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IS (empty, toList)
+import Data.Bifunctor (second)
+
-- import GHC.Driver.Ppr
--
@@ -138,14 +154,12 @@ initTyState = TySt 0 emptyInert
-- 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 term variables.
+
+ -- ROMES:TODO: ts_dirty looks a bit to me like the bookkeeping done by the
+ -- analysis rebuilding mechanism, so 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@).
}
@@ -161,6 +175,7 @@ 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: Do we still need this?
, vi_pos :: ![PmAltConApp]
-- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
@@ -168,7 +183,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.
@@ -227,7 +242,13 @@ instance Outputable BotInfo where
-- | Not user-facing.
instance Outputable TmState where
- ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
+ ppr (TmSt state dirty) =
+ (vcat $ getConst $ _iclasses (\(i,cl) -> Const [ppr i <> text ":" <+> ppr cl]) state)
+ $$ ppr (IS.toList dirty)
+
+
+instance Outputable (EG.EClass (Maybe VarInfo) CoreExprF) where
+ ppr cl = ppr (cl^._nodes) $$ ppr (cl^._data)
-- | Not user-facing.
instance Outputable VarInfo where
@@ -248,7 +269,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
@@ -302,7 +323,9 @@ emptyVarInfo x
lookupVarInfo :: TmState -> Id -> VarInfo
-- (lookupVarInfo tms x) tells what we know about 'x'
-lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
+lookupVarInfo ts@(TmSt env _) x = fromMaybe (emptyVarInfo x) $ do
+ xid <- lookupId ts x
+ env ^. _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
@@ -324,12 +347,27 @@ lookupVarInfoNT ts x = case lookupVarInfo ts x of
| isNewDataCon dc = Just y
go _ = Nothing
-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
- = set_vi <$> f (lookupVarInfo ts x)
+trvVarInfo :: forall f a. Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla
+ -> (ClassId,Id)
+ -- ^ The ClassId of the VarInfo to traverse, and the Id represented
+ -- to get it, to determine the empty var info in case it isn't available.
+ -- ... Feels a bit weird, but let's see if it works at all
+ -> f (a, Nabla)
+trvVarInfo f nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts = env} } (xid,x)
+ = second (\g -> nabla{nabla_tm_st = ts{ts_facts=g}}) <$>
+ updateAccum (_class xid._data.defaultEmpty) f env
where
- set_vi (a, vi') =
- (a, nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env (vi_id vi') vi' } })
+ 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)
+
+ defaultEmpty :: Lens' (Maybe VarInfo) VarInfo
+ defaultEmpty f s = Just <$> (f (fromMaybe (emptyVarInfo x) s))
+
+------------------------------------------
+-- * Utility for looking up Ids in 'Nabla'
+
+lookupId :: TmState -> Id -> Maybe ClassId
+lookupId TmSt{ts_facts = eg0} x = EGN.lookupNM (EG.Node (FreeVarF x)) (EGI.memo eg0)
------------------------------------------------
-- * Exported utility functions querying 'Nabla'
@@ -797,3 +835,19 @@ instance Outputable PmAltCon where
instance Outputable PmEquality where
ppr = text . show
+
+-----------------------------------------------------
+-- * E-graphs to represent normalised refinment types
+
+type TmEGraph = EGraph (Maybe VarInfo) CoreExprF
+
+-- TODO delete orphans for showing TmEGraph for debugging reasons
+instance Show VarInfo where
+ show = showPprUnsafe . ppr
+
+-- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
+-- There ought to be a better way.
+-- ROMES:TODO:
+instance Eq VarInfo where
+ (==) a b = vi_id a == vi_id b -- ROMES:TODO: The rest of the equality comparisons
+
=====================================
compiler/GHC/Types/Unique/SDFM.hs deleted
=====================================
@@ -1,121 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ApplicativeDo #-}
-{-# OPTIONS_GHC -Wall #-}
-
--- | Like a 'UniqDFM', but maintains equivalence classes of keys sharing the
--- same entry. See 'UniqSDFM'.
-module GHC.Types.Unique.SDFM (
- -- * Unique-keyed, /shared/, deterministic mappings
- UniqSDFM,
-
- emptyUSDFM,
- lookupUSDFM,
- equateUSDFM, addToUSDFM,
- traverseUSDFM
- ) where
-
-import GHC.Prelude
-
-import GHC.Types.Unique
-import GHC.Types.Unique.DFM
-import GHC.Utils.Outputable
-
--- | Either @Indirect x@, meaning the value is represented by that of @x@, or
--- an @Entry@ containing containing the actual value it represents.
-data Shared key ele
- = Indirect !key
- | Entry !ele
-
--- | A 'UniqDFM' whose domain is /sets/ of 'Unique's, each of which share a
--- common value of type @ele at .
--- Every such set (\"equivalence class\") has a distinct representative
--- 'Unique'. Supports merging the entries of multiple such sets in a union-find
--- like fashion.
---
--- An accurate model is that of @[(Set key, Maybe ele)]@: A finite mapping from
--- sets of @key at s to possibly absent entries @ele@, where the sets don't overlap.
--- Example:
--- @
--- m = [({u1,u3}, Just ele1), ({u2}, Just ele2), ({u4,u7}, Nothing)]
--- @
--- On this model we support the following main operations:
---
--- * @'lookupUSDFM' m u3 == Just ele1@, @'lookupUSDFM' m u4 == Nothing@,
--- @'lookupUSDFM' m u5 == Nothing at .
--- * @'equateUSDFM' m u1 u3@ is a no-op, but
--- @'equateUSDFM' m u1 u2@ merges @{u1,u3}@ and @{u2}@ to point to
--- @Just ele2@ and returns the old entry of @{u1,u3}@, @Just ele1 at .
--- * @'addToUSDFM' m u3 ele4@ sets the entry of @{u1,u3}@ to @Just ele4 at .
---
--- As well as a few means for traversal/conversion to list.
-newtype UniqSDFM key ele
- = USDFM { unUSDFM :: UniqDFM key (Shared key ele) }
-
-emptyUSDFM :: UniqSDFM key ele
-emptyUSDFM = USDFM emptyUDFM
-
-lookupReprAndEntryUSDFM :: Uniquable key => UniqSDFM key ele -> key -> (key, Maybe ele)
-lookupReprAndEntryUSDFM (USDFM env) = go
- where
- go x = case lookupUDFM env x of
- Nothing -> (x, Nothing)
- Just (Indirect y) -> go y
- Just (Entry ele) -> (x, Just ele)
-
--- | @lookupSUDFM env x@ looks up an entry for @x@, looking through all
--- 'Indirect's until it finds a shared 'Entry'.
---
--- Examples in terms of the model (see 'UniqSDFM'):
--- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 == Just ele1
--- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Just ele2)] u4 == Nothing
--- >>> lookupUSDFM [({u1,u3}, Just ele1), ({u2}, Nothing)] u2 == Nothing
-lookupUSDFM :: Uniquable key => UniqSDFM key ele -> key -> Maybe ele
-lookupUSDFM usdfm x = snd (lookupReprAndEntryUSDFM usdfm x)
-
--- | @equateUSDFM 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'):
--- >>> equateUSDFM [] u1 u2 == (Nothing, [({u1,u2}, Nothing)])
--- >>> 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)])
-equateUSDFM
- :: Uniquable key => UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele)
-equateUSDFM usdfm@(USDFM env) x y =
- case (lu x, lu y) of
- ((x', _) , (y', _))
- | getUnique x' == getUnique y' -> (Nothing, usdfm) -- nothing to do
- ((x', _) , (y', Nothing)) -> (Nothing, set_indirect y' x')
- ((x', mb_ex), (y', _)) -> (mb_ex, set_indirect x' y')
- where
- lu = lookupReprAndEntryUSDFM usdfm
- set_indirect a b = USDFM $ addToUDFM env a (Indirect b)
-
--- | @addToUSDFM env x a@ sets the entry @x@ is associated with to @a@,
--- thereby modifying its whole equivalence class.
---
--- Examples in terms of the model (see 'UniqSDFM'):
--- >>> addToUSDFM [] u1 ele1 == [({u1}, Just ele1)]
--- >>> addToUSDFM [({u1,u3}, Just ele1)] u3 ele2 == [({u1,u3}, Just ele2)]
-addToUSDFM :: Uniquable key => UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
-addToUSDFM usdfm@(USDFM env) x v =
- USDFM $ addToUDFM env (fst (lookupReprAndEntryUSDFM usdfm x)) (Entry v)
-
-traverseUSDFM :: forall key a b f. Applicative f => (a -> f b) -> UniqSDFM key a -> f (UniqSDFM key b)
-traverseUSDFM f = fmap (USDFM . listToUDFM_Directly) . traverse g . udfmToList . unUSDFM
- where
- g :: (Unique, Shared key a) -> f (Unique, Shared key b)
- g (u, Indirect y) = pure (u,Indirect y)
- g (u, Entry a) = do
- a' <- f a
- pure (u,Entry a')
-
-instance (Outputable key, Outputable ele) => Outputable (Shared key ele) where
- ppr (Indirect x) = ppr x
- ppr (Entry a) = ppr a
-
-instance (Outputable key, Outputable ele) => Outputable (UniqSDFM key ele) where
- ppr (USDFM env) = ppr env
=====================================
compiler/ghc.cabal.in
=====================================
@@ -114,6 +114,7 @@ Library
filepath >= 1 && < 1.5,
template-haskell == 2.21.*,
hpc >= 0.6 && < 0.8,
+ hegg,
transformers >= 0.5 && < 0.7,
exceptions == 0.10.*,
semaphore-compat,
@@ -328,6 +329,7 @@ Library
GHC.Core.ConLike
GHC.Core.DataCon
GHC.Core.FamInstEnv
+ GHC.Core.Equality
GHC.Core.FVs
GHC.Core.InstEnv
GHC.Core.Lint
@@ -865,7 +867,6 @@ Library
GHC.Types.Unique.FM
GHC.Types.Unique.Map
GHC.Types.Unique.MemoFun
- GHC.Types.Unique.SDFM
GHC.Types.Unique.Set
GHC.Types.Unique.Supply
GHC.Types.Var
=====================================
hadrian/src/Packages.hs
=====================================
@@ -6,7 +6,7 @@ module Packages (
compareSizes, compiler, containers, deepseq, deriveConstants, directory, dumpDecls,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh, ghcPlatform,
ghcCompact, ghcConfig, ghcExperimental, ghcHeap, ghcInternal, ghci, ghciWrapper, ghcPkg, ghcPrim,
- ghcToolchain, ghcToolchainBin, haddock, haskeline,
+ ghcToolchain, ghcToolchainBin, haddock, haskeline, 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,
@@ -39,7 +39,7 @@ ghcPackages =
, compareSizes, compiler, containers, deepseq, deriveConstants, directory, dumpDecls
, exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh, ghcPlatform
, ghcCompact, ghcConfig, ghcExperimental, ghcHeap, ghcInternal, ghci, ghciWrapper, ghcPkg, ghcPrim
- , ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs
+ , ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs, hegg
, 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
@@ -56,7 +56,7 @@ array, base, binary, bytestring, cabalSyntax, cabal, checkPpr, checkExact, count
compareSizes, compiler, containers, deepseq, deriveConstants, directory, dumpDecls,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh, ghcPlatform,
ghcCompact, ghcConfig, ghcExperimental, ghcHeap, ghci, ghcInternal, ghciWrapper, ghcPkg, ghcPrim,
- ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs,
+ ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs, hegg,
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,
@@ -102,6 +102,7 @@ ghcToolchain = lib "ghc-toolchain" `setPath` "utils/ghc-toolchain"
ghcToolchainBin = prg "ghc-toolchain-bin" `setPath` "utils/ghc-toolchain/exe" -- workaround for #23690
haddock = util "haddock"
haskeline = lib "haskeline"
+hegg = lib "hegg"
hsc2hs = util "hsc2hs"
hp2ps = util "hp2ps"
hpc = lib "hpc"
=====================================
hadrian/src/Rules/ToolArgs.hs
=====================================
@@ -165,6 +165,7 @@ toolTargets = [ binary
, ghci
, ghcPkg -- # executable
-- , haddock -- # depends on ghc library
+ , hegg
, hsc2hs -- # executable
, hpc
, hpcBin -- # executable
=====================================
hadrian/src/Settings/Default.hs
=====================================
@@ -99,6 +99,7 @@ stage0Packages = do
, ghci
, ghcPkg
, haddock
+ , hegg
, hsc2hs
, hpc
, hpcBin
@@ -149,6 +150,7 @@ stage1Packages = do
, ghcPkg
, ghcPrim
, haskeline
+ , hegg
, hp2ps
, hsc2hs
, integerGmp
=====================================
libraries/hegg
=====================================
@@ -0,0 +1 @@
+Subproject commit e124cb2a999c0058b6cca283142ac18b289416f2
=====================================
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
=====================================
testsuite/tests/count-deps/CountDepsParser.stdout
=====================================
@@ -21,11 +21,11 @@ GHC.Core.Coercion.Axiom
GHC.Core.Coercion.Opt
GHC.Core.ConLike
GHC.Core.DataCon
+GHC.Core.Equality
GHC.Core.FVs
GHC.Core.FamInstEnv
GHC.Core.InstEnv
GHC.Core.Make
-GHC.Core.Map.Expr
GHC.Core.Map.Type
GHC.Core.Multiplicity
GHC.Core.Opt.Arity
@@ -194,7 +194,6 @@ GHC.Types.Unique.DFM
GHC.Types.Unique.DSet
GHC.Types.Unique.FM
GHC.Types.Unique.Map
-GHC.Types.Unique.SDFM
GHC.Types.Unique.Set
GHC.Types.Unique.Supply
GHC.Types.Var
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/1917b37fc1df990caf61fbda0a05dddfc9775914...af60b03e6638d951282f59eab14b92da5046192a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/1917b37fc1df990caf61fbda0a05dddfc9775914...af60b03e6638d951282f59eab14b92da5046192a
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/20240502/534f318e/attachment-0001.html>
More information about the ghc-commits
mailing list