[Agda-dev] MAlonzo / Treeless syntax / SizeUniv

[Philipp Hausmann]

>> 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 guess this also takes care of the problematic catch-all-clauses?
Yes.
>> 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?
>
> I am fine with either solution.  I am not very firm with
> primitives/builtins and what is their difference.  SizeUniv only
> occurs in types, thus, strictly speaking, does not need a compiled
> representation, but nothing speaks against adding one.

I agree that the SizeUniv builtin will never be evaluated because it can
only occur in types, but it may still be referenced in function bodies.
For example:

f : SizeUniv
f = SizeUniv

If we just drop SizeUniv during compilation, all references to SizeUniv
need to be fixed/changed to unit. So I decided that it is easier to just
keep the dummy definition
and extend it with a CompiledClause. The definition is very simple anyway.


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/20150705/4f3ee6ae/signature.bin