Total Parser Combinators - Agdarsec

Problem

Currently all our parsers terminate, but this is done by a check at runtime:

https://github.com/steve-chavez/CParseC/blob/2ec0da5107febbef3b1ffce02f842a24a8542a5d/cparsec.h#L164-L166

It'd be much better for this to not be possible at compile time

Research

I've found this paper on agdarsec (https://github.com/gallais/agdarsec/). A parser combinator library for Agda, which has "total parser combinators", that is parsers combinators that always terminate.

To do that it adds constraints and tradeoffs:

• For a parser to be successful, it must consume some of its input
• Failure is implemented by always returning the empty result list.
• Several combinators are incompatible, like many, sepby, etc. Essentially all the ones that succeed on zero or more occurrences.
• eof is not representable by agdarsec
• There is no pure parser (since it succeeds but doesn't have to consume input)

Some breaking changes might be acceptable but one thing I'm not sure is it's expressive enough. I haven't found many examples.

Start with the runtime termination check in cparsec.h at lines 164–166, then read the linked agdarsec paper and compare its constraints with the existing parser combinators. Determine whether a total design remains expressive enough, including the listed incompatible combinators and breaking changes. Done means documenting a concrete design direction and its tradeoffs.