From 5e5310b3cb4f78e30cc7b90879eb016e97c214cb Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Sat, 20 Sep 2008 23:20:24 +0000 Subject: [PATCH] Comments only: replace ":=:" by "~" (notation for equality predicates) --- compiler/basicTypes/DataCon.lhs | 14 +++++++------- compiler/basicTypes/MkId.lhs | 2 +- compiler/basicTypes/Var.lhs | 2 +- compiler/coreSyn/CoreUtils.lhs | 6 +++--- compiler/hsSyn/HsExpr.lhs | 2 ++ compiler/iface/BuildTyCl.lhs | 2 +- compiler/iface/IfaceType.lhs | 2 +- compiler/typecheck/TcInstDcls.lhs | 4 ++-- compiler/typecheck/TcPat.lhs | 4 ++-- compiler/typecheck/TcSimplify.lhs | 2 +- compiler/typecheck/TcTyClsDecls.lhs | 2 +- compiler/typecheck/TcUnify.lhs | 6 +++--- compiler/types/Coercion.lhs | 18 +++++++++--------- compiler/types/FunDeps.lhs | 4 ++-- compiler/types/TyCon.lhs | 12 ++++++------ compiler/types/Unify.lhs | 12 ++++++------ 16 files changed, 48 insertions(+), 46 deletions(-) diff --git a/compiler/basicTypes/DataCon.lhs b/compiler/basicTypes/DataCon.lhs index 5a67ffe..1b354c6 100644 --- a/compiler/basicTypes/DataCon.lhs +++ b/compiler/basicTypes/DataCon.lhs @@ -164,7 +164,7 @@ Why might the wrapper have anything to do? Two reasons: \$wMkT :: a -> T [a] \$wMkT a x = MkT [a] a [a] x The third argument is a coerion - [a] :: [a]:=:[a] + [a] :: [a]~[a] INVARIANT: the dictionary constructor for a class never has a wrapper. @@ -246,14 +246,14 @@ data DataCon -- *** As represented internally -- data T a where - -- MkT :: forall a. forall x y. (a:=:(x,y),x~y,Ord x) => x -> y -> T a + -- MkT :: forall a. forall x y. (a~(x,y),x~y,Ord x) => x -> y -> T a -- -- The next six fields express the type of the constructor, in pieces -- e.g. -- -- dcUnivTyVars = [a] -- dcExTyVars = [x,y] - -- dcEqSpec = [a:=:(x,y)] + -- dcEqSpec = [a~(x,y)] -- dcEqTheta = [x~y] -- dcDictTheta = [Ord x] -- dcOrigArgTys = [a,List b] @@ -286,9 +286,9 @@ data DataCon -- _as written by the programmer_ -- This field allows us to move conveniently between the two ways -- of representing a GADT constructor's type: - -- MkT :: forall a b. (a :=: [b]) => b -> T a + -- MkT :: forall a b. (a ~ [b]) => b -> T a -- MkT :: forall b. b -> T [b] - -- Each equality is of the form (a :=: ty), where 'a' is one of + -- Each equality is of the form (a ~ ty), where 'a' is one of -- the universally quantified type variables -- The next two fields give the type context of the data constructor @@ -346,7 +346,7 @@ data DataCon dcRepTyCon :: TyCon, -- Result tycon, T dcRepType :: Type, -- Type of the constructor - -- forall a x y. (a:=:(x,y), x~y, Ord x) => + -- forall a x y. (a~(x,y), x~y, Ord x) => -- x -> y -> T a -- (this is *not* of the constructor wrapper Id: -- see Note [Data con representation] below) @@ -355,7 +355,7 @@ data DataCon -- case (e :: T t) of -- MkT x y co1 co2 (d:Ord x) (v:r) (w:F s) -> ... -- It's convenient to apply the rep-type of MkT to 't', to get - -- forall x y. (t:=:(x,y), x~y, Ord x) => x -> y -> T t + -- forall x y. (t~(x,y), x~y, Ord x) => x -> y -> T t -- and use that to check the pattern. Mind you, this is really only -- used in CoreLint. diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs index f9eae93..ae2d837 100644 --- a/compiler/basicTypes/MkId.lhs +++ b/compiler/basicTypes/MkId.lhs @@ -188,7 +188,7 @@ tyConFamInst_maybe). A coercion allows you to move between representation and family type. It is accessible from :R123Map via tyConFamilyCoercion_maybe and has kind - Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v} + Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v} The wrapper and worker of MapPair get the types diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index ee09c3e..4f1ed2e 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -289,7 +289,7 @@ mkTcTyVar name kind details \begin{code} type CoVar = TyVar -- A coercion variable is simply a type - -- variable of kind @ty1 :=: ty2@. Hence its + -- variable of kind @ty1 ~ ty2@. Hence its -- 'varType' is always @PredTy (EqPred t1 t2)@ coVarName :: CoVar -> Name diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index eb9ea41..f44967e 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/compiler/coreSyn/CoreUtils.lhs @@ -740,12 +740,12 @@ dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys -- ... -- -- has representation type --- forall a. forall a1. forall b. (a :=: (a1,b)) => +-- forall a. forall a1. forall b. (a ~ (a1,b)) => -- Int -> b -> T a -- -- dataConInstPat fss us T1 (a1',b') will return -- --- ([a1'', b''], [c :: (a1', b'):=:(a1'', b'')], [x :: Int, y :: b'']) +-- ([a1'', b''], [c :: (a1', b')~(a1'', b'')], [x :: Int, y :: b'']) -- -- where the double-primed variables are created with the FastStrings and -- Uniques given as fss and us @@ -801,7 +801,7 @@ exprIsConApp_maybe (Cast expr co) -- The transformation applies iff we have -- (C e1 ... en) `cast` co - -- where co :: (T t1 .. tn) :=: (T s1 ..sn) + -- where co :: (T t1 .. tn) ~ (T s1 ..sn) -- That is, with a T at the top of both sides -- The left-hand one must be a T, because exprIsConApp returned True -- but the right-hand one might not be. (Though it usually will.) diff --git a/compiler/hsSyn/HsExpr.lhs b/compiler/hsSyn/HsExpr.lhs index 17a8c3f..bcc5084 100644 --- a/compiler/hsSyn/HsExpr.lhs +++ b/compiler/hsSyn/HsExpr.lhs @@ -164,6 +164,8 @@ data HsExpr id -- Record update | RecordUpd (LHsExpr id) (HsRecordBinds id) +-- (HsMatchGroup Id) -- Filled in by the type checker to be +-- -- a match that does the job [DataCon] -- Filled in by the type checker to the -- _non-empty_ list of DataCons that have -- all the upd'd fields diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs index 296b430..12668ab 100644 --- a/compiler/iface/BuildTyCl.lhs +++ b/compiler/iface/BuildTyCl.lhs @@ -93,7 +93,7 @@ buildAlgTyCon tc_name tvs stupid_theta rhs is_rec want_generics gadt_syn -- -- (1) create a coercion that identifies the family instance type and the -- representation type from Step (1); ie, it is of the form --- `Co tvs :: F ts :=: R tvs', where `Co' is the name of the coercion, +-- `Co tvs :: F ts ~ R tvs', where `Co' is the name of the coercion, -- `F' the family tycon and `R' the (derived) representation tycon, -- and -- (2) produce a `TyConParent' value containing the parent and coercion diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs index 59fb3e9..1688344 100644 --- a/compiler/iface/IfaceType.lhs +++ b/compiler/iface/IfaceType.lhs @@ -238,7 +238,7 @@ ppr_tc tc = ppr tc ------------------- instance Outputable IfacePredType where -- Print without parens - ppr (IfaceEqPred ty1 ty2)= hsep [ppr ty1, ptext (sLit ":=:"), ppr ty2] + ppr (IfaceEqPred ty1 ty2)= hsep [ppr ty1, ptext (sLit "~"), ppr ty2] ppr (IfaceIParam ip ty) = hsep [ppr ip, dcolon, ppr ty] ppr (IfaceClassP cls ts) = parenSymOcc (getOccName cls) (ppr cls) <+> sep (map pprParendIfaceType ts) diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index f3d37e7..e7c472b 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -571,7 +571,7 @@ tcInstDecl2 :: InstInfo Name -> TcM (LHsBinds Id) -- newtype N a = MkN (Tree [a]) deriving( Foo Int ) -- -- The newtype gives an FC axiom looking like --- axiom CoN a :: N a :=: Tree [a] +-- axiom CoN a :: N a ~ Tree [a] -- (see Note [Newtype coercions] in TyCon for this unusual form of axiom) -- -- So all need is to generate a binding looking like: @@ -637,7 +637,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived }) -- make_coercion -- The inst_head looks like (C s1 .. sm (T a1 .. ak)) -- But we want the coercion (C s1 .. sm (sym (CoT a1 .. ak))) - -- with kind (C s1 .. sm (T a1 .. ak) :=: C s1 .. sm ) + -- with kind (C s1 .. sm (T a1 .. ak) ~ C s1 .. sm ) -- where rep_ty is the (eta-reduced) type rep of T -- So we just replace T with CoT, and insert a 'sym' -- NB: we know that k will be >= arity of CoT, because the latter fully eta-reduced diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 9511619..984b2e5 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -568,7 +568,7 @@ the split arguments for the representation tycon :R123Map as {Int, c, w} In other words, boxySplitTyConAppWithFamily implicitly takes the coercion - Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v} + Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v} moving between representation and family type into account. To produce type correct Core, this coercion needs to be used to case the type of the scrutinee @@ -594,7 +594,7 @@ to express the local scope of GADT refinements. \begin{code} -- Running example: --- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a +-- MkT :: forall a b c. (a~[b]) => b -> c -> T a -- with scrutinee of type (T ty) tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index cb6021c..1e51ee0 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -861,7 +861,7 @@ Note [NO TYVARS] The excitement comes when simplifying the bindings for h. Initially try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}. -From this we get t1:=:t2, but also various bindings. We can't forget +From this we get t1~t2, but also various bindings. We can't forget the bindings (because of [LOOP]), but in fact t1 is what g is polymorphic in. diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 5a2f773..2400838 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -878,7 +878,7 @@ tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty) -- E.g. data T a b c where -- MkT :: forall x y z. T (x,y) z z -- Then we generate - -- ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T) + -- ([a,z,c], [x,y], [a~(x,y), c~z], T) = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 9f5daeb..72df161 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -1294,8 +1294,8 @@ Note [TyCon app] When we find two TyConApps, the argument lists are guaranteed equal length. Reason: intially the kinds of the two types to be unified is the same. The only way it can become not the same is when unifying two -AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in -the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first, +AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in +the f1,f2 (because it'd absorb the app). If we unify f1~f2 first, which we do, that ensures that f1,f2 have the same kind; and that means a1,a2 have the same kind. And now the argument repeats. @@ -1870,7 +1870,7 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k -- If the flag is False, it requires k <: sk -- E.g. kindSimpleKind False ?? = * --- What about (kv -> *) :=: ?? -> * +-- What about (kv -> *) ~ ?? -> * kindSimpleKind orig_swapped orig_kind = go orig_swapped orig_kind where diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index d6b92fa..59a1a15 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -74,14 +74,14 @@ import FastString -- | A 'Coercion' represents a 'Type' something should be coerced to. type Coercion = Type --- | A 'CoercionKind' is always of form @ty1 :=: ty2@ and indicates the +-- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the -- types that a 'Coercion' will work on. type CoercionKind = Kind ------------------------------ --- | This breaks a 'Coercion' with 'CoercionKind' @T A B C :=: T D E F@ into --- a list of 'Coercion's of kinds @A :=: D@, @B :=: E@ and @E :=: F@. Hence: +-- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into +-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence: -- -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c] decomposeCo :: Arity -> Coercion -> [Coercion] @@ -134,7 +134,7 @@ splitCoercionKind_maybe _ = Nothing -- | If it is the case that -- --- > c :: (t1 :=: t2) +-- > c :: (t1 ~ t2) -- -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@. -- See also 'coercionKindPredTy' @@ -218,8 +218,8 @@ mkFunCoercion co1 co2 = mkFunTy co1 co2 mkSymCoercion :: Coercion -> Coercion -- ^ Create a symmetric version of the given 'Coercion' that asserts equality between --- the same types but in the other "direction", so a kind of @t1 :=: t2@ becomes the --- kind @t2 :=: t1@. +-- the same types but in the other "direction", so a kind of @t1 ~ t2@ becomes the +-- kind @t2 ~ t1@. -- -- This function attempts to simplify the generated 'Coercion' by removing redundant applications -- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that @@ -405,7 +405,7 @@ mkNewTypeCoercion name tycon tvs rhs_ty (TyConApp tycon args, substTyWith tvs args rhs_ty) -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type --- and its family instance. It has the form @Co tvs :: F ts :=: R tvs@, where @Co@ is +-- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived) -- representation tycon. mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon @@ -420,7 +420,7 @@ mkFamInstCoercion name tvs family instTys rep_tycon coArity = length tvs rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs], TyConApp family instTys, -- sigma (F ts) - TyConApp rep_tycon args) -- :=: R tys + TyConApp rep_tycon args) -- ~ R tys -------------------------------------- -- Coercion Type Constructors... @@ -478,7 +478,7 @@ splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type)) -- Helper for left and right. Finds coercion kind of its input and -- returns the left and right projections of the coercion... -- --- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) +-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) splitCoercionKindOf co | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co) , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1 diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs index 7f9f050..170304c 100644 --- a/compiler/types/FunDeps.lhs +++ b/compiler/types/FunDeps.lhs @@ -203,7 +203,7 @@ type Equation = (TyVarSet, [(Type, Type)]) pprEquation :: Equation -> SDoc pprEquation (qtvs, pairs) = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)), - nest 2 (vcat [ ppr t1 <+> ptext (sLit ":=:") <+> ppr t2 | (t1,t2) <- pairs])] + nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])] \end{code} Given a bunch of predicates that must hold, such as @@ -320,7 +320,7 @@ checkClsFD qtvs fd clas_tvs tys1 tys2 -- tys2 = [Maybe t1, t2] -- -- We can instantiate x to t1, and then we want to force --- (Tree x) [t1/x] :=: t2 +-- (Tree x) [t1/x] ~ t2 -- -- This function is also used when matching two Insts (rather than an Inst -- against an instance decl. In that case, qtvs is empty, and we are doing diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 09caf8e..256b141 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -112,7 +112,7 @@ import Constants -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@ -- -- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ as a 'Type', where --- that type has kind @t1 :=: t2@. See "Coercion" for more on this +-- that type has kind @t1 ~ t2@. See "Coercion" for more on this -- -- This data type also encodes a number of primitive, built in type constructors such as those -- for function and tuple types. @@ -211,7 +211,7 @@ data TyCon tyConExtName :: Maybe FastString -- ^ @Just e@ for foreign-imported types, holds the name of the imported thing } - -- | Type coercions, such as @(:=:)@, @sym@, @trans@, @left@ and @right@. + -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@. -- INVARIANT: coercions are always fully applied | CoercionTyCon { tyConUnique :: Unique, @@ -393,7 +393,7 @@ newtype, to the newtype itself. For example, newtype T a = MkT (a -> a) -the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: t -> +the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t. This TyCon is a CoercionTyCon, so it does not have a kind on its own; it basically has its own typing rule for the fully-applied version. If the newtype T has k type variables then CoT has arity at @@ -403,11 +403,11 @@ ending with the same type variables as the left hand side, we newtype S a = MkT [a] -then we would generate the arity 0 coercion CoS : S :=: []. The +then we would generate the arity 0 coercion CoS : S ~ []. The primary reason we do this is to make newtype deriving cleaner. In the paper we'd write - axiom CoT : (forall t. T t) :=: (forall t. [t]) + axiom CoT : (forall t. T t) ~ (forall t. [t]) and then when we used CoT at a particular type, s, we'd say CoT @ s which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s]) @@ -418,7 +418,7 @@ be saturated, but which encodes as TyConApp CoT [s] In the vocabulary of the paper it's as if we had axiom declarations like - axiom CoT t : T t :=: [t] + axiom CoT t : T t ~ [t] Note [Newtype eta] ~~~~~~~~~~~~~~~~~~ diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 3e35ac6..07c927c 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -384,7 +384,7 @@ dataConCannotMatch tys con data Refinement = Reft InScopeSet InternalReft type InternalReft = TyVarEnv (Coercion, Type) --- INVARIANT: a->(co,ty) then co :: (a:=:ty) +-- INVARIANT: a->(co,ty) then co :: (a~ty) -- Not necessarily idemopotent instance Outputable Refinement where @@ -401,7 +401,7 @@ isEmptyRefinement (Reft _ env) = isEmptyVarEnv env refineType :: Refinement -> Type -> Maybe (Coercion, Type) -- Apply the refinement to the type. -- If (refineType r ty) = (co, ty') --- Then co :: ty:=:ty' +-- Then co :: ty~ty' -- Nothing => the refinement does nothing to this type refineType (Reft in_scope env) ty | not (isEmptyVarEnv env), -- Common case @@ -427,7 +427,7 @@ refinePred (Reft in_scope env) pred refineResType :: Refinement -> Type -> Maybe (Coercion, Type) -- Like refineType, but returns the 'sym' coercion -- If (refineResType r ty) = (co, ty') --- Then co :: ty':=:ty +-- Then co :: ty'~ty refineResType reft ty = case refineType reft ty of Just (co, ty1) -> Just (mkSymCoercion co, ty1) @@ -617,8 +617,8 @@ uVar :: TvSubstEnv -- An existing substitution to extend -> UM TvSubstEnv -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that --- if swap=False (tv1:=:ty) --- if swap=True (ty:=:tv1) +-- if swap=False (tv1~ty) +-- if swap=True (ty~tv1) uVar subst tv1 ty = -- Check to see whether tv1 is refined by the substitution @@ -640,7 +640,7 @@ uUnrefined subst tv1 ty2 ty2' = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms -- This is essential, in case we have -- type Foo a = a - -- and then unify a :=: Foo a + -- and then unify a ~ Foo a uUnrefined subst tv1 ty2 (TyVarTy tv2) | tv1 == tv2 -- Same type variable -- 1.7.10.4