[Agda] Compiler internals for projection functions

[Alan Jeffrey]

I have now pushed a compiler patch to add dummy parameters / arguments 
to projection functions in the JS back end.

A.

On 09/23/2011 08:33 AM, Jeffrey, Alan S A (Alan) wrote:
> Ah, this is related to the recent performance gains. I'd say that's a
> pretty benefit for a minor bump in the road for the JS FFI. I'll try to
> come up with a form of words which describes when arguments may end up
> with dummy values.
>
> A.
>
> On 09/23/2011 03:34 AM, Ulf Norell wrote:
>>
>> On Fri, Sep 23, 2011 at 10:21 AM, Vincent Siles
>> <vincent.siles at ens-lyon.org<mailto:vincent.siles at ens-lyon.org>>  wrote:
>>
>>      Is this related to the performance issue  you were talking about a
>>      few week ago
>>      (related to using Sigma instead of build-in records) ?
>>
>>
>> Yes. With this optimisation using Sigma (record or datatype version) to
>> define the
>> type of categories doesn't make the type checker explode defining the
>> projection functions.
>>
>> / Ulf