Tue Mar 25 10:02:18 PDT 2008 Tim Chevalier <[EMAIL PROTECTED]>
* 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.
M ./compiler/coreSyn/CoreSyn.lhs -1 +1
M ./compiler/coreSyn/ExternalCore.lhs -1 +4
M ./compiler/coreSyn/MkExternalCore.lhs -3 +20
M ./compiler/coreSyn/PprExternalCore.lhs -13 +24
M ./compiler/types/TyCon.lhs -2 +2
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
