Re: [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance status / community fork (again)]

[Alain Frisch <alain@frisch.fr>]

On 12/11/2011 12:34 AM, Gabriel Scherer wrote:
> the Coq
> team which has user-defined notations using Camlp4 and, huh, I really
> don't want to know the details

My understanding (please correct me if I'm wrong) is that Coq uses 
camlp{4,5} only as an extensible parser library in order to parse its 
own language (which can be extended with user-defined notations). In 
particular, Coq does not use the following camlp{4,5} features:

   - the revised OCaml syntax
   - the alternative representation of OCaml AST
   - the Camlp4 grammar definitions for OCaml syntax(es)
   - quotations/antiquotations to produce fragments of the OCaml AST
   - OCaml syntax extensions to define grammar entries
   - custom OCaml syntax extension for the Coq source code itself
     (or maybe only very simple one, like macro/conditional compilation?)

I wonder how much energy it would take to create a stand-alone 
extensible parser library, implemented in pure OCaml (normal syntax), 
and following a similar API and semantics as camlp{4,5}, on which Coq 
parsing could be built. The same library could be used as a foundation 
for future versions of camlp{4,5}.  It would be a simple library, with 
no external dependency (in particular, no dependency to the OCaml 
internals), and very little maintenance burden.

My guess is: this would not take so much energy. After all, the 
representation of extensible grammars and the top-down parsing 
technology are not so complex. But I would be interested to hear from 
people who know Coq and camlp{4,5} better.


-- Alain