[Agda] slow file with many constructors

[Aaron Stump]

Ok, I have done this now.
Cheers,
Aaron

On Mon 27 Jan 2014 05:43:03 PM CST, Andreas Abel wrote:
> 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
>>>
>>>
>>
>
>