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

["Stéphane Glondu" <steph@glondu.net>]

Le 11/12/2011 14:27, Alain Frisch a écrit :
> 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:
> 
>  [1] the revised OCaml syntax
>  [2] the alternative representation of OCaml AST
>  [3] the Camlp4 grammar definitions for OCaml syntax(es)
>  [4] quotations/antiquotations to produce fragments of the OCaml AST
>  [5] OCaml syntax extensions to define grammar entries
>  [6] custom OCaml syntax extension for the Coq source code itself
>     (or maybe only very simple one, like macro/conditional compilation?)

As far as I know, Coq uses:

  [1,2,3] not at all
  [4] a bit (e.g. tactics/tauto.ml4)
  [5] a lot (e.g. most of *.ml4 files)
  [6] for macros and conditional compilation indeed

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

I've heard of some attempts to port Coq to dypgen, but since no public
announcement was made, I guess this is quite difficult...

Are there other such libraries? It's not really Coq's business to create
a new one...


Cheers,

-- 
Stéphane