[Agda-dev] MAlonzo / Treeless syntax / SizeUniv

[Andreas Abel]

Thanks, Philipp!  (See more below.)

On 03.07.2015 14:33, Philipp Hausmann wrote:
> 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?

> 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?

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.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/