The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  A somewhat generic solution is provided by RTac (Malecha and Bengston) and is quite elaborate. I think Template-Coq should allow you to program your quotation mechanism as you wish (baring potential performance problems). At least using this you’d have direct access to the syntax of your term, no typechecking involved. According to J. Gross et al ITP paper performance is close to the “pattern” option, as far as I could tell.

My 2 cents,
— Matthieu

Le dim. 22 juil. 2018 à 11:36, Hugo Herbelin <Hugo.Herbelin AT inria.fr> a écrit :

Hi,

Somehow, a question is also whether it would be worth that someone
eventually provides a generic-enough quote function in Coq, for use at
both the vernac level or the plugin level.

My understanding of the Gross-Erbsen-Chlipala ITP 2018
reification-by-parametricity paper is that this quote function almost
already exists, it is "pattern". Then, what about going in the
direction of providing a variant of "pattern" which encapsulates the
boilerplate of the technique and which, maybe, also abstracts over the
foreign subterms?

Idem at the plugin level. Already e.g. ring, micromega, btauto have
their own reification mechanisms (sometimes even in Ltac) and this
seems suboptimal.

Best,

Hugo

On Fri, Jul 20, 2018 at 11:45:32AM -0700, John Wiegley wrote:
> I would also support dropping Quote; each time I've been able to use it, I
> ended up just copying Ltac macros from existing templates so I would have the
> configurability needed for future changes.

On Fri, Jul 20, 2018 at 08:41:28AM -0400, Tej Chajed wrote:
> I definitely support getting rid of Quote. I used it once and then ran into an
> issue: my unquote function took a type parameter, which is unsupported, even if
> you try specializing it. I talked to Jason Gross, copied some code from their 
> reification-by-parametricity paper, and got it working fairly easily in pure
> Ltac.
>
> It would be great to have some examples from that paper coped into the Coq test
> suite and try to give it visibility, instead of maintaining Quote. It's a more
> powerful technique and I believe with just a little boilerplate can replace
> uses of Quote (if anybody actually weighs in and is using it).
>
> On Fri, Jul 20, 2018 at 3:20 AM Maxime Dénès <mail AT maximedenes.fr> wrote:
>
>     Dear Coq-clubbers,
>
>     I'm trying to clean up the set of plugins shipped with Coq, so that we
>     can make the maintenance done by the development team more focused and
>     effective.
>
>     I was wondering if anybody was using the Quote plugin in real-world
>     developments. See https://github.com/coq/coq/pull/7894 for more context.
>
>     Thank you in advance for your feedback!
>
>     Maxime.
>