From: Tim Chevalier Date: Tue, 25 Mar 2008 17:02:18 +0000 (+0000) Subject: Change syntax for newtypes in External Core X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=2fbab1a0f1a017799e8f5130bdf1078060623f29 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. --- 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