From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBBDgMFG016128
	for <caml-list@sympa-roc.inria.fr>; Sun, 11 Dec 2011 14:42:22 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AmQCAAyy5E7UGyoDlGdsb2JhbABDqnAiAQEBAQcCCwkJFAMigXIBAQU4QRALGAklDwJGBg0BBwEBEId2tC+LbQSUcYVLjF0
X-IronPort-AV: E=Sophos;i="4.71,335,1320620400"; 
   d="scan'208";a="134907411"
Received: from smtp3-g21.free.fr ([212.27.42.3])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 11 Dec 2011 14:42:16 +0100
Received: from [192.168.0.10] (unknown [78.192.0.38])
	by smtp3-g21.free.fr (Postfix) with ESMTP id 87D4EA659D;
	Sun, 11 Dec 2011 14:42:09 +0100 (CET)
Message-ID: <4EE4B330.70403@frisch.fr>
Date: Sun, 11 Dec 2011 14:42:08 +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: 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> <4EE4AFB8.5040509@frisch.fr> <CAPFanBFnjHNuTOARDFqsgMmvF+3x_3xymg357P65vDChde3=pA@mail.gmail.com>
In-Reply-To: <CAPFanBFnjHNuTOARDFqsgMmvF+3x_3xymg357P65vDChde3=pA@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 2:35 PM, Gabriel Scherer wrote:
>> 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.

Agreed. It would probably be a lot easier to adapt Coq to work with a 
(new) parsing library that uses the same parsing algorithms as Camlp4.


-- Alain