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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> 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.

You are suggesting a dynamic parser tool. This is already available as
the dypgen tool:
  http://dypgen.free.fr/

I suspect adapting Coq to such a tool would require considerable work,
because the devil is in the details and they really need backward
compatibility. I'm already impressed they managed to support both
camlp4 and camlp5.

On Sun, Dec 11, 2011 at 2:27 PM, Alain Frisch <alain@frisch.fr> wrote:
> 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