The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi,

I found one use of quote "in the wild": Adam Chlipala's CPDT.

Indeed, teaching is one reason why it might be good if Coq where to ship
with some easy to use reflection mechanism supporting, like quote does,
simple data types and foreign subterms.

So keeping quote and developing it to the point where the reflective
tactics shipped with Coq (can) make use of it, might be worthwhile. I
suppose that would require handling type parameters (denote : ∀ X,
varmap X -> tm -> X), or allowing quote to take a nonempty initial
varmap (to ease reifying two sides of an equation with a common varmap,
etc.

The, closely related, question that got me interested in this is: What
is currently the simplest way to do reification into ones own
inductively defined data type (with variables) in such a way that the
variable map containing the foreign subterms is injective not just with
respect to syntactic equality but with respect to conversion.

Best,
Christian

On 22/07/18 11:35, Hugo Herbelin wrote:
> 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.
>>