[Git][ghc/ghc][wip/romes/eqsat-pmc] 15 commits: Add e-graphs submodule (hegg)
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Mon Jul 3 00:34:51 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
435b3d8b by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Add e-graphs submodule (hegg)
- - - - -
b9753941 by Rodrigo Mesquita at 2023-07-03T01:34:10+01: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.
- - - - -
f2423412 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Question
- - - - -
0a7c6086 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Was going great until I started needing to thread ClassIds together with Ids. Ret-think this.
- - - - -
584927f3 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
A solution with more lookups
- - - - -
de53fb4c by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Fixes to Pmc.Ppr module
- - - - -
8d388828 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Wow, a lot (stage1) is working actually, without PMC errprs
- - - - -
ca3ef188 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
We're still not there yet.
- - - - -
37e057e2 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
WiP
- - - - -
940b9d44 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Add instances for debugging
- - - - -
d30c27f5 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Things that were broken due to unlawfulness of e-graph instances
- - - - -
71836c72 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Scuffed merging without effects to salvage some information that might get lost in merging that happens outside of addVarCt
- - - - -
88a82772 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Improve a little bit the mixing of Ids and ClassIds
- - - - -
5b375081 by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
Drop SDFM module
- - - - -
9d2039ee by Rodrigo Mesquita at 2023-07-03T01:34:10+01:00
tWeaks
- - - - -
23 changed files:
- .gitmodules
- + compiler/GHC/Core/Equality.hs
- compiler/GHC/Core/Map/Expr.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/HsToCore/Errors/Ppr.hs
- compiler/GHC/HsToCore/Errors/Types.hs
- compiler/GHC/HsToCore/Pmc.hs
- compiler/GHC/HsToCore/Pmc/Check.hs
- compiler/GHC/HsToCore/Pmc/Desugar.hs
- compiler/GHC/HsToCore/Pmc/Ppr.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- compiler/GHC/Types/Hint.hs
- compiler/GHC/Types/TyThing/Ppr.hs-boot
- − 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/CountDepsAst.stdout
- 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
=====================================
compiler/GHC/Core/Equality.hs
=====================================
@@ -0,0 +1,384 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module GHC.Core.Equality where
+
+-- ROMES:TODO:
+-- I think, for the particular usages of Core e-graphs, we can do much better
+-- than this for equality.
+-- E.g. representation could transform the CoreExpr to an actual debruijnized one (with Ints for Vars)
+
+import GHC.Exts (dataToTag#, tagToEnum#, (>#), (<#))
+import GHC.Prelude
+
+import GHC.Core
+import GHC.Core.TyCo.Rep
+import GHC.Core.Map.Type
+import GHC.Core.Map.Expr
+import GHC.Types.Var
+import GHC.Types.Literal
+import GHC.Types.Tickish
+import Unsafe.Coerce (unsafeCoerce)
+
+import Control.Monad.Trans.State.Strict (state)
+import Data.Equality.Graph as EG
+import Data.Equality.Analysis
+import qualified Data.Equality.Graph.Monad as EGM
+import Data.Equality.Utils (Fix(..))
+
+import GHC.Utils.Misc (all2)
+import GHC.Utils.Outputable
+import GHC.Core.Coercion (coercionType)
+
+-- 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
+
+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
+type CoreAltF
+ = AltF CoreBndr
+type CoreBindF
+ = BindF CoreBndr
+
+newtype DeBruijnF f a = DF (DeBruijn (f a))
+ deriving (Functor, Foldable, Traversable)
+
+eqDeBruijnExprF :: forall a. Eq a => DeBruijn (CoreExprF a) -> DeBruijn (CoreExprF a) -> Bool
+eqDeBruijnExprF (D env1 e1) (D env2 e2) = go e1 e2 where
+ go :: CoreExprF a -> CoreExprF a -> Bool
+ go (VarF v1) (VarF v2) = eqDeBruijnVar (D env1 v1) (D env2 v2)
+ go (LitF lit1) (LitF lit2) = lit1 == lit2
+ go (TypeF t1) (TypeF t2) = eqDeBruijnType (D env1 t1) (D env2 t2)
+ -- See Note [Alpha-equality for Coercion arguments]
+ go (CoercionF {}) (CoercionF {}) = True
+ go (CastF e1 co1) (CastF e2 co2) = D env1 co1 == D env2 co2 && e1 == e2
+ go (AppF f1 a1) (AppF f2 a2) = f1 == f2 && a1 == a2
+ go (TickF n1 e1) (TickF n2 e2)
+ = eqDeBruijnTickish (D env1 n1) (D env2 n2)
+ && e1 == e2
+
+ go (LamF b1 e1) (LamF b2 e2)
+ = eqDeBruijnType (D env1 (varType b1)) (D env2 (varType b2))
+ && D env1 (varMultMaybe b1) == D env2 (varMultMaybe b2)
+ && e1 == e2
+
+ go (LetF abs e1) (LetF bbs e2)
+ = D env1 abs == D env2 bbs
+ && e1 == e2
+
+ go (CaseF e1 _b1 t1 a1) (CaseF e2 _b2 t2 a2)
+ | null a1 -- See Note [Empty case alternatives]
+ = null a2 && e1 == e2 && D env1 t1 == D env2 t2
+ | otherwise
+ = e1 == e2 && D env1 a1 == D env2 a2
+
+ go _ _ = False
+
+-- ROMES:TODO: This one can be derived automatically, but perhaps it's better
+-- to be explicit here? We don't even really require the DeBruijn context here
+eqDeBruijnAltF :: forall a. Eq a => DeBruijn (CoreAltF a) -> DeBruijn (CoreAltF a) -> Bool
+eqDeBruijnAltF (D _env1 a1) (D _env2 a2) = go a1 a2 where
+ go (AltF DEFAULT _ rhs1) (AltF DEFAULT _ rhs2)
+ = rhs1 == rhs2
+ go (AltF (LitAlt lit1) _ rhs1) (AltF (LitAlt lit2) _ rhs2)
+ = lit1 == lit2 && rhs1 == rhs2
+ go (AltF (DataAlt dc1) _bs1 rhs1) (AltF (DataAlt dc2) _bs2 rhs2)
+ = dc1 == dc2 &&
+ rhs1 == rhs2 -- the CM environments were extended on representation (see 'representDBAltExpr')
+ go _ _ = False
+
+-- | 'unsafeCoerce' mostly because I'm too lazy to write the boilerplate.
+fromCoreExpr :: CoreExpr -> Fix CoreExprF
+fromCoreExpr = unsafeCoerce
+
+toCoreExpr :: CoreExpr -> Fix CoreExprF
+toCoreExpr = unsafeCoerce
+
+-- | Represents a DeBruijn CoreExpr being careful to correctly debruijnizie the expression as it is represented
+--
+-- Always represent Ids, at least for now. We're seemingly using inexistent ids
+-- ROMES:TODO: do this all inside EGraphM instead
+representDBCoreExpr :: Analysis a (DeBruijnF CoreExprF)
+ => DeBruijn CoreExpr
+ -> EGraph a (DeBruijnF CoreExprF)
+ -> (ClassId, EGraph a (DeBruijnF CoreExprF))
+representDBCoreExpr (D cmenv expr) eg0 = case expr of
+ Var v -> add (Node $ DF (D cmenv (VarF v))) eg0
+ Lit lit -> add (Node $ DF (D cmenv (LitF lit))) eg0
+ Type t -> add (Node $ DF (D cmenv (TypeF t))) eg0
+ Coercion c -> add (Node $ DF (D cmenv (CoercionF c))) eg0
+ Cast e co -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
+ in add (Node $ DF (D cmenv (CastF eid co))) eg1
+ App f a -> let (fid,eg1) = representDBCoreExpr (D cmenv f) eg0
+ (aid,eg2) = representDBCoreExpr (D cmenv a) eg1
+ in add (Node $ DF (D cmenv (AppF fid aid))) eg2
+ Tick n e -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
+ in add (Node $ DF (D cmenv (TickF n eid))) eg1
+ Lam b e -> let (eid,eg1) = representDBCoreExpr (D (extendCME cmenv b) e) eg0
+ in add (Node $ DF (D cmenv (LamF b eid))) eg1
+ Let (NonRec v r) e -> let (rid,eg1) = representDBCoreExpr (D cmenv r) eg0
+ (eid,eg2) = representDBCoreExpr (D (extendCME cmenv v) e) eg1
+ in add (Node $ DF (D cmenv (LetF (NonRecF v rid) eid))) eg2
+ Let (Rec (unzip -> (bs,rs))) e ->
+ let cmenv' = extendCMEs cmenv bs
+ (bsids, eg1) = EGM.runEGraphM eg0 $
+ traverse (state . representDBCoreExpr . D cmenv') rs
+ (eid, eg2) = representDBCoreExpr (D cmenv' e) eg1
+ in add (Node $ DF (D cmenv (LetF (RecF (zip bs bsids)) eid))) eg2
+ Case e b t as -> let (eid, eg1) = representDBCoreExpr (D cmenv e) eg0
+ (as', eg2) = EGM.runEGraphM eg1 $
+ traverse (state . representDBAltExpr . D (extendCME cmenv b)) as
+ in add (Node $ DF (D cmenv (CaseF eid b t as'))) eg2
+
+representDBAltExpr :: Analysis a (DeBruijnF CoreExprF)
+ => DeBruijn CoreAlt
+ -> EGraph a (DeBruijnF CoreExprF)
+ -> (CoreAltF ClassId, EGraph a (DeBruijnF CoreExprF))
+representDBAltExpr (D cm (Alt cons bs a)) eg0 =
+ let (ai, eg1) = representDBCoreExpr (D (extendCMEs cm bs) a) eg0
+ in (AltF cons bs ai, eg1)
+
+instance Eq a => Eq (DeBruijn (CoreAltF a)) where
+ (==) = eqDeBruijnAltF
+
+instance Eq a => Eq (DeBruijn (CoreExprF a)) where
+ (==) = eqDeBruijnExprF
+
+instance Eq a => Eq (DeBruijnF CoreExprF a) where
+ (==) (DF a) (DF b) = eqDeBruijnExprF a b
+
+instance Eq a => Eq (DeBruijnF CoreAltF a) where
+ (==) (DF a) (DF b) = eqDeBruijnAltF a b
+
+deriving instance Ord a => Ord (DeBruijnF CoreExprF a)
+
+instance Ord a => Ord (DeBruijn (CoreExprF a)) where
+ -- We must assume that if `a` is DeBruijn expression, it is already correctly "extended" because 'representDBCoreExpr' ensures that.
+ -- RM:TODO: We don't yet compare the CmEnv at any point. Should we?
+ -- RM: I don't think so, the CmEnv is used to determine whether bound variables are equal, but they don't otherwise influence the result.
+ -- Or rather, if the subexpression with variables is equal, then the CmEnv is necessarily equal too?
+ -- So I think that just works...
+ -- Wait, in that sense, couldn't we find a way to derive ord? the important part being that to compare Types and Vars we must use the DeBruijn Env ...
+ compare a b
+ = case a of
+ D cma (VarF va)
+ -> case b of
+ D cmb (VarF vb) -> cmpDeBruijnVar (D cma va) (D cmb vb)
+ _ -> LT
+ D _ (LitF la)
+ -> case b of
+ D _ VarF{} -> GT
+ D _ (LitF lb) -> la `compare` lb
+ _ -> LT
+ D _ (AppF af aarg)
+ -> case dataToTag# b of
+ bt
+ -> if tagToEnum# (bt ># 2#) then
+ LT
+ else
+ case b of
+ D _ (AppF bf barg)
+ -> case compare af bf of
+ LT -> LT
+ EQ -> aarg `compare` barg -- e.g. here, if we had for children other expresssions debruijnized, they would have the *correct* environments, so we needn't worry.
+ -- the issue to automatically deriving is only really the 'Var' and 'Type' parameters ...
+ GT -> GT
+ _ -> GT
+ D _ (LamF _abind abody)
+ -> case dataToTag# b of
+ bt
+ -> if tagToEnum# (bt ># 3#) then
+ LT
+ else
+ case b of
+ D _ (LamF _bbind bbody) -- we can ignore the binder since the represented DB expression has the correct DB environments by construction (see 'representDBCoreExpr')
+ -> compare abody bbody
+ _ -> GT
+ D cma (LetF as abody)
+ -> case dataToTag# b of
+ bt
+ -> if tagToEnum# (bt ># 4#) then
+ LT
+ else
+ case b of
+ D cmb (LetF bs bbody)
+ -> case compare (D cma as) (D cmb bs) of
+ LT -> LT
+ EQ -> compare abody bbody
+ GT -> GT
+ _ -> GT
+ D cma (CaseF cax _cabind catype caalt)
+ -> case dataToTag# b of
+ bt
+ -> if tagToEnum# (bt <# 5#) then
+ GT
+ else
+ case b of
+ D cmb (CaseF cbx _cbbind cbtype cbalt)
+ -> case compare cax cbx of
+ LT -> LT
+ -- ROMES:TODO: Consider changing order of comparisons to a more efficient one
+ EQ -> case cmpDeBruijnType (D cma catype) (D cmb cbtype) of
+ LT -> LT
+ EQ -> D cma caalt `compare` D cmb cbalt
+ GT -> GT
+ GT -> GT
+ _ -> LT
+ D cma (CastF cax caco)
+ -> case dataToTag# b of
+ bt
+ -> if tagToEnum# (bt <# 6#) then
+ GT
+ else
+ case b of
+ D cmb (CastF cbx cbco)
+ -> case compare cax cbx of
+ LT -> LT
+ EQ -> cmpDeBruijnCoercion (D cma caco) (D cmb cbco)
+ GT -> GT
+ _ -> LT
+ D cma (TickF tatickish tax)
+ -> case dataToTag# b of
+ bt
+ -> if tagToEnum# (bt <# 7#) then
+ GT
+ else
+ case b of
+ D cmb (TickF tbtickish tbx)
+ -> case cmpDeBruijnTickish (D cma tatickish) (D cmb tbtickish) of
+ LT -> LT
+ EQ -> tax `compare` tbx
+ GT -> GT
+ _ -> LT
+ D cma (TypeF at)
+ -> case b of
+ D _ CoercionF{} -> LT
+ D cmb (TypeF bt) -> cmpDeBruijnType (D cma at) (D cmb bt)
+ _ -> GT
+ D cma (CoercionF aco)
+ -> case b of
+ D cmb (CoercionF bco) -> cmpDeBruijnCoercion (D cma aco) (D cmb bco)
+ _ -> GT
+
+instance Eq a => Eq (DeBruijn (CoreBindF a)) where
+ D cma a == D cmb b = go a b where
+ go (NonRecF _v1 r1) (NonRecF _v2 r2)
+ = r1 == r2 -- See Note [Alpha-equality for let-bindings]
+
+ go (RecF ps1) (RecF ps2)
+ =
+ -- See Note [Alpha-equality for let-bindings]
+ all2 (\b1 b2 -> eqDeBruijnType (D cma (varType b1))
+ (D cmb (varType b2)))
+ bs1 bs2
+ && rs1 == rs2
+ where
+ (bs1,rs1) = unzip ps1
+ (bs2,rs2) = unzip ps2
+
+ go _ _ = False
+
+
+instance Ord a => Ord (DeBruijn (CoreBindF a)) where
+ compare a b
+ = case a of
+ D _cma (NonRecF _ab ax)
+ -> case b of
+ D _cmb (NonRecF _bb bx) -- Again, we ignore the binders bc on representation they were accounted for correctly.
+ -> ax `compare` bx
+ _ -> LT
+ D _cma (RecF as)
+ -> case b of
+ D _cmb (RecF bs) -> compare (map snd as) (map snd bs)
+ _ -> GT
+
+
+instance Ord a => Ord (DeBruijn (CoreAltF a)) where
+ compare a b
+ = case a of
+ D _cma (AltF ac _abs arhs)
+ -> case b of
+ D _cmb (AltF bc _bbs brhs)
+ -> case compare ac bc of
+ LT -> LT
+ EQ -> -- Again, we don't look at binders bc we assume on representation they were accounted for correctly.
+ arhs `compare` brhs
+ GT -> GT
+
+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: Is this OK?
+ 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 (DeBruijnF CoreExprF a) where
+ show (DF (D _ (VarF id) )) = showPprUnsafe $ text "VarF" <+> ppr id
+ show (DF (D _ (LitF lit))) = showPprUnsafe $ text "LitF" <+> ppr lit
+ show (DF (D _ (AppF a b))) = "AppF " ++ show a ++ " " ++ show b
+ show (DF (D _ (LamF b a))) = showPprUnsafe (text "LamF" <+> ppr b <+> text "") ++ show a
+ show (DF (D _ (LetF b a))) = "LetF " ++ show b ++ " " ++ show a
+ show (DF (D _ (CaseF a b t alts))) = "CaseF " ++ show a ++ showPprUnsafe (ppr b <+> ppr t) ++ show alts
+
+ show (DF (D _ (CastF _a _cor) )) = "CastF"
+ show (DF (D _ (TickF _cotick _a))) = "Tick"
+ show (DF (D _ (TypeF t) )) = "TypeF " ++ showPprUnsafe (ppr t)
+ show (DF (D _ (CoercionF co) )) = "CoercionF " ++ showPprUnsafe co
+
+
+instance Show a => Show (BindF CoreBndr a) where
+ show (NonRecF b a) = "NonRecF " ++ showPprUnsafe b ++ show a
+ show (RecF bs) = "RecF " ++ unwords (map (\(a,b) -> showPprUnsafe a ++ show b) bs)
+
+instance Show a => Show (AltF CoreBndr 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
@@ -16,12 +17,13 @@ module GHC.Core.Map.Type (
LooseTypeMap,
-- ** With explicit scoping
CmEnv, lookupCME, extendTypeMapWithScope, lookupTypeMapWithScope,
- mkDeBruijnContext, extendCME, extendCMEs, emptyCME,
+ mkDeBruijnContext, extendCME, extendCMEs, emptyCME, sizeCME,
-- * Utilities for use by friends only
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 [])
@@ -505,6 +517,10 @@ extendCMEs env vs = foldl' extendCME env vs
lookupCME :: CmEnv -> Var -> Maybe BoundVar
lookupCME (CME { cme_env = env }) v = lookupVarEnv env v
+-- | \(O(1)\). Number of elements in the CmEnv.
+sizeCME :: CmEnv -> Int
+sizeCME CME{cme_next=next} = next
+
-- | @DeBruijn a@ represents @a@ modulo alpha-renaming. This is achieved
-- by equipping the value with a 'CmEnv', which tracks an on-the-fly deBruijn
-- numbering. This allows us to define an 'Eq' instance for @DeBruijn a@, even
@@ -512,6 +528,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 +542,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/Errors/Ppr.hs
=====================================
@@ -72,7 +72,8 @@ instance Diagnostic DsMessage where
case vars of -- See #11245
[] -> text "Guards do not cover entire pattern space"
_ -> let us = map (\nabla -> pprUncovered nabla vars) nablas
- pp_tys = pprQuotedList $ map idType vars
+ -- pp_tys = pprQuotedList $ map idType vars
+ pp_tys = empty
in hang
(text "Patterns of type" <+> pp_tys <+> text "not matched:")
4
=====================================
compiler/GHC/HsToCore/Errors/Types.hs
=====================================
@@ -20,6 +20,8 @@ import GHC.Types.Id
import GHC.Types.Name (Name)
import qualified GHC.LanguageExtensions as LangExt
+import Data.Equality.Graph (ClassId)
+
import GHC.Generics (Generic)
newtype MinBound = MinBound Integer
@@ -99,7 +101,7 @@ data DsMessage
| DsNonExhaustivePatterns !(HsMatchContext GhcRn)
!ExhaustivityCheckType
!MaxUncoveredPatterns
- [Id]
+ [ClassId]
[Nabla]
| DsTopLevelBindsNotAllowed !BindsType !(HsBindLR GhcTc GhcTc)
=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -75,6 +75,8 @@ import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Data.Coerce
+import Data.Equality.Graph (ClassId)
+
--
-- * Exported entry points to the checker
--
@@ -104,9 +106,20 @@ pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
!missing <- getLdiNablas
pat_bind <- noCheckDs $ desugarPatBind loc var p
tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
- result <- unCA (checkPatBind pat_bind) missing
- tracePm "}: " (ppr (cr_uncov result))
- formatReportWarnings ReportPatBind ctxt [var] result
+ result0 <- unCA (checkPatBind pat_bind) missing
+ tracePm "}: " (ppr (cr_uncov result0))
+ -- romes:todo: this seems redundant, hints that the right thing might be for desugar to return already the match variables already "represented" in the e-graph
+ -- doing this, however, wouuld require for desugar pat binds to care about/thread through nablas
+ -- DESIGN:TODO: However, if we represent the variables while desugaring, we
+ -- would no longer need representId to represent VarF in the e-class, and can
+ -- instead do newEClass. This would further reduce allocations.
+ -- The reason why we can't do that currently is that on checkPatBind we'll
+ -- representIds, and when we represent them again in the next line, we want
+ -- them to match the ones we represented during checkPatBind. If we made
+ -- empty-eclasses, the representId on the next line wouldn't match the match
+ -- ids we defined in checkPatBind.
+ let (varid, cr_uncov') = representId var (cr_uncov result0)
+ formatReportWarnings ReportPatBind ctxt [varid] result0{cr_uncov = cr_uncov'}
pmcPatBind _ _ _ = pure ()
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -165,18 +178,20 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
-- This must be an -XEmptyCase. See Note [Checking EmptyCase]
let var = only vars
empty_case <- noCheckDs $ desugarEmptyCase var
- result <- unCA (checkEmptyCase empty_case) missing
- tracePm "}: " (ppr (cr_uncov result))
- formatReportWarnings ReportEmptyCase ctxt vars result
+ result0 <- unCA (checkEmptyCase empty_case) missing
+ tracePm "}: " (ppr (cr_uncov result0))
+ let (varids, cr_uncov') = representIds vars (cr_uncov result0) -- romes:todo: this seems redundant, hints that the right thing might be for desugar to return already the match variables already "represented" in the e-graph
+ formatReportWarnings ReportEmptyCase ctxt varids result0{cr_uncov=cr_uncov'}
return []
Just matches -> do
matches <- {-# SCC "desugarMatches" #-}
noCheckDs $ desugarMatches vars matches
- result <- {-# SCC "checkMatchGroup" #-}
+ result0 <- {-# SCC "checkMatchGroup" #-}
unCA (checkMatchGroup matches) missing
- tracePm "}: " (ppr (cr_uncov result))
- {-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt vars result
- return (NE.toList (ldiMatchGroup (cr_ret result)))
+ tracePm "}: " (ppr (cr_uncov result0))
+ let (varids, cr_uncov') = representIds vars (cr_uncov result0) -- romes:todo: this seems redundant, hints that the right thing might be for desugar to return already the match variables already "represented" in the e-graph
+ {-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt varids result0{cr_uncov=cr_uncov'}
+ return (NE.toList (ldiMatchGroup (cr_ret result0)))
{- Note [pmcPatBind only checks PatBindRhs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -340,7 +355,7 @@ collectInMode ReportEmptyCase = cirbsEmptyCase
-- | Given a 'FormatReportWarningsMode', this function will emit warnings
-- for a 'CheckResult'.
-formatReportWarnings :: FormatReportWarningsMode ann -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
+formatReportWarnings :: FormatReportWarningsMode ann -> DsMatchContext -> [ClassId] -> CheckResult ann -> DsM ()
formatReportWarnings report_mode ctx vars cr at CheckResult { cr_ret = ann } = do
cov_info <- collectInMode report_mode ann
dflags <- getDynFlags
@@ -348,7 +363,7 @@ formatReportWarnings report_mode ctx vars cr at CheckResult { cr_ret = ann } = do
-- | Issue all the warnings
-- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
-reportWarnings :: DynFlags -> FormatReportWarningsMode ann -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
+reportWarnings :: DynFlags -> FormatReportWarningsMode ann -> DsMatchContext -> [ClassId] -> CheckResult CIRB -> DsM ()
reportWarnings dflags report_mode (DsMatchContext kind loc) vars
CheckResult { cr_ret = CIRB { cirb_inacc = inaccessible_rhss
, cirb_red = redundant_rhss
@@ -387,7 +402,7 @@ reportWarnings dflags report_mode (DsMatchContext kind loc) vars
maxPatterns = maxUncoveredPatterns dflags
-getNFirstUncovered :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nablas -> DsM [Nabla]
+getNFirstUncovered :: GenerateInhabitingPatternsMode -> [ClassId] -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered mode vars n (MkNablas nablas) = go n (bagToList nablas)
where
go 0 _ = pure []
@@ -428,9 +443,10 @@ addTyCs origin ev_vars m = do
-- to be added for multiple scrutinees rather than just one.
addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs [] _ k = k
-addCoreScrutTmCs (scr:scrs) (x:xs) k =
- flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas ->
- addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
+addCoreScrutTmCs (scr:scrs) (x0:xs) k =
+ flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas0 ->
+ let (x, nablas) = representId x0 nablas0
+ in addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: numbers of scrutinees and match ids differ"
-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.
=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -103,16 +103,20 @@ emptyRedSets :: RedSets
emptyRedSets = RedSets mempty mempty mempty
checkGrd :: PmGrd -> CheckAction RedSets
-checkGrd grd = CA $ \inc -> case grd of
+checkGrd grd = CA $ \inc0 -> case grd of
-- let x = e: Refine with x ~ e
- PmLet x e -> do
+ PmLet x0 e -> do
+ let (x, inc) = representId x0 inc0
+ -- romes: we could potentially do update the trees to use e-class ids here,
+ -- or in pmcMatches
matched <- addPhiCtNablas inc (PhiCoreCt x e)
tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
, cr_uncov = mempty
, cr_approx = Precise }
-- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
- PmBang x mb_info -> do
+ PmBang x0 mb_info -> do
+ let (x, inc) = representId x0 inc0
div <- addPhiCtNablas inc (PhiBotCt x)
matched <- addPhiCtNablas inc (PhiNotBotCt x)
-- See Note [Dead bang patterns]
@@ -131,7 +135,9 @@ checkGrd grd = CA $ \inc -> case grd of
, cr_uncov = mempty
, cr_approx = Precise }
-- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
- PmCon x con tvs dicts args -> do
+ PmCon x0 con tvs dicts args0 -> do
+ let (x, inc1) = representId x0 inc0
+ let (args, inc) = representIds args0 inc1
!div <- if isPmAltConMatchStrict con
then addPhiCtNablas inc (PhiBotCt x)
else pure mempty
@@ -179,10 +185,11 @@ checkGRHS (PmGRHS { pg_grds = GrdVec grds, pg_rhs = rhs_info }) =
checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
-- See Note [Checking EmptyCase]
checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
- unc <- addPhiCtNablas inc (PhiNotBotCt var)
+ let (varid, inc') = representId var inc
+ unc <- addPhiCtNablas inc' (PhiNotBotCt varid)
pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
-checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
+checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
checkPatBind = coerce checkGRHS
{- Note [Checking EmptyCase]
=====================================
compiler/GHC/HsToCore/Pmc/Desugar.hs
=====================================
@@ -326,6 +326,13 @@ desugarEmptyCase :: Id -> DsM PmEmptyCase
desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
-- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
+--
+-- Returns a desugared guard tree of guard expressions.
+--
+-- These e-graphs have an equivalence class for each match-id in the guard
+-- expression, and are required in the subsequent passes of the PMC
+--
+-- Furthermore, the match-ids in the PmGrd expressions are e-class ids from said e-graph
desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
-> DsM (PmMatchGroup Pre)
desugarMatches vars matches =
=====================================
compiler/GHC/HsToCore/Pmc/Ppr.hs
=====================================
@@ -12,9 +12,6 @@ import GHC.Prelude
import GHC.Data.List.Infinite (Infinite (..))
import qualified GHC.Data.List.Infinite as Inf
import GHC.Types.Basic
-import GHC.Types.Id
-import GHC.Types.Var.Env
-import GHC.Types.Unique.DFM
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Builtin.Types
@@ -27,6 +24,10 @@ import Data.List.NonEmpty (NonEmpty, nonEmpty, toList)
import GHC.HsToCore.Pmc.Types
+import Data.Equality.Graph (ClassId)
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IM
+
-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
-- components and refutable shapes associated to any mentioned variables.
--
@@ -40,11 +41,11 @@ import GHC.HsToCore.Pmc.Types
--
-- When the set of refutable shapes contains more than 3 elements, the
-- additional elements are indicated by "...".
-pprUncovered :: Nabla -> [Id] -> SDoc
+pprUncovered :: Nabla -> [ClassId] -> SDoc
pprUncovered nabla vas
- | isNullUDFM refuts = fsep vec -- there are no refutations
- | otherwise = hang (fsep vec) 4 $
- text "where" <+> vcat (map (pprRefutableShapes . snd) (udfmToList refuts))
+ | IM.null refuts = fsep vec -- there are no refutations
+ | otherwise = hang (fsep vec) 4 $
+ text "where" <+> vcat (map (pprRefutableShapes . snd) (IM.toList refuts))
where
init_prec
-- No outer parentheses when it's a unary pattern by assuming lowest
@@ -96,35 +97,37 @@ substitution to the vectors before printing them out (see function `pprOne' in
-- | Extract and assigns pretty names to constraint variables with refutable
-- shapes.
-prettifyRefuts :: Nabla -> DIdEnv (Id, SDoc) -> DIdEnv (SDoc, [PmAltCon])
-prettifyRefuts nabla = listToUDFM_Directly . map attach_refuts . udfmToList
+prettifyRefuts :: Nabla -> IntMap (ClassId, SDoc) -> IntMap (SDoc, [PmAltCon])
+prettifyRefuts nabla = IM.mapWithKey attach_refuts
where
- attach_refuts (u, (x, sdoc)) = (u, (sdoc, lookupRefuts nabla x))
+ -- RM: why map with key?
+ attach_refuts :: ClassId -> (ClassId, SDoc) -> (SDoc, [PmAltCon])
+ attach_refuts _u (x, sdoc) = (sdoc, lookupRefuts nabla x)
-type PmPprM a = RWS Nabla () (DIdEnv (Id, SDoc), Infinite SDoc) a
+type PmPprM a = RWS Nabla () (IntMap (ClassId, SDoc), Infinite SDoc) a
-- Try nice names p,q,r,s,t before using the (ugly) t_i
nameList :: Infinite SDoc
nameList = map text ["p","q","r","s","t"] Inf.++ flip Inf.unfoldr (0 :: Int) (\ u -> (text ('t':show u), u+1))
-runPmPpr :: Nabla -> PmPprM a -> (a, DIdEnv (Id, SDoc))
-runPmPpr nabla m = case runRWS m nabla (emptyDVarEnv, nameList) of
+runPmPpr :: Nabla -> PmPprM a -> (a, IntMap (ClassId, SDoc))
+runPmPpr nabla m = case runRWS m nabla (IM.empty, nameList) of
(a, (renamings, _), _) -> (a, renamings)
-- | Allocates a new, clean name for the given 'Id' if it doesn't already have
-- one.
-getCleanName :: Id -> PmPprM SDoc
+getCleanName :: ClassId -> PmPprM SDoc
getCleanName x = do
(renamings, name_supply) <- get
let Inf clean_name name_supply' = name_supply
- case lookupDVarEnv renamings x of
+ case IM.lookup x renamings of
Just (_, nm) -> pure nm
Nothing -> do
- put (extendDVarEnv renamings x (x, clean_name), name_supply')
+ put (IM.insert x (x, clean_name) renamings, name_supply')
pure clean_name
-checkRefuts :: Id -> PmPprM (Maybe SDoc) -- the clean name if it has negative info attached
+checkRefuts :: ClassId -> PmPprM (Maybe SDoc) -- the clean name if it has negative info attached
checkRefuts x = do
nabla <- ask
case lookupRefuts nabla x of
@@ -134,20 +137,20 @@ checkRefuts x = do
-- | Pretty print a variable, but remember to prettify the names of the variables
-- that refer to neg-literals. The ones that cannot be shown are printed as
-- underscores.
-pprPmVar :: PprPrec -> Id -> PmPprM SDoc
+pprPmVar :: PprPrec -> ClassId -> PmPprM SDoc
pprPmVar prec x = do
nabla <- ask
case lookupSolution nabla x of
Just (PACA alt _tvs args) -> pprPmAltCon prec alt args
Nothing -> fromMaybe underscore <$> checkRefuts x
-pprPmAltCon :: PprPrec -> PmAltCon -> [Id] -> PmPprM SDoc
+pprPmAltCon :: PprPrec -> PmAltCon -> [ClassId] -> PmPprM SDoc
pprPmAltCon _prec (PmAltLit l) _ = pure (ppr l)
pprPmAltCon prec (PmAltConLike cl) args = do
nabla <- ask
pprConLike nabla prec cl args
-pprConLike :: Nabla -> PprPrec -> ConLike -> [Id] -> PmPprM SDoc
+pprConLike :: Nabla -> PprPrec -> ConLike -> [ClassId] -> PmPprM SDoc
pprConLike nabla _prec cl args
| Just pm_expr_list <- pmExprAsList nabla (PmAltConLike cl) args
= case pm_expr_list of
@@ -174,8 +177,8 @@ pprConLike _nabla prec cl args
-- | The result of 'pmExprAsList'.
data PmExprList
- = NilTerminated [Id]
- | WcVarTerminated (NonEmpty Id) Id
+ = NilTerminated [ClassId]
+ | WcVarTerminated (NonEmpty ClassId) ClassId
-- | Extract a list of 'Id's out of a sequence of cons cells, optionally
-- terminated by a wildcard variable instead of @[]@. Some examples:
@@ -186,7 +189,7 @@ data PmExprList
-- ending in a wildcard variable x (of list type). Should be pretty-printed as
-- (1:2:_).
-- * @pmExprAsList [] == Just ('NilTerminated' [])@
-pmExprAsList :: Nabla -> PmAltCon -> [Id] -> Maybe PmExprList
+pmExprAsList :: Nabla -> PmAltCon -> [ClassId] -> Maybe PmExprList
pmExprAsList nabla = go_con []
where
go_var rev_pref x
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -1,4 +1,6 @@
{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
@@ -49,18 +51,17 @@ import GHC.Data.Bag
import GHC.Types.CompleteMatch
import GHC.Types.Unique.Set
import GHC.Types.Unique.DSet
-import GHC.Types.Unique.SDFM
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Var (EvVar)
import GHC.Types.Var.Env
-import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
import GHC.Core
import GHC.Core.FVs (exprFreeVars)
import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Map.Expr
+import GHC.Core.Map.Type
+import GHC.Core.Equality
import GHC.Core.Predicate (typeDeterminesValue)
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils (exprType)
@@ -99,6 +100,13 @@ import Data.List (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
+import Data.Equality.Graph (ClassId)
+import Data.Equality.Graph.Lens
+import qualified Data.Equality.Graph as EG
+import Data.Bifunctor (second)
+import Data.Function ((&))
+import qualified Data.IntSet as IS
+
--
-- * Main exports
--
@@ -556,23 +564,26 @@ where you can find the solution in a perhaps more digestible format.
-- | A high-level pattern-match constraint. Corresponds to φ from Figure 3 of
-- the LYG paper.
+-- ROMES:TODO: Ultimately, all these Ids could be replaced by e-class ids which
+-- are generated during desugaring, but there are some details to it
+-- (propagating the e-graphs in which these e-classes were created)
data PhiCt
= PhiTyCt !PredType
-- ^ A type constraint "T ~ U".
- | PhiCoreCt !Id !CoreExpr
+ | PhiCoreCt !ClassId !CoreExpr
-- ^ @PhiCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e at .
- | PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id]
+ | PhiConCt !ClassId !PmAltCon ![TyVar] ![PredType] ![ClassId]
-- ^ @PhiConCt x K tvs dicts ys@ encodes @K \@tvs dicts ys <- x@, matching @x@
-- against the 'PmAltCon' application @K \@tvs dicts ys@, binding @tvs@,
-- @dicts@ and possibly unlifted fields @ys@ in the process.
-- See Note [Strict fields and variables of unlifted type].
- | PhiNotConCt !Id !PmAltCon
+ | PhiNotConCt !ClassId !PmAltCon
-- ^ @PhiNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed
-- by @K at .
- | PhiBotCt !Id
+ | PhiBotCt !ClassId
-- ^ @PhiBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
-- by @K at .
- | PhiNotBotCt !Id
+ | PhiNotBotCt !ClassId
-- ^ @PhiNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥.
instance Outputable PhiCt where
@@ -668,68 +679,71 @@ 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'' <- addConCt nabla' x con tvs args
- foldlM addNotBotCt nabla'' (filterUnliftedFields con args)
+ nabla1 <- addTyCts nabla (listToBag dicts)
+ -- romes: here we could have something like (merge (add K arg_ids) x)
+ -- or actually that should be done by addConCt?
+ nabla2 <- addConCt nabla1 x con tvs args
+ foldlM addNotBotCt nabla2 (filterUnliftedFields nabla2 con args)
addPhiTmCt nabla (PhiNotConCt x con) = addNotConCt nabla x con
addPhiTmCt nabla (PhiBotCt x) = addBotCt nabla x
addPhiTmCt nabla (PhiNotBotCt x) = addNotBotCt nabla x
-filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
-filterUnliftedFields con args =
- [ arg | (arg, bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con)
- , isBanged bang || definitelyUnliftedType (idType arg) ]
+filterUnliftedFields :: Nabla -> PmAltCon -> [ClassId] -> [ClassId]
+filterUnliftedFields nabla con args =
+ [ arg_id | (arg_id, bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con)
+ , isBanged bang || definitelyUnliftedType (eclassType arg_id nabla) ]
-- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@
-- 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 :: Nabla -> ClassId -> MaybeT DsM Nabla
+addBotCt nabla x = updateVarInfo x go nabla
+ where
+ go :: VarInfo -> MaybeT DsM VarInfo
+ go vi at VI { vi_bot = bot }
+ = case bot of
+ IsNotBot -> mzero -- There was x ≁ ⊥. Contradiction!
+ IsBot -> return vi -- There already is x ~ ⊥. Nothing left to do
+ MaybeBot -- We add x ~ ⊥
+ | definitelyUnliftedType (eclassType x nabla)
+ -- Case (3) in Note [Strict fields and variables of unlifted type]
+ -> mzero -- unlifted vars can never be ⊥
+ | otherwise
+ -> do
+ return 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 -> ClassId -> 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
+ let (yid, vi at VI { vi_bot = bot }) = lookupVarInfoNT ts 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' } }
+ pure $ markDirty yid
+ $ nabla{nabla_tm_st = ts{ ts_facts = env & _class yid . _data .~ vi'}}
-- | 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
-- that leads to a contradiction.
-- See Note [TmState invariants].
-addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
+addNotConCt :: Nabla -> ClassId -> 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
pure $ case mb_mark_dirty of
- Just x -> markDirty x nabla'
- Nothing -> nabla'
+ True -> markDirty x 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 :: VarInfo -> MaybeT DsM (Bool, 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))
@@ -748,12 +762,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, 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, vi')
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike cl) = notNull req_theta
@@ -767,8 +781,9 @@ hasRequiredTheta _ = False
-- have on @x@, reject (@Nothing@) otherwise.
--
-- 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
+addConCt :: Nabla -> ClassId -> PmAltCon -> [TyVar] -> [ClassId] -> MaybeT DsM Nabla
+addConCt nabla at MkNabla{ nabla_tm_st = ts } x alt tvs args = do
+ -- ROMES:TODO: Also looks like a function on varinfo (adjust)
let vi@(VI _ pos neg bot _) = lookupVarInfo ts x
-- First try to refute with a negative fact
guard (not (elemPmAltConSet alt neg))
@@ -788,7 +803,7 @@ addConCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x alt tvs args =
Nothing -> do
let pos' = PACA alt tvs args : pos
let nabla_with bot' =
- nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
+ nabla{nabla_tm_st = ts{ts_facts = ts_facts ts & _class x ._data .~ 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 ->
@@ -816,12 +831,23 @@ equateTys ts us =
-- @nabla@ has integrated the knowledge from the equality constraint.
--
-- See Note [TmState invariants].
-addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
+addVarCt :: Nabla -> ClassId -> ClassId -> MaybeT DsM Nabla
+-- This is where equality-graphs really come into play.
addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
- case equateUSDFM env x y of
- (Nothing, env') -> pure (nabla{ nabla_tm_st = ts{ ts_facts = env' } })
+ -- ROMES:TODO: equate auxiliary var that finds both vars, and lookups up the domain associated. However, I think we no longer should have Just/Nothing but rather always store emptyVarInfo for new e-nodes
+ -- equate should also update e-graph, basically re-implement "equateUSDFM" in terms of the e-graph, or inline it or so
+ case equate env x y of
-- Add the constraints we had for x to y
- (Just vi_x, env') -> do
+ -- See Note (TODO) Joining e-classes PMC] todo mention from joinA
+ -- Now, here's a really tricky bit (TODO Write note, is it the one above?)
+ -- Bc the joinA operation is unlawful, and because the makeA operation for
+ -- expressions is also unlawful (sets the type to ()::(), mostly out of
+ -- laziness, we could reconstruct the type if we wanted),
+ -- Then we must make sure that when we're "completing the joinA manually",
+ -- We *also update the type* (WTF1).
+ -- This is because every e-class should always have a match-var first, which will always have a type, and it should appear on "the left"
+ -- We also rebuild here, we did just merge two things. TODO: Where and when exactly should we merge?
+ (vi_x, EG.rebuild -> 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
@@ -829,6 +855,22 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- Do the same for negative info
let add_neg nabla nalt = addNotConCt nabla y nalt
foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x))
+ where
+ -- @equate env x y@ makes @x@ and @y@ point to the same entry,
+ -- thereby merging @x@'s class with @y@'s.
+ -- If both @x@ and @y@ are in the domain of the map, then @y@'s entry will be
+ -- chosen as the new entry and @x@'s old entry will be returned.
+ --
+ -- Examples in terms of the model (see 'UniqSDFM'):
+ -- >>> equate [] u1 u2 == (Nothing, [({u1,u2}, Nothing)])
+ -- >>> equate [({u1,u3}, Just ele1)] u3 u4 == (Nothing, [({u1,u3,u4}, Just ele1)])
+ -- >>> equate [({u1,u3}, Just ele1)] u4 u3 == (Nothing, [({u1,u3,u4}, Just ele1)])
+ -- >>> equate [({u1,u3}, Just ele1), ({u2}, Just ele2)] u3 u2 == (Just ele1, [({u2,u1,u3}, Just ele2)])
+ equate :: TmEGraph -> ClassId -> ClassId -> (VarInfo, TmEGraph)
+ equate eg x y = let (_, eg') = EG.merge x y eg
+ in (eg ^. _class x ._data, eg')
+ -- Note: lookup in @eg@, not @eg'@, because we want to return x's data before the merge.
+
-- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
-- on the shape of the 'CoreExpr' @e at . Examples:
@@ -842,7 +884,7 @@ addVarCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
-- for other literals. See 'coreExprAsPmLit'.
-- * Finally, if we have @let x = e@ and we already have seen @let y = e@, we
-- want to record @x ~ y at .
-addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla
+addCoreCt :: Nabla -> ClassId -> CoreExpr -> MaybeT DsM Nabla
addCoreCt nabla x e = do
simpl_opts <- initSimpleOpts <$> getDynFlags
let e' = simpleOptExpr simpl_opts e
@@ -851,8 +893,10 @@ addCoreCt nabla x e = do
where
-- Takes apart a 'CoreExpr' and tries to extract as much information about
-- literals and constructor applications as possible.
- core_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
+ -- ROMES:TODO: Consider CoreExprF instead of CoreExpr already here?
+ core_expr :: ClassId -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
-- TODO: Handle newtypes properly, by wrapping the expression in a DataCon
+ -- RM: Could this be done better with e-graphs? The whole newtype stuff
-- This is the right thing for casts involving data family instances and
-- their representation TyCon, though (which are not visible in source
-- syntax). See Note [COMPLETE sets on data families]
@@ -873,14 +917,19 @@ addCoreCt nabla x e = do
| Just (in_scope, _empty_floats@[], dc, _arg_tys, args)
<- exprIsConApp_maybe in_scope_env e
= data_con_app x in_scope dc args
- -- See Note [Detecting pattern synonym applications in expressions]
- | Var y <- e, Nothing <- isDataConId_maybe x
- -- We don't consider DataCons flexible variables
- = modifyT (\nabla -> addVarCt nabla x y)
| otherwise
- -- Any other expression. Try to find other uses of a semantically
- -- equivalent expression and represent them by the same variable!
= equate_with_similar_expr x e
+ -- nabla' <- get
+ -- if
+ -- See Note [Detecting pattern synonym applications in expressions]
+ -- ROMES:TODO: Can we fix this more easily with e-graphs?
+ -- x| Var y <- e, Nothing <- isDataConId_maybe (eclassMatchId x nabla')
+ -- We don't consider DataCons flexible variables
+ -- -> modifyT (\nabla -> addVarCt nabla' x y)
+ -- x| otherwise
+ -- Any other expression. Try to find other uses of a semantically
+ -- equivalent expression and represent them by the same variable!
+ -- -> equate_with_similar_expr x e
where
expr_ty = exprType e
expr_in_scope = mkInScopeSet (exprFreeVars e)
@@ -894,15 +943,18 @@ addCoreCt nabla x e = do
-- see if we already encountered a constraint @let y = e'@ with @e'@
-- 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 :: ClassId -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
+ equate_with_similar_expr _x e = do
+ rep <- StateT $ \nabla -> pure (representCoreExpr nabla e)
-- Note that @rep == x@ if we encountered @e@ for the first time.
+
+ -- ROMES:TODO: I don't think we need to do the following anymore, represent should directly do so in the right e-class (if rebuilt)
modifyT (\nabla -> addVarCt nabla x rep)
+ -- ROMES:TODO: When to rebuild?
- bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id
+ bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) ClassId
bind_expr e = do
- x <- lift (lift (mkPmId (exprType e)))
+ x <- StateT $ \nabla -> lift (mkPmMatchId (exprType e) nabla)
core_expr x e
pure x
@@ -913,7 +965,7 @@ addCoreCt nabla x e = do
-- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
-- 4. @x ~ K as ys@
-- This is quite similar to PmCheck.pmConCts.
- data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) ()
+ data_con_app :: ClassId -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) ()
data_con_app x in_scope dc args = do
let dc_ex_tvs = dataConExTyCoVars dc
arty = dataConSourceArity dc
@@ -936,13 +988,13 @@ addCoreCt nabla x e = do
-- Adds a literal constraint, i.e. @x ~ 42 at .
-- Also we assume that literal expressions won't diverge, so this
-- will add a @x ~/ ⊥@ constraint.
- pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT DsM) ()
+ pm_lit :: ClassId -> PmLit -> StateT Nabla (MaybeT DsM) ()
pm_lit x lit = do
modifyT $ \nabla -> addNotBotCt nabla x
pm_alt_con_app x (PmAltLit lit) [] []
-- Adds the given constructor application as a solution for @x at .
- pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Nabla (MaybeT DsM) ()
+ pm_alt_con_app :: ClassId -> PmAltCon -> [TyVar] -> [ClassId] -> StateT Nabla (MaybeT DsM) ()
pm_alt_con_app x con tvs args = modifyT $ \nabla -> addConCt nabla x con tvs args
-- | Like 'modify', but with an effectful modifier action
@@ -953,24 +1005,18 @@ modifyT f = StateT $ fmap ((,) ()) . f
-- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
-- equivalent to @e'@) we encountered earlier, or a fresh identifier if
-- there weren't any such constraints.
-representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
-representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_reps = reps } } e
- | Just rep <- lookupCoreMap reps key = pure (rep, nabla)
- | otherwise = do
- rep <- mkPmId (exprType e)
- let reps' = extendCoreMap reps key rep
- let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
- pure (rep, nabla')
- where
- key = makeDictsCoherent e
- -- Use a key in which dictionaries for the same type become equal.
- -- See Note [Unique dictionaries in the TmOracle CoreMap]
+representCoreExpr :: Nabla -> CoreExpr -> (ClassId, Nabla)
+representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = egraph } } e =
+ second (\g -> nabla{nabla_tm_st = ts{ts_facts = g}}) $ representDBCoreExpr (deBruijnize (makeDictsCoherent e)) egraph
+ -- Use a key in which dictionaries for the same type become equal.
+ -- See Note [Unique dictionaries in the TmOracle CoreMap]
-- | Change out 'Id's which are uniquely determined by their type to a
-- common value, so that different names for dictionaries of the same type
-- are considered equal when building a 'CoreMap'.
--
-- See Note [Unique dictionaries in the TmOracle CoreMap]
+-- ROMES:TODO: I suppose this should be taken into account by the Eq instance of DeBruijnF CoreExprF -- if we do that there then we're sure that EG.represent takes that into account.
makeDictsCoherent :: CoreExpr -> CoreExpr
makeDictsCoherent var@(Var v)
| let ty = idType v
@@ -1059,6 +1105,7 @@ In the end, replacing dictionaries with an error value in the pattern-match
checker was the most self-contained, although we might want to revisit once
we implement a more robust approach to computing equality in the pattern-match
checker (see #19272).
+ROMES:TODO: I don't think e-graphs avoid this situation, because the names of the binders will still differ (although the Eq instance could take this into account?)
-}
{- Note [The Pos/Neg invariant]
@@ -1271,22 +1318,23 @@ 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 -> 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')
+ vi' <- f x (lookupVarInfo ts x)
+ 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 -> VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll f ts at TmSt{ts_facts = env} = do
- env' <- traverseUSDFM f env
+ env' <- (_iclasses.(\fab (i,cl) -> let mvi = fab (i,cl^._data) in (cl &) . (_data .~) <$> mvi)) (uncurry f) env
pure ts{ts_facts = env'}
-- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate
@@ -1308,31 +1356,34 @@ 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 -> VarInfo -> MaybeT DsM VarInfo
+ test_one cid 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
+ instantiate (fuel-1) nabla_not_dirty (cid,vi)
+ _ -> return vi
+
+-- ROMES:TODO: The dirty shortcutting bit seems like the bookeeping on nodes to
+-- upward merge, perhaps we can rid of it too
-- | Checks whether the given 'VarInfo' needs to be tested for inhabitants.
-- Returns `False` when we can skip the inhabitation test, presuming it would
-- say "yes" anyway. See Note [Shortcutting the inhabitation test].
-varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
-varNeedsTesting _ MkNabla{nabla_tm_st=tm_st} vi
- | elemDVarSet (vi_id vi) (ts_dirty tm_st) = pure True
-varNeedsTesting _ _ vi
+varNeedsTesting :: TyState -> Nabla -> ClassId -> VarInfo -> DsM Bool
+varNeedsTesting _ MkNabla{nabla_tm_st=tm_st} cid _
+ | IS.member cid (ts_dirty tm_st) = pure True
+varNeedsTesting _ _ _ vi
| notNull (vi_pos vi) = pure False
-varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _
+varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _ _
-- Same type state => still inhabited
| not (tyStateRefined old_ty_st new_ty_st) = pure False
-varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = do
+varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _ vi = do
-- These normalisations are relatively expensive, but still better than having
-- to perform a full inhabitation test
(_, _, old_norm_ty) <- tntrGuts <$> pmTopNormaliseType old_ty_st (idType $ vi_id vi)
@@ -1349,25 +1400,25 @@ varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = do
-- NB: Does /not/ filter each CompleteMatch with the oracle; members may
-- remain that do not satisfy it. This lazy approach just
-- avoids doing unnecessary work.
-instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
-instantiate fuel nabla vi = {-# SCC "instantiate" #-}
- (instBot fuel nabla vi <|> instCompleteSets fuel nabla vi)
+instantiate :: Int -> Nabla -> (ClassId, VarInfo) -> MaybeT DsM VarInfo
+instantiate fuel nabla (ci,vi) = {-# SCC "instantiate" #-}
+ (instBot fuel nabla (ci,vi) <|> instCompleteSets fuel nabla ci)
-- | The \(⊢_{Bot}\) rule from the paper
-instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
-instBot _fuel nabla vi = {-# SCC "instBot" #-} do
- _nabla' <- addBotCt nabla (vi_id vi)
+instBot :: Int -> Nabla -> (ClassId,VarInfo) -> MaybeT DsM VarInfo
+instBot _fuel nabla (cid,vi) = {-# SCC "instBot" #-} do
+ _nabla' <- addBotCt nabla cid
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 -> ClassId -> DsM (ResidualCompleteMatches, Nabla)
+addNormalisedTypeMatches nabla at MkNabla{ nabla_ty_st = ty_st } xid
+ = trvVarInfo add_matches nabla 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)
add_matches vi at VI{ vi_rcm = rcm } = do
- norm_res_ty <- normaliseSourceTypeWHNF ty_st (idType x)
+ norm_res_ty <- normaliseSourceTypeWHNF ty_st (eclassType xid nabla)
env <- dsGetFamInstEnvs
rcm' <- case splitReprTyConApp_maybe env norm_res_ty of
Just (rep_tc, _args, _co) -> addTyConMatches rep_tc rcm
@@ -1388,12 +1439,11 @@ splitReprTyConApp_maybe env ty =
-- inhabitant, the whole thing is uninhabited. It returns the updated 'VarInfo'
-- where all the attempted ConLike instantiations have been purged from the
-- 'ResidualCompleteMatches', which functions as a cache.
-instCompleteSets :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
-instCompleteSets fuel nabla vi = {-# SCC "instCompleteSets" #-} do
- let x = vi_id vi
- (rcm, nabla) <- lift (addNormalisedTypeMatches nabla x)
- nabla <- foldM (\nabla cls -> instCompleteSet fuel nabla x cls) nabla (getRcm rcm)
- pure (lookupVarInfo (nabla_tm_st nabla) x)
+instCompleteSets :: Int -> Nabla -> ClassId -> MaybeT DsM VarInfo
+instCompleteSets fuel nabla cid = {-# SCC "instCompleteSets" #-} do
+ (rcm, nabla) <- lift (addNormalisedTypeMatches nabla cid)
+ nabla <- foldM (\nabla cls -> instCompleteSet fuel nabla cid cls) nabla (getRcm rcm)
+ pure (lookupVarInfo (nabla_tm_st nabla) cid)
anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution p = any (go . paca_con)
@@ -1411,18 +1461,18 @@ anyConLikeSolution p = any (go . paca_con)
-- original Nabla, not a proper refinement! No positive information will be
-- added, only negative information from failed instantiation attempts,
-- entirely as an optimisation.
-instCompleteSet :: Int -> Nabla -> Id -> CompleteMatch -> MaybeT DsM Nabla
-instCompleteSet fuel nabla x cs
- | anyConLikeSolution (`elementOfUniqDSet` (cmConLikes cs)) (vi_pos vi)
+instCompleteSet :: Int -> Nabla -> ClassId -> CompleteMatch -> MaybeT DsM Nabla
+instCompleteSet fuel nabla xid cs
+ | anyConLikeSolution (`elementOfUniqDSet` cmConLikes cs) (vi_pos vi)
-- No need to instantiate a constructor of this COMPLETE set if we already
-- have a solution!
= pure nabla
- | not (completeMatchAppliesAtType (varType x) cs)
+ | not (completeMatchAppliesAtType (eclassType xid nabla) cs)
= pure nabla
| otherwise
= {-# SCC "instCompleteSet" #-} go nabla (sorted_candidates cs)
where
- vi = lookupVarInfo (nabla_tm_st nabla) x
+ vi = lookupVarInfo (nabla_tm_st nabla) xid
sorted_candidates :: CompleteMatch -> [ConLike]
sorted_candidates cm
@@ -1443,12 +1493,11 @@ instCompleteSet fuel nabla x cs
| isDataConTriviallyInhabited dc
= pure nabla
go nabla (con:cons) = do
- let x = vi_id vi
let recur_not_con = do
- nabla' <- addNotConCt nabla x (PmAltConLike con)
+ nabla' <- addNotConCt nabla xid (PmAltConLike con)
go nabla' cons
- (nabla <$ instCon fuel nabla x con) -- return the original nabla, not the
- -- refined one!
+ (nabla <$ instCon fuel nabla xid con) -- return the original nabla, not the
+ -- refined one!
<|> recur_not_con -- Assume that x can't be con. Encode that fact
-- with addNotConCt and recur.
@@ -1509,11 +1558,11 @@ compareConLikeTestability (RealDataCon a) (RealDataCon b) = mconcat
-- adding the proper constructor constraint.
--
-- See Note [Instantiating a ConLike].
-instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla
-instCon fuel nabla at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} MaybeT $ do
+instCon :: Int -> Nabla -> ClassId -> ConLike -> MaybeT DsM Nabla
+instCon fuel nabla0 at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} MaybeT $ do
let hdr what = "instCon " ++ show fuel ++ " " ++ what
env <- dsGetFamInstEnvs
- let match_ty = idType x
+ let match_ty = eclassType x nabla0
tracePm (hdr "{") $
ppr con <+> text "... <-" <+> ppr x <+> dcolon <+> ppr match_ty
norm_match_ty <- normaliseSourceTypeWHNF ty_st match_ty
@@ -1531,23 +1580,23 @@ instCon fuel nabla at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} Ma
let gammas = substTheta sigma_ex (eqSpecPreds eq_spec ++ thetas)
-- (4) Instantiate fresh term variables as arguments to the constructor
let field_tys' = substTys sigma_ex $ map scaledThing field_tys
- arg_ids <- mapM mkPmId field_tys'
+ (arg_ids, nabla1) <- runStateT (mapM (StateT @Nabla . mkPmMatchId) field_tys') nabla0
tracePm (hdr "(cts)") $ vcat
[ ppr x <+> dcolon <+> ppr match_ty
, text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
, ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
, ppr (map (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs)
, ppr gammas
- , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids)
+ , ppr (map (\x -> ppr x <+> dcolon <+> ppr (eclassType x nabla1)) arg_ids)
]
-- (5) Finally add the new constructor constraint
runMaybeT $ do
-- Case (2) of Note [Strict fields and variables of unlifted type]
let alt = PmAltConLike con
- let branching_factor = length $ filterUnliftedFields alt arg_ids
+ let branching_factor = length $ filterUnliftedFields nabla1 alt arg_ids
let ct = PhiConCt x alt ex_tvs gammas arg_ids
- nabla1 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $
- addPhiTmCt nabla ct
+ nabla2 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $
+ addPhiTmCt nabla1 ct
-- See Note [Fuel for the inhabitation test]
let new_fuel
| branching_factor <= 1 = fuel
@@ -1559,18 +1608,18 @@ instCon fuel nabla at MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} Ma
, ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
, ppr (map (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs)
, ppr gammas
- , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids)
+ , ppr (map (\x -> ppr x <+> dcolon <+> ppr (eclassType x nabla1)) arg_ids)
, ppr branching_factor
, ppr new_fuel
]
- nabla2 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla1) $
- inhabitationTest new_fuel (nabla_ty_st nabla) nabla1
- lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla2)
- pure nabla2
+ nabla3 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla2) $
+ inhabitationTest new_fuel (nabla_ty_st nabla1) nabla2
+ lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla3)
+ pure nabla3
Nothing -> do
tracePm (hdr "(match_ty not instance of res_ty) }") empty
- pure (Just nabla) -- Matching against match_ty failed. Inhabited!
- -- See Note [Instantiating a ConLike].
+ pure (Just nabla0) -- Matching against match_ty failed. Inhabited!
+ -- See Note [Instantiating a ConLike].
-- | @matchConLikeResTy _ _ ty K@ tries to match @ty@ against the result
-- type of @K@, @res_ty at . It returns a substitution @s@ for @K@'s universal
@@ -1905,13 +1954,15 @@ instance Outputable GenerateInhabitingPatternsMode where
-- perhaps empty) refinements of @nabla@ that represent inhabited patterns.
-- Negative information is only retained if literals are involved or for
-- recursive GADTs.
-generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla]
+--
+-- The list of 'Id's @vs@ is the list of match-ids ? and they have all already been represented in the e-graph, we just represent them again to re-gain class id information
+generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [ClassId] -> Int -> Nabla -> DsM [Nabla]
-- See Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
generateInhabitingPatterns _ _ 0 _ = pure []
generateInhabitingPatterns _ [] _ nabla = pure [nabla]
-generateInhabitingPatterns mode (x:xs) n nabla = do
+generateInhabitingPatterns mode (x:xs) n nabla at MkNabla{nabla_tm_st=ts} = do
tracePm "generateInhabitingPatterns" (ppr mode <+> ppr n <+> ppr (x:xs) $$ ppr nabla)
- let VI _ pos neg _ _ = lookupVarInfo (nabla_tm_st nabla) x
+ let VI _ pos neg _ _ = lookupVarInfo ts x
case pos of
_:_ -> do
-- Example for multiple solutions (must involve a PatSyn):
@@ -1941,15 +1992,15 @@ generateInhabitingPatterns mode (x:xs) n nabla = do
-- Tries to instantiate a variable by possibly following the chain of
-- newtypes and then instantiating to all ConLikes of the wrapped type's
-- minimal residual COMPLETE set.
- try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
+ try_instantiate :: ClassId -> [ClassId] -> Int -> Nabla -> DsM [Nabla]
-- Convention: x binds the outer constructor in the chain, y the inner one.
try_instantiate x xs n nabla = do
- (_src_ty, dcs, rep_ty) <- tntrGuts <$> pmTopNormaliseType (nabla_ty_st nabla) (idType x)
+ (_src_ty, dcs, rep_ty) <- tntrGuts <$> pmTopNormaliseType (nabla_ty_st nabla) (eclassType x nabla)
mb_stuff <- runMaybeT $ instantiate_newtype_chain x nabla dcs
case mb_stuff of
Nothing -> pure []
- Just (y, newty_nabla) -> do
- let vi = lookupVarInfo (nabla_tm_st newty_nabla) y
+ Just (y, newty_nabla at MkNabla{nabla_tm_st=ts}) -> do
+ let vi = lookupVarInfo ts y
env <- dsGetFamInstEnvs
rcm <- case splitReprTyConApp_maybe env rep_ty of
Just (tc, _, _) -> addTyConMatches tc (vi_rcm vi)
@@ -1973,16 +2024,16 @@ generateInhabitingPatterns mode (x:xs) n nabla = do
-- Instantiates a chain of newtypes, beginning at @x at .
-- Turns @x nabla [T,U,V]@ to @(y, nabla')@, where @nabla'@ we has the fact
-- @x ~ T (U (V y))@.
- instantiate_newtype_chain :: Id -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (Id, Nabla)
+ instantiate_newtype_chain :: ClassId -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (ClassId, Nabla)
instantiate_newtype_chain x nabla [] = pure (x, nabla)
instantiate_newtype_chain x nabla ((_ty, dc, arg_ty):dcs) = do
- y <- lift $ mkPmId arg_ty
+ (y,nabla') <- lift $ mkPmMatchId arg_ty nabla
-- Newtypes don't have existentials (yet?!), so passing an empty
-- list as ex_tvs.
- nabla' <- addConCt nabla x (PmAltConLike (RealDataCon dc)) [] [y]
- instantiate_newtype_chain y nabla' dcs
+ nabla'' <- addConCt nabla' x (PmAltConLike (RealDataCon dc)) [] [y]
+ instantiate_newtype_chain y nabla'' dcs
- instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
+ instantiate_cons :: ClassId -> Type -> [ClassId] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
instantiate_cons _ _ _ _ _ [] = pure []
instantiate_cons _ _ _ 0 _ _ = pure []
instantiate_cons _ ty xs n nabla _
@@ -1992,7 +2043,7 @@ generateInhabitingPatterns mode (x:xs) n nabla = do
instantiate_cons x ty xs n nabla (cl:cls) = do
-- The following line is where we call out to the inhabitationTest!
mb_nabla <- runMaybeT $ instCon 4 nabla x cl
- tracePm "instantiate_cons" (vcat [ ppr x <+> dcolon <+> ppr (idType x)
+ tracePm "instantiate_cons" (vcat [ ppr x <+> dcolon <+> ppr (eclassType x nabla)
, ppr ty
, ppr cl
, ppr nabla
@@ -2082,3 +2133,25 @@ 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 -> (VarInfo -> f VarInfo) -> Nabla -> f Nabla
+-- Update the data at class @xid@ using lenses and the monadic action @go@
+updateVarInfo xid f nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=eg } } = (\eg' -> nabla{ nabla_tm_st = ts{ts_facts = eg'} }) <$> (_class xid . _data) f eg
+
+eclassMatchId :: HasCallStack => ClassId -> Nabla -> Id
+eclassMatchId cid = vi_id . (^. _class cid . _data) . (ts_facts . nabla_tm_st)
+
+eclassType :: ClassId -> Nabla -> Type
+eclassType cid = idType . eclassMatchId cid
+
+-- ROMES:TODO: When exactly to rebuild?
+
+-- | Generate a fresh class for matching, returning the class-id as the match-id
+mkPmMatchId :: Type -> Nabla -> DsM (ClassId, Nabla)
+mkPmMatchId ty (MkNabla tyst ts at TmSt{ts_facts = egr}) = do
+ x <- mkPmId ty -- romes:Todo: for now, we still use mkPmId to get an Id for emptyVarInfo, but we want to get rid of this too
+ let (xid, egr') = EG.newEClass (emptyVarInfo x) egr
+ return (xid, MkNabla tyst ts{ts_facts=egr'})
+{-# NOINLINE mkPmMatchId #-} -- We'll CPR deeply, that should be enough
+
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,7 +1,12 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiWayIf #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
-- | Domain types used in "GHC.HsToCore.Pmc.Solver".
-- The ultimate goal is to define 'Nabla', which models normalised refinement
@@ -10,12 +15,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, representIds,
-- ** Caching residual COMPLETE sets
CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
@@ -42,10 +47,9 @@ 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.Equality
import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Utils.Outputable
@@ -58,7 +62,7 @@ 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.Map.Type
import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
@@ -75,6 +79,17 @@ import Data.Ratio
import GHC.Real (Ratio(..))
import qualified Data.Semigroup as Semi
+import Data.Tuple (swap)
+import Data.Traversable (mapAccumL)
+import Data.Functor.Compose
+import Data.Equality.Analysis (Analysis(..))
+import Data.Equality.Graph (EGraph, ClassId)
+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, bimap)
+
-- import GHC.Driver.Ppr
--
@@ -131,21 +146,19 @@ instance Outputable TyState where
initTyState :: TyState
initTyState = TySt 0 emptyInert
--- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
--- entries are possibly shared when we figure out that two variables must be
--- equal, thus represent the same set of values.
+-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's and
+-- 'CoreExpr's. These entries are possibly shared when we figure out that two
+-- variables must be equal, thus represent the same set of values.
--
-- See Note [TmState invariants] in "GHC.HsToCore.Pmc.Solver".
data TmState
= TmSt
- { ts_facts :: !(UniqSDFM Id VarInfo)
- -- ^ Facts about term variables. Deterministic env, so that we generate
- -- deterministic error messages.
- , ts_reps :: !(CoreMap Id)
- -- ^ An environment for looking up whether we already encountered semantically
- -- equivalent expressions that we want to represent by the same 'Id'
- -- representative.
- , ts_dirty :: !DIdSet
+ { ts_facts :: !TmEGraph
+ -- ^ Facts about terms.
+
+ -- ROMES:TODO: ts_dirty looks a bit to me like the bookeeping needed to know
+ -- which nodes to upward merge, perhaps we can get rid of it too.
+ , ts_dirty :: !IntSet
-- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
-- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
}
@@ -161,6 +174,8 @@ data VarInfo
{ vi_id :: !Id
-- ^ The 'Id' in question. Important for adding new constraints relative to
-- this 'VarInfo' when we don't easily have the 'Id' available.
+ -- ROMES:TODO: What is the Id in question when we might have multiple Ids in the same equivalence class?
+ -- It seems currenlty this is the representative of the e-class, so we could probably drop it, in favour of Type or so (since sometimes we need to know the type, and that's also reasonable data for the e-class to have)
, vi_pos :: ![PmAltConApp]
-- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
@@ -168,7 +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.
@@ -206,7 +221,7 @@ data PmAltConApp
= PACA
{ paca_con :: !PmAltCon
, paca_tvs :: ![TyVar]
- , paca_ids :: ![Id]
+ , paca_ids :: ![ClassId]
}
-- | See 'vi_bot'.
@@ -227,7 +242,7 @@ instance Outputable BotInfo where
-- | Not user-facing.
instance Outputable TmState where
- ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
+ ppr (TmSt eg dirty) = text (show eg) $$ ppr dirty
-- | Not user-facing.
instance Outputable VarInfo where
@@ -248,7 +263,7 @@ instance Outputable VarInfo where
-- | Initial state of the term oracle.
initTmState :: TmState
-initTmState = TmSt emptyUSDFM emptyCoreMap emptyDVarSet
+initTmState = TmSt EG.emptyEGraph IS.empty
-- | A data type that caches for the 'VarInfo' of @x@ the results of querying
-- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
@@ -300,9 +315,13 @@ emptyVarInfo x
, vi_rcm = emptyRCM
}
-lookupVarInfo :: TmState -> Id -> VarInfo
--- (lookupVarInfo tms x) tells what we know about 'x'
-lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
+-- | @lookupVarInfo tms x@ tells what we know about 'x'
+--- romes:TODO: This will have a different type. I don't know what yet.
+-- romes:TODO I don't think this is what we want any longer, more like represent Id and see if it was previously represented by some data or not?
+lookupVarInfo :: TmState -> ClassId -> VarInfo
+lookupVarInfo (TmSt eg _) x
+-- RM: Yea, I don't like the fact that currently all e-classes are created by Ids and have an Empty Var info, yet we must call "fromMaybe" here. Not good.
+ = eg ^._class x._data
-- | Like @lookupVarInfo ts x@, but @lookupVarInfo ts x = (y, vi)@ also looks
-- through newtype constructors. We have @x ~ N1 (... (Nk y))@ such that the
@@ -314,27 +333,33 @@ lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
-- modulo type normalisation!
--
-- See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
-lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
+--
+-- RM: looks like we could get perhaps represent the newtypes in the e-graph instead and somehow simplify this?
+lookupVarInfoNT :: TmState -> ClassId -> (ClassId, VarInfo)
lookupVarInfoNT ts x = case lookupVarInfo ts x of
VI{ vi_pos = as_newtype -> Just y } -> lookupVarInfoNT ts y
- res -> (x, res)
+ res -> (x, res)
where
as_newtype = listToMaybe . mapMaybe go
go PACA{paca_con = PmAltConLike (RealDataCon dc), paca_ids = [y]}
| isNewDataCon dc = Just y
go _ = Nothing
-trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
+-- romes: We could probably inline this
+trvVarInfo :: forall f a. Functor f => (VarInfo -> f (a,VarInfo)) -> Nabla -> ClassId -> f (a,Nabla)
trvVarInfo f nabla at MkNabla{ nabla_tm_st = ts at TmSt{ts_facts = env} } x
- = set_vi <$> f (lookupVarInfo ts x)
- where
- set_vi (a, vi') =
- (a, nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env (vi_id vi') vi' } })
+ = second (\g -> nabla{nabla_tm_st = ts{ts_facts=g}}) <$> updateAccum (_class x._data) f env
+ where
+ updateAccum :: forall f a s c. Functor f => Lens' s a -> (a -> f (c,a)) -> s -> f (c,s)
+ updateAccum lens g = getCompose . lens @(Compose f ((,) c)) (Compose . g)
------------------------------------------------
-- * Exported utility functions querying 'Nabla'
-lookupRefuts :: Nabla -> Id -> [PmAltCon]
+-- ROMES:TODO: Document
+-- | Lookup the refutable patterns, i.e. the pattern alt cons that certainly can't happen??
+-- ROMES:TODO: ClassId?
+lookupRefuts :: Nabla -> ClassId -> [PmAltCon]
-- Unfortunately we need the extra bit of polymorphism and the unfortunate
-- duplication of lookupVarInfo here.
lookupRefuts MkNabla{ nabla_tm_st = ts } x =
@@ -346,7 +371,7 @@ 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 -> ClassId -> Maybe PmAltConApp
lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of
[] -> Nothing
pos@(x:_)
@@ -465,6 +490,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
@@ -789,7 +815,7 @@ instance Outputable PmLit where
, (charPrimTy, primCharSuffix)
, (floatPrimTy, primFloatSuffix)
, (doublePrimTy, primDoubleSuffix) ]
- suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
+ suffix = maybe empty snd (find (eqType ty . fst) tbl)
instance Outputable PmAltCon where
ppr (PmAltConLike cl) = ppr cl
@@ -797,3 +823,91 @@ instance Outputable PmAltCon where
instance Outputable PmEquality where
ppr = text . show
+
+--
+-- * E-graphs to represent normalised refinment types
+--
+
+type TmEGraph = EGraph VarInfo (DeBruijnF CoreExprF)
+-- TODO delete orphans for showing TmEGraph for debugging reasons
+instance Show VarInfo where
+ show = showPprUnsafe . ppr
+
+representId :: Id -> Nablas -> (ClassId, Nablas)
+-- Will need to justify this well
+representId x (MkNablas nbs) = bimap (fromJust . headMaybe) MkNablas $ unzipBag $ mapBag go nbs where
+ go (MkNabla tyst tmst at TmSt{ts_facts=eg0})
+ = case EG.add (EG.Node (DF (deBruijnize (VarF x)))) eg0 of
+ (xid, eg1) -> (xid, MkNabla tyst tmst{ts_facts=eg1})
+
+representIds :: [Id] -> Nablas -> ([ClassId], Nablas)
+representIds xs nablas = swap $ mapAccumL (\acc x -> swap $ representId x acc) nablas xs
+
+-- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
+-- There ought to be a better way.
+instance Eq VarInfo where
+ (==) a b = vi_id a == vi_id b
+instance Analysis VarInfo (DeBruijnF CoreExprF) where
+ {-# INLINE makeA #-}
+ {-# INLINE joinA #-}
+
+ -- 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
+ makeA (DF (D _ (VarF x))) = emptyVarInfo x
+ makeA _ = emptyVarInfo unitDataConId -- ROMES:TODO: this is dummy information which should never be used, this is quite wrong :)
+ -- I think the reason we end up in this
+ -- situation is bc we first represent an expression and only then merge it with some Id.
+ -- we'd need a way to represent directly into an e-class then, to not trigger the new e-class.
+
+ -- 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
+ -- Hacks hacks hacks
+ -- Do some "obvious" things in this merge, despite keeping all the nuanced
+ -- joining operations in addVarCt. Some part of them will be redundant, but
+ -- if we don't do the simple things here we might end up losing information
+ -- when merging things through the e-graph outside of 'addVarCt'
+
+-- I think we really need effects, because the operation is only well-defined
+-- since it can fail when it is conflicting
+-- and that would allow us to do the merge procedure correcly here instead of in addVarCt
+-- we may be able to have Analysis (Effect VarInfo) (...)
+ joinA a b = b{ vi_id = if vi_id b == unitDataConId && vi_id a /= unitDataConId then vi_id a else vi_id b
+ , vi_pos = case (vi_pos a, vi_pos b) of
+ ([], []) -> []
+ ([], x) -> x
+ (x, []) -> x
+ (_x, y) -> y -- keep right
+ , vi_neg = foldr (flip extendPmAltConSet) (vi_neg b) (pmAltConSetElems $ vi_neg a)
+ , vi_bot = case (vi_bot a, vi_bot b) of
+ (IsBot,IsBot) -> IsBot
+ (IsBot,IsNotBot) -> IsNotBot -- keep b, achhhhh
+ (IsBot,MaybeBot) -> IsBot
+ (IsNotBot,IsBot) -> IsBot -- keep b, achhhhh
+ (IsNotBot,IsNotBot) -> IsNotBot
+ (IsNotBot,MaybeBot) -> IsNotBot
+ (MaybeBot, IsBot) -> IsBot
+ (MaybeBot, IsNotBot) -> IsNotBot
+ (MaybeBot, MaybeBot) -> MaybeBot
+ , vi_rcm = case (vi_rcm a, vi_rcm b) of
+ (RCM Nothing Nothing,RCM a b) -> RCM a b
+ (RCM Nothing (Just a),RCM Nothing Nothing) -> RCM Nothing (Just a)
+ (RCM Nothing (Just _a),RCM Nothing (Just b)) -> RCM Nothing (Just b) -- keep right
+ (RCM Nothing (Just a),RCM (Just b) Nothing) -> RCM (Just b) (Just a)
+ (RCM Nothing (Just _a),RCM (Just b) (Just c)) -> RCM (Just b) (Just c) -- keep right
+ (RCM (Just a) Nothing,RCM Nothing Nothing) -> RCM (Just a) Nothing
+ (RCM (Just a) Nothing,RCM Nothing (Just b)) -> RCM (Just a) (Just b)
+ (RCM (Just _a) Nothing,RCM (Just b) Nothing) -> RCM (Just b) Nothing -- keep right
+ (RCM (Just _a) Nothing,RCM (Just b) (Just c)) -> RCM (Just b) (Just c)
+ (RCM (Just a) (Just b),RCM Nothing Nothing) -> RCM (Just a) (Just b)
+ (RCM (Just a) (Just _b),RCM Nothing (Just c)) -> RCM (Just a) (Just c)
+ (RCM (Just _a) (Just b),RCM (Just c) Nothing) -> RCM (Just c) (Just b)
+ (RCM (Just _a) (Just _b),RCM (Just c) (Just d)) -> RCM (Just c) (Just d)
+ -- we could also have _ _, (Just c) (Just d) -> (Just c, Just d)
+ }
+
=====================================
compiler/GHC/Types/Hint.hs
=====================================
@@ -41,7 +41,7 @@ import GHC.Types.SrcLoc (SrcSpan)
import GHC.Types.Basic (Activation, RuleName)
import {-# SOURCE #-} GHC.Tc.Types.Origin ( ClsInstOrQC(..) )
import GHC.Parser.Errors.Basic
-import {-# SOURCE #-} Language.Haskell.Syntax.Expr
+import Language.Haskell.Syntax.Expr
import GHC.Unit.Module.Imported (ImportedModsVal)
import GHC.Data.FastString (fsLit)
import Language.Haskell.Syntax (LPat, LIdP)
=====================================
compiler/GHC/Types/TyThing/Ppr.hs-boot
=====================================
@@ -3,7 +3,7 @@ module GHC.Types.TyThing.Ppr (
pprTyThingInContext
) where
-import {-# SOURCE #-} GHC.Iface.Type ( ShowSub )
+import GHC.Iface.Type ( ShowSub )
import GHC.Types.TyThing ( TyThing )
import GHC.Utils.Outputable ( SDoc )
=====================================
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
=====================================
@@ -88,6 +88,7 @@ Library
array >= 0.1 && < 0.6,
filepath >= 1 && < 1.5,
template-haskell == 2.20.*,
+ hegg,
hpc == 0.6.*,
transformers >= 0.5 && < 0.7,
exceptions == 0.10.*,
@@ -299,6 +300,7 @@ Library
GHC.Core.ConLike
GHC.Core.DataCon
GHC.Core.FamInstEnv
+ GHC.Core.Equality
GHC.Core.FVs
GHC.Core.InstEnv
GHC.Core.Lint
@@ -816,7 +818,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,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh,
ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline,
- hsc2hs, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy,
+ hegg, hsc2hs, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy,
libffi, mtl, parsec, pretty, primitive, process, remoteIserv, rts,
runGhc, semaphoreCompat, stm, templateHaskell, terminfo, text, time, timeout, touchy,
transformers, unlit, unix, win32, xhtml,
@@ -37,8 +37,8 @@ ghcPackages =
[ array, base, binary, bytestring, cabalSyntax, cabal, checkPpr, checkExact, countDeps
, compareSizes, compiler, containers, deepseq, deriveConstants, directory
, exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh
- , ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline, hsc2hs
- , hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, libffi, mtl
+ , ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline
+ , hegg, hsc2hs, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, libffi, mtl
, parsec, pretty, process, rts, runGhc, stm, semaphoreCompat, templateHaskell
, terminfo, text, time, touchy, transformers, unlit, unix, win32, xhtml
, timeout
@@ -53,7 +53,7 @@ isGhcPackage = (`elem` ghcPackages)
array, base, binary, bytestring, cabalSyntax, cabal, checkPpr, checkExact, countDeps,
compareSizes, compiler, containers, deepseq, deriveConstants, directory,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh,
- ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline, hsc2hs,
+ ghcCompact, ghcConfig, ghcHeap, ghci, ghciWrapper, ghcPkg, ghcPrim, haddock, haskeline, hegg, hsc2hs,
hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy, remoteIserv, libffi, mtl,
parsec, pretty, primitive, process, rts, runGhc, semaphoreCompat, stm, templateHaskell,
terminfo, text, time, touchy, transformers, unlit, unix, win32, xhtml,
@@ -93,6 +93,7 @@ ghcPkg = util "ghc-pkg"
ghcPrim = lib "ghc-prim"
haddock = util "haddock"
haskeline = lib "haskeline"
+hegg = lib "hegg"
hsc2hs = util "hsc2hs"
hp2ps = util "hp2ps"
hpc = lib "hpc"
=====================================
hadrian/src/Rules/ToolArgs.hs
=====================================
@@ -162,6 +162,7 @@ toolTargets = [ binary
, ghci
, ghcPkg -- # executable
-- , haddock -- # depends on ghc library
+ , hegg
, hsc2hs -- # executable
, hpc
, hpcBin -- # executable
=====================================
hadrian/src/Settings/Default.hs
=====================================
@@ -89,6 +89,7 @@ stage0Packages = do
, ghci
, ghcPkg
, haddock
+ , hegg
, hsc2hs
, hpc
, hpcBin
@@ -137,6 +138,7 @@ stage1Packages = do
, ghcPkg
, ghcPrim
, haskeline
+ , hegg
, hp2ps
, hsc2hs
, integerGmp
=====================================
libraries/hegg
=====================================
@@ -0,0 +1 @@
+Subproject commit 238557096a773b8cbe70d141ed63aef302918a62
=====================================
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/CountDepsAst.stdout
=====================================
@@ -248,7 +248,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
=====================================
testsuite/tests/count-deps/CountDepsParser.stdout
=====================================
@@ -255,7 +255,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/ebaf87dc732ac437b5f452c425456abe1895fdda...9d2039eecbf8e8ca071c63803640a3e32c05ee01
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ebaf87dc732ac437b5f452c425456abe1895fdda...9d2039eecbf8e8ca071c63803640a3e32c05ee01
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/20230702/93719285/attachment-0001.html>
More information about the ghc-commits
mailing list