[Git][ghc/ghc][wip/romes/eqsat-pmc] 13 commits: Add e-graphs submodule (hegg)
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Tue Aug 22 21:39:13 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
9d37014f by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Add e-graphs submodule (hegg)
- - - - -
8f3d6bae by Rodrigo Mesquita at 2023-08-22T22:38:42+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.
- - - - -
2eb7382c by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Question
- - - - -
42efcef5 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Was going great until I started needing to thread ClassIds together with Ids. Ret-think this.
- - - - -
a6a90389 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
A solution with more lookups
Fixes to Pmc.Ppr module
Wow, a lot (stage1) is working actually, without PMC errprs
We're still not there yet.
WiP
- - - - -
3c779872 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Add instances for debugging
- - - - -
f5fa7c62 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Things that were broken due to unlawfulness of e-graph instances
- - - - -
6812a792 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Scuffed merging without effects to salvage some information that might get lost in merging that happens outside of addVarCt
- - - - -
553a8638 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
This is the commit where it does works:
* Drops SDFM module
- - - - -
f2f3bc8a by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Improve a little bit the mixing of Ids and ClassIds
tWeaks
Don't use EG.rebuild as a view pattern
Debuggging
Touches
Fix to representId over multiple (different) nablas
Paper over
Chagnes2
Then....Start going the other direction
- - - - -
949f0ce6 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Get compilation with more exhaustiveness working again,
but this time with a cleaner story, since in PhiCt we already only have
ClassIds.
It works for the first two examples in #19272, but it does not solve the
latest contrived example we came up with -- I think it's likely because
of rebuilding.
RE rebuilding: It doesn't look like usually there are many/any things in
the worklist, meaning it's probably quite cheap to rebuild often.
- - - - -
17c43d59 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
Improve term representation in e-graph and code complexity too, it's almost reasonable
Fixes
- - - - -
0b0270e3 by Rodrigo Mesquita at 2023-08-22T22:38:42+01:00
WIP
- - - - -
20 changed files:
- .gitmodules
- compiler/GHC/Core.hs
- + 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/Ppr.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- − compiler/GHC/Types/Unique/SDFM.hs
- compiler/ghc.cabal.in
- hadrian/src/Packages.hs
- hadrian/src/Rules/ToolArgs.hs
- hadrian/src/Settings/Default.hs
- + libraries/hegg
- packages
- testsuite/tests/count-deps/CountDepsParser.stdout
Changes:
=====================================
.gitmodules
=====================================
@@ -117,3 +117,6 @@
[submodule "utils/hpc"]
path = utils/hpc
url = https://gitlab.haskell.org/hpc/hpc-bin.git
+[submodule "libraries/hegg"]
+ path = libraries/hegg
+ url = https://github.com/alt-romes/hegg.git
=====================================
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
=====================================
@@ -0,0 +1,184 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DerivingVia #-}
+
+-- TODO: Rename to GHC.HsToCore.CoreEquality or something
+module GHC.Core.Equality where
+
+import GHC.Prelude
+
+-- import GHC.Types.Name (Name)
+import GHC.Core
+import GHC.Core.DataCon
+import GHC.Core.TyCo.Rep
+import GHC.Core.Map.Type
+import GHC.Types.Var
+import GHC.Types.Literal
+import GHC.Types.Tickish
+
+import Data.Equality.Graph as EG
+import Data.Equality.Analysis.Monadic
+import qualified Data.Equality.Graph.Monad as EGM
+import GHC.Utils.Outputable
+import GHC.Core.Coercion (coercionType)
+
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Reader
+
+-- Important to note the binders are also represented by $a$
+-- This is because in the e-graph we will represent binders with the
+-- equivalence class id of things equivalent to it.
+--
+-- Unfortunately type binders are still not correctly accounted for.
+-- Perhaps it'd really be better to make DeBruijn work over these types
+
+-- In the pattern match checker, expressions will always be kind of shallow.
+-- In practice, no-one writes gigantic lambda expressions in guards and view patterns
+
+data AltF a
+ = AltF AltCon' [()] a -- [()] tells us the number of constructors..., bad representation TODO
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
+
+data BindF a
+ = NonRecF a
+ | RecF [a]
+ deriving (Functor, Foldable, Traversable, Eq, Ord, Show)
+
+type BoundVar = Int
+-- If we use this datatype specifically for representing HsToCore.Pmc, we may
+-- be able to drop the coercion field, and add a specific one for constructor
+-- application
+data ExprF r
+ = VarF BoundVar
+ -- ROMES:TODO: what about using Names for comparison? Since this is only for equality purposes...
+ -- It makes it possible to use the ConLikeName as the FreeVar Name, since there is conLikeName for PmAltConLike
+ | FreeVarF Id
+ | LitF Literal
+ | AppF r r
+ | LamF r
+ | LetF (BindF r) r
+ | CaseF r [AltF r] -- can we drop the case type for expr equality? we don't need them back, we just need to check equality. (perhaps this specialization makes this more suitable in the Pmc namespace)
+
+ -- | CastF a (DeBruijn CoercionR) -- can we drop this
+ -- | TickF CoreTickish a -- this, when representing expressions for equality?
+ -- but it'll be pretty hard to trigger any bug related to equality matching wrt coercions and casts on view and guard patterns solely
+ | TypeF DBType
+ | CoercionF DBCoercion
+ deriving (Functor, Foldable, Traversable, Eq, Ord)
+
+newtype DBType = DBT (DeBruijn Type) deriving Eq
+instance Ord DBType where
+ compare (DBT dt) (DBT dt') = cmpDeBruijnType dt dt'
+newtype DBCoercion = DBC (DeBruijn Coercion) deriving Eq
+instance Ord DBCoercion where
+ compare (DBC dt) (DBC dt') = cmpDeBruijnCoercion dt dt'
+
+newtype AltCon' = AC' AltCon deriving Eq
+ deriving Outputable via AltCon
+
+instance Ord AltCon' where
+ compare (AC' (DataAlt a)) (AC' (DataAlt b))
+ = case compare (dataConName a) (dataConName b) of
+ LT -> LT
+ EQ -> compare (DataAlt a) (DataAlt b) -- AltCon's Ord instance only works for same datatypes
+ GT -> GT
+ compare (AC' a) (AC' b) = compare a b
+
+-- this makes perfect sense, if we already have to represent this in the e-graph
+-- we might as well make it a better suited representation for the e-graph...
+-- keeping the on-fly debruijn is harder
+representCoreExprEgr :: forall a m
+ . Analysis m a CoreExprF
+ => CoreExpr
+ -> EGraph a CoreExprF
+ -> m (ClassId, EGraph a CoreExprF)
+representCoreExprEgr expr egr = EGM.runEGraphMT egr (runReaderT (go expr) emptyCME) where
+ go :: CoreExpr -> ReaderT CmEnv (EGM.EGraphMT a CoreExprF m) ClassId
+ go = \case
+ Var v -> do
+ env <- ask
+ case lookupCME env v of
+ -- Nothing -> addE (FreeVarF $ varName v)
+ Nothing -> addE (FreeVarF v)
+ Just i -> addE (VarF i)
+ Lit lit -> addE (LitF lit)
+ Type t -> addE (TypeF (DBT $ deBruijnize t))
+ Coercion c -> addE (CoercionF (DBC $ deBruijnize c))
+ Tick _ e -> go e -- bypass ticks!
+ Cast e _ -> go e -- bypass casts! ouch? TODO
+ App f a -> do
+ f' <- go f
+ a' <- go a
+ addE (AppF f' a')
+ Lam b e -> do
+ e' <- local (`extendCME` b) $ go e
+ addE (LamF e')
+ Let (NonRec v r) e -> do
+ r' <- go r
+ e' <- local (`extendCME` v) $ go e
+ addE (LetF (NonRecF r') e')
+ Let (Rec (unzip -> (bs,rs))) e -> do
+ rs' <- traverse (local (`extendCMEs` bs) . go) rs
+ e' <- local (`extendCMEs` bs) $ go e
+ addE (LetF (RecF rs') e')
+ Case e b _t as -> do
+ e' <- go e
+ as' <- traverse (local (`extendCME` b) . goAlt) as
+ addE (CaseF e' as')
+
+ goAlt :: CoreAlt -> ReaderT CmEnv (EGM.EGraphMT a CoreExprF m) (CoreAltF ClassId)
+ goAlt (Alt c bs e) = do
+ e' <- local (`extendCMEs` bs) $ go e
+ return (AltF (AC' c) (map (const ()) bs) e')
+
+ addE :: Analysis m a CoreExprF => CoreExprF ClassId -> ReaderT CmEnv (EGM.EGraphMT a CoreExprF m) ClassId
+ addE e = lift $ EGM.addM $ Node e
+
+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
+ go (Breakpoint lext lid lids _) (Breakpoint rext rid rids _)
+ = case compare lid rid of
+ LT -> LT
+ EQ -> case compare (D env1 lids) (D env2 rids) of
+ LT -> LT
+ EQ -> compare lext rext
+ GT -> GT
+ GT -> GT
+ go l r = compare l r
+
+cmpDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Ordering
+cmpDeBruijnType d1@(D _ t1) d2@(D _ t2)
+ = if eqDeBruijnType d1 d2
+ then EQ
+ -- ROMES:TODO: This definitely does not look OK.
+ else compare (showPprUnsafe t1) (showPprUnsafe t2)
+
+cmpDeBruijnCoercion :: DeBruijn Coercion -> DeBruijn Coercion -> Ordering
+cmpDeBruijnCoercion (D env1 co1) (D env2 co2)
+ = cmpDeBruijnType (D env1 (coercionType co1)) (D env2 (coercionType co2))
+
+-- -- instances for debugging purposes
+instance Show a => Show (CoreExprF a) where
+ show (VarF id) = showPprUnsafe $ text "VarF" <+> ppr id
+ show (FreeVarF id) = showPprUnsafe $ ppr id
+ show (LitF lit) = showPprUnsafe $ text "LitF" <+> ppr lit
+ show (AppF a b) = "AppF " ++ show a ++ " " ++ show b
+ show (LamF a) = "LamF " ++ show a
+ show (LetF b a) = "LetF " ++ show b ++ " " ++ show a
+ show (CaseF a alts) = "CaseF " ++ show a ++ show alts
+
+ -- show (CastF _a _cor) = "CastF"
+ -- show (TickF _cotick _a) = "Tick"
+ show (TypeF (DBT (D _ t))) = "TypeF " ++ showPprUnsafe (ppr t)
+ show (CoercionF (DBC (D _ co))) = "CoercionF " ++ showPprUnsafe co
+
+instance Show a => Show (AltF a) where
+ show (AltF alt bs a) = "AltF " ++ showPprUnsafe (ppr alt <+> ppr bs) ++ show a
+
=====================================
compiler/GHC/Core/Map/Expr.hs
=====================================
@@ -18,6 +18,8 @@ module GHC.Core.Map.Expr (
CoreMap, emptyCoreMap, extendCoreMap, lookupCoreMap, foldCoreMap,
-- * Alpha equality
eqDeBruijnExpr, eqCoreExpr,
+ -- ** Exports for CoreExprF instances
+ eqDeBruijnTickish, eqDeBruijnVar,
-- * 'TrieMap' class reexports
TrieMap(..), insertTM, deleteTM,
lkDFreeVar, xtDFreeVar,
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -6,6 +6,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DeriveTraversable #-}
module GHC.Core.Map.Type (
-- * Re-export generic interface
@@ -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
=====================================
@@ -22,6 +22,8 @@ import GHC.Utils.Misc
import GHC.Utils.Outputable
import qualified GHC.LanguageExtensions as LangExt
import GHC.HsToCore.Pmc.Ppr
+import GHC.HsToCore.Pmc.Solver.Types (lookupMatchIdMap)
+import Data.Maybe (fromJust)
instance Diagnostic DsMessage where
@@ -71,7 +73,8 @@ instance Diagnostic DsMessage where
pprContext False kind (text "are non-exhaustive") $ \_ ->
case vars of -- See #11245
[] -> text "Guards do not cover entire pattern space"
- _ -> let us = map (\nabla -> pprUncovered nabla vars) nablas
+ -- See Note (TODO) [The MatchIds for error reporting] (and possibly factor this map lookupMatchIdMap outside)
+ _ -> let us = map (\nabla -> pprUncovered nabla (map (fromJust . (`lookupMatchIdMap` nabla)) vars)) nablas
pp_tys = pprQuotedList $ map idType vars
in hang
(text "Patterns of type" <+> pp_tys <+> text "not matched:")
=====================================
compiler/GHC/HsToCore/Errors/Types.hs
=====================================
@@ -100,7 +100,7 @@ data DsMessage
| DsNonExhaustivePatterns !(HsMatchContext GhcTc)
!ExhaustivityCheckType
!MaxUncoveredPatterns
- [Id]
+ [Id] -- ^ The MatchIds, see Note (TODO) [The MatchIds for error reporting]
[Nabla]
| DsTopLevelBindsNotAllowed !BindsType !(HsBindLR GhcTc GhcTc)
=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -75,6 +75,10 @@ import qualified Data.List.NonEmpty as NE
import Data.Coerce
import GHC.Tc.Utils.Monad
+import Control.Monad.Trans.Maybe
+
+import Data.Maybe (fromJust)
+
--
-- * Exported entry points to the checker
--
@@ -101,7 +105,11 @@ 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]
+ Just missing <- runMaybeT $ 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
@@ -170,11 +178,16 @@ 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]
+ Just missing <- runMaybeT $ representIdsNablas vars missing0
+
tracePm "pmcMatches {" $
hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
2
(vcat (map ppr matches) $$ ppr missing)
+
case NE.nonEmpty matches of
Nothing -> do
-- This must be an -XEmptyCase. See Note [Checking EmptyCase]
@@ -252,7 +265,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]
+ Just missing <- runMaybeT $ representIdNablas sel_id missing0
tracePm "pmcRecSel {" (ppr sel_id)
CheckResult{ cr_ret = PmRecSel{ pr_arg_var = arg_id }, cr_uncov = uncov_nablas }
@@ -268,7 +284,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
@@ -278,7 +295,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
@@ -445,7 +461,11 @@ 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
+ -> [Id] -- ^ The MatchIds, see Note (TODO) [The MatchIds for error reporting]
+ -> CheckResult ann
+ -> DsM ()
formatReportWarnings report_mode ctx vars cr at CheckResult { cr_ret = ann } = do
cov_info <- collectInMode report_mode ann
dflags <- getDynFlags
@@ -492,13 +512,16 @@ reportWarnings dflags report_mode (DsMatchContext kind loc) vars
maxPatterns = maxUncoveredPatterns dflags
-getNFirstUncovered :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nablas -> DsM [Nabla]
+getNFirstUncovered :: GenerateInhabitingPatternsMode
+ -> [Id] -- ^ The MatchIds, see Note (TODO) [The MatchIds for error reporting]
+ -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered mode vars n (MkNablas nablas) = go n (bagToList nablas)
where
go 0 _ = pure []
go _ [] = pure []
go n (nabla:nablas) = do
- front <- generateInhabitingPatterns mode vars n nabla
+ -- See Note (TODO) [The MatchIds for error reporting] (and possibly factor this map lookupMatchIdMap to an independent function since its used twice, here and in the call of pprUncovered)
+ front <- generateInhabitingPatterns mode (map (fromJust . (`lookupMatchIdMap` nabla)) vars) n nabla
back <- go (n - length front) nablas
pure (front ++ back)
@@ -535,7 +558,7 @@ 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))
+ addPhiCtNablasWithRep nablas x (`PhiCoreCt` scr)
addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: numbers of scrutinees and match ids differ"
-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.
@@ -586,4 +609,18 @@ unreachable.
We make sure to always start from an inhabited 'Nablas' by calling
'getLdiNablas', which falls back to the trivially inhabited 'Nablas' if the
long-distance info returned by 'GHC.HsToCore.Monad.getPmNablas' is empty.
+
+Note [The MatchId for error reporting]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Something sometihng, when we're talking about MatchIds that might occur in
+Nablas (rather than just in a Nabla), we have to refer to them by Id, rather
+than by e-class-id.
+
+This is because e-class-ids will vary between Nabla, but each Nabla maps Ids to e-class-ids.
+So an Id is the only identifier that identifies the same match-id across Nablas.
+
+We can safely query each Nabla for the MatchIds because we make sure to
+represent the MatchIds in the Nablas as soon as possible (in pmcMatches and
+friends)
+
-}
=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -1,4 +1,5 @@
+{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
@@ -43,6 +44,8 @@ import GHC.Types.Var
import GHC.Core
import GHC.Core.Utils
+import Control.Monad.Trans.Maybe
+
-- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
newtype CheckAction a = CA { unCA :: Nablas -> DsM (CheckResult a) }
deriving Functor
@@ -110,15 +113,15 @@ checkGrd :: PmGrd -> CheckAction RedSets
checkGrd grd = CA $ \inc -> case grd of
-- let x = e: Refine with x ~ e
PmLet x e -> do
- matched <- addPhiCtNablas inc (PhiCoreCt x e)
+ matched <- addPhiCtNablasWithRep inc x (`PhiCoreCt` 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
- div <- addPhiCtNablas inc (PhiBotCt x)
- matched <- addPhiCtNablas inc (PhiNotBotCt x)
+ div <- addPhiCtNablasWithRep inc x PhiBotCt
+ matched <- addPhiCtNablasWithRep inc x PhiNotBotCt -- it will do a redundant lookup to represent x again... we would like @inc@ to have the rep already for both
-- See Note [Dead bang patterns]
-- mb_info = Just info <==> PmBang originates from bang pattern in source
let bangs | Just info <- mb_info = unitOL (div, info)
@@ -136,11 +139,12 @@ checkGrd grd = CA $ \inc -> case grd of
, 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
+ -- romes: for now we do the redundant representation of vars, but whatever
!div <- if isPmAltConMatchStrict con
- then addPhiCtNablas inc (PhiBotCt x)
+ then addPhiCtNablasWithRep inc x PhiBotCt
else pure mempty
- !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
- !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
+ !matched <- addPhiCtNablasWithReps inc (x:args) (\case (xi:argsi) -> PhiConCt xi con tvs (map evVarPred dicts) argsi; _ -> error "impossible")
+ !uncov <- addPhiCtNablasWithRep inc x (`PhiNotConCt` con)
tracePm "check:Con" $ vcat
[ ppr grd
, ppr inc
@@ -183,10 +187,10 @@ 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)
+ unc <- addPhiCtNablasWithRep inc var PhiNotBotCt
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
checkRecSel :: PmRecSel () -> CheckAction (PmRecSel Id)
@@ -196,10 +200,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 -> do
+ Just (arg_id', d') <- runMaybeT $ representId arg_id d
+ let con_cts = map (PhiNotConCt arg_id' . PmAltConLike) cons
+ arg_ct = PhiCoreCt arg_id' arg
+ phi_cts = listToBag (arg_ct : con_cts)
+ 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/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,6 +1,13 @@
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RankNTypes, GADTs #-}
+{-# OPTIONS_GHC -Wno-orphans #-} -- Analysis........
{-
Authors: George Karachalias <george.karachalias at cs.kuleuven.be>
@@ -26,14 +33,20 @@ module GHC.HsToCore.Pmc.Solver (
PhiCt(..), PhiCts,
addPhiCtNablas,
addPhiCtsNablas,
+ addPhiCtNablasWithRep, addPhiCtNablasWithReps,
+ liftNablasM,
+ addPhiCts,
isInhabited,
- generateInhabitingPatterns, GenerateInhabitingPatternsMode(..)
+ generateInhabitingPatterns, GenerateInhabitingPatternsMode(..),
+
+ representId, representIds, representIdNablas, representIdsNablas
) where
import GHC.Prelude
+import GHC.HsToCore.Monad
import GHC.HsToCore.Pmc.Types
import GHC.HsToCore.Pmc.Utils (tracePm, traceWhenFailPm, mkPmId)
@@ -49,22 +62,21 @@ 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.Equality
import GHC.Core.Predicate (typeDeterminesValue)
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils (exprType)
import GHC.Core.Make (mkListExpr, mkCharExpr, mkImpossibleExpr)
+import GHC.Core.Map.Type (deBruijnize) -- ROMES:TODO: Doesn't look good great. At least export some function from HsToCore Equality module to create the types. It's wrong; we should keep a debruijn map while representing the expression, and assign it correctly to each type? Not sure.
import GHC.Data.FastString
import GHC.Types.SrcLoc
@@ -83,7 +95,6 @@ import GHC.Tc.Solver (tcNormalise, tcCheckGivens, tcCheckWanteds)
import GHC.Core.Unify (tcMatchTy)
import GHC.Core.Coercion
import GHC.Core.Reduction
-import GHC.HsToCore.Monad hiding (foldlM)
import GHC.Tc.Instance.Family
import GHC.Core.FamInstEnv
@@ -93,12 +104,20 @@ import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict
import Data.Coerce
import Data.Either (partitionEithers)
-import Data.Foldable (foldlM, minimumBy, toList)
+import Data.Foldable (minimumBy, toList, foldrM)
import Data.Monoid (Any(..))
import Data.List (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
+import Data.Equality.Analysis.Monadic
+import Data.Equality.Graph (ClassId)
+import Data.Equality.Graph.Lens
+import qualified Data.Equality.Graph as EG
+import qualified Data.Equality.Graph.Monad as EGM
+import Data.Function ((&))
+import qualified Data.IntSet as IS
+
--
-- * Main exports
--
@@ -112,6 +131,16 @@ addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
+-- | 'addPmCtsNablas' for a single 'PmCt', but first represent the Id in each Nabla.
+addPhiCtNablasWithRep :: Nablas -> Id -> (ClassId -> PhiCt) -> DsM Nablas
+addPhiCtNablasWithRep nablas x ctf
+ = liftNablasM (\d -> do Just (xi, d') <- runMaybeT (representId x d); addPhiCts d' (unitBag (ctf xi))) nablas
+
+-- | Represent all Id in each Nabla.
+addPhiCtNablasWithReps :: Nablas -> [Id] -> ([ClassId] -> PhiCt) -> DsM Nablas
+addPhiCtNablasWithReps nablas xs ctf
+ = liftNablasM (\d -> do Just (xsi, d') <- runMaybeT (representIds xs d); addPhiCts d' (unitBag (ctf xsi))) nablas
+
liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds)
@@ -556,23 +585,24 @@ 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.
+-- Additionally, we use class-ids instead of ids (note... TODO)
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
@@ -663,97 +693,105 @@ nameTyCt pred_ty = do
addPhiTmCt :: Nabla -> PhiCt -> MaybeT DsM Nabla
addPhiTmCt _ (PhiTyCt ct) = pprPanic "addPhiCt:TyCt" (ppr ct) -- See the precondition
addPhiTmCt nabla (PhiCoreCt x e) = addCoreCt nabla x e
-addPhiTmCt nabla (PhiConCt x con tvs dicts args) = do
+addPhiTmCt nabla0 (PhiConCt x con tvs dicts args) = do
-- Case (1) of Note [Strict fields and variables of unlifted type]
-- 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 nabla0 (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 mergeBotCt nabla
+
+-- ROMES:TODO: we should only add bot constraints to the "underlying" match-id of newtypes...
+mergeBotCt :: VarInfo -> MaybeT DsM VarInfo
+mergeBotCt vi at VI { vi_bot = bot }
+-- oops, we should be looking up VarInfo NT here too.
+ -- ROMES:TODO:!!!! let (y, vi at VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x
+ = 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 (idType (vi_id vi))
+ -- 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
+ -- This means we only add not-bottom constraints to the true match-id of newtype constructors (ie skipping NT classes)
+ -- This is the only occurrence of lookupVarInfoNT.
+ 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
+ (mb_mark_dirty, nabla') <- trvVarInfo (mergeNotConCt nalt) nabla x
pure $ case mb_mark_dirty of
- Just x -> markDirty x nabla'
- Nothing -> nabla'
- where
- -- Update `x`'s 'VarInfo' entry. Fail ('MaybeT') if contradiction,
- -- otherwise return updated entry and `Just x'` if `x` should be marked dirty,
- -- where `x'` is the representative of `x`.
- go :: VarInfo -> MaybeT DsM (Maybe Id, VarInfo)
- go vi@(VI x' pos neg _ rcm) = do
- -- 1. Bail out quickly when nalt contradicts a solution
- let contradicts nalt sol = eqPmAltCon (paca_con sol) nalt == Equal
- guard (not (any (contradicts nalt) pos))
- -- 2. Only record the new fact when it's not already implied by one of the
- -- solutions
- let implies nalt sol = eqPmAltCon (paca_con sol) nalt == Disjoint
- let neg'
- | any (implies nalt) pos = neg
- -- See Note [Completeness checking with required Thetas]
- | hasRequiredTheta nalt = neg
- | otherwise = extendPmAltConSet neg nalt
- massert (isPmAltConMatchStrict nalt)
- let vi' = vi{ vi_neg = neg', vi_bot = IsNotBot }
- -- 3. Make sure there's at least one other possible constructor
- mb_rcm' <- lift (markMatched nalt rcm)
- pure $ case mb_rcm' of
- -- If nalt could be removed from a COMPLETE set, we'll get back Just and
- -- have to mark x dirty, by returning Just x'.
- Just rcm' -> (Just x', vi'{ vi_rcm = rcm' })
- -- Otherwise, nalt didn't occur in any residual COMPLETE set and we
- -- don't have to mark it dirty. So we return Nothing, which in the case
- -- above would have compromised precision.
- -- See Note [Shortcutting the inhabitation test], grep for T17836.
- Nothing -> (Nothing, vi')
+ True -> markDirty x nabla'
+ False -> nabla'
+
+-- Update `x`'s 'VarInfo' entry. Fail ('MaybeT') if contradiction,
+-- otherwise return updated entry and `Just x'` if `x` should be marked dirty,
+-- where `x'` is the representative of `x`.
+mergeNotConCt :: PmAltCon -> VarInfo -> MaybeT DsM (Bool, VarInfo)
+mergeNotConCt nalt vi@(VI _x' pos neg _ rcm) = do
+ -- 1. Bail out quickly when nalt contradicts a solution
+ let contradicts nalt sol = eqPmAltCon (paca_con sol) nalt == Equal
+ guard (not (any (contradicts nalt) pos))
+ -- 2. Only record the new fact when it's not already implied by one of the
+ -- solutions
+ let implies nalt sol = eqPmAltCon (paca_con sol) nalt == Disjoint
+ let neg'
+ | any (implies nalt) pos = neg
+ -- See Note [Completeness checking with required Thetas]
+ | hasRequiredTheta nalt = neg
+ | otherwise = extendPmAltConSet neg nalt
+ massert (isPmAltConMatchStrict nalt)
+ let vi' = vi{ vi_neg = neg', vi_bot = IsNotBot }
+ -- 3. Make sure there's at least one other possible constructor
+ mb_rcm' <- lift (markMatched nalt rcm)
+ pure $ case mb_rcm' of
+ -- If nalt could be removed from a COMPLETE set, we'll get back Just and
+ -- have to mark x dirty, by returning Just x'.
+ Just rcm' -> (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 -> (False, vi')
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike cl) = notNull req_theta
@@ -767,9 +805,87 @@ 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
- let vi@(VI _ pos neg bot _) = lookupVarInfo ts x
+addConCt :: Nabla -> ClassId -> PmAltCon -> [TyVar] -> [ClassId] -> MaybeT DsM Nabla
+addConCt (MkNabla tyst ts at TmSt{ts_facts=egr0}) x alt tvs args = do
+ (((), egr), tyst') <- (`runStateT` tyst) $ EGM.runEGraphMT egr0 $ do
+ -- ROMES:TODO: using the conLikeName will not allow us to match the pattern
+ -- constructors with core expressions that use the same constructor?
+ -- ROMES:TODO: what about using Names for comparison? Since this is only for equality purposes...
+ -- It makes it possible to use the ConLikeName as the FreeVar Name
+ -- Better thing is to just call the correct builder, using Ids.
+ case alt of
+ PmAltLit _ ->
+ -- We don't need to do anything in the case of PmAltLit.
+ -- The Constructor information is recorded in the positive info e-class
+ -- it is represented in, so when we merge we take care of handling this
+ -- equality right.
+ -- If we did this even more ideally, we'd just represent PmAltLit in the e-graph and it would fail on merge without having to edit the e-class.
+ -- Wait, is it even safe to edit the e-class? Won't that *NOT* trigger the merging??
+ -- Here I suppose we're creating the e-class. So we can add information at will. When we eventually merge this class with another one, we can do things.
+ -- But we could definitely check whether the information we're adding isn't colliding with the existing one.
+ return ()
+ PmAltConLike conLike -> do
+ -- We must represent the constructor application in the e-graph to make
+ -- sure the children are recursively merged against other children of
+ -- other constructors represneted in the same e-class.
+ -- We need to represent the constructor correctly to ensure existing
+ -- constructors match or not the new one
+ -- dsHsConLike basically implements the logic we want. That will
+ -- certainly cause a cycle, so the next thing one could do is copy the
+ -- logic over. ROMES:TODO
+ con <- modifyM (representCoreExprEgr (dsHsConLike conLike))
+ tvs' <- mapM (EGM.addM . EG.Node . TypeF . DBT . deBruijnize . TyVarTy) tvs
+ foldlM (\acc i -> EGM.addM (EG.Node $ AppF acc i)) con (tvs' ++ args)
+ return ()
+
+ -- Do (2) in Note [Coverage checking Newtype matches]
+ -- ROMES:TODO: SOMEWHERE
+ -- case (alt, args) of
+ -- (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
+ return (MkNabla tyst' ts{ts_facts=egr})
+
+
+ -- case find ((== Equal) . eqPmAltCon alt . paca_con) pos of
+ -- Just (PACA _con other_tvs other_args) -> do
+ -- -- We must unify existentially bound ty vars and arguments!
+ -- -- (We may be able to do this eventually through e-graph analysis joining, but for now we keep it separate.)
+ -- let ty_cts = equateTys (map mkTyVarTy tvs) (map mkTyVarTy other_tvs)
+ -- nabla' <- MaybeT $ addPhiCts nabla (listToBag ty_cts)
+ -- let add_var_ct nabla (a, b) = addVarCt nabla a b
+ -- foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args
+ -- Nothing -> do
+ -- -- Instead of adding all the pos info to the pos info we should instead
+ -- -- just represent all Con Cts as e-graph nodes, which will handle
+ -- -- automatically all recursive merging of children ty vars and terms.
+ -- -- That means we only need to record the said pos constructor in the var
+ -- -- info, since the children and ty vars are stored in the e-graph.
+ -- let pos' = PACA alt tvs args : pos
+ -- let nabla_with 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 ->
+ -- case bot of
+ -- MaybeBot -> pure (nabla_with MaybeBot)
+ -- IsBot -> addBotCt (nabla_with MaybeBot) y
+ -- IsNotBot -> addNotBotCt (nabla_with MaybeBot) y
+ -- _ -> assert (isPmAltConMatchStrict alt )
+ -- pure (nabla_with IsNotBot) -- strict match ==> not ⊥
+
+-- | Extend the 'VarInfo' of x with the @x ~ K tvs args ts@ constraint.
+-- @mergeConCt x K tvs args ts@ extends the 'VarInfo' with a solution TODO
+-- @x :-> (K, tvs, args)@ if compatible with the negative and positive info we
+-- have on @x@, reject (@Nothing@) otherwise.
+--
+-- The children args are automatically merged by congruence (see that new note) TODO
+--
+-- See Note [TmState invariants]??
+mergeConCt :: VarInfo -- ^ The 'VarInfo' of @x@ into which we're merging the ConCt.
+ -> PmAltCon -- ^ The constructor @K@
+ -> [TyVar] -- ^ The type vars of the constructor
+ -> [ClassId] -- ^ The constructor arguments (unused for merging, but stored in the PACA)
+ -> StateT TyState (MaybeT DsM) VarInfo -- ^ We also track the type information to merge constructor existential variables against.
+mergeConCt vi@(VI _ pos neg bot _) alt tvs args = StateT $ \tyst -> do
-- First try to refute with a negative fact
guard (not (elemPmAltConSet alt neg))
-- Then see if any of the other solutions (remember: each of them is an
@@ -779,25 +895,36 @@ addConCt nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts=env } } x alt tvs args =
-- Now we should be good! Add (alt, tvs, args) as a possible solution, or
-- refine an existing one
case find ((== Equal) . eqPmAltCon alt . paca_con) pos of
- Just (PACA _con other_tvs other_args) -> do
+ Just (PACA _con other_tvs _other_args) -> do
-- We must unify existentially bound ty vars and arguments!
+ -- But this is already done automatically by representing K in
+ -- the e-class...! all equivalent things will be merged.
let ty_cts = equateTys (map mkTyVarTy tvs) (map mkTyVarTy other_tvs)
- nabla' <- MaybeT $ addPhiCts nabla (listToBag ty_cts)
- let add_var_ct nabla (a, b) = addVarCt nabla a b
- foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args
+ tyst' <- MaybeT (tyOracle tyst (listToBag $ map (\(PhiTyCt pred) -> pred) ty_cts))
+ return (vi, tyst') -- All good, and we get no new information.
Nothing -> do
let pos' = PACA alt tvs args : pos
- let nabla_with bot' =
- nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
+ let varinfo_with bot' = (vi{vi_pos = pos', vi_bot = bot'}, tyst)
-- Do (2) in Note [Coverage checking Newtype matches]
- case (alt, args) of
- (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
+ case alt of
+ -- Now (2) is done here and elsewhere, when we're merging VarInfos we
+ -- only have to worry about merging them into a valid VarInfo. (In the
+ -- place where the Newtype will be merged into the @x@ e-class we must
+ -- take this care. Probably addConCt)
+ PmAltConLike (RealDataCon dc) | isNewDataCon dc ->
case bot of
- MaybeBot -> pure (nabla_with MaybeBot)
- IsBot -> addBotCt (nabla_with MaybeBot) y
- IsNotBot -> addNotBotCt (nabla_with MaybeBot) y
- _ -> assert (isPmAltConMatchStrict alt )
- pure (nabla_with IsNotBot) -- strict match ==> not ⊥
+ MaybeBot -> pure (varinfo_with MaybeBot)
+ IsBot -> pure (varinfo_with MaybeBot)
+ IsNotBot -> pure (varinfo_with MaybeBot)
+ -- ROMES:TODO: Still have to do the two cases that we used to have here:
+ -- Likely in addConCt
+ -- Or better, in the analysis merge function, if we're merging a Newtype
+ -- constructor application, we should do something like this...
+ -- IsBot -> addBotCt (nabla_with MaybeBot) y
+ -- IsNotBot -> addNotBotCt (nabla_with MaybeBot) y
+ _ -> assert (isPmAltConMatchStrict alt)
+ pure (varinfo_with IsNotBot) -- strict match ==> not ⊥
+
equateTys :: [Type] -> [Type] -> [PhiCt]
equateTys ts us =
@@ -816,19 +943,17 @@ 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 at MkNabla{ nabla_tm_st = ts at TmSt{ ts_facts = env } } x y =
- case equateUSDFM env x y of
- (Nothing, env') -> pure (nabla{ nabla_tm_st = ts{ ts_facts = env' } })
- -- Add the constraints we had for x to y
- (Just vi_x, env') -> do
- let nabla_equated = nabla{ nabla_tm_st = ts{ts_facts = env'} }
- -- and then gradually merge every positive fact we have on x into y
- let add_pos nabla (PACA cl tvs args) = addConCt nabla y cl tvs args
- nabla_pos <- foldlM add_pos nabla_equated (vi_pos vi_x)
- -- Do the same for negative info
- let add_neg nabla nalt = addNotConCt nabla y nalt
- foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x))
+addVarCt :: Nabla -> ClassId -> ClassId -> MaybeT DsM Nabla
+-- This is where equality-graphs really come into play.
+addVarCt (MkNabla tyst ts at TmSt{ts_facts = egr}) x y = do
+ -- @merge env x y@ makes @x@ and @y@ point to the same entry,
+ -- thereby merging @x@'s class with @y@'s.
+ (egr', tyst') <- (`runStateT` tyst) $ do
+ -- Merging will also merge all the constraints from x with y
+ -- However, doing so
+ (_, egr') <- EG.mergeM x y egr
+ EG.rebuildM egr'
+ return (MkNabla tyst' ts{ts_facts=egr'})
-- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
-- on the shape of the 'CoreExpr' @e at . Examples:
@@ -842,17 +967,19 @@ 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
- -- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
+ lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (eclassType x nabla) $$ ppr e $$ ppr e')
execStateT (core_expr x e') nabla
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 +1000,21 @@ 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
+ = do
+ nabla' <- get
+ if
+ -- See Note [Detecting pattern synonym applications in expressions]
+ -- ROMES:TODO: Can we fix this more easily with e-graphs?
+ | Var y <- e, Nothing <- isDataConId_maybe (eclassMatchId x nabla')
+ -- We don't consider DataCons flexible variables
+ -> modifyT (\nabla -> do (yid, nabla') <- representId y nabla
+ lift (tracePm "foundIdVar:" (ppr y <+> text "->>>" <+> ppr yid))
+ addVarCt nabla' x yid)
+ | 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 +1028,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 $ (`representCoreExpr` 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 +1050,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 +1073,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 +1090,22 @@ 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 -> MaybeT DsM (ClassId, Nabla)
+representCoreExpr (MkNabla tyst ts at TmSt{ ts_facts = egraph }) e = do
+ ((xid, egr''), tysty') <- (`runStateT` tyst) $ do
+ (xid, egr') <- representCoreExprEgr (makeDictsCoherent e) egraph
+ egr'' <- EG.rebuildM egr'
+ return (xid, egr'')
+ return (xid, MkNabla tysty' ts{ts_facts = egr''})
+ -- 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 +1194,8 @@ 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: Looks like a good idea, we could try to do this now.
-}
{- Note [The Pos/Neg invariant]
@@ -1271,22 +1408,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 +1446,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 +1490,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 +1529,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 +1551,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 +1583,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 +1648,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 +1670,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 +1698,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 +2044,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 +2082,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 +2114,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 +2133,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 +2223,114 @@ 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 :: 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
+
+-- There are too many cycles for this to be in Solver.Types...
+-- We need the TyState to check insoluble constraints while merging VarInfos
+instance Analysis (StateT TyState (MaybeT DsM)) VarInfo ExprF where
+ {-# INLINE makeA #-}
+
+ -- When an e-class is created for a variable, we create an VarInfo from it.
+ -- It doesn't matter if this variable is bound or free, since it's the first
+ -- variable in this e-class (and all others would have to be equivalent to
+ -- it)
+ --
+ -- Also, the Eq instance for DeBruijn Vars will ensure that two free
+ -- variables with the same Id are equal and so they will be represented in
+ -- the same e-class
+ makeA (FreeVarF x) = pure $ emptyVarInfo x
+ makeA _ = pure $ 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
+ -- 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 Nothing Nothing = Nothing
+ -- joinA Nothing (Just b) = Just b
+ -- joinA (Just a) Nothing = Just a
+ -- joinA (Just a) (Just b)
+
+ -- Add the constraints we had for x to y
+ joinA vi_x vi_y = do
+ -- Gradually merge every positive fact we have on x into y
+ -- The args are merged by congruence, since we represent the
+ -- constructor in the e-graph in addConCt.
+ let add_pos y (PACA cl tvs args) = mergeConCt y cl tvs args
+ vi_res <- foldlM add_pos vi_y (vi_pos vi_x)
+
+ -- Do the same for negative info
+ let add_neg vi nalt = lift $ snd <$> mergeNotConCt nalt vi
+ foldlM add_neg vi_res (pmAltConSetElems (vi_neg vi_x))
+
+{-
+Note [mergeXXXCt vs addXXXCt in the Pmc Solver]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+* mergeXXXCt handles merging information into some VarInfo
+* addXXXCt handles adding information into the nablas by calling out to
+ mergeXXXCt for particular terms/e-classes
+
+-}
+
+-- | Represents a match-id in 'Nablas'
+representIdNablas :: Id -> Nablas -> MaybeT DsM Nablas
+representIdNablas x (MkNablas nbs) = MkNablas <$> mapBagM (fmap snd . representId x) nbs
+
+representIdsNablas :: [Id] -> Nablas -> MaybeT DsM Nablas
+representIdsNablas xs = execStateT (mapM (\x -> StateT (fmap (((),)) . representIdNablas x)) xs)
+
+-- Are these even used? don't we always use the ones above?
+-- | Like 'representId' but for a single Nabla
+representId :: Id -> Nabla -> MaybeT DsM (ClassId, Nabla)
+representId x (MkNabla tyst tmst at TmSt{ts_facts=eg0, ts_reps=idmp})
+ = do
+ ((xid, tmst'),tyst') <- (`runStateT` tyst) $
+ 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 '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 -> do
+ (xid, eg1) <- EG.addM (EG.Node (FreeVarF x)) eg0
+ eg2 <- EG.rebuildM eg1
+ return (xid, tmst{ts_facts=eg2, ts_reps=extendVarEnv idmp x xid})
+ Just xid -> return (xid, tmst)
+ return (xid, MkNabla tyst' tmst')
+
+
+representIds :: [Id] -> Nabla -> MaybeT DsM ([ClassId], Nabla)
+representIds xs = runStateT (mapM (StateT . representId) xs)
+
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,7 +1,14 @@
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TupleSections #-}
+{-# 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 +17,14 @@
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,
+
+ lookupMatchIdMap,
-- ** Caching residual COMPLETE sets
CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
@@ -42,10 +51,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,13 +66,13 @@ import GHC.Core.TyCon
import GHC.Types.Literal
import GHC.Core
import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Map.Expr
import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim
import GHC.Tc.Solver.InertSet (InertSet, emptyInert)
import GHC.Tc.Utils.TcType (isStringTy)
+import GHC.Types.Var.Env
import GHC.Types.CompleteMatch (CompleteMatch(..))
import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
, fractionalLitFromRational
@@ -75,6 +83,14 @@ import Data.Ratio
import GHC.Real (Ratio(..))
import qualified Data.Semigroup as Semi
+import Data.Functor.Compose
+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)
+
-- import GHC.Driver.Ppr
--
@@ -131,26 +147,29 @@ 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.
+ , ts_reps :: !(IdEnv ClassId)
+ -- ^ A mapping from match-id Ids to the class-id representing that match-id
+
+ -- 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@).
}
--- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
+lookupMatchIdMap :: Id -> Nabla -> Maybe ClassId
+lookupMatchIdMap id (MkNabla _ TmSt{ts_reps}) = lookupVarEnv ts_reps id
+
+-- | 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').
@@ -161,6 +180,11 @@ 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_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
@@ -168,7 +192,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 +230,9 @@ data PmAltConApp
= PACA
{ paca_con :: !PmAltCon
, paca_tvs :: ![TyVar]
- , paca_ids :: ![Id]
+ , paca_ids :: ![ClassId] -- TODO(talk about merging things by congruence in
+ -- the e-graph) ... the merging is done automatically when the pms are
+ -- represented, but we keep these still for error reporting and what not...
}
-- | See 'vi_bot'.
@@ -225,9 +251,12 @@ instance Outputable BotInfo where
ppr IsBot = text "~⊥"
ppr IsNotBot = text "≁⊥"
+instance Outputable IntSet where
+ ppr = text . show
+
-- | Not user-facing.
instance Outputable TmState where
- ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
+ ppr (TmSt eg idmp dirty) = text (show eg) $$ ppr idmp $$ ppr dirty
-- | Not user-facing.
instance Outputable VarInfo where
@@ -248,7 +277,7 @@ instance Outputable VarInfo where
-- | Initial state of the term oracle.
initTmState :: TmState
-initTmState = TmSt emptyUSDFM emptyCoreMap emptyDVarSet
+initTmState = TmSt EG.emptyEGraph mempty 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 +329,14 @@ 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
+-- 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
-- | 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 +348,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 +386,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 +505,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 +830,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 +838,19 @@ instance Outputable PmAltCon where
instance Outputable PmEquality where
ppr = text . show
+
+--
+-- * E-graphs to represent normalised refinment types
+--
+
+type TmEGraph = EGraph VarInfo CoreExprF
+-- TODO delete orphans for showing TmEGraph for debugging reasons
+instance Show VarInfo where
+ show = showPprUnsafe . ppr
+
+-- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
+-- There ought to be a better way.
+-- ROMES:TODO:
+instance Eq VarInfo where
+ (==) a b = vi_id a == vi_id b
+
=====================================
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
=====================================
@@ -105,6 +105,7 @@ Library
array >= 0.1 && < 0.6,
filepath >= 1 && < 1.5,
template-haskell == 2.21.*,
+ hegg,
hpc == 0.6.*,
transformers >= 0.5 && < 0.7,
exceptions == 0.10.*,
@@ -320,6 +321,7 @@ Library
GHC.Core.ConLike
GHC.Core.DataCon
GHC.Core.FamInstEnv
+ GHC.Core.Equality
GHC.Core.FVs
GHC.Core.InstEnv
GHC.Core.Lint
@@ -857,7 +859,6 @@ Library
GHC.Types.Unique.FM
GHC.Types.Unique.Map
GHC.Types.Unique.MemoFun
- GHC.Types.Unique.SDFM
GHC.Types.Unique.Set
GHC.Types.Unique.Supply
GHC.Types.Var
=====================================
hadrian/src/Packages.hs
=====================================
@@ -6,7 +6,7 @@ module Packages (
compareSizes, compiler, containers, deepseq, deriveConstants, directory, dumpDecls,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh, ghcPlatform,
ghcCompact, ghcConfig, ghcExperimental, ghcHeap, ghcInternal, ghci, ghciWrapper, ghcPkg, ghcPrim,
- ghcToolchain, ghcToolchainBin, haddock, haskeline,
+ ghcToolchain, ghcToolchainBin, haddock, haskeline, hegg,
hsc2hs, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy,
libffi, mtl, parsec, pretty, primitive, process, remoteIserv, rts,
runGhc, semaphoreCompat, stm, templateHaskell, terminfo, text, time, timeout, touchy,
@@ -39,7 +39,7 @@ ghcPackages =
, compareSizes, compiler, containers, deepseq, deriveConstants, directory, dumpDecls
, exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh, ghcPlatform
, ghcCompact, ghcConfig, ghcExperimental, ghcHeap, ghcInternal, ghci, ghciWrapper, ghcPkg, ghcPrim
- , ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs
+ , ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs, hegg
, hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, libffi, mtl
, parsec, pretty, process, rts, runGhc, stm, semaphoreCompat, templateHaskell
, terminfo, text, time, touchy, transformers, unlit, unix, win32, xhtml
@@ -56,7 +56,7 @@ array, base, binary, bytestring, cabalSyntax, cabal, checkPpr, checkExact, count
compareSizes, compiler, containers, deepseq, deriveConstants, directory, dumpDecls,
exceptions, filepath, genapply, genprimopcode, ghc, ghcBignum, ghcBoot, ghcBootTh, ghcPlatform,
ghcCompact, ghcConfig, ghcExperimental, ghcHeap, ghci, ghcInternal, ghciWrapper, ghcPkg, ghcPrim,
- ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs,
+ ghcToolchain, ghcToolchainBin, haddock, haskeline, hsc2hs, hegg,
hp2ps, hpc, hpcBin, integerGmp, integerSimple, iserv, iservProxy, remoteIserv, libffi, mtl,
parsec, pretty, primitive, process, rts, runGhc, semaphoreCompat, stm, templateHaskell,
terminfo, text, time, touchy, transformers, unlit, unix, win32, xhtml,
@@ -102,6 +102,7 @@ ghcToolchain = lib "ghc-toolchain" `setPath` "utils/ghc-toolchain"
ghcToolchainBin = prg "ghc-toolchain-bin" `setPath` "utils/ghc-toolchain/exe" -- workaround for #23690
haddock = util "haddock"
haskeline = lib "haskeline"
+hegg = lib "hegg"
hsc2hs = util "hsc2hs"
hp2ps = util "hp2ps"
hpc = lib "hpc"
=====================================
hadrian/src/Rules/ToolArgs.hs
=====================================
@@ -163,6 +163,7 @@ toolTargets = [ binary
, ghci
, ghcPkg -- # executable
-- , haddock -- # depends on ghc library
+ , hegg
, hsc2hs -- # executable
, hpc
, hpcBin -- # executable
=====================================
hadrian/src/Settings/Default.hs
=====================================
@@ -99,6 +99,7 @@ stage0Packages = do
, ghci
, ghcPkg
, haddock
+ , hegg
, hsc2hs
, hpc
, hpcBin
@@ -149,6 +150,7 @@ stage1Packages = do
, ghcPkg
, ghcPrim
, haskeline
+ , hegg
, hp2ps
, hsc2hs
, integerGmp
=====================================
libraries/hegg
=====================================
@@ -0,0 +1 @@
+Subproject commit 54761a0dc2e55087fd241669f74f1a4b3ad3176a
=====================================
packages
=====================================
@@ -51,6 +51,7 @@ libraries/deepseq - - ssh://g
libraries/directory - - ssh://git@github.com/haskell/directory.git
libraries/filepath - - ssh://git@github.com/haskell/filepath.git
libraries/haskeline - - https://github.com/judah/haskeline.git
+libraries/hegg - - https://github.com/alt-romes/hegg.git
libraries/hpc - - -
libraries/mtl - - https://github.com/haskell/mtl.git
libraries/parsec - - https://github.com/haskell/parsec.git
=====================================
testsuite/tests/count-deps/CountDepsParser.stdout
=====================================
@@ -194,7 +194,6 @@ GHC.Types.Unique.DFM
GHC.Types.Unique.DSet
GHC.Types.Unique.FM
GHC.Types.Unique.Map
-GHC.Types.Unique.SDFM
GHC.Types.Unique.Set
GHC.Types.Unique.Supply
GHC.Types.Var
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6a65109848a2687f934e6801007c5ff1d57387ed...0b0270e36d8f1483b5046b0408321128f692e492
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6a65109848a2687f934e6801007c5ff1d57387ed...0b0270e36d8f1483b5046b0408321128f692e492
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/20230822/5ed182b7/attachment-0001.html>
More information about the ghc-commits
mailing list