[commit: ghc] master: Define MCoercion type (9aac442)
git at git.haskell.org
git at git.haskell.org
Wed May 30 20:31:08 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/9aac442f70b0b58decd56fb52dd4ec2289b03759/ghc
>---------------------------------------------------------------
commit 9aac442f70b0b58decd56fb52dd4ec2289b03759
Author: ningning <xnningxie at gmail.com>
Date: Sun May 27 11:49:06 2018 -0400
Define MCoercion type
An attempt on #14975:
During compilation, reflexive casts is discarded for computation.
Currently in some places we use Maybe coercion as inputs. So if a cast
is reflexive it is denoted as Nothing, otherwise Just coercion.
This patch defines the type
data MCoercion = MRefl | MCo Coercion
which is isomorphic to Maybe Coercion but useful in a number of places,
and super-helpful documentation.
Test Plan: validate
Reviewers: bgamari, goldfire, simonpj
Reviewed By: goldfire
Subscribers: mpickering, rwbarton, thomie, carter
GHC Trac Issues: #14975
Differential Revision: https://phabricator.haskell.org/D4699
>---------------------------------------------------------------
9aac442f70b0b58decd56fb52dd4ec2289b03759
compiler/coreSyn/CoreOpt.hs | 26 +++++++++++++-------------
compiler/coreSyn/CoreSyn.hs | 3 ++-
compiler/simplCore/Simplify.hs | 8 ++++----
compiler/types/Coercion.hs | 2 +-
compiler/types/TyCoRep.hs | 10 ++++++++++
5 files changed, 30 insertions(+), 19 deletions(-)
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 2027928..73bb427 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -754,8 +754,8 @@ exprIsConApp_maybe (in_scope, id_unf) expr
| Just (args', m_co1') <- pushCoArgs (subst_co subst co1) args
-- See Note [Push coercions in exprIsConApp_maybe]
= case m_co1' of
- Just co1' -> go subst expr (CC args' (co1' `mkTransCo` co2))
- Nothing -> go subst expr (CC args' co2)
+ MCo co1' -> go subst expr (CC args' (co1' `mkTransCo` co2))
+ MRefl -> go subst expr (CC args' co2)
go subst (App fun arg) (CC args co)
= go subst fun (CC (subst_arg subst arg : args) co)
go subst (Lam var body) (CC (arg:args) co)
@@ -949,15 +949,15 @@ Here we implement the "push rules" from FC papers:
by pushing the coercion into the arguments
-}
-pushCoArgs :: CoercionR -> [CoreArg] -> Maybe ([CoreArg], Maybe Coercion)
-pushCoArgs co [] = return ([], Just co)
+pushCoArgs :: CoercionR -> [CoreArg] -> Maybe ([CoreArg], MCoercion)
+pushCoArgs co [] = return ([], MCo co)
pushCoArgs co (arg:args) = do { (arg', m_co1) <- pushCoArg co arg
; case m_co1 of
- Just co1 -> do { (args', m_co2) <- pushCoArgs co1 args
+ MCo co1 -> do { (args', m_co2) <- pushCoArgs co1 args
; return (arg':args', m_co2) }
- Nothing -> return (arg':args, Nothing) }
+ MRefl -> return (arg':args, MRefl) }
-pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, Maybe Coercion)
+pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, MCoercion)
-- We have (fun |> co) arg, and we want to transform it to
-- (fun arg) |> co
-- This may fail, e.g. if (fun :: N) where N is a newtype
@@ -969,7 +969,7 @@ pushCoArg co (Type ty) = do { (ty', m_co') <- pushCoTyArg co ty
pushCoArg co val_arg = do { (arg_co, m_co') <- pushCoValArg co
; return (val_arg `mkCast` arg_co, m_co') }
-pushCoTyArg :: CoercionR -> Type -> Maybe (Type, Maybe CoercionR)
+pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR)
-- We have (fun |> co) @ty
-- Push the coercion through to return
-- (fun @ty') |> co'
@@ -983,11 +983,11 @@ pushCoTyArg co ty
-- -- = Just (ty, Nothing)
| isReflCo co
- = Just (ty, Nothing)
+ = Just (ty, MRefl)
| isForAllTy tyL
= ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
- Just (ty `mkCastTy` mkSymCo co1, Just co2)
+ Just (ty `mkCastTy` mkSymCo co1, MCo co2)
| otherwise
= Nothing
@@ -1007,7 +1007,7 @@ pushCoTyArg co ty
-- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
-- Arg of mkInstCo is always nominal, hence mkNomReflCo
-pushCoValArg :: CoercionR -> Maybe (Coercion, Maybe Coercion)
+pushCoValArg :: CoercionR -> Maybe (Coercion, MCoercion)
-- We have (fun |> co) arg
-- Push the coercion through to return
-- (fun (arg |> co_arg)) |> co_res
@@ -1021,7 +1021,7 @@ pushCoValArg co
-- -- = Just (mkRepReflCo arg, Nothing)
| isReflCo co
- = Just (mkRepReflCo arg, Nothing)
+ = Just (mkRepReflCo arg, MRefl)
| isFunTy tyL
, (co1, co2) <- decomposeFunCo Representational co
@@ -1029,7 +1029,7 @@ pushCoValArg co
-- then co1 :: tyL1 ~ tyR1
-- co2 :: tyL2 ~ tyR2
= ASSERT2( isFunTy tyR, ppr co $$ ppr arg )
- Just (mkSymCo co1, Just co2)
+ Just (mkSymCo co1, MCo co2)
| otherwise
= Nothing
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index 2cb8079..729825f 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -18,7 +18,7 @@ module CoreSyn (
InId, InBind, InExpr, InAlt, InArg, InType, InKind,
InBndr, InVar, InCoercion, InTyVar, InCoVar,
OutId, OutBind, OutExpr, OutAlt, OutArg, OutType, OutKind,
- OutBndr, OutVar, OutCoercion, OutTyVar, OutCoVar,
+ OutBndr, OutVar, OutCoercion, OutTyVar, OutCoVar, MOutCoercion,
-- ** 'Expr' construction
mkLet, mkLets, mkLetNonRec, mkLetRec, mkLams,
@@ -793,6 +793,7 @@ type OutBind = CoreBind
type OutExpr = CoreExpr
type OutAlt = CoreAlt
type OutArg = CoreArg
+type MOutCoercion = MCoercion
{- *********************************************************************
diff --git a/compiler/simplCore/Simplify.hs b/compiler/simplCore/Simplify.hs
index 5e514c5..6d1b434 100644
--- a/compiler/simplCore/Simplify.hs
+++ b/compiler/simplCore/Simplify.hs
@@ -1248,11 +1248,11 @@ simplCast env body co0 cont0
else addCoerce co1 cont0
; {-#SCC "simplCast-simplExprF" #-} simplExprF env body cont1 }
where
- -- If the first parameter is Nothing, then simplifying revealed a
+ -- If the first parameter is MRefl, then simplifying revealed a
-- reflexive coercion. Omit.
- addCoerceM :: Maybe OutCoercion -> SimplCont -> SimplM SimplCont
- addCoerceM Nothing cont = return cont
- addCoerceM (Just co) cont = addCoerce co cont
+ addCoerceM :: MOutCoercion -> SimplCont -> SimplM SimplCont
+ addCoerceM MRefl cont = return cont
+ addCoerceM (MCo co) cont = addCoerce co cont
addCoerce :: OutCoercion -> SimplCont -> SimplM SimplCont
addCoerce co1 (CastIt co2 cont) -- See Note [Optimising reflexivity]
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index d0c5eed..8085e10 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -10,7 +10,7 @@
--
module Coercion (
-- * Main data type
- Coercion, CoercionN, CoercionR, CoercionP,
+ Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
LeftOrRight(..),
Var, CoVar, TyCoVar,
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 27f28ae..bd10ac8 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -34,6 +34,7 @@ module TyCoRep (
UnivCoProvenance(..),
CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
CoercionN, CoercionR, CoercionP, KindCoercion,
+ MCoercion(..), MCoercionR,
-- * Functions over types
mkTyConTy, mkTyVarTy, mkTyVarTys,
@@ -942,6 +943,15 @@ type CoercionR = Coercion -- always representational
type CoercionP = Coercion -- always phantom
type KindCoercion = CoercionN -- always nominal
+-- | A semantically more meaningful type to represent what may or may not be a
+-- useful 'Coercion'.
+data MCoercion
+ = MRefl
+ -- A trivial Reflexivity coercion
+ | MCo Coercion
+ -- Other coercions
+type MCoercionR = MCoercion
+
{-
Note [Refl invariant]
~~~~~~~~~~~~~~~~~~~~~
More information about the ghc-commits
mailing list