<br><br><div class="gmail_quote">On Mon, Aug 15, 2011 at 12:44 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se">nad@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On 2011-08-14 23:45, Arseniy Alekseyev wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'm running the code from emacs' "Evaluate term to normal form"<br>
command.<br>
</blockquote>
<br></div>
This evaluator does not perform this kind of optimisation. Neither does<br>
the Haskell backend. I'm not sure how well the Epic backend handles this<br>
code. Daniel and Olle, have you tested this?<br>
<br>
-- <br><font color="#888888">
/NAD<br>
</font></blockquote></div><br>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. <br>
<br>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.<br><br>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. <br>
<br>/Daniel<br>