<div dir="ltr">I've grepped the code a bit and it seems that the speedup was mainly because abstract definitions are skipped by the termination checker [1], hence avoiding the instantiation of metavariables.<br><div class="gmail_extra">
<div class="gmail_extra"><br></div><div class="gmail_extra">In my case a syntax for non-recursive definitions would solve the slowdown, but it seems like a better solution could be to teach the termination checker how to share work between different instantiations of the same metavariable, if that's possible.</div>
<div class="gmail_extra"><br></div><div class="gmail_extra" style>The code: <a href="https://github.com/Saizan/categories/blob/abstract/Categories/Adjunction.agda">https://github.com/Saizan/categories/blob/abstract/Categories/Adjunction.agda</a></div>
<div class="gmail_extra">[1] <a href="https://code.google.com/p/agda/issues/detail?id=847">https://code.google.com/p/agda/issues/detail?id=847</a></div><div class="gmail_extra"><br></div><div class="gmail_extra"><br></div>
<div class="gmail_quote">On Mon, May 13, 2013 at 1:45 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Hi Andrea,<br>
<br>
"abstract" means that this definition is only expanded when checking other "abstract" definitions.<br>
<br>
Irrelevant arguments are not compared during equality checking, however, they might still be computed for other reasons, e.g. to determine their precise set of free variables. Substitution also has to traverse irrelevant arguments, due to the lack of explicit substitutions in the Agda engine.<br>
<br>
The implementation of these features is scattered all over the Agda engine (TypeChecking.*), you might wanna grep for "AbstractMode" and "releva" to get to interesting source locations.<br>
<br>
Cheers,<br>
Andreas<div><div class="h5"><br>
<br>
On 12.05.2013 12:00, Andrea Vezzosi wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div><div class="h5">
Hi,<br>
<br>
I've noticed some very promising speedups by making definitions abstract<br>
in addition to irrelevant and I'd like to understand why.<br>
<br>
Skimming the code I couldn't figure out where the main pieces of the<br>
implementation of these features are, is there a commentary on how they<br>
are implemented? And what work does abstract save on top of irrelevance?<br>
<br>
<br>
Thanks,<br>
Andrea<br>
<br>
<br>
<br></div></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span class=""><font color="#888888">
</font></span></blockquote><span class=""><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div></div>