Stream: Coq users

Topic: Custom Entries breaking `constr` parsing


view this post on Zulip Janno (Mar 30 2022 at 08:28):

Is it expected that notations using custom entries conflict with constr parsing?

Declare Custom Entry e.
Notation "'[this' := x ]" := (x = x) (in custom e, x constr).
From Coq Require Import List. Import List.ListNotations.
Succeed Check fun that : nat => [that] : list nat.
Fail    Check fun this : nat => [this] : list nat.

(Note that the notation is entirely unused in the example and its body doesn't matter.)
I was under the impression that custom entries lived in different parsing tables. I already know the notion of a keyword is shared but I didn't know that even non-keywords can cause conflicts.

view this post on Zulip Guillaume Melquiond (Mar 30 2022 at 08:45):

But that is not a non-keyword. You are actually defining a new keyword. Did you perhaps mean the following?

Notation "'[' 'this' := x ]" := (x = x) (in custom e, x constr).

view this post on Zulip Janno (Mar 30 2022 at 08:48):

Oh! Interesting! I guess I was going by the absence of a warning about defining a new keyword. Maybe these only show up for keywords that could also be regular names?

view this post on Zulip Janno (Mar 30 2022 at 08:50):

I think this solves my problem. Thank you very much!

view this post on Zulip Guillaume Melquiond (Mar 30 2022 at 09:01):

Janno said:

Maybe these only show up for keywords that could also be regular names?

Yes, identifiers and numbers. That said, it has been a long time since I last saw this warning. I wonder if it has not been inadvertently removed.

view this post on Zulip Paolo Giarrusso (Mar 30 2022 at 09:03):

@Janno how does this solve the problem? IIUC, everything within quotes is a keyword?

view this post on Zulip Janno (Mar 30 2022 at 09:04):

No, it seems only the first item in quotes needs to become a keyword. The suggestion does not make this a keyword.

view this post on Zulip Paolo Giarrusso (Mar 30 2022 at 09:06):

O_O. Is this documented anywhere?

view this post on Zulip Michael Soegtrop (Mar 30 2022 at 09:09):

Out of curiosity: do the quotes around the [ make a difference?

view this post on Zulip Janno (Mar 30 2022 at 09:10):

I don't think it makes a difference

view this post on Zulip Paolo Giarrusso (Mar 30 2022 at 09:11):

https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#basic-notations would also suggest "no difference", but it doesn't mention keywords...

view this post on Zulip Paolo Giarrusso (Mar 30 2022 at 09:11):

The notation consists of tokens separated by spaces. Tokens which are identifiers (such as A, x0', etc.) are the parameters of the notation. Each of them must occur at least once in the abbreviated term. The other elements of the string (such as /\) are the symbols.

Identifiers enclosed in single quotes are treated as symbols and thus lose their role of parameters.

view this post on Zulip Ali Caglayan (Mar 30 2022 at 13:02):

When notations are being searched there is a process that unqoutes a notation string, and replaces free(?) terms with underscores. So 'this' x would get processed to this _ and that is how the notation is looked up in a table. Of course not every method processing notations does the same things, so take this explanation with a pinch of salt. I only found out about this when working on implementing the Print Notation command.


Last updated: Feb 04 2023 at 21:02 UTC