[Agda] slow file with many constructors

[Nils Anders Danielsson]

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:

  * eps: Most of the time is spent type-checking individual clauses.

  * 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.

-- 
/NAD