The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Somewhat belatedly responding to this:

> 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?

I'd be quite interested in this.  In particular, there are two useful things I'd like to see here, which have different degrees of difficulty:

(1) The `pattern` tactic currently abstracts over terms, and then applies the result to the terms that are abstracted over.  I'd like a version that does not create the application node.  If `pattern` is implemented by sequencing these two, this should be as simple as exposing the first step to the tactic layer

(2) The only thing `quote` supports that reification by parametricity doesn't is, as you say, foreign subterms.  I think it would be useful to have a version of pattern that does this.

> I think Template-Coq should allow you to program your quotation mechanism as you wish (baring potential performance problems).

I actually don't see how this would work in Template-Coq.  In particular, I'm not aware of any Gallina denotation function for template-coq terms, so it seems like there'd need to be a separate tactic phase where I denote the map of foreign terms.

> performance is close to the “pattern” option, as far as I could tell.

This is true, though template-coq stack overflows on reifying enormous terms in a way that pattern does not.

On Mon, Jul 23, 2018 at 1:48 PM Matthieu Sozeau <mattam AT mattam.org> wrote:

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.
>