Change syntax for newtypes in External Core
authorTim Chevalier <chevalier@alum.wellesley.edu>
Tue, 25 Mar 2008 17:02:18 +0000 (17:02 +0000)
committerTim Chevalier <chevalier@alum.wellesley.edu>
Tue, 25 Mar 2008 17:02:18 +0000 (17:02 +0000)
commit2fbab1a0f1a017799e8f5130bdf1078060623f29
tree5816db50efaa42caba005b6f351c6afa934036cd
parent68ed90d8b2f31f9bcae7b869413819eb8fa0aa40
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
compiler/coreSyn/ExternalCore.lhs
compiler/coreSyn/MkExternalCore.lhs
compiler/coreSyn/PprExternalCore.lhs
compiler/types/TyCon.lhs