[Agda] slow file with many constructors

[Andreas Abel]

Aaron, please do file an issue (google: agda issues) with a reproducible 
test case for the performance problem you experienced.  To attract some 
attention from the developer community to this bug.

Thanks,
Andreas


On 27.01.2014 16:28, Aaron Stump wrote:
> 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
>>
>>
>


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