From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBBDRUIi015365
	for <caml-list@sympa-roc.inria.fr>; Sun, 11 Dec 2011 14:27:30 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ao0CAAKv5E7UGyoDlGdsb2JhbABDqDGCPyIBAQEBBwILCQkUAyKBcgEBBThAARALGAkWDwkDAgECAUUGDQEHAQEQh3a0K4ttBJRxhUuMXQ
X-IronPort-AV: E=Sophos;i="4.71,335,1320620400"; 
   d="scan'208";a="122913378"
Received: from smtp3-g21.free.fr ([212.27.42.3])
  by mail4-smtp-sop.national.inria.fr with ESMTP; 11 Dec 2011 14:27:28 +0100
Received: from [192.168.0.10] (unknown [78.192.0.38])
	by smtp3-g21.free.fr (Postfix) with ESMTP id 5FC8FA6597;
	Sun, 11 Dec 2011 14:27:21 +0100 (CET)
Message-ID: <4EE4AFB8.5040509@frisch.fr>
Date: Sun, 11 Dec 2011 14:27:20 +0100
From: Alain Frisch <alain@frisch.fr>
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:8.0) Gecko/20111105 Thunderbird/8.0
MIME-Version: 1.0
To: Gabriel Scherer <gabriel.scherer@gmail.com>
CC: Wojciech Meyer <wojciech.meyer@googlemail.com>,
        =?ISO-8859-1?Q?J=E9r=E9?=
 =?ISO-8859-1?Q?mie_Dimino?= <jeremie@dimino.org>,
        caml-list@inria.fr
References: <55531934-37A5-4CC5-AB67-20CE4CCE8269@googlemail.com> <4EE37070.4010702@inria.fr> <1323541702.32136.8.camel@aurora> <wfhb18wa1c.fsf@gmail.com> <wf1uscw8cu.fsf@gmail.com> <1323550544.32136.19.camel@aurora> <wfmxb0umuc.fsf_-_@gmail.com> <CAPFanBFm9kdeo5XoeN9tYuMssU5vri0fp8SN1BQWBLdK1DzNqQ@mail.gmail.com>
In-Reply-To: <CAPFanBFm9kdeo5XoeN9tYuMssU5vri0fp8SN1BQWBLdK1DzNqQ@mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance
 status / community fork (again)]

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