[Agda] slow file with many constructors

[Andreas Abel]

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/