[Agda] Compiler internals for projection functions

[Ulf Norell]

On Fri, Sep 23, 2011 at 3:15 AM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

> Thanks for the pointer.
>
> Is there any way to recreate the dropped arguments? I don't fancy having to
> document in the FFI interface that the compliler may sometimes drop
> arguments based on projection analysis.


The reason why they are dropped is that (a) they're not used and (b) that
they can be recovered from the type of the first proper argument. An
optimised js implementation of the function shouldn't really look at these
arguments so it should be safe to just insert dummy values for the dropped
arguments.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110923/ea0ebae1/attachment-0001.html