[Git][ghc/ghc][wip/amg/dcoercion-TransCoDCo] Starting coercion opt for TransCoDCo
Adam Gundry (@adamgundry)
gitlab at gitlab.haskell.org
Mon Oct 31 21:18:00 UTC 2022
Adam Gundry pushed to branch wip/amg/dcoercion-TransCoDCo at Glasgow Haskell Compiler / GHC
Commits:
6cd650a3 by Adam Gundry at 2022-10-31T21:17:46+00:00
Starting coercion opt for TransCoDCo
- - - - -
3 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1330,10 +1330,10 @@ mkDehydrateCo :: Coercion -> DCoercion
mkDehydrateCo co | isReflCo co = ReflDCo
mkDehydrateCo (SymCo (GRefl _ _ MRefl))
= ReflDCo
-mkDehydrateCo (SymCo (GRefl _ _ (MCo co)))
- = mkGReflLeftDCo co
+--mkDehydrateCo (SymCo (GRefl _ _ (MCo co)))
+-- = mkGReflLeftDCo co
mkDehydrateCo (GRefl _ _ MRefl) = ReflDCo
-mkDehydrateCo (GRefl _ _ (MCo co)) = mkGReflRightDCo co
+--mkDehydrateCo (GRefl _ _ (MCo co)) = mkGReflRightDCo co
--mkDehydrateCo (TyConAppCo _ _ cos)
-- = mkTyConAppDCo $ map mkDehydrateCo cos
--mkDehydrateCo (AppCo co1 co2)
@@ -1349,10 +1349,10 @@ mkDehydrateCo (AxiomInstCo coax _branch cos)
mkDehydrateCo (AxiomRuleCo _coax cos)
| all isReflCo cos -- AMG TODO: can we avoid the need for this check?
= singleStepDCo
-mkDehydrateCo (CoVarCo cv)
- = CoVarDCo cv
-mkDehydrateCo (SubCo co)
- = mkSubDCo (coercionLKind co) (mkDehydrateCo co) (coercionRKind co)
+--mkDehydrateCo (CoVarCo cv)
+-- = CoVarDCo cv
+--mkDehydrateCo (SubCo co)
+-- = mkSubDCo (coercionLKind co) (mkDehydrateCo co) (coercionRKind co)
--mkDehydrateCo (TransCo co1 co2)
-- = mkTransDCo (mkDehydrateCo co1) (mkDehydrateCo co2)
mkDehydrateCo co
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -159,6 +159,10 @@ type NormalCo = Coercion
type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
+type NormalDCo = DCoercion
+
+type NormalNonIdDCo = NormalDCo
+
-- | Do we apply a @sym@ to the result?
type SymFlag = Bool
@@ -333,10 +337,14 @@ opt_co4 env sym rep r (TransCo co1 co2)
co2' = opt_co4_wrap env sym rep r co2
in_scope = lcInScopeSet env
-opt_co4 env@(LC _ lift_co_env) sym rep r co at TransCoDCo{}
- | isEmptyVarEnv lift_co_env =
- wrapRole rep r $ wrapSym sym $ substCo (lcSubst env) co
- | otherwise = error "AMG TODO"
+opt_co4 env sym rep r (TransCoDCo co1 dco2 _)
+ = wrapSym sym $ mkTransCoDCo co1' dco2' -- TODO: any optimizations at this level? Use RHS type?
+ -- TODO handle roles properly here
+ -- TODO if we had PeakCo we could push Sym inside more easily
+ where
+ co1' = opt_co4_wrap env False rep r co1
+ dco2' = opt_dco4 env False rep r dco2
+ -- in_scope = lcInScopeSet env
opt_co4 env _sym rep r (NthCo _r n co)
| Just (ty, _) <- isReflCo_maybe co
@@ -494,6 +502,22 @@ We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
in GHC.Core.Coercion.
-}
+
+opt_dco4 :: LiftingContext -> SymFlag -> ReprFlag -> Role -> DCoercion -> NormalDCo
+
+opt_dco4 _ _ _ _ dco at ReflDCo = dco -- TODO: role change?
+
+opt_dco4 env sym rep r (TyConAppDCo dcos) = mkTyConAppDCo (map (opt_dco4 env sym rep r) dcos) -- TODO: roles
+
+opt_dco4 _ _ _ _ dco at AxiomInstDCo{} = dco
+opt_dco4 _ _ _ _ dco at StepsDCo{} = dco
+opt_dco4 env sym rep r (TransDCo dco1 dco2) = opt_trans_dco in_scope (opt_dco4 env sym rep r dco1) (opt_dco4 env sym rep r dco2)
+ where
+ in_scope = lcInScopeSet env
+opt_dco4 env sym rep r (DehydrateCo co) = mkDehydrateCo (opt_co4_wrap env sym rep r co)
+opt_dco4 _ _ _ _ dco = pprTrace "opt_dco4" (ppr dco) $ dco
+
+
-------------
-- | Optimize a phantom coercion. The input coercion may not necessarily
-- be a phantom, but the output sure will be.
@@ -896,6 +920,55 @@ fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule _rule _co1 _co2 res
= Just res
+
+opt_transList_dco :: HasDebugCallStack => InScopeSet -> [NormalDCo] -> [NormalDCo] -> [NormalDCo]
+opt_transList_dco is = zipWithEqual "opt_transList_dco" (opt_trans_dco is)
+
+opt_trans_dco :: InScopeSet -> NormalDCo -> NormalDCo -> NormalDCo
+opt_trans_dco is co1 co2
+ | isReflDCo co1 = co2
+ -- optimize when co1 is a Refl Co
+ | otherwise = opt_trans1_dco is co1 co2
+
+opt_trans1_dco :: InScopeSet -> NormalNonIdDCo -> NormalDCo -> NormalDCo
+-- First arg is not the identity
+opt_trans1_dco is co1 co2
+ | isReflDCo co2 = co1
+ -- optimize when co2 is a Refl Co
+ | otherwise = opt_trans2_dco is co1 co2
+
+opt_trans2_dco :: InScopeSet -> NormalNonIdDCo -> NormalNonIdDCo -> NormalDCo
+-- Neither arg is the identity
+opt_trans2_dco is (TransDCo co1a co1b) co2
+ -- Don't know whether the sub-coercions are the identity
+ = opt_trans_dco is co1a (opt_trans_dco is co1b co2)
+
+opt_trans2_dco is co1 co2
+ | Just co <- opt_trans_rule_dco is co1 co2
+ = co
+
+opt_trans2_dco is co1 (TransDCo co2a co2b)
+ | Just co1_2a <- opt_trans_rule_dco is co1 co2a
+ = opt_trans_dco is co1_2a co2b
+
+opt_trans2_dco _ co1 co2
+ = mkTransDCo co1 co2
+
+
+opt_trans_rule_dco :: InScopeSet -> NormalNonIdDCo -> NormalNonIdDCo -> Maybe NormalDCo
+
+-- Push transitivity down through matching top-level constructors.
+-- Unlike TyConAppCo, we can't have a type synonym in a TyConAppDCo so the head constructors must match
+opt_trans_rule_dco is (TyConAppDCo cos1) (TyConAppDCo cos2)
+ = Just $ mkTyConAppDCo (opt_transList_dco is cos1 cos2)
+
+-- TODO: DehydrateCo, maybe Identity rule with LHS/RHS types pushed in?
+
+opt_trans_rule_dco _ _ _ = Nothing
+
+
+
+
{-
Note [Conflict checking with AxiomInstCo]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -585,6 +585,7 @@ mkTransCoAlt (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2)) _xi
= GRefl r t1 (MCo $ mkTransCo co1 co2)
mkTransCoAlt co1 at AxiomInstCo{} co2 xi = TransCoDCo co1 (dehydrateCo co2) xi
mkTransCoAlt (TransCo co1 co2) co3 xi = TransCo co1 (mkTransCoAlt co2 co3 xi)
+mkTransCoAlt co1 at CoVarCo{} co2 _xi = TransCo co1 co2
mkTransCoAlt co1 co2 xi
= pprTrace "AMG mkTransCoAlt" (ppr co1 $$ ppr co2 $$ ppr xi) $ TransCo co1 co2
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6cd650a3e2e77709721e7d0817e695d8dfb89637
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6cd650a3e2e77709721e7d0817e695d8dfb89637
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/20221031/99acfb73/attachment-0001.html>
More information about the ghc-commits
mailing list