[Agda] Implementation of abstract vs. irrelevance

[Andrea Vezzosi]

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.

Cheers,
  Andrea


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 [1],
> 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://github.com/Saizan/categories/blob/abstract/Categories/Adjunction.agda
> [1] 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
>> engine.
>>
>> 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.
>>
>> Cheers,
>> Andreas
>>
>>
>> On 12.05.2013 12:00, Andrea Vezzosi wrote:
>>
>>> Hi,
>>>
>>> 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?
>>>
>>>
>>> Thanks,
>>>     Andrea
>>>
>>>
>>>
>>> ______________________________**_________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>>
>>>
>>
>> --
>> 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...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130516/4e97c580/attachment.html