[Agda] Agda's mixfix parser

[Nils Anders Danielsson]

On 2010-05-26 18:45, Stefan Monnier wrote:
> While reading "Parsing Mixfix Operators"
> http://www.cs.nott.ac.uk/~nad/publications/danielsson-aim8-talk.handout.pdf
> I wondered: why use a memoizing backtracking implementation rather than
> something based on Floyd's operator precedence parsers?

Two reasons:

1) Using parser combinators we can write down the intended grammar
    directly (more or less).

2) Our grammars are not in general operator-precedence grammars. We
    allow the same name part to be used in several operators, or multiple
    times in the same operator.

Ulf and I motivate our choices further in "Parsing Mixfix Operators":

   http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.html

Unfortunately I have not yet gotten around to changing Agda to use the
approach to precedences discussed in that paper. (In fact, for
modularity reasons I am now leaning towards accepting cyclic precedence
graphs.)

-- 
/NAD