Commit e992317b authored by Herbert Valerio Riedel's avatar Herbert Valerio Riedel 🕺

unlit compiler/types/ modules

Differential Revision: https://phabricator.haskell.org/D544
parent 4b16ff6d
%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-- (c) The University of Glasgow 2006
-- (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
--
-- The @Class@ datatype
The @Class@ datatype
\begin{code}
{-# LANGUAGE CPP, DeriveDataTypeable #-}
module Class (
......@@ -38,17 +35,17 @@ import BooleanFormula (BooleanFormula)
import Data.Typeable (Typeable)
import qualified Data.Data as Data
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
\subsection[Class-basic]{@Class@: basic definition}
%* *
%************************************************************************
* *
************************************************************************
A @Class@ corresponds to a Greek kappa in the static semantics:
-}
\begin{code}
data Class
= Class {
classTyCon :: TyCon, -- The data type constructor for
......@@ -108,8 +105,8 @@ defMethSpecOfDefMeth meth
NoDefMeth -> NoDM
DefMeth _ -> VanillaDM
GenDefMeth _ -> GenericDM
\end{code}
{-
Note [Associated type defaults]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The following is an example of associated type defaults:
......@@ -142,8 +139,8 @@ Note that
the default Type rhs
The @mkClass@ function fills in the indirect superclasses.
-}
\begin{code}
mkClass :: [TyVar]
-> [([TyVar], [TyVar])]
-> [PredType] -> [Id]
......@@ -165,8 +162,8 @@ mkClass tyvars fds super_classes superdict_sels at_stuff
classOpStuff = op_stuff,
classMinimalDef = mindef,
classTyCon = tycon }
\end{code}
{-
Note [Associated type tyvar names]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The TyCon of an associated type should use the same variable names as its
......@@ -186,15 +183,15 @@ Having the same variables for class and tycon is also used in checkValidRoles
(in TcTyClsDecls) when checking a class's roles.
%************************************************************************
%* *
************************************************************************
* *
\subsection[Class-selectors]{@Class@: simple selectors}
%* *
%************************************************************************
* *
************************************************************************
The rest of these functions are just simple selectors.
-}
\begin{code}
classArity :: Class -> Arity
classArity clas = length (classTyVars clas)
-- Could memoise this
......@@ -240,18 +237,17 @@ classExtraBigSig (Class {classTyVars = tyvars, classFunDeps = fundeps,
classSCTheta = sc_theta, classSCSels = sc_sels,
classATStuff = ats, classOpStuff = op_stuff})
= (tyvars, fundeps, sc_theta, sc_sels, ats, op_stuff)
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
\subsection[Class-instances]{Instance declarations for @Class@}
%* *
%************************************************************************
* *
************************************************************************
We compare @Classes@ by their keys (which include @Uniques@).
-}
\begin{code}
instance Eq Class where
c1 == c2 = classKey c1 == classKey c2
c1 /= c2 = classKey c1 /= classKey c2
......@@ -262,9 +258,7 @@ instance Ord Class where
c1 >= c2 = classKey c1 >= classKey c2
c1 > c2 = classKey c1 > classKey c2
compare c1 c2 = classKey c1 `compare` classKey c2
\end{code}
\begin{code}
instance Uniquable Class where
getUnique c = classKey c
......@@ -291,4 +285,3 @@ instance Data.Data Class where
toConstr _ = abstractConstr "Class"
gunfold _ _ = error "gunfold"
dataTypeOf _ = mkNoRepType "Class"
\end{code}
%
% (c) The University of Glasgow 2012
%
\begin{code}
-- (c) The University of Glasgow 2012
{-# LANGUAGE CPP, DeriveDataTypeable, GADTs, ScopedTypeVariables #-}
......@@ -16,7 +12,7 @@ module CoAxiom (
brListLength, brListNth, brListMap, brListFoldr, brListMapM,
brListFoldlM_, brListZipWith,
CoAxiom(..), CoAxBranch(..),
CoAxiom(..), CoAxBranch(..),
toBranchedAxiom, toUnbranchedAxiom,
coAxiomName, coAxiomArity, coAxiomBranches,
......@@ -30,7 +26,7 @@ module CoAxiom (
CoAxiomRule(..), Eqn,
BuiltInSynFamily(..), trivialBuiltInFamily
) where
) where
import {-# SOURCE #-} TypeRep ( Type )
import {-# SOURCE #-} TyCon ( TyCon )
......@@ -49,8 +45,7 @@ import qualified Data.Data as Data
#include "HsVersions.h"
\end{code}
{-
Note [Coercion axiom branches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In order to allow type family instance groups, an axiom needs to contain an
......@@ -120,13 +115,13 @@ longer needs to remain compatible with GHC 7.2.x, then please update this
code to use promoted types.
%************************************************************************
%* *
************************************************************************
* *
Branch lists
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
type BranchIndex = Int -- The index of the branch in the list of branches
-- Counting from zero
......@@ -205,13 +200,13 @@ brListZipWith f (NextBranch a ta) (NextBranch b tb) = f a b : brListZipWith f ta
instance Outputable a => Outputable (BranchList a br) where
ppr = ppr . fromBranchList
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Coercion axioms
%* *
%************************************************************************
* *
************************************************************************
Note [Storing compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -231,8 +226,8 @@ axiom as a whole, and they are computed only when the final axiom is built.
During serialization, the list is converted into a list of the indices
of the branches.
-}
\begin{code}
-- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
-- If you edit this type, you may need to update the GHC formalism
......@@ -331,15 +326,14 @@ coAxBranchIncomps = cab_incomps
placeHolderIncomps :: [CoAxBranch]
placeHolderIncomps = panic "placeHolderIncomps"
\end{code}
{-
Note [CoAxBranch type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the case of a CoAxBranch of an associated type-family instance,
In the case of a CoAxBranch of an associated type-family instance,
we use the *same* type variables (where possible) as the
enclosing class or instance. Consider
class C a b where
type F x b
type F x b
type F [y] b = ... -- Second param must be b
instance C Int [z] where
......@@ -347,7 +341,7 @@ enclosing class or instance. Consider
In the CoAxBranch in the instance decl (F Int [z]) we use the
same 'z', so that it's easy to check that that type is the same
as that in the instance header.
as that in the instance header.
Similarly in the CoAxBranch for the default decl for F in the
class decl, we use the same 'b' to make the same check easy.
......@@ -381,11 +375,11 @@ the newtype tycon; family axioms are all at role N.
Note [CoAxiom locations]
~~~~~~~~~~~~~~~~~~~~~~~~
The source location of a CoAxiom is stored in two places in the
datatype tree.
datatype tree.
* The first is in the location info buried in the Name of the
CoAxiom. This span includes all of the branches of a branched
CoAxiom.
* The second is in the cab_loc fields of the CoAxBranches.
* The second is in the cab_loc fields of the CoAxBranches.
In the case of a single branch, we can extract the source location of
the branch from the name of the CoAxiom. In other cases, we need an
......@@ -402,8 +396,8 @@ See also Note [Implicit TyThings] in HscTypes
That is, it does not have its own IfaceAxiom declaration in an
interface file; instead the CoAxiom is generated by type-checking
the newtype declaration
-}
\begin{code}
instance Eq (CoAxiom br) where
a == b = case (a `compare` b) of { EQ -> True; _ -> False }
a /= b = case (a `compare` b) of { EQ -> False; _ -> True }
......@@ -429,17 +423,16 @@ instance Typeable br => Data.Data (CoAxiom br) where
toConstr _ = abstractConstr "CoAxiom"
gunfold _ _ = error "gunfold"
dataTypeOf _ = mkNoRepType "CoAxiom"
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Roles
%* *
%************************************************************************
* *
************************************************************************
Roles are defined here to avoid circular dependencies.
\begin{code}
-}
-- See Note [Roles] in Coercion
-- defined here to avoid cyclic dependency with Coercion
......@@ -469,15 +462,13 @@ instance Binary Role where
3 -> return Phantom
_ -> panic ("get Role " ++ show tag)
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
CoAxiomRule
Rules for building Evidence
%* *
%************************************************************************
* *
************************************************************************
Conditional axioms. The general idea is that a `CoAxiomRule` looks like this:
......@@ -487,8 +478,8 @@ My intention is to reuse these for both (~) and (~#).
The short-term plan is to use this datatype to represent the type-nat axioms.
In the longer run, it may be good to unify this and `CoAxiom`,
as `CoAxiom` is the special case when there are no assumptions.
-}
\begin{code}
-- | A more explicit representation for `t1 ~ t2`.
type Eqn = Pair Type
......@@ -539,6 +530,3 @@ trivialBuiltInFamily = BuiltInSynFamily
, sfInteractTop = \_ _ -> []
, sfInteractInert = \_ _ _ _ -> []
}
\end{code}
%
% (c) The University of Glasgow 2006
%
-- (c) The University of Glasgow 2006
\begin{code}
{-# LANGUAGE CPP, DeriveDataTypeable #-}
-- | Module for (a) type kinds and (b) type coercions,
......@@ -110,15 +107,15 @@ import ListSetOps
import qualified Data.Data as Data hiding ( TyCon )
import Control.Arrow ( first )
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Coercions
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
......@@ -215,8 +212,8 @@ instance Binary LeftOrRight where
pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft (l,_) = l
pickLR CRight (_,r) = r
\end{code}
{-
Note [Refl invariant]
~~~~~~~~~~~~~~~~~~~~~
Coercions have the following invariant
......@@ -490,13 +487,13 @@ necessary for soundness, but this choice removes ambiguity.
The rules here also dictate what the parameters to mkTyConAppCo.
%************************************************************************
%* *
************************************************************************
* *
\subsection{Coercion variables}
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
coVarName :: CoVar -> Name
coVarName = varName
......@@ -515,10 +512,7 @@ isCoVarType ty -- Tests for t1 ~# t2, the unboxed equality
Just (tc,tys) -> (tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
&& tys `lengthAtLeast` 2
Nothing -> False
\end{code}
\begin{code}
tyCoVarsOfCo :: Coercion -> VarSet
-- Extracts type and coercion variables from a coercion
tyCoVarsOfCo (Refl _ ty) = tyVarsOfType ty
......@@ -575,15 +569,15 @@ coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
coercionSize (SubCo co) = 1 + coercionSize co
coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
+ sum (map coercionSize cos)
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Tidying coercions
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo env@(_, subst) co
= go co
......@@ -616,21 +610,21 @@ tidyCo env@(_, subst) co
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Pretty-printing coercions
%* *
%************************************************************************
* *
************************************************************************
@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.
-}
\begin{code}
instance Outputable Coercion where
ppr = pprCo
......@@ -718,9 +712,7 @@ ppr_forall_co p ty
(tvs, rho) = split1 [] ty
split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
split1 tvs ty = (reverse tvs, ty)
\end{code}
\begin{code}
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
= hang (ptext (sLit "axiom") <+> ppr ax <+> dcolon)
......@@ -746,15 +738,15 @@ pprCoAxBranchHdr ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name }) index
| otherwise
= ptext (sLit "in") <+>
quotes (ppr (nameModule name))
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Functions over Kinds
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
--
......@@ -827,13 +819,13 @@ isReflCo _ = False
isReflCo_maybe :: Coercion -> Maybe Type
isReflCo_maybe (Refl _ ty) = Just ty
isReflCo_maybe _ = Nothing
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Building coercions
%* *
%************************************************************************
* *
************************************************************************
Note [Role twiddling functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -883,8 +875,8 @@ So, that's why this function is exported from this module.
One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as appropriate?
I (Richard E.) have decided not to do this, because upgrading a role is bizarre and
a caller should have to ask for this behavior explicitly.
-}
\begin{code}
mkCoVarCo :: CoVar -> Coercion
-- cv :: s ~# t
mkCoVarCo cv
......@@ -1215,15 +1207,15 @@ mkCoCast c g
[_reflk, g1, g2] = decomposeCo 3 g
-- Remember, (~#) :: forall k. k -> k -> *
-- so it takes *three* arguments, not two
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Newtypes
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
-- | If @co :: T ts ~ rep_ty@ then:
--
-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
......@@ -1276,16 +1268,15 @@ topNormaliseNewType_maybe ty
| otherwise -- No progress
= Nothing
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Equality of coercions
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
-- | Determines syntactic equality of coercions
coreEqCoercion :: Coercion -> Coercion -> Bool
coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
......@@ -1334,15 +1325,15 @@ coreEqCoercion2 env (AxiomRuleCo a1 ts1 cs1) (AxiomRuleCo a2 ts2 cs2)
= a1 == a2 && all2 (eqTypeX env) ts1 ts2 && all2 (coreEqCoercion2 env) cs1 cs2
coreEqCoercion2 _ _ _ = False
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Substitution of coercions
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
-- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
-- doing a \"lifting\" substitution)
type CvSubstEnv = VarEnv Coercion
......@@ -1501,14 +1492,14 @@ lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
lookupCoVar :: CvSubst -> Var -> Maybe Coercion
lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
"Lifting" substitution
[(TyVar,Coercion)] -> Type -> Coercion
%* *
%************************************************************************
* *
************************************************************************
Note [Lifting coercions over types: liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1551,8 +1542,8 @@ Happily we can do this because we know that all kind coercions
subst_kind: LiftCoSubst -> Kind -> Kind
that expects a Refl coercion (or something equivalent to Refl)
when it looks up a kind variable.
-}
\begin{code}
-- ----------------------------------------------------
-- See Note [Lifting coercions over types: liftCoSubst]
-- ----------------------------------------------------
......@@ -1604,8 +1595,7 @@ ty_co_subst subst role ty
lift_phantom ty = mkUnivCo Phantom (liftCoSubstLeft subst ty)
(liftCoSubstRight subst ty)
\end{code}
{-
Note [liftCoSubstTyVar]
~~~~~~~~~~~~~~~~~~~~~~~
This function can fail (i.e., return Nothing) for two separate reasons:
......@@ -1622,8 +1612,8 @@ you find that liftCoSubst is doing weird things (like leaving out-of-scope
variables lying around), disable coercion optimization (bypassing matchAxiom)
and use downgradeRole instead of downgradeRole_maybe. The panic will then happen,
and you may learn something useful.
-}
\begin{code}
liftCoSubstTyVar :: LiftCoSubst -> Role -> TyVar -> Maybe Coercion
liftCoSubstTyVar (LCS _ cenv) r tv
= do { co <- lookupVarEnv cenv tv
......@@ -1680,9 +1670,7 @@ subst_kind subst@(LCS _ cenv) kind
pFst co_kind
| otherwise
= TyVarTy kv
\end{code}
\begin{code}
-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
-- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
-- That is, it matches a type against a coercion of the same
......@@ -1759,15 +1747,15 @@ pushRefl (Refl r (TyConApp tc tys))
= Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
pushRefl (Refl r (ForAllTy tv ty)) = Just (ForAllCo tv (Refl r ty))
pushRefl _ = Nothing
\end{code}
%************************************************************************
%* *
{-
************************************************************************
* *
Sequencing on coercions
%* *
%************************************************************************
* *
************************************************************************
-}
\begin{code}
seqCo :: Coercion -> ()
seqCo (Refl eq ty) = eq `seq` seqType ty
seqCo (TyConAppCo eq tc cos) = eq `seq` tc `seq` seqCos cos
......@@ -1787,14 +1775,13 @@ seqCo (AxiomRuleCo _ ts cs) = seqTypes ts `seq` seqCos cs
seqCos :: [Coercion] -> ()
seqCos [] = ()