Stream: MetaCoq

Topic: Splicing a kername

spaceloop (Oct 25 2023 at 11:45):

Hi, is it possible to splice the kername of an identifier in gallina code? I'd like to use something similar to <% %> notation, but for resolving names.

Yannick Forster (Oct 25 2023 at 14:22):

Can you give a concrete an example of what you'd like to be able to do?

spaceloop (Oct 26 2023 at 07:45):

I've realised that I'm actually looking for a convenient way of pattern matching on certain references in an AST (let's say inductives). I'd imagine writing something like this:

fun t => match t with
  | tApp <? list ?> [ty] => ...
  | ...
  end

where <? ?> would expand to a pattern (which I'd rather not write myself):

(tInd
   {|
     inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "list");
     inductive_ind := 0
   |} [])

Perhaps there is already a convenient way to do this? Right now, I'm doing something like:

Notation listPat := (tInd
   {|
     inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "list");
     inductive_ind := 0
   |} []).

And use listPat in pattern matching.

Théo Winterhalter (Oct 26 2023 at 07:52):

You can probably use this amazing notation by @Yannick Forster:

Notation "'$quote' x" :=
  ltac:((let p y := exact y in quote_term x p))
  (at level 0).

Then $quote list is the term you want.

spaceloop (Oct 26 2023 at 08:00):

Interesting! I'm afraid it is not working for patterns though, for example:

Definition g : term -> bool :=
  fun t => match t with
    | $quote list => true
    | _ => false
  end.

Fails with Pattern "_" is redundant in this clause., it seems to be matching anything.

Gaëtan Gilbert (Oct 26 2023 at 08:05):

coq <8.18 confuses ltac:() and _ when used in patterns (with ltac:() only being possible through a notation)
after 8.18 it should instead say Quotations not supported in patterns.

Théo Winterhalter (Oct 26 2023 at 08:06):

Interesting, for me it says "quotations not supported in patterns". But it still doesn't work indeed. But you can still test for equality with term_eqb.

spaceloop (Oct 26 2023 at 08:08):

Right, I'm on a coq<8.18 right now.

Théo Winterhalter (Oct 26 2023 at 08:09):

Me too, I'm on 8.16.1.

spaceloop (Oct 26 2023 at 08:10):

I've considered using term_eqb, but that limits the possibilities of doing pattern matching, e.g. in the original example, I also want to match on a list of length one (lists only type parameter)
edit: this example:

fun t => match t with
  | tApp <? list ?> [ty] => ...
  | ...
  end

Gaëtan Gilbert (Oct 26 2023 at 08:12):

actually the "Quotations not supported in patterns" is since 8.15

Yannick Forster (Oct 26 2023 at 17:17):

You need to use term_eqb, no way around it

Yannick Forster (Oct 26 2023 at 17:18):

So tApp c [ty] => if c == $quote list... with == being notation for a suitable call to term_eqb

Théo Winterhalter (Oct 26 2023 at 17:20):

I realise now, that anyway it's better for performance because pattern matching on strings is very inefficient right?

Yannick Forster (Oct 26 2023 at 17:23):

Yep, the pattern match will be way too inefficient

Yannick Forster (Oct 26 2023 at 17:24):

We could think about having quotation of patterns such that you can do match t with $quote_pattern cons x nil =>..., but for my purposes term_eqb has usually be sufficient

Paolo Giarrusso (Oct 26 2023 at 18:51):

The question is just how much inspection people want to write with MetaCoq, and is pattern quotation predictable enough

spaceloop (Oct 27 2023 at 10:38):

Would the pattern match performance problem be solved by doing the plugin extraction approach?

Yannick Forster (Oct 27 2023 at 11:19):

Maybe, I don't think we ever tried :)

Last updated: Oct 13 2024 at 01:02 UTC