GitLab

commutableOp seems to be unused, so we're no 100% there yet.

- In a previous patch I broke the printing of fully-applied arrow
types (e.g., "a -> b" was "(ghczmprim:GHCziPrim a b)") by z-encoding
package names and not updating the primitive module name as defined in
External Core accordingly. Fixed. (Mega sigh...)

- Make newtype decls print slightly more readably.

The External Core printer was printing out rational literals of the
form: 
2.0e-2
when the External Core grammar doesn't allow this. (This
bug has apparently been there since the beginning...)

It's now printing rationals in the same form that (show (r::Rational))
does. This requires a parser change as well (soon to come.)

Two changes that make the ext-core code uglier but the parser easier:

- Prefix qualified names with "^" so that we can more easily
distinguish a qualified name:
   ^a:Foo.Bar.quux 
from an unqualified name:
   a

- z-encode package names ("ghc-prim" was the culprit.)

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.