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
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
