Stream: Coq users

Topic: Notation in custom entry


view this post on Zulip spaceloop (May 23 2022 at 16:43):

Hi, the following fails:

Inductive term := tm_unit.

Declare Custom Entry term.
Notation "[ e ]" := e (e custom term at level 99).
Notation "'unit'" := tm_unit (in custom term at level 0).

Check unit.
(* Syntax error: [lconstr] expected after 'Check' (in [query_command]). *)

I expected the Notation "'unit'" to not affect the main grammar.

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:01):

As a fix, you replace Notation “‘unit’” with Notation unit?

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:02):

I don’t think this is a bug, because this is not changing the main grammar. The semantics of what you typed is to add a new keyword to the lexing stage, which happens before parsing proper and is shared between main and custom entries.

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:03):

I’m sure that’s not what you meant, but that is the effect.

view this post on Zulip spaceloop (May 23 2022 at 17:11):

Thanks. I think I was unclear about the behaviour I want (I actually don't want to change the main grammar, hence the custom entry), e.g. I'd like

Check unit.
(* unit : Set *)

Check [unit].
(* [unit] : term *)

Notation unit := tm_unit (in custom term_e at level 0) is not accepted.

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:15):

Uh, what’s the error?

view this post on Zulip spaceloop (May 23 2022 at 17:17):

Notation unit := tm_unit (in custom term_e at level 0).
(* Syntax error: '.' expected after [syntax_command] (in [vernac_aux]). *)

view this post on Zulip spaceloop (May 23 2022 at 17:17):

It tries to parse it as an abbreviation, I think

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:20):

Yes, it is an abbreviation, but those take modifiers as well according to the manual…

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:21):

It’s not clear if abbreviations in custom entries are supported cc @Hugo Herbelin , but I’d expect them to be?

view this post on Zulip spaceloop (May 23 2022 at 17:22):

I'm using Coq 8.13.2 by the way

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:22):

To have them used, you probably need Notation "x" := x (in custom expr at level 0, x ident).

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:22):

Ah, I was using the manual for 8.15.

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:22):

I don’t recall if custom entries were usable back then, not an expert but they matured pretty recently

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:23):

Okay, the parsing error is explained in the 8.13.2 grammar: https://coq.inria.fr/distrib/V8.13.2/refman/user-extensions/syntax-extensions.html#abbreviations

view this post on Zulip Paolo Giarrusso (May 23 2022 at 17:24):

Contrast with https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#abbreviations

view this post on Zulip spaceloop (May 23 2022 at 17:44):

Thanks, I guess I'll have to upgrade then :) Single-quote keywords in Notation affecting all grammar entries was surprising behavior to me. I couldn't find that on the manual page, which presents the single quotes as a way to write symbols that are not parameters.

view this post on Zulip Paolo Giarrusso (May 24 2022 at 03:56):

I agree the manual needs improvements there; the problem is that it tries to hide the implementation.

view this post on Zulip Hugo Herbelin (May 30 2022 at 10:57):

Hi, did you find a way to circumvent the problem? I'm afraid keywords such as unit (as implied by using "'unit'") are only global (this should be improved!) and abbreviations are insensitive to scopes or custom entries (this could certainly be improved too).

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:25):

IIUC, avoiding global keywords is WONTFIX-level hard (without scannerless parsers), but abbreviations in custom entries seems _much_ easier and maybe easy?

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:28):

filed https://github.com/coq/coq/issues/16103 for the latter

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:32):

also filed https://github.com/coq/coq/issues/16104 in case it helps, but I'd want to hide it away/link it to some bigger refactoring. Or close it for now if the ETA is +inf...


Last updated: Feb 04 2023 at 21:02 UTC