<div dir="ltr">It seems I was completely wrong when blaming instantiation, the vast majority of the time is spent pretty-printing function calls to populate the CallInfo in Calls, maybe there's a way to store the call itself and the needed context in Calls and only pretty-print if there's a need, for error messages I guess, later?<div>
<br></div><div style>I've also implemented a simple traversal that checks if there's circularity in a mutual block and skips termination checking if there isn't, it seems to get back almost the original speedup for Adjunction.agda, if typechecking the std-lib doesn't get slower I will prepare a patch.</div>
<div style><br></div><div style>Cheers,</div><div style> Andrea</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, May 13, 2013 at 9:53 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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">The code: <a href="https://github.com/Saizan/categories/blob/abstract/Categories/Adjunction.agda" target="_blank">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" target="_blank">https://code.google.com/p/agda/issues/detail?id=847</a></div><div><div class="h5"><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><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>
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><font color="#888888">
</font></span></blockquote><span><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></div></div>
</blockquote></div><br></div>