[Agda] slow file with many constructors

[Gabriel Scherer]

A technique I've seen used in coq-land (where desugaring of
simultaneous pattern-matching on two values can lead to quadratic
blowup, typically in inequality-proofs) is to "hash" your values into
integers, and then map/compare those integer keys. This is described
for example in this blog post (
http://gallium.inria.fr/blog/verifying-a-parser-for-a-c-compiler/ ),
section "Using Int31".

On Mon, Jan 27, 2014 at 4:28 PM, Aaron Stump <aaron-stump at uiowa.edu> 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
>>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda