Commit 2fbab1a0 authored by chevalier@alum.wellesley.edu's avatar chevalier@alum.wellesley.edu
Browse files

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.
parent 68ed90d8
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
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