[Agda] Implementation of abstract vs. irrelevance
sanzhiyan at gmail.com
Thu May 16 22:13:37 CEST 2013
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?
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.
On Mon, May 13, 2013 at 9:53 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> I've grepped the code a bit and it seems that the speedup was mainly
> because abstract definitions are skipped by the termination checker ,
> hence avoiding the instantiation of metavariables.
> 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.
> The code:
>  https://code.google.com/p/agda/issues/detail?id=847
> On Mon, May 13, 2013 at 1:45 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:
>> Hi Andrea,
>> "abstract" means that this definition is only expanded when checking
>> other "abstract" definitions.
>> 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
>> 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.
>> On 12.05.2013 12:00, Andrea Vezzosi wrote:
>>> I've noticed some very promising speedups by making definitions abstract
>>> in addition to irrelevant and I'd like to understand why.
>>> Skimming the code I couldn't figure out where the main pieces of the
>>> implementation of these features are, is there a commentary on how they
>>> are implemented? And what work does abstract save on top of irrelevance?
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>> Andreas Abel <>< Du bist der geliebte Mensch.
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda