From 2fbab1a0f1a017799e8f5130bdf1078060623f29 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Tue, 25 Mar 2008 17:02:18 +0000 Subject: [PATCH 1/1] Change syntax for newtypes in External Core The way that newtype declarations were printed in External Core files was incomplete, since there was no declaration for the coercion introduced by a newtype. For example, the Haskell source: newtype T a = MkT (a -> a) foo (MkT x) = x got printed out in External Core as (roughly): %newtype T a = a -> a; foo :: %forall t . T t -> t -> t = %cast (\ @ t -> a1 @ t) (%forall t . T t -> ZCCoT t); There is no declaration anywhere in the External Core program for :CoT, so that's bad. I changed the newtype decl syntax so as to include the declaration for the coercion axiom introduced by the newtype. Now, it looks like: %newtype T a ^ (ZCCoT :: ((T a) :=: (a -> a))) = a -> a; And an external typechecker could conceivably typecheck code that uses this. The major changes are to MkExternalCore and PprExternalCore (as well as ExternalCore, to change the External Core AST.) I also corrected some typos in comments in other files. Documentation and external tool changes to follow. --- compiler/coreSyn/CoreSyn.lhs | 2 +- compiler/coreSyn/ExternalCore.lhs | 5 ++++- compiler/coreSyn/MkExternalCore.lhs | 23 ++++++++++++++++++--- compiler/coreSyn/PprExternalCore.lhs | 37 ++++++++++++++++++++++------------ compiler/types/TyCon.lhs | 4 ++-- 5 files changed, 51 insertions(+), 20 deletions(-) diff --git a/compiler/coreSyn/CoreSyn.lhs b/compiler/coreSyn/CoreSyn.lhs index 7687317..9b67515 100644 --- a/compiler/coreSyn/CoreSyn.lhs +++ b/compiler/coreSyn/CoreSyn.lhs @@ -138,7 +138,7 @@ Invariant: The remaining cases are in order of increasing Invariant: The list of alternatives is ALWAYS EXHAUSTIVE, meaning that it covers all cases that can occur - An "exhausive" case does not necessarily mention all constructors: + An "exhaustive" case does not necessarily mention all constructors: data Foo = Red | Green | Blue ...case x of diff --git a/compiler/coreSyn/ExternalCore.lhs b/compiler/coreSyn/ExternalCore.lhs index 86a0d03..5754f84 100644 --- a/compiler/coreSyn/ExternalCore.lhs +++ b/compiler/coreSyn/ExternalCore.lhs @@ -10,12 +10,15 @@ data Module data Tdef = Data (Qual Tcon) [Tbind] [Cdef] - | Newtype (Qual Tcon) [Tbind] (Maybe Ty) + | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty) data Cdef = Constr Dcon [Tbind] [Ty] | GadtConstr Dcon Ty +-- Newtype coercion +type Axiom = (Qual Tcon, Kind) + data Vdefg = Rec [Vdef] | Nonrec Vdef diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs index c1e5217..1dc3b7e 100644 --- a/compiler/coreSyn/MkExternalCore.lhs +++ b/compiler/coreSyn/MkExternalCore.lhs @@ -61,9 +61,23 @@ collect_tdefs tcon tdefs | isAlgTyCon tcon = tdef: tdefs where tdef | isNewTyCon tcon = - C.Newtype (make_con_qid (tyConName tcon)) (map make_tbind tyvars) repclause + C.Newtype (qtc tcon) (map make_tbind tyvars) + (case newTyConCo_maybe tcon of + Just coercion -> (qtc coercion, + make_kind $ (uncurry mkCoKind) $ + case isCoercionTyCon_maybe coercion of + -- See Note [Newtype coercions] in + -- types/TyCon + Just (arity,coKindFun) -> coKindFun $ + map mkTyVarTy $ take arity tyvars + Nothing -> pprPanic ("MkExternalCore:\ + coercion tcon should have a kind fun") + (ppr tcon)) + Nothing -> pprPanic ("MkExternalCore: newtype tcon\ + should have a coercion: ") (ppr tcon)) + repclause | otherwise = - C.Data (make_con_qid (tyConName tcon)) (map make_tbind tyvars) (map make_cdef (tyConDataCons tcon)) + C.Data (qtc tcon) (map make_tbind tyvars) (map make_cdef (tyConDataCons tcon)) where repclause | isRecursiveTyCon tcon || isOpenTyCon tcon= Nothing | otherwise = Just (make_ty (repType rhs)) where (_, rhs) = newTyConRhs tcon @@ -71,6 +85,9 @@ collect_tdefs tcon tdefs collect_tdefs _ tdefs = tdefs +qtc :: TyCon -> C.Qual C.Tcon +qtc = make_con_qid . tyConName + make_cdef :: DataCon -> C.Cdef make_cdef dcon = C.Constr dcon_name existentials tys @@ -160,7 +177,7 @@ make_ty (TyVarTy tv) = C.Tvar (make_var_id (tyVarName tv)) make_ty (AppTy t1 t2) = C.Tapp (make_ty t1) (make_ty t2) make_ty (FunTy t1 t2) = make_ty (TyConApp funTyCon [t1,t2]) make_ty (ForAllTy tv t) = C.Tforall (make_tbind tv) (make_ty t) -make_ty (TyConApp tc ts) = foldl C.Tapp (C.Tcon (make_con_qid (tyConName tc))) +make_ty (TyConApp tc ts) = foldl C.Tapp (C.Tcon (qtc tc)) (map make_ty ts) -- Newtypes are treated just like any other type constructor; not expanded -- Reason: predTypeRep does substitution and, while substitution deals diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs index 6808144..22449df 100644 --- a/compiler/coreSyn/PprExternalCore.lhs +++ b/compiler/coreSyn/PprExternalCore.lhs @@ -5,11 +5,13 @@ \begin{code} module PprExternalCore () where -import Pretty import ExternalCore -import Char import Encoding +import Pretty +import Char + + instance Show Module where showsPrec _ m = shows (pmodule m) @@ -52,11 +54,20 @@ ptdef (Data tcon tbinds cdefs) = (text "%data" <+> pqname tcon <+> (hsep (map ptbind tbinds)) <+> char '=') $$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs))))) -ptdef (Newtype tcon tbinds rep ) = - text "%newtype" <+> pqname tcon <+> (hsep (map ptbind tbinds)) <+> repclause - where repclause = case rep of - Just ty -> char '=' <+> pty ty - Nothing -> empty +ptdef (Newtype tcon tbinds (coercion,k) rep) = +-- Here we take apart the newtype tycon in order to get the newtype coercion, +-- which needs to be represented in the External Core file because it's not +-- straightforward to derive its definition from the newtype declaration alone. +-- At the same time, we need the newtype decl to declare the tycon itself. +-- Sigh. + text "%newtype" <+> pqname tcon <+> (hsep (map ptbind tbinds)) + <+> axiomclause <+> repclause + where axiomclause = char '^' <+> parens (pqname coercion <+> text "::" + <+> pkind k) + repclause = case rep of + Just ty -> char '=' <+> pty ty + Nothing -> empty + pcdef :: Cdef -> Doc pcdef (Constr dcon tbinds tys) = @@ -84,7 +95,8 @@ pakind (Kopen) = char '?' pakind k = parens (pkind k) pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2) -pkind (Keq t1 t2) = parens (pty t1 <> text ":=:" <> pty t2) +pkind (Keq t1 t2) = parens (parens (pty t1) <+> text ":=:" <+> + parens (pty t2)) pkind k = pakind k paty, pbty, pty :: Ty -> Doc @@ -113,13 +125,12 @@ pvdefg (Rec vdefs) = text "%rec" $$ braces (indent (vcat (punctuate (char ';') ( pvdefg (Nonrec vdef) = pvdef vdef pvdef :: Vdef -> Doc -pvdef (l,v,t,e) = sep [plocal l <+> pname v <+> text "::" <+> pty t <+> char '=', +-- note: at one point every vdef was getting printed out as "local". +-- I think that's manifestly wrong. Right now, the "%local" keyword +-- is never used. +pvdef (_l,v,t,e) = sep [pname v <+> text "::" <+> pty t <+> char '=', indent (pexp e)] -plocal :: Bool -> Doc -plocal True = text "%local" -plocal False = empty - paexp, pfexp, pexp :: Exp -> Doc paexp (Var x) = pqname x paexp (Dcon x) = pqname x diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index ddcb665..e6366be 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -186,7 +186,7 @@ data TyCon tyConName :: Name, tyConArity :: Arity, coKindFun :: [Type] -> (Type,Type) - } -- INVARAINT: coKindFun is always applied to exactly 'arity' args + } -- INVARIANT: coKindFun is always applied to exactly 'arity' args -- E.g. for trans (c1 :: ta=tb) (c2 :: tb=tc), the coKindFun returns -- the kind as a pair of types: (ta,tc) @@ -372,7 +372,7 @@ Source code: w2 :: Foo T w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x) -After desugaring, and discading the data constructors for the newtypes, +After desugaring, and discarding the data constructors for the newtypes, we get: w2 :: Foo T w2 = w1 -- 1.7.10.4