[Agda] hello, I've done something terrible...

[Nils Anders Danielsson]

On 2011-07-26 06:58, Jeremy Shaw wrote:
> The biggest known flaw is that the many1 parser does not prove
> termination, so I had to enable --no-termination-check. That is
> probably the second thing I will look at.

I have not studied your code in detail, but my guess is that many1 p can
fail to terminate if p can succeed without consuming any input. I
discuss total implementations of many and many1 in the following paper
(Sections 3.1 and 4.4):

   Total Parser Combinators
   http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html

-- 
/NAD