[Git][ghc/ghc][wip/romes/eqsat-pmc] Paper over
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Thu Jul 6 12:33:52 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC
Commits:
11731595 by Rodrigo Mesquita at 2023-07-06T13:33:42+01:00
Paper over
- - - - -
4 changed files:
- compiler/GHC/HsToCore/Pmc.hs
- compiler/GHC/HsToCore/Pmc/Check.hs
- compiler/GHC/HsToCore/Pmc/Solver/Types.hs
- libraries/hegg
Changes:
=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -76,6 +76,7 @@ import qualified Data.List.NonEmpty as NE
import Data.Coerce
import Data.Equality.Graph (ClassId)
+import Data.Maybe (maybeToList)
--
-- * Exported entry points to the checker
@@ -119,7 +120,7 @@ pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
-- empty-eclasses, the representId on the next line wouldn't match the match
-- ids we defined in checkPatBind.
let (varid, cr_uncov') = representId var (cr_uncov result0)
- formatReportWarnings ReportPatBind ctxt [varid] result0{cr_uncov = cr_uncov'}
+ formatReportWarnings ReportPatBind ctxt (maybeToList varid) result0{cr_uncov = cr_uncov'}
pmcPatBind _ _ _ = pure ()
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -189,7 +190,10 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
result0 <- {-# SCC "checkMatchGroup" #-}
unCA (checkMatchGroup matches) missing
tracePm "}: " (ppr (cr_uncov result0))
- let (varids, cr_uncov') = representIds vars (cr_uncov result0) -- romes:todo: this seems redundant, hints that the right thing might be for desugar to return already the match variables already "represented" in the e-graph
+ let (varids, cr_uncov') = representIds vars (cr_uncov result0)
+ -- romes:todo: this seems redundant, hints that the right thing might be
+ -- for desugar to return already the match variable already "represented"
+ -- in the e-graph
{-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt varids result0{cr_uncov=cr_uncov'}
return (NE.toList (ldiMatchGroup (cr_ret result0)))
@@ -445,8 +449,10 @@ addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs [] _ k = k
addCoreScrutTmCs (scr:scrs) (x0:xs) k =
flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas0 ->
- let (x, nablas) = representId x0 nablas0
- in addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
+ let (mvarid, nablas) = representId x0 nablas0
+ in case mvarid of
+ Nothing -> return nablas0 -- return the empty nablas unchanged
+ Just x -> addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: numbers of scrutinees and match ids differ"
-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.
=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -106,27 +106,32 @@ checkGrd :: PmGrd -> CheckAction RedSets
checkGrd grd = CA $ \inc0 -> case grd of
-- let x = e: Refine with x ~ e
PmLet x0 e -> do
- let (x, inc) = representId x0 inc0
- -- romes: we could potentially do update the trees to use e-class ids here,
- -- or in pmcMatches
- matched <- addPhiCtNablas inc (PhiCoreCt x e)
- tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
- pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
- , cr_uncov = mempty
- , cr_approx = Precise }
+ -- It'd be better to do this earlier even, maybe
+ let (mx, inc) = representId x0 inc0
+ case mx of
+ Nothing -> emptyCheckResult
+ Just x -> do
+ matched <- addPhiCtNablas inc (PhiCoreCt x e)
+ tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
-- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
PmBang x0 mb_info -> do
- let (x, inc) = representId x0 inc0
- div <- addPhiCtNablas inc (PhiBotCt x)
- matched <- addPhiCtNablas inc (PhiNotBotCt x)
- -- See Note [Dead bang patterns]
- -- mb_info = Just info <==> PmBang originates from bang pattern in source
- let bangs | Just info <- mb_info = unitOL (div, info)
- | otherwise = NilOL
- tracePm "check:Bang" (ppr x <+> ppr div)
- pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
- , cr_uncov = mempty
- , cr_approx = Precise }
+ let (mx, inc) = representId x0 inc0
+ case mx of
+ Nothing -> emptyCheckResult
+ Just x -> do
+ div <- addPhiCtNablas inc (PhiBotCt x)
+ matched <- addPhiCtNablas inc (PhiNotBotCt x)
+ -- 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)
+ | otherwise = NilOL
+ tracePm "check:Bang" (ppr x <+> ppr div)
+ pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
-- See point (3) of Note [considerAccessible]
PmCon x (PmAltConLike con) _ _ _
| x `hasKey` considerAccessibleIdKey
@@ -136,24 +141,32 @@ checkGrd grd = CA $ \inc0 -> case grd of
, cr_approx = Precise }
-- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
PmCon x0 con tvs dicts args0 -> do
- let (x, inc1) = representId x0 inc0
+ let (mx, inc1) = representId x0 inc0
(args, inc) = representIds args0 inc1
- pprTraceM "PmCon" (ppr inc $$ text "args:" <+> ppr args)
- !div <- if isPmAltConMatchStrict con
- then addPhiCtNablas inc (PhiBotCt x)
- else pure mempty
- !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
- !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
- tracePm "check:Con" $ vcat
- [ ppr grd
- , ppr inc
- , hang (text "div") 2 (ppr div)
- , hang (text "matched") 2 (ppr matched)
- , hang (text "uncov") 2 (ppr uncov)
- ]
- pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
- , cr_uncov = uncov
- , cr_approx = Precise }
+ case mx of
+ Nothing -> emptyCheckResult
+ Just x -> do
+ pprTraceM "PmCon" (ppr inc $$ text "args:" <+> ppr args)
+ !div <- if isPmAltConMatchStrict con
+ then addPhiCtNablas inc (PhiBotCt x)
+ else pure mempty
+ !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
+ !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
+ tracePm "check:Con" $ vcat
+ [ ppr grd
+ , ppr inc
+ , hang (text "div") 2 (ppr div)
+ , hang (text "matched") 2 (ppr matched)
+ , hang (text "uncov") 2 (ppr uncov)
+ ]
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
+ , cr_uncov = uncov
+ , cr_approx = Precise }
+ where
+ -- We return this when we know the nablas are empty
+ emptyCheckResult = pure CheckResult { cr_ret = emptyRedSets
+ , cr_uncov = mempty
+ , cr_approx = Precise }
checkGrds :: [PmGrd] -> CheckAction RedSets
checkGrds [] = CA $ \inc ->
@@ -186,9 +199,12 @@ 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
- let (varid, inc') = representId var inc
- unc <- addPhiCtNablas inc' (PhiNotBotCt varid)
- pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
+ let (mvarid, inc') = representId var inc
+ case mvarid of
+ Nothing -> pure (CheckResult pe mempty Precise)
+ Just varid -> do
+ unc <- addPhiCtNablas inc' (PhiNotBotCt varid)
+ pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
checkPatBind = coerce checkGRHS
=====================================
compiler/GHC/HsToCore/Pmc/Solver/Types.hs
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MagicHash #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE MultiParamTypeClasses #-}
@@ -84,12 +85,15 @@ import Data.Equality.Analysis (Analysis(..))
import Data.Equality.Graph (EGraph, ClassId)
import Data.Equality.Graph.Lens
import qualified Data.Equality.Graph as EG
+import qualified Data.Equality.Graph.Internal as EG
+import qualified Data.Equality.Graph.ReprUnionFind as EG
import Data.IntSet (IntSet)
import qualified Data.IntSet as IS (empty)
import Data.Bifunctor (second)
import Control.Monad.Trans.State (runState, state)
import Data.List (sortOn)
import Data.Ord (Down(..))
+import GHC.Int (Int(..))
-- import GHC.Driver.Ppr
@@ -834,27 +838,35 @@ type TmEGraph = EGraph VarInfo (DeBruijnF CoreExprF)
instance Show VarInfo where
show = showPprUnsafe . ppr
-representId :: Id -> Nablas -> (ClassId, Nablas)
+
+-- I think the right thing to do here is have representId always return a ClassId, or panic
+-- and have an additional method which is called by representIds...
+--
+-- | Represents a match-id in 'Nablas' and returns the match-id in terms of the e-graph
+--
+-- It returns Nothing if the Nablas is empty, and hence there's no returned
+-- match-id in terms of e-graphs (there are none in which we can represent that Id)
+representId :: Id -> Nablas -> (Maybe ClassId, Nablas)
-- TODO:TOMORROW: pick the highest Id, and use newPointerToClassId on the Nablas on which the represented Id got a lower clsas Id
--
-- I suppose that if we do it earlier, we can make all the nablas share the exact same match-ids and avoid this complexity.
representId x (MkNablas nbs)
- = case unzip $ map go (bagToList nbs) of
- (ids,nablas) ->
- case sortOn Down ids of
- [] -> MkNablas emptyBag
- (max_i:_) ->
- let go_zip i nabla@(MkNabla tyst tmst at TmSt{ts_facts=eg0}) = if max_i > i
- then MkNabla tyst tmst{ts_facts=EG.newPointerToClassId max_i i eg0}
- else nabla
- in (max_i, MkNablas $ listToBag $ zipWith go_zip ids nablas)
+ = case unzip3 $ map go (bagToList nbs) of
+ (counters,ids,nablas) ->
+ case sortOn Down counters of
+ [] -> (Nothing, MkNablas nbs)
+ (max_counter:_) ->
+ let go_zip i (MkNabla tyst tmst at TmSt{ts_facts=eg0})
+ -- The max counter will be never be an id already in these e-graphs
+ = MkNabla tyst tmst{ts_facts=EG.newPointerToClassId max_counter i eg0}
+ in (Just max_counter, MkNablas $ listToBag $ zipWith go_zip ids nablas)
where
go (MkNabla tyst tmst at TmSt{ts_facts=eg0})
= case EG.add (EG.Node (DF (deBruijnize (VarF x)))) eg0 of
- (xid, eg1) -> (xid, MkNabla tyst tmst{ts_facts=eg1})
+ (xid, eg1) -> (case EG.unionFind eg0 of EG.RUF _ size# -> I# size#, xid, MkNabla tyst tmst{ts_facts=eg1})
representIds :: [Id] -> Nablas -> ([ClassId], Nablas)
-representIds xs = runState (mapM (state . representId) xs)
+representIds xs = runState (catMaybes <$> mapM (state . representId) xs)
-- | This instance is seriously wrong for general purpose, it's just required for instancing Analysis.
-- There ought to be a better way.
=====================================
libraries/hegg
=====================================
@@ -1 +1 @@
-Subproject commit f2cb5d7671f9135340fd2bd782f08614c34bceeb
+Subproject commit ff5fa306092c6539866d5ebffde9a3041d83444f
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1173159511519aa49f6301ecd61cddd0258159c4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1173159511519aa49f6301ecd61cddd0258159c4
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/20230706/f0b02ebc/attachment-0001.html>
More information about the ghc-commits
mailing list