[Agda-dev] MAlonzo / Treeless syntax / SizeUniv

[Philipp Hausmann]

Hi,

I started working on porting the MAlonzo backend to the new Treeless
intermediate syntax. This should allow us
to get rid of the clauses/compiled clauses code in MAlonzo itself, as
that part will be handled in the translation from Internal to Treeless
syntax.
I got most things working, my current version is here:
https://github.com/agda/agda/compare/master...phile314:malonzo-treeless

I'm going to keep it in my own branch until it has feature-parity with
the old-code, but I think
that shouldn't take much longer. Does anybody object to merging this
when it's finished?

---

The main missing thing is compilation of the SIZEUNIV builtin. At the
moment, the SIZEUNIV builtin is defined as a function with a clause, but
no compiled clauses:
https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Rules/Builtin.hs#L509-514
I think SIZEUNIV should be changed to either have compiled clauses as
well, or to be a primitive. Any thoughts?

Cheers,
Philipp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
Url : http://lists.chalmers.se/pipermail/agda-dev/attachments/20150703/6d4d7cc8/signature.bin