Commit 79cfb199 authored by Richard Eisenberg's avatar Richard Eisenberg

Remove old coercion pretty-printer

Now, all coercions are printed from IfaceType, just like types.

This also changes the rendering of TransCo to use ; instead of
a prefix operator.
parent bb2a446a
......@@ -1070,7 +1070,8 @@ ppr_co ctxt_prec (IfaceAxiomInstCo n i cos)
ppr_co ctxt_prec (IfaceSymCo co)
= ppr_special_co ctxt_prec (text "Sym") [co]
ppr_co ctxt_prec (IfaceTransCo co1 co2)
= ppr_special_co ctxt_prec (text "Trans") [co1,co2]
= maybeParen ctxt_prec TyOpPrec $
ppr_co TyOpPrec co1 <+> semi <+> ppr_co TyOpPrec co2
ppr_co ctxt_prec (IfaceNthCo d co)
= ppr_special_co ctxt_prec (text "Nth:" <> int d) [co]
ppr_co ctxt_prec (IfaceLRCo lr co)
......
......@@ -22,7 +22,7 @@ module ToIface
, tidyToIfaceContext
, tidyToIfaceTcArgs
-- * Coercions
, toIfaceCoercion
, toIfaceCoercion, toIfaceCoercionX
-- * Pattern synonyms
, patSynToIfaceDecl
-- * Expressions
......@@ -216,7 +216,7 @@ toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
toIfaceCoercionX fr co
= go co
where
go (Refl r ty) = IfaceReflCo r (toIfaceType ty)
go (Refl r ty) = IfaceReflCo r (toIfaceTypeX fr ty)
go (CoVarCo cv)
-- See [TcTyVars in IfaceType] in IfaceType
| cv `elemVarSet` fr = IfaceFreeCoVar cv
......
......@@ -13,4 +13,4 @@ toIfaceTyLit :: TyLit -> IfaceTyLit
toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
toIfaceTyCon :: TyCon -> IfaceTyCon
toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
toIfaceCoercion :: Coercion -> IfaceCoercion
toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
......@@ -95,7 +95,7 @@ module Coercion (
seqCo,
-- * Pretty-printing
pprCo, pprParendCo, pprCoBndr,
pprCo, pprParendCo,
pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
-- * Tidying
......@@ -152,117 +152,32 @@ setCoVarUnique = setVarUnique
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName = setVarName
{-
%************************************************************************
%* *
Pretty-printing coercions
Pretty-printing CoAxioms
%* *
%************************************************************************
@pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
function is defined to use this. @pprParendCo@ is the same, except it
puts parens around the type, except for the atomic cases.
@pprParendCo@ works just by setting the initial context precedence
very high.
-}
-- Outputable instances are in TyCoRep, to avoid orphans
pprCo, pprParendCo :: Coercion -> SDoc
pprCo co = ppr_co TopPrec co
pprParendCo co = ppr_co TyConPrec co
ppr_co :: TyPrec -> Coercion -> SDoc
ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
ppr_co _ (TyConAppCo r tc cos) = pprTcAppCo TyConPrec ppr_co tc cos <> ppr_role r
ppr_co p (AppCo co arg) = maybeParen p TyConPrec $
pprCo co <+> ppr_co TyConPrec arg
ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
ppr_co p co@(FunCo {}) = ppr_fun_co p co
ppr_co _ (CoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
ppr_co p (AxiomInstCo con index args)
= pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
(map (ppr_co TyConPrec) args)
ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
case trans_co_list co [] of
[] -> panic "ppr_co"
(co:cos) -> sep ( ppr_co FunPrec co
: [ char ';' <+> ppr_co FunPrec co | co <- cos])
ppr_co p (InstCo co arg) = maybeParen p TyConPrec $
pprParendCo co <> text "@" <> ppr_co TopPrec arg
ppr_co p (UnivCo UnsafeCoerceProv r ty1 ty2)
= pprPrefixApp p (text "UnsafeCo" <+> ppr r)
[pprParendType ty1, pprParendType ty2]
ppr_co _ (UnivCo p r t1 t2)
= char 'U'
<> parens (ppr_prov <> comma <+> ppr t1 <> comma <+> ppr t2)
<> ppr_role r
where
ppr_prov = case p of
HoleProv h -> text "hole:" <> ppr h
PhantomProv kind_co -> text "phant:" <> ppr kind_co
ProofIrrelProv co -> text "irrel:" <> ppr co
PluginProv s -> text "plugin:" <> text s
UnsafeCoerceProv -> text "unsafe"
ppr_co p (SymCo co) = pprPrefixApp p (text "Sym") [pprParendCo co]
ppr_co p (NthCo n co) = pprPrefixApp p (text "Nth:" <> int n) [pprParendCo co]
ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
ppr_co p (CoherenceCo c1 c2) = maybeParen p TyConPrec $
(ppr_co FunPrec c1) <+> (text "|>") <+>
(ppr_co FunPrec c2)
ppr_co p (KindCo co) = pprPrefixApp p (text "kind") [pprParendCo co]
ppr_co p (SubCo co) = pprPrefixApp p (text "Sub") [pprParendCo co]
ppr_co p (AxiomRuleCo co cs) = maybeParen p TopPrec $ ppr_axiom_rule_co co cs
ppr_axiom_rule_co :: CoAxiomRule -> [Coercion] -> SDoc
ppr_axiom_rule_co co ps = ppr (coaxrName co) <+> parens (interpp'SP ps)
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'
trans_co_list :: Coercion -> [Coercion] -> [Coercion]
trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
trans_co_list co cos = co : cos
ppr_fun_co :: TyPrec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
where
split :: Coercion -> [SDoc]
split (FunCo _ arg res)
= ppr_co FunPrec arg : split res
split co = [ppr_co TopPrec co]
Defined here to avoid module loops. CoAxiom is loaded very early on.
ppr_forall_co :: TyPrec -> Coercion -> SDoc
ppr_forall_co p (ForAllCo tv h co)
= maybeParen p FunPrec $
sep [pprCoBndr (tyVarName tv) h, ppr_co TopPrec co]
ppr_forall_co _ _ = panic "ppr_forall_co"
pprCoBndr :: Name -> Coercion -> SDoc
pprCoBndr name eta =
forAllLit <+> parens (ppr name <+> dcolon <+> ppr eta) <> dot
-}
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
= hang (text "axiom" <+> ppr ax <+> dcolon)
2 (vcat (map (ppr_co_ax_branch (const ppr) ax) $ fromBranches branches))
2 (vcat (map (ppr_co_ax_branch (const pprType) ax) $ fromBranches branches))
pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
pprCoAxBranch = ppr_co_ax_branch pprRhs
where
pprRhs fam_tc (TyConApp tycon _)
| isDataFamilyTyCon fam_tc
pprRhs fam_tc rhs
| Just (tycon, _) <- splitTyConApp_maybe rhs
, isDataFamilyTyCon fam_tc
= pprDataCons tycon
pprRhs _ rhs = ppr rhs
| otherwise
= ppr rhs
pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
......
......@@ -8,7 +8,6 @@ import {-# SOURCE #-} TyCon
import BasicTypes ( LeftOrRight )
import CoAxiom
import Var
import Outputable
import Pair
import Util
......@@ -47,5 +46,3 @@ seqCo :: Coercion -> ()
coercionKind :: Coercion -> Pair Type
coercionType :: Coercion -> Type
pprCo :: Coercion -> SDoc
......@@ -62,10 +62,12 @@ module TyCoRep (
pprTyVar, pprTyVars,
pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprTyLit,
TyPrec(..), maybeParen, pprTcAppCo,
TyPrec(..), maybeParen,
pprPrefixApp, pprArrowChain,
pprDataCons, ppSuggestExplicitKinds,
pprCo, pprParendCo,
-- * Free variables
tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
tyCoFVsBndr, tyCoFVsOfType, tyCoVarsOfTypeList,
......@@ -139,13 +141,14 @@ import {-# SOURCE #-} DataCon( dataConFullSig
import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy
, tyCoVarsOfTypeWellScoped
, tyCoVarsOfTypesWellScoped
, toposortTyVars
, coreView, typeKind )
-- Transitively pulls in a LOT of stuff, better to break the loop
import {-# SOURCE #-} Coercion
import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr
, toIfaceTyCon, toIfaceTcArgs, toIfaceCoercion )
, toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX )
-- friends:
import IfaceType
......@@ -2472,6 +2475,29 @@ tidyToIfaceType ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env ty)
env = tidyFreeTyCoVars emptyTidyEnv free_tcvs
free_tcvs = tyCoVarsOfTypeWellScoped ty
------------
pprCo, pprParendCo :: Coercion -> SDoc
pprCo co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty)
pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty)
tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion
tidyToIfaceCoSty co sty
| userStyle sty = tidyToIfaceCo co
| otherwise = toIfaceCoercionX (tyCoVarsOfCo co) co
-- in latter case, don't tidy, as we'll be printing uniques.
tidyToIfaceCo :: Coercion -> IfaceCoercion
-- It's vital to tidy before converting to an IfaceType
-- or nested binders will become indistinguishable!
--
-- Also for the free type variables, tell toIfaceCoercionX to
-- leave them as IfaceFreeCoVar. This is super-important
-- for debug printing.
tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co)
where
env = tidyFreeTyCoVars emptyTidyEnv free_tcvs
free_tcvs = toposortTyVars $ tyCoVarsOfCoList co
------------
pprClassPred :: Class -> [Type] -> SDoc
pprClassPred clas tys = pprTypeApp (classTyCon clas) tys
......@@ -2596,11 +2622,6 @@ pprTypeApp tc tys
(toIfaceTcArgs tc tys)
-- TODO: toIfaceTcArgs seems rather wasteful here
pprTcAppCo :: TyPrec -> (TyPrec -> Coercion -> SDoc)
-> TyCon -> [Coercion] -> SDoc
pprTcAppCo p _pp tc cos
= pprIfaceCoTcApp p (toIfaceTyCon tc) (map toIfaceCoercion cos)
------------------
pprPrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
......
......@@ -1828,7 +1828,7 @@ predTypeEqRel ty
--
-- This is a deterministic sorting operation
-- (that is, doesn't depend on Uniques).
toposortTyVars :: [TyVar] -> [TyVar]
toposortTyVars :: [TyCoVar] -> [TyCoVar]
toposortTyVars tvs = reverse $
[ node_payload node | node <- topologicalSortG $
graphFromEdgedVerticesOrd nodes ]
......
......@@ -2,7 +2,7 @@
module Type where
import TyCon
import Var ( TyVar )
import Var ( TyCoVar )
import {-# SOURCE #-} TyCoRep( Type, Coercion, Kind )
import Util
......@@ -21,6 +21,7 @@ partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
coreView :: Type -> Maybe Type
tcView :: Type -> Maybe Type
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypesWellScoped :: [Type] -> [TyCoVar]
tyCoVarsOfTypeWellScoped :: Type -> [TyCoVar]
toposortTyVars :: [TyCoVar] -> [TyCoVar]
splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment