[Agda] slow file with many constructors

[Liam O'Connor]

If the large number of constructors prove to be the source of the problem and it’s not easy to fix, you might have better luck using the Fin type to represent your states? I don’t know if it would be more efficient, but it’s an alternative representation. 

On 25 January 2014 at 7:51:38 am, Aaron Stump (aaron-stump at uiowa.edu) wrote:

Dear Agda list,  

Over winter break, I wrote a parser generator which targets Agda! Yes,  
it is exciting, I know. It's not quite ready for release, partly  
because I am getting really slow checking times for some of the  
generated files. Attached is a standalone Agda file of 1500 lines which  
takes about 30 seconds to check on my machine, with the 2.3.2 release of  
Agda. This was generated from a tiny expression grammar, and I have  
found that Agda is taking too long and way too much memory (many GB) on  
bigger generated files from more interesting grammars.  

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. So I am sending in this  
file, in case there is such a bug, or for any advice on how to speed up  
checking time. The "len-dec-rewrite" function towards the end of the  
file will induce some reduction; in particular, normalizing some calls  
to the list length function on some particular lists (of length maybe 12  
or 15 max). Otherwise, it's almost just simply typed, so one would hope  
it would check much more quickly.  

Thanks,  
Aaron  
- exampleSlow.agda, 118 KB
_______________________________________________  
Agda mailing list  
Agda at lists.chalmers.se  
https://lists.chalmers.se/mailman/listinfo/agda  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140125/2c1665c9/attachment.html