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 pBBDa1vV015863 for ; Sun, 11 Dec 2011 14:36:01 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvYAAHyw5E5KfVI0imdsb2JhbABDqmgIIgEBAQoJDQcSBiGBcgEBAQMBEgIsARsdAQMBCwYFCw0uIgERAQUBHAYTFA6HZpgvCotkgmuDcj2IcQIFDIthBJRxjXE9g3o X-IronPort-AV: E=Sophos;i="4.71,335,1320620400"; d="scan'208";a="134907105" Received: from mail-ww0-f52.google.com ([74.125.82.52]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-MD5; 11 Dec 2011 14:35:56 +0100 Received: by wgbdr12 with SMTP id dr12so11186428wgb.9 for ; Sun, 11 Dec 2011 05:35:56 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=rPHJ/IyehPCLU+Q/SPedzdliQV7RoR0IXfDmdVxE6QI=; b=BFLYzMZ6brYM/mnw9+3wlYXCix2r144zChLlbGaxkkA5y1ekWKv1Z9fVkWTdodixvO mBmeEd+rtOWt4vVEBYN9YfU/b1G6cSHnCN/39+ONoYaslwNdCoZzzUSEGt1kDhjqNRxv KwqDFoX2OMrdEIavZhxvTSI1/8OeTcywiARAc= Received: by 10.227.207.67 with SMTP id fx3mr12095250wbb.0.1323610556198; Sun, 11 Dec 2011 05:35:56 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.43.4 with HTTP; Sun, 11 Dec 2011 05:35:35 -0800 (PST) In-Reply-To: <4EE4AFB8.5040509@frisch.fr> References: <55531934-37A5-4CC5-AB67-20CE4CCE8269@googlemail.com> <4EE37070.4010702@inria.fr> <1323541702.32136.8.camel@aurora> <1323550544.32136.19.camel@aurora> <4EE4AFB8.5040509@frisch.fr> From: Gabriel Scherer Date: Sun, 11 Dec 2011 14:35:35 +0100 Message-ID: To: Alain Frisch Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id pBBDa1vV015863 Subject: Re: [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance status / community fork (again)] > 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 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