[Agda] Efficient numeric computations in Agda

[Daniel Gustafsson]

On Mon, Aug 15, 2011 at 12:44 AM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> On 2011-08-14 23:45, Arseniy Alekseyev wrote:
>
>> I'm running the code from emacs' "Evaluate term to normal form"
>> command.
>>
>
> This evaluator does not perform this kind of optimisation. Neither does
> the Haskell backend. I'm not sure how well the Epic backend handles this
> code. Daniel and Olle, have you tested this?
>
> --
> /NAD
>

I haven't tested this code due to my agda version and library version have
gone out of sync so are getting annoying error messages but will look into
that later. But the Epic-backend should compile the lem-functions into
boring (but fast) constant functions.

Now the problem is that Epic backend with this optimisation is not yet in
the darcs tree since we require a slightly patched Epic version. This remind
me to annoy Edwin about that.

Regarding the optimisations for well-founded recursion: I don't really
follow how it all works, so can't really say if it would compile to
something good.

/Daniel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110815/943f2a98/attachment.html