[Agda] slow file with many constructors

[Aaron Stump]

Thanks a lot for investigating this.  I am guessing that in the short 
term, I could work around some of these issues simply by trying to 
avoid having a lot of clauses, and instead do more work on right-hand 
sides.  Naturally, I'd prefer it if Agda did this work for me :-), but 
for now this could help.

Cheers,
Aaron

On Mon 27 Jan 2014 03:28:34 AM CST, Andreas Abel wrote:
> On 26.01.2014 00:14, Nils Anders Danielsson wrote:
>> On 2014-01-24 12:51, Aaron Stump wrote:
>>> I talked to Nils Anders at PLPV, and he was speculating that perhaps
>>> the rather large number of constructors in a datatype representing a
>>> set of states (grep for s183) could perhaps be exposing a
>>> quadratic-time algorithm somewhere in the implementation.
>>
>> Interactive highlighting indicates that most of the time is spent in eps
>> and len-dec-rewrite:
>
> Thanks for looking into this!
>
>>   * eps: Most of the time is spent type-checking individual clauses.
>
> There is definitely a source for quadratic behavior here:  Each clause
> is checked individually, starting with variables for the function
> arguments and splitting them according to the patterns of this clause.
> If you have a datatype with n cases, and consequently a function with
> n clauses, Agda does n splits generating n reference clauses (lhss)
> each time.
>
>>   * len-dec-rewrite: A majority of the time is spent doing something
>>     after the individual clauses have been type-checked. A bit of
>>     detective work indicates that most of this work is done by the
>> clause
>>     compiler, which turns the list of clauses into a case tree.
>>
>> Perhaps the clause compiler can be optimised.
>
> I'd think so.  First time I looked at it, it seemed to be
> quick-and-dirty code...
>
> Cheers,
> Andreas
>
>