[Git][ghc/ghc][wip/romes/eqsat-pmc] Improve term representation in e-graph and code complexity too, it's almost reasonable
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Tue Aug 1 17:35:29 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
f44f0fd4 by Rodrigo Mesquita at 2023-08-01T18:34:55+01:00
Improve term representation in e-graph and code complexity too, it's almost reasonable
Fixes
- - - - -
7 changed files:
- compiler/GHC/Core.hs
- compiler/GHC/Core/Equality.hs
- compiler/GHC/HsToCore/Pmc.hs
- compiler/GHC/HsToCore/Pmc/Check.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- compiler/GHC/Types/Hint.hs
Changes:
=====================================
compiler/GHC/Core.hs
=====================================
@@ -295,6 +295,7 @@ data AltCon
-- The instance adheres to the order described in Note [Case expression invariants]
instance Ord AltCon where
compare (DataAlt con1) (DataAlt con2) =
+ -- ROMES:TODO: Couldn't simply do this right by comparing the dataConName of the cons?
assert (dataConTyCon con1 == dataConTyCon con2) $
compare (dataConTag con1) (dataConTag con2)
compare (DataAlt _) _ = GT
=====================================
compiler/GHC/Core/Equality.hs
=====================================
@@ -1,39 +1,31 @@
-{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DerivingVia #-}
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.DataCon
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)
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Reader
+
-- Important to note the binders are also represented by $a$
-- This is because in the e-graph we will represent binders with the
-- equivalence class id of things equivalent to it.
@@ -41,300 +33,105 @@ import GHC.Core.Coercion (coercionType)
-- 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)
+-- In the pattern match checker, expressions will always be kind of shallow.
+-- In practice, no-one writes gigantic lambda expressions in guards and view patterns
-data BindF b a
- = NonRecF b a
- | RecF [(b, a)]
- deriving (Functor, Foldable, Traversable)
+data AltF a
+ = AltF AltCon' [()] a
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
-data ExprF b a
- = VarF Id
+data BindF a
+ = NonRecF a
+ | RecF [a]
+ deriving (Functor, Foldable, Traversable, Eq, Ord, Show)
+
+type BoundVar = Int
+data ExprF a
+ = VarF BoundVar
+ | FreeVarF 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
+ | LamF a
+ | LetF (BindF a) a
+ | CaseF a [AltF a] -- can we drop the case type for expr equality? we don't need them back, we just need to check equality. (perhaps this specialization makes this more suitable in the Pmc namespace)
+
+ -- | CastF a (DeBruijn CoercionR) -- can we drop this
+ -- | TickF CoreTickish a -- this, when representing expressions for equality?
+ -- but it'll be pretty hard to trigger any bug related to equality matching wrt coercions and casts on view and guard patterns solely
+ | TypeF DBType
+ | CoercionF DBCoercion
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
+
+newtype DBType = DBT (DeBruijn Type) deriving Eq
+instance Ord DBType where
+ compare (DBT dt) (DBT dt') = cmpDeBruijnType dt dt'
+newtype DBCoercion = DBC (DeBruijn Coercion) deriving Eq
+instance Ord DBCoercion where
+ compare (DBC dt) (DBC dt') = cmpDeBruijnCoercion dt dt'
+
+newtype AltCon' = AC' AltCon deriving Eq
+ deriving Outputable via AltCon
+
+instance Ord AltCon' where
+ compare (AC' (DataAlt a)) (AC' (DataAlt b))
+ = case compare (dataConName a) (dataConName b) of
+ LT -> LT
+ EQ -> compare (DataAlt a) (DataAlt b) -- AltCon's Ord instance only works for same datatypes
+ GT -> GT
+ compare (AC' a) (AC' b) = compare a b
+
+-- this makes perfect sense, if we already have to represent this in the e-graph
+-- we might as well make it a better suited representation for the e-graph...
+-- keeping the on-fly debruijn is harder
+representCoreExprEgr :: forall a
+ . Analysis a CoreExprF
+ => CoreExpr
+ -> EGraph a CoreExprF
+ -> (ClassId, EGraph a CoreExprF)
+representCoreExprEgr expr egr = EGM.runEGraphM egr (runReaderT (go expr) emptyCME) where
+ go :: CoreExpr -> ReaderT CmEnv (EGM.EGraphM a CoreExprF) ClassId
+ go = \case
+ Var v -> do
+ env <- ask
+ case lookupCME env v of
+ Nothing -> addE (FreeVarF v)
+ Just i -> addE (VarF i)
+ Lit lit -> addE (LitF lit)
+ Type t -> addE (TypeF (DBT $ deBruijnize t))
+ Coercion c -> addE (CoercionF (DBC $ deBruijnize c))
+ Tick _ e -> go e -- bypass ticks!
+ Cast e _ -> go e -- bypass casts! ouch? TODO
+ App f a -> do
+ f' <- go f
+ a' <- go a
+ addE (AppF f' a')
+ Lam b e -> do
+ e' <- local (`extendCME` b) $ go e
+ addE (LamF e')
+ Let (NonRec v r) e -> do
+ r' <- go r
+ e' <- local (`extendCME` v) $ go e
+ addE (LetF (NonRecF r') e')
+ Let (Rec (unzip -> (bs,rs))) e -> do
+ rs' <- traverse (local (`extendCMEs` bs) . go) rs
+ e' <- local (`extendCMEs` bs) $ go e
+ addE (LetF (RecF rs') e')
+ Case e b _t as -> do
+ e' <- go e
+ as' <- traverse (local (`extendCME` b) . goAlt) as
+ addE (CaseF e' as')
+
+ goAlt :: CoreAlt -> ReaderT CmEnv (EGM.EGraphM a CoreExprF) (CoreAltF ClassId)
+ goAlt (Alt c bs e) = do
+ e' <- local (`extendCMEs` bs) $ go e
+ return (AltF (AC' c) (map (const ()) bs) e')
+
+ addE :: Analysis a CoreExprF => CoreExprF ClassId -> ReaderT CmEnv (EGM.EGraphM a CoreExprF) ClassId
+ addE e = lift $ EGM.add $ Node e
+
+type CoreExprF = ExprF
+type CoreAltF = AltF
+type CoreBindF = BindF
cmpDeBruijnTickish :: DeBruijn CoreTickish -> DeBruijn CoreTickish -> Ordering
cmpDeBruijnTickish (D env1 t1) (D env2 t2) = go t1 t2 where
@@ -352,33 +149,28 @@ cmpDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Ordering
cmpDeBruijnType d1@(D _ t1) d2@(D _ t2)
= if eqDeBruijnType d1 d2
then EQ
- -- ROMES:TODO: Is this OK?
+ -- ROMES:TODO: This definitely does not look 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
+-- -- instances for debugging purposes
+instance Show a => Show (CoreExprF a) where
+ show (VarF id) = showPprUnsafe $ text "VarF" <+> ppr id
+ show (FreeVarF id) = showPprUnsafe $ ppr id
+ show (LitF lit) = showPprUnsafe $ text "LitF" <+> ppr lit
+ show (AppF a b) = "AppF " ++ show a ++ " " ++ show b
+ show (LamF a) = "LamF " ++ show a
+ show (LetF b a) = "LetF " ++ show b ++ " " ++ show a
+ show (CaseF a alts) = "CaseF " ++ show a ++ show alts
+
+ -- show (CastF _a _cor) = "CastF"
+ -- show (TickF _cotick _a) = "Tick"
+ show (TypeF (DBT (D _ t))) = "TypeF " ++ showPprUnsafe (ppr t)
+ show (CoercionF (DBC (D _ co))) = "CoercionF " ++ showPprUnsafe co
+
+instance Show a => Show (AltF a) where
show (AltF alt bs a) = "AltF " ++ showPprUnsafe (ppr alt <+> ppr bs) ++ show a
-
=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -103,19 +103,19 @@ noCheckDs = updTopFlags (\dflags -> foldl' wopt_unset dflags allPmCheckWarnings)
pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM Nablas
pmcPatBind ctxt@(DsMatchContext match_ctxt loc) var p
= mb_discard_warnings $ do
- !missing <- getLdiNablas
+ !missing0 <- getLdiNablas
-- See Note (TODO) [Represent the MatchIds before the CheckAction]
- let missing' = representIdNablas var missing
+ let missing = representIdNablas var missing0
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 "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
+ result <- unCA (checkPatBind pat_bind) missing
let ldi = ldiGRHS $ ( \ pb -> case pb of PmPatBind grhs -> grhs) $ cr_ret result
tracePm "pmcPatBind }: " $
vcat [ text "cr_uncov:" <+> ppr (cr_uncov result)
, text "ldi:" <+> ppr ldi ]
- formatReportWarnings ReportPatBind ctxt [var] result{cr_uncov = cr_uncov'}
+ formatReportWarnings ReportPatBind ctxt [var] result
return ldi
where
-- See Note [pmcPatBind doesn't warn on pattern guards]
@@ -176,21 +176,22 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
-- We have to force @missing@ before printing out the trace message,
-- otherwise we get interleaved output from the solver. This function
-- should be strict in @missing@ anyway!
- !missing <- getLdiNablas
+ !missing0 <- getLdiNablas
+
+ -- See Note (TODO) [Represent the MatchIds before the CheckAction]
+ let missing = representIdsNablas vars missing0
+
tracePm "pmcMatches {" $
hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
2
(vcat (map ppr matches) $$ ppr missing)
- -- See Note (TODO) [Represent the MatchIds before the CheckAction]
- let missing' = representIdsNablas vars missing
-
case NE.nonEmpty matches of
Nothing -> 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'
+ result <- unCA (checkEmptyCase empty_case) missing
tracePm "}: " (ppr (cr_uncov result))
formatReportWarnings ReportEmptyCase ctxt vars result
return []
@@ -198,7 +199,7 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
matches <- {-# SCC "desugarMatches" #-}
noCheckDs $ desugarMatches vars matches
result <- {-# SCC "checkMatchGroup" #-}
- unCA (checkMatchGroup matches) missing'
+ unCA (checkMatchGroup matches) missing
tracePm "}: " (ppr (cr_uncov result))
{-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt vars result
return (NE.toList (ldiMatchGroup (cr_ret result)))
@@ -262,7 +263,10 @@ pmcRecSel :: Id -- ^ Id of the selector
-> DsM ()
pmcRecSel sel_id arg
| RecSelId{ sel_cons = (cons_w_field, _ : _) } <- idDetails sel_id = do
- !missing <- getLdiNablas
+ !missing0 <- getLdiNablas
+
+ -- See Note (TODO) [Represent the MatchIds before the CheckAction]
+ let missing = representIdNablas sel_id missing0
tracePm "pmcRecSel {" (ppr sel_id)
CheckResult{ cr_ret = PmRecSel{ pr_arg_var = arg_id }, cr_uncov = uncov_nablas }
@@ -278,7 +282,8 @@ pmcRecSel sel_id arg
let maxConstructors = maxUncoveredPatterns dflags
unc_examples <- getNFirstUncovered MinimalCover [arg_id] (maxConstructors + 1) uncov_nablas
let cons = [con | unc_example <- unc_examples
- , Just (PACA (PmAltConLike con) _ _) <- [lookupSolution unc_example arg_id]]
+ -- we've represented this Id above, see Note...
+ , Just (PACA (PmAltConLike con) _ _) <- [lookupSolution unc_example (fromJust (arg_id `lookupMatchIdMap` unc_example))]]
not_full_examples = length cons == (maxConstructors + 1)
cons' = take maxConstructors cons
diagnosticDs $ DsIncompleteRecordSelector sel_name cons' not_full_examples
@@ -288,7 +293,6 @@ pmcRecSel _ _ = return ()
{- Note [pmcPatBind doesn't warn on pattern guards]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@pmcPatBind@'s main purpose is to check vanilla pattern bindings, like
->>>>>>> 8760510af3 (This MR is an implementation of the proposal #516.)
@x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
But its caller is also called for individual pattern guards in a @StmtCtxt at .
For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
@@ -550,11 +554,9 @@ 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) (x0:xs) k =
- flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas0 ->
- liftNablasM (\d ->
- let (x, d') = representId x0 d
- in addPhiCts d' (unitBag (PhiCoreCt x scr))) nablas0
+addCoreScrutTmCs (scr:scrs) (x:xs) k =
+ flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas ->
+ addPhiCtNablasWithRep nablas x (`PhiCoreCt` scr)
addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: numbers of scrutinees and match ids differ"
-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.
=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -198,10 +198,12 @@ checkRecSel pr@(PmRecSel { pr_arg = arg, pr_cons = cons }) = CA $ \inc -> do
Var arg_id -> return arg_id
_ -> mkPmId $ exprType arg
- let con_cts = map (PhiNotConCt arg_id . PmAltConLike) cons
- arg_ct = PhiCoreCt arg_id arg
- phi_cts = listToBag (arg_ct : con_cts)
- unc <- addPhiCtsNablas inc phi_cts
+ unc <- liftNablasM (\d ->
+ let (arg_id', d') = representId arg_id d
+ con_cts = map (PhiNotConCt arg_id' . PmAltConLike) cons
+ arg_ct = PhiCoreCt arg_id' arg
+ phi_cts = listToBag (arg_ct : con_cts)
+ in addPhiCts d' phi_cts) inc
pure CheckResult { cr_ret = pr{ pr_arg_var = arg_id }, cr_uncov = unc, cr_approx = mempty }
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -64,7 +64,6 @@ import GHC.Types.Unique.Supply
import GHC.Core
import GHC.Core.FVs (exprFreeVars)
import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Map.Type
import GHC.Core.Equality
import GHC.Core.Predicate (typeDeterminesValue)
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
@@ -1022,7 +1021,7 @@ modifyT f = StateT $ fmap ((,) ()) . f
-- there weren't any such constraints.
representCoreExpr :: Nabla -> CoreExpr -> (ClassId, Nabla)
representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = egraph } } e =
- second (\g -> nabla{nabla_tm_st = ts{ts_facts = g}}) $ representDBCoreExpr (deBruijnize (makeDictsCoherent e)) egraph
+ second (\g -> nabla{nabla_tm_st = ts{ts_facts = EG.rebuild g}}) $ representCoreExprEgr (makeDictsCoherent e) egraph
-- Use a key in which dictionaries for the same type become equal.
-- See Note [Unique dictionaries in the TmOracle CoreMap]
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -67,7 +67,6 @@ import GHC.Core.TyCon
import GHC.Types.Literal
import GHC.Core
import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Map.Type
import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
@@ -173,7 +172,7 @@ data TmState
lookupMatchIdMap :: Id -> Nabla -> Maybe ClassId
lookupMatchIdMap id (MkNabla _ TmSt{ts_reps}) = lookupVarEnv ts_reps id
--- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
+-- | Information about a match id. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
-- and negative ('vi_neg') facts, like "x is not (:)".
-- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
-- ('vi_rcm').
@@ -187,6 +186,9 @@ data VarInfo
-- 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_ty :: !Type
+ -- The type of the match-id
+
, vi_pos :: ![PmAltConApp]
-- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
-- at the same time (i.e. conjunctive). We need a list because of nested
@@ -333,6 +335,7 @@ emptyVarInfo x
-- 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
+-- We used to only create an emptyVarInfo when we looked up that id. Now we do it always, even if we never query the Id back T_T
-- 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
@@ -841,7 +844,7 @@ instance Outputable PmEquality where
-- * E-graphs to represent normalised refinment types
--
-type TmEGraph = EGraph VarInfo (DeBruijnF CoreExprF)
+type TmEGraph = EGraph VarInfo CoreExprF
-- TODO delete orphans for showing TmEGraph for debugging reasons
instance Show VarInfo where
show = showPprUnsafe . ppr
@@ -858,13 +861,14 @@ representIdsNablas xs = execState (mapM (\x -> state (((),) . representIdNablas
representId :: Id -> Nabla -> (ClassId, Nabla)
representId x (MkNabla tyst tmst at TmSt{ts_facts=eg0, ts_reps=idmp})
= case lookupVarEnv idmp x of
- -- The reason why we can't use an empty new class is that we don't account for the IdMap in the 'representDBCoreExpr'
+ -- The reason why we can't use an empty new class is that we don't account for the IdMap in the 'representCoreExprEgr'
-- In particular, if we represent "reverse @a xs" in the e-graph, the
-- node in which "xs" will be represented won't match the e-class id
-- representing "xs", because that class doesn't contain "VarF xs"
+ -- (but at least we can still mkMatchIds without storing the VarF for that one)
-- Nothing -> case EG.newEClass (emptyVarInfo x) eg0 of
- Nothing -> case EG.add (EG.Node (DF (deBruijnize (VarF x)))) eg0 of
- (xid, eg1) -> (xid, MkNabla tyst tmst{ts_facts=eg1, ts_reps=extendVarEnv idmp x xid})
+ Nothing -> case EG.add (EG.Node (FreeVarF x)) eg0 of
+ (xid, eg1) -> (xid, MkNabla tyst tmst{ts_facts=EG.rebuild eg1, ts_reps=extendVarEnv idmp x xid})
Just xid -> (xid, MkNabla tyst tmst)
representIds :: [Id] -> Nabla -> ([ClassId], Nabla)
@@ -874,7 +878,7 @@ representIds xs = runState (mapM (state . representId) xs)
-- 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
+instance Analysis VarInfo CoreExprF where
{-# INLINE makeA #-}
{-# INLINE joinA #-}
@@ -886,11 +890,10 @@ instance Analysis VarInfo (DeBruijnF CoreExprF) where
-- 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.
+ makeA (FreeVarF x) = emptyVarInfo x
+ makeA _ = emptyVarInfo unitDataConId
+ -- makeA _ = Nothing
+ -- Always start with Nothing, and add things as we go?
-- 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
@@ -904,7 +907,12 @@ instance Analysis VarInfo (DeBruijnF CoreExprF) where
-- 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
+ -- joinA Nothing Nothing = Nothing
+ -- joinA Nothing (Just b) = Just b
+ -- joinA (Just a) Nothing = Just a
+ -- joinA (Just a) (Just b)
+ 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
=====================================
compiler/GHC/Types/Hint.hs
=====================================
@@ -21,6 +21,7 @@ module GHC.Types.Hint (
, noStarIsTypeHints
) where
+import Language.Haskell.Syntax.Expr (LHsExpr)
import Language.Haskell.Syntax (LPat, LIdP)
import GHC.Prelude
@@ -46,9 +47,6 @@ import GHC.Utils.Outputable
import GHC.Data.FastString (fsLit, FastString)
import Data.Typeable ( Typeable )
-import Language.Haskell.Syntax.Expr
- -- This {-# SOURCE #-} import should be removable once
- -- 'Language.Haskell.Syntax.Bind' no longer depends on 'GHC.Tc.Types.Evidence'.
-- | The bindings we have available in scope when
-- suggesting an explicit type signature.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f44f0fd4366cc5df2a782e13b26cee48ead528c8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f44f0fd4366cc5df2a782e13b26cee48ead528c8
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/20230801/59eceb0c/attachment-0001.html>
More information about the ghc-commits
mailing list