[Agda] Implementation of abstract vs. irrelevance

[Andreas Abel]

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
>


-- 
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/