module TcEvidence (
HsWrapper(..),
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCast,
mkWpFun, idHsWrapper, isIdHsWrapper, pprHsWrapper,
TcEvBinds(..), EvBindsVar(..),
EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
EvTerm(..), mkEvCast, evVarsOfTerm, mkEvTupleSelectors, mkEvScSelectors,
EvLit(..), evTermCoercion,
EvTypeable(..),
EvCallStack(..),
TcCoercion(..), LeftOrRight(..), pickLR,
mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
tcDowngradeRole, mkTcTransAppCo,
mkTcAxiomRuleCo, mkTcPhantomCo,
tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
isTcReflCo, getTcCoVar_maybe,
tcCoercionRole, eqVarRole,
unwrapIP, wrapIP
) where
#include "HsVersions.h"
import Var
import Coercion
import PprCore ()
import TypeRep
import TcType
import Type
import TyCon
import Class( Class )
import CoAxiom
import PrelNames
import VarEnv
import VarSet
import Name
import Util
import Bag
import Pair
#if __GLASGOW_HASKELL__ < 709
import Control.Applicative
import Data.Traversable (traverse, sequenceA)
#endif
import qualified Data.Data as Data
import Outputable
import FastString
import SrcLoc
import Data.IORef( IORef )
data TcCoercion
= TcRefl Role TcType
| TcTyConAppCo Role TyCon [TcCoercion]
| TcAppCo TcCoercion TcCoercion
| TcForAllCo TyVar TcCoercion
| TcCoVarCo EqVar
| TcAxiomInstCo (CoAxiom Branched) Int [TcCoercion]
| TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
| TcPhantomCo TcType TcType
| TcSymCo TcCoercion
| TcTransCo TcCoercion TcCoercion
| TcNthCo Int TcCoercion
| TcLRCo LeftOrRight TcCoercion
| TcSubCo TcCoercion
| TcCastCo TcCoercion TcCoercion
| TcLetCo TcEvBinds TcCoercion
| TcCoercion Coercion
deriving (Data.Data, Data.Typeable)
isEqVar :: Var -> Bool
isEqVar v = case tyConAppTyCon_maybe (varType v) of
Just tc -> tc `hasKey` eqTyConKey
Nothing -> False
isTcReflCo_maybe :: TcCoercion -> Maybe TcType
isTcReflCo_maybe (TcRefl _ ty) = Just ty
isTcReflCo_maybe _ = Nothing
isTcReflCo :: TcCoercion -> Bool
isTcReflCo (TcRefl {}) = True
isTcReflCo _ = False
getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
getTcCoVar_maybe (TcCoVarCo v) = Just v
getTcCoVar_maybe _ = Nothing
mkTcReflCo :: Role -> TcType -> TcCoercion
mkTcReflCo = TcRefl
mkTcNomReflCo :: TcType -> TcCoercion
mkTcNomReflCo = TcRefl Nominal
mkTcRepReflCo :: TcType -> TcCoercion
mkTcRepReflCo = TcRefl Representational
mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcTyConAppCo role tc cos
| Just tys <- traverse isTcReflCo_maybe cos
= TcRefl role (mkTyConApp tc tys)
| otherwise = TcTyConAppCo role tc cos
mkTcSubCo :: TcCoercion -> TcCoercion
mkTcSubCo co = ASSERT2( tcCoercionRole co == Nominal, ppr co)
TcSubCo co
tcDowngradeRole_maybe :: Role
-> Role
-> TcCoercion -> Maybe TcCoercion
tcDowngradeRole_maybe Representational Nominal = Just . mkTcSubCo
tcDowngradeRole_maybe Nominal Representational = const Nothing
tcDowngradeRole_maybe Phantom _
= panic "tcDowngradeRole_maybe Phantom"
tcDowngradeRole_maybe _ Phantom = const Nothing
tcDowngradeRole_maybe _ _ = Just
tcDowngradeRole :: Role
-> Role
-> TcCoercion -> TcCoercion
tcDowngradeRole r1 r2 co
= case tcDowngradeRole_maybe r1 r2 co of
Just co' -> co'
Nothing -> pprPanic "tcDowngradeRole" (ppr r1 <+> ppr r2 <+> ppr co)
maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
maybeTcSubCo NomEq = id
maybeTcSubCo ReprEq = mkTcSubCo
mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion
mkTcAxInstCo role ax index tys
| ASSERT2( not (role == Nominal && ax_role == Representational) , ppr (ax, tys) )
arity == n_tys = tcDowngradeRole role ax_role $
TcAxiomInstCo ax_br index rtys
| otherwise = ASSERT( arity < n_tys )
tcDowngradeRole role ax_role $
foldl TcAppCo (TcAxiomInstCo ax_br index (take arity rtys))
(drop arity rtys)
where
n_tys = length tys
ax_br = toBranchedAxiom ax
branch = coAxiomNthBranch ax_br index
arity = length $ coAxBranchTyVars branch
ax_role = coAxiomRole ax
arg_roles = coAxBranchRoles branch
rtys = zipWith mkTcReflCo (arg_roles ++ repeat Nominal) tys
mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
mkTcAxiomRuleCo = TcAxiomRuleCo
mkTcUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [TcType] -> TcCoercion
mkTcUnbranchedAxInstCo role ax tys
= mkTcAxInstCo role ax 0 tys
mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
mkTcAppCo (TcRefl r ty1) (TcRefl _ ty2) = TcRefl r (mkAppTy ty1 ty2)
mkTcAppCo co1 co2 = TcAppCo co1 co2
mkTcTransAppCo :: Role
-> TcCoercion
-> TcType
-> TcType
-> Role
-> TcCoercion
-> TcType
-> TcType
-> Role
-> TcCoercion
mkTcTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
= case (r1, r2, r3) of
(_, _, Phantom)
-> mkTcPhantomCo (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
(_, _, Nominal)
-> ASSERT( r1 == Nominal && r2 == Nominal )
mkTcAppCo co1 co2
(Nominal, Nominal, Representational)
-> mkTcSubCo (mkTcAppCo co1 co2)
(_, Nominal, Representational)
-> ASSERT( r1 == Representational )
mkTcAppCo co1 co2
(Nominal, Representational, Representational)
-> go (mkTcSubCo co1)
(_ , _, Representational)
-> ASSERT( r1 == Representational && r2 == Representational )
go co1
where
go co1_repr
| Just (tc1b, tys1b) <- tcSplitTyConApp_maybe ty1b
, nextRole ty1b == r2
= (co1_repr `mkTcAppCo` mkTcNomReflCo ty2a) `mkTcTransCo`
(mkTcTyConAppCo Representational tc1b
(zipWith mkTcReflCo (tyConRolesX Representational tc1b) tys1b
++ [co2]))
| Just (tc1a, tys1a) <- tcSplitTyConApp_maybe ty1a
, nextRole ty1a == r2
= (mkTcTyConAppCo Representational tc1a
(zipWith mkTcReflCo (tyConRolesX Representational tc1a) tys1a
++ [co2]))
`mkTcTransCo`
(co1_repr `mkTcAppCo` mkTcNomReflCo ty2b)
| otherwise
= pprPanic "mkTcTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
, ppr r2, ppr co2, ppr ty2a, ppr ty2b
, ppr r3 ])
mkTcSymCo :: TcCoercion -> TcCoercion
mkTcSymCo co@(TcRefl {}) = co
mkTcSymCo (TcSymCo co) = co
mkTcSymCo co = TcSymCo co
mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo (TcRefl {}) co = co
mkTcTransCo co (TcRefl {}) = co
mkTcTransCo co1 co2 = TcTransCo co1 co2
mkTcNthCo :: Int -> TcCoercion -> TcCoercion
mkTcNthCo n (TcRefl r ty) = TcRefl r (tyConAppArgN n ty)
mkTcNthCo n co = TcNthCo n co
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcLRCo lr (TcRefl r ty) = TcRefl r (pickLR lr (tcSplitAppTy ty))
mkTcLRCo lr co = TcLRCo lr co
mkTcPhantomCo :: TcType -> TcType -> TcCoercion
mkTcPhantomCo = TcPhantomCo
mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
mkTcForAllCo tv (TcRefl r ty) = ASSERT( isTyVar tv ) TcRefl r (mkForAllTy tv ty)
mkTcForAllCo tv co = ASSERT( isTyVar tv ) TcForAllCo tv co
mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
mkTcForAllCos tvs (TcRefl r ty) = ASSERT( all isTyVar tvs ) TcRefl r (mkForAllTys tvs ty)
mkTcForAllCos tvs co = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
mkTcCoVarCo :: EqVar -> TcCoercion
mkTcCoVarCo ipv = TcCoVarCo ipv
tcCoercionKind :: TcCoercion -> Pair Type
tcCoercionKind co = go co
where
go (TcRefl _ ty) = Pair ty ty
go (TcLetCo _ co) = go co
go (TcCastCo _ co) = case getEqPredTys (pSnd (go co)) of
(ty1,ty2) -> Pair ty1 ty2
go (TcTyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
go (TcAppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
go (TcForAllCo tv co) = mkForAllTy tv <$> go co
go (TcCoVarCo cv) = eqVarKind cv
go (TcAxiomInstCo ax ind cos)
= let branch = coAxiomNthBranch ax ind
tvs = coAxBranchTyVars branch
Pair tys1 tys2 = sequenceA (map go cos)
in ASSERT( cos `equalLength` tvs )
Pair (substTyWith tvs tys1 (coAxNthLHS ax ind))
(substTyWith tvs tys2 (coAxBranchRHS branch))
go (TcPhantomCo ty1 ty2) = Pair ty1 ty2
go (TcSymCo co) = swap (go co)
go (TcTransCo co1 co2) = Pair (pFst (go co1)) (pSnd (go co2))
go (TcNthCo d co) = tyConAppArgN d <$> go co
go (TcLRCo lr co) = (pickLR lr . tcSplitAppTy) <$> go co
go (TcSubCo co) = go co
go (TcAxiomRuleCo ax ts cs) =
case coaxrProves ax ts (map tcCoercionKind cs) of
Just res -> res
Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo"
go (TcCoercion co) = coercionKind co
eqVarRole :: EqVar -> Role
eqVarRole cv = getEqPredRole (varType cv)
eqVarKind :: EqVar -> Pair Type
eqVarKind cv
| Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
= ASSERT(tc `hasKey` eqTyConKey)
Pair ty1 ty2
| otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
tcCoercionRole :: TcCoercion -> Role
tcCoercionRole = go
where
go (TcRefl r _) = r
go (TcTyConAppCo r _ _) = r
go (TcAppCo co _) = go co
go (TcForAllCo _ co) = go co
go (TcCoVarCo cv) = eqVarRole cv
go (TcAxiomInstCo ax _ _) = coAxiomRole ax
go (TcPhantomCo _ _) = Phantom
go (TcSymCo co) = go co
go (TcTransCo co1 _) = go co1
go (TcNthCo n co) = let Pair ty1 _ = tcCoercionKind co
(tc, _) = tcSplitTyConApp ty1
in nthRole (go co) tc n
go (TcLRCo _ _) = Nominal
go (TcSubCo _) = Representational
go (TcAxiomRuleCo c _ _) = coaxrRole c
go (TcCastCo c _) = go c
go (TcLetCo _ c) = go c
go (TcCoercion co) = coercionRole co
coVarsOfTcCo :: TcCoercion -> VarSet
coVarsOfTcCo tc_co
= go tc_co
where
go (TcRefl _ _) = emptyVarSet
go (TcTyConAppCo _ _ cos) = mapUnionVarSet go cos
go (TcAppCo co1 co2) = go co1 `unionVarSet` go co2
go (TcCastCo co1 co2) = go co1 `unionVarSet` go co2
go (TcForAllCo _ co) = go co
go (TcCoVarCo v) = unitVarSet v
go (TcAxiomInstCo _ _ cos) = mapUnionVarSet go cos
go (TcPhantomCo _ _) = emptyVarSet
go (TcSymCo co) = go co
go (TcTransCo co1 co2) = go co1 `unionVarSet` go co2
go (TcNthCo _ co) = go co
go (TcLRCo _ co) = go co
go (TcSubCo co) = go co
go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
`minusVarSet` get_bndrs bs
go (TcLetCo {}) = emptyVarSet
go (TcAxiomRuleCo _ _ cos) = mapUnionVarSet go cos
go (TcCoercion co) =
ASSERT( isEmptyVarSet (coVarsOfCo co) )
emptyVarSet
go_bind :: EvBind -> VarSet
go_bind (EvBind _ tm) = go (evTermCoercion tm)
get_bndrs :: Bag EvBind -> VarSet
get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet
instance Outputable TcCoercion where
ppr = pprTcCo
pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
pprTcCo co = ppr_co TopPrec co
pprParendTcCo co = ppr_co TyConPrec co
ppr_co :: TyPrec -> TcCoercion -> SDoc
ppr_co _ (TcRefl r ty) = angleBrackets (ppr ty) <> ppr_role r
ppr_co p co@(TcTyConAppCo _ tc [_,_])
| tc `hasKey` funTyConKey = ppr_fun_co p co
ppr_co p (TcTyConAppCo r tc cos) = pprTcApp p ppr_co tc cos <> ppr_role r
ppr_co p (TcLetCo bs co) = maybeParen p TopPrec $
sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
ppr_co p (TcAppCo co1 co2) = maybeParen p TyConPrec $
pprTcCo co1 <+> ppr_co TyConPrec co2
ppr_co p (TcCastCo co1 co2) = maybeParen p FunPrec $
ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
ppr_co p co@(TcForAllCo {}) = ppr_forall_co p co
ppr_co _ (TcCoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
ppr_co p (TcAxiomInstCo con ind cos)
= pprPrefixApp p (ppr (getName con) <> brackets (ppr ind)) (map pprParendTcCo cos)
ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
ppr_co FunPrec co1
<+> ptext (sLit ";")
<+> ppr_co FunPrec co2
ppr_co p (TcPhantomCo t1 t2) = pprPrefixApp p (ptext (sLit "PhantomCo")) [pprParendType t1, pprParendType t2]
ppr_co p (TcSymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
ppr_co p (TcNthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
ppr_co p (TcLRCo lr co) = pprPrefixApp p (ppr lr) [pprParendTcCo co]
ppr_co p (TcSubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendTcCo co]
ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
$ ppr_tc_axiom_rule_co co ts ps
ppr_co p (TcCoercion co) = pprPrefixApp p (text "Core co:") [ppr co]
ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc
ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
where
ppTs [] = Outputable.empty
ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t
ppTs ts = ptext (sLit "@") <>
parens (hsep $ punctuate comma $ map pprType ts)
ppPs [] = Outputable.empty
ppPs [p] = pprParendTcCo p
ppPs (p : ps) = ptext (sLit "(") <+> pprTcCo p $$
vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$
ptext (sLit ")")
ppr_role :: Role -> SDoc
ppr_role r = underscore <> pp_role
where pp_role = case r of
Nominal -> char 'N'
Representational -> char 'R'
Phantom -> char 'P'
ppr_fun_co :: TyPrec -> TcCoercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
where
split :: TcCoercion -> [SDoc]
split (TcTyConAppCo _ f [arg,res])
| f `hasKey` funTyConKey
= ppr_co FunPrec arg : split res
split co = [ppr_co TopPrec co]
ppr_forall_co :: TyPrec -> TcCoercion -> SDoc
ppr_forall_co p ty
= maybeParen p FunPrec $
sep [pprForAll tvs, ppr_co TopPrec rho]
where
(tvs, rho) = split1 [] ty
split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
split1 tvs ty = (reverse tvs, ty)
data HsWrapper
= WpHole
| WpCompose HsWrapper HsWrapper
| WpFun HsWrapper HsWrapper TcType TcType
| WpCast TcCoercion
| WpEvLam EvVar
| WpEvApp EvTerm
| WpTyLam TyVar
| WpTyApp KindOrType
| WpLet TcEvBinds
deriving (Data.Data, Data.Typeable)
(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> c = c
c <.> WpHole = c
c1 <.> c2 = c1 `WpCompose` c2
mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper
mkWpFun WpHole WpHole _ _ = WpHole
mkWpFun WpHole (WpCast co2) t1 _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
mkWpFun (WpCast co1) WpHole _ t2 = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
mkWpFun (WpCast co1) (WpCast co2) _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
mkWpFun co1 co2 t1 t2 = WpFun co1 co2 t1 t2
mkWpCast :: TcCoercion -> HsWrapper
mkWpCast co
| isTcReflCo co = WpHole
| otherwise = ASSERT2(tcCoercionRole co == Representational, ppr co)
WpCast co
mkWpTyApps :: [Type] -> HsWrapper
mkWpTyApps tys = mk_co_app_fn WpTyApp tys
mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvApps args = mk_co_app_fn WpEvApp args
mkWpEvVarApps :: [EvVar] -> HsWrapper
mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
mkWpTyLams :: [TyVar] -> HsWrapper
mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
mkWpLams :: [Var] -> HsWrapper
mkWpLams ids = mk_co_lam_fn WpEvLam ids
mkWpLet :: TcEvBinds -> HsWrapper
mkWpLet (EvBinds b) | isEmptyBag b = WpHole
mkWpLet ev_binds = WpLet ev_binds
mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
idHsWrapper :: HsWrapper
idHsWrapper = WpHole
isIdHsWrapper :: HsWrapper -> Bool
isIdHsWrapper WpHole = True
isIdHsWrapper _ = False
data TcEvBinds
= TcEvBinds
EvBindsVar
| EvBinds
(Bag EvBind)
deriving( Data.Typeable )
data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
instance Data.Data TcEvBinds where
toConstr _ = abstractConstr "TcEvBinds"
gunfold _ _ = error "gunfold"
dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
newtype EvBindMap
= EvBindMap {
ev_bind_varenv :: VarEnv EvBind
}
emptyEvBindMap :: EvBindMap
emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
extendEvBinds bs v t
= EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }
lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
evBindMapBinds :: EvBindMap -> Bag EvBind
evBindMapBinds bs
= foldVarEnv consBag emptyBag (ev_bind_varenv bs)
data EvBind = EvBind EvVar EvTerm
data EvTerm
= EvId EvId
| EvCoercion TcCoercion
| EvCast EvTerm TcCoercion
| EvDFunApp DFunId
[Type] [EvTerm]
| EvTupleSel EvTerm Int
| EvTupleMk [EvTerm]
| EvDelayedError Type FastString
| EvSuperClass EvTerm Int
| EvLit EvLit
| EvTypeable EvTypeable
| EvCallStack EvCallStack
deriving( Data.Data, Data.Typeable )
data EvTypeable
= EvTypeableTyCon TyCon [Kind]
| EvTypeableTyApp (EvTerm,Type) (EvTerm,Type)
| EvTypeableTyLit Type
deriving ( Data.Data, Data.Typeable )
data EvLit
= EvNum Integer
| EvStr FastString
deriving( Data.Data, Data.Typeable )
data EvCallStack
= EvCsEmpty
| EvCsPushCall Name RealSrcSpan EvTerm
| EvCsTop FastString RealSrcSpan EvTerm
deriving( Data.Data, Data.Typeable )
mkEvCast :: EvTerm -> TcCoercion -> EvTerm
mkEvCast ev lco
| ASSERT2(tcCoercionRole lco == Representational, (vcat [ptext (sLit "Coercion of wrong role passed to mkEvCast:"), ppr ev, ppr lco]))
isTcReflCo lco = ev
| otherwise = EvCast ev lco
mkEvTupleSelectors :: EvTerm -> [TcPredType] -> [(TcPredType, EvTerm)]
mkEvTupleSelectors ev preds = zipWith mk_pr preds [0..]
where
mk_pr pred i = (pred, EvTupleSel ev i)
mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
mkEvScSelectors ev cls tys
= zipWith mk_pr (immSuperClasses cls tys) [0..]
where
mk_pr pred i = (pred, EvSuperClass ev i)
emptyTcEvBinds :: TcEvBinds
emptyTcEvBinds = EvBinds emptyBag
isEmptyTcEvBinds :: TcEvBinds -> Bool
isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
evTermCoercion :: EvTerm -> TcCoercion
evTermCoercion (EvId v) = mkTcCoVarCo v
evTermCoercion (EvCoercion co) = co
evTermCoercion (EvCast tm co) = TcCastCo (evTermCoercion tm) co
evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm (EvId v) = unitVarSet v
evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co
evVarsOfTerm (EvDFunApp _ _ evs) = evVarsOfTerms evs
evVarsOfTerm (EvTupleSel v _) = evVarsOfTerm v
evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
evVarsOfTerm (EvTupleMk evs) = evVarsOfTerms evs
evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
evVarsOfTerm (EvLit _) = emptyVarSet
evVarsOfTerm (EvTypeable ev) = evVarsOfTypeable ev
evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs
evVarsOfTerms :: [EvTerm] -> VarSet
evVarsOfTerms = mapUnionVarSet evVarsOfTerm
evVarsOfTypeable :: EvTypeable -> VarSet
evVarsOfTypeable ev =
case ev of
EvTypeableTyCon _ _ -> emptyVarSet
EvTypeableTyApp e1 e2 -> evVarsOfTerms (map fst [e1,e2])
EvTypeableTyLit _ -> emptyVarSet
evVarsOfCallStack :: EvCallStack -> VarSet
evVarsOfCallStack cs = case cs of
EvCsEmpty -> emptyVarSet
EvCsTop _ _ tm -> evVarsOfTerm tm
EvCsPushCall _ _ tm -> evVarsOfTerm tm
instance Outputable HsWrapper where
ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
pprHsWrapper :: SDoc -> HsWrapper -> SDoc
pprHsWrapper doc wrap
= getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
where
help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help it WpHole = it
help it (WpCompose f1 f2) = help (help it f2) f1
help it (WpFun f1 f2 t1 _) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+>
help (\_ -> it True <+> help (\_ -> ptext (sLit "x")) f1 True) f2 False
help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
<+> pprParendTcCo co)]
help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
help it (WpTyApp ty) = no_parens $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
help it (WpEvLam id) = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
help it (WpTyLam tv) = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
pp_bndr v = pprBndr LambdaBind v <> dot
add_parens, no_parens :: SDoc -> Bool -> SDoc
add_parens d True = parens d
add_parens d False = d
no_parens d _ = d
instance Outputable TcEvBinds where
ppr (TcEvBinds v) = ppr v
ppr (EvBinds bs) = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
instance Outputable EvBindsVar where
ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
instance Outputable EvBind where
ppr (EvBind v e) = sep [ ppr v, nest 2 $ equals <+> ppr e ]
instance Outputable EvTerm where
ppr (EvId v) = ppr v
ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co
ppr (EvTupleSel v n) = ptext (sLit "tupsel") <> parens (ppr (v,n))
ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs
ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
ppr (EvLit l) = ppr l
ppr (EvCallStack cs) = ppr cs
ppr (EvDelayedError ty msg) = ptext (sLit "error")
<+> sep [ char '@' <> ppr ty, ppr msg ]
ppr (EvTypeable ev) = ppr ev
instance Outputable EvLit where
ppr (EvNum n) = integer n
ppr (EvStr s) = text (show s)
instance Outputable EvTypeable where
ppr ev =
case ev of
EvTypeableTyCon tc ks -> parens (ppr tc <+> sep (map ppr ks))
EvTypeableTyApp t1 t2 -> parens (ppr (fst t1) <+> ppr (fst t2))
EvTypeableTyLit x -> ppr x
instance Outputable EvCallStack where
ppr EvCsEmpty
= ptext (sLit "[]")
ppr (EvCsTop name loc tm)
= angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
ppr (EvCsPushCall name loc tm)
= angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
unwrapIP :: Type -> Coercion
unwrapIP ty =
case unwrapNewTyCon_maybe tc of
Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys
Nothing -> pprPanic "unwrapIP" $
text "The dictionary for" <+> quotes (ppr tc)
<+> text "is not a newtype!"
where
(tc, tys) = splitTyConApp ty
wrapIP :: Type -> Coercion
wrapIP ty = mkSymCo (unwrapIP ty)