<html><head><style>body{font-family:Helvetica,Arial;font-size:13px}</style></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">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. </div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div class="" id="bloop_sign_1390599075021985024"><span style="font-family:helvetica,arial;font-size:13px"></span></div><p style="color:#A0A0A8;">On 25 January 2014 at 7:51:38 am, Aaron Stump (<a href="mailto://aaron-stump@uiowa.edu">aaron-stump@uiowa.edu</a>) wrote:</p> <blockquote type="cite" class="clean_bq"><span><div><div>Dear Agda list,
<br>
<br>Over winter break, I wrote a parser generator which targets Agda! Yes,
<br>it is exciting, I know. It's not quite ready for release, partly
<br>because I am getting really slow checking times for some of the
<br>generated files. Attached is a standalone Agda file of 1500 lines which
<br>takes about 30 seconds to check on my machine, with the 2.3.2 release of
<br>Agda. This was generated from a tiny expression grammar, and I have
<br>found that Agda is taking too long and way too much memory (many GB) on
<br>bigger generated files from more interesting grammars.
<br>
<br>I talked to Nils Anders at PLPV, and he was speculating that perhaps the
<br>rather large number of constructors in a datatype representing a set of
<br>states (grep for s183) could perhaps be exposing a quadratic-time
<br>algorithm somewhere in the implementation. So I am sending in this
<br>file, in case there is such a bug, or for any advice on how to speed up
<br>checking time. The "len-dec-rewrite" function towards the end of the
<br>file will induce some reduction; in particular, normalizing some calls
<br>to the list length function on some particular lists (of length maybe 12
<br>or 15 max). Otherwise, it's almost just simply typed, so one would hope
<br>it would check much more quickly.
<br>
<br>Thanks,
<br>Aaron
<br><hr> <div>- exampleSlow.agda, 118 KB</div> _______________________________________________
<br>Agda mailing list
<br>Agda@lists.chalmers.se
<br>https://lists.chalmers.se/mailman/listinfo/agda
<br></div></div></span></blockquote></body></html>