The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thanks -- at this point, I'm rather convinced that:

http://en.wikipedia.org/wiki/Parsec + http://en.wikipedia.org/wiki/Shunting-yard_algorithm will suffice.

On Mon, Aug 5, 2013 at 5:20 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

I think Coq use's OCaml's camlp4/camlp5 for parsing.  Perhaps searching for this will be fruitful.

Note also that the top-level grammar is fixed before parsing, and that Coq does not deal well with, e.g., re-defining '.' (period).  So you cannot, I believe change which things are parsed as Notations.  Additionally, Coq cannot reverse changes to the parser (i.e., "Undo" doesn't work so well after "Reserved Notation").  So parsing in Coq is by no means ideal.  (I think, though, that even in Haskell, the grammar might not be fixed, as fixity declarations can change the precedence of operators.) 

-Jason

On Monday, August 5, 2013, gallais wrote:

Hi,

I don't know about Coq's counterpart of this but this is, I believe, the
standard reference for the parsing of agda's mixfix operators. Notations
may be somewhat related.

http://www.cse.chalmers.se/~nad/publications/danielsson-norell-mixfix.html

Cheers,
--
gallais


On 5 August 2013 22:53, t x <txrev319 AT gmail.com> wrote:
> Hi,
>
>   I'm currently (past few days, trying to) writing a parser for Coq. With
> the exception of Notation (for which I hard coded the common cases I use)
> and proper handling of precedence (i.e. "1 + 2 * 3" is incorrectly parsed as
> "(1+2)*3"), everything appears to work.
>
>   Courses I had previously take in compilers / automata theory tend to
> assume that the grammar is fixed before the program is compiled. Notation
> breaks this assumption. Can someone explain to me (or point me at a paper)
> on the theoretical foundations behind notation and how it's implemented?
>
> Thanks!