spaceloop (May 23 2022 at 16:43): 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.
Paolo Giarrusso (May 23 2022 at 17:01):As a fix, you replace Notation “‘unit’” with Notation unit?
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.
Paolo Giarrusso (May 23 2022 at 17:03):I’m sure that’s not what you meant, but that is the effect.
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.
Paolo Giarrusso (May 23 2022 at 17:15):Uh, what’s the error?
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]). *)
It tries to parse it as an abbreviation, I think
Paolo Giarrusso (May 23 2022 at 17:20):Yes, it is an abbreviation, but those take modifiers as well according to the manual…
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?
spaceloop (May 23 2022 at 17:22):I'm using Coq 8.13.2 by the way
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).
Paolo Giarrusso (May 23 2022 at 17:22):Ah, I was using the manual for 8.15.
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
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
Paolo Giarrusso (May 23 2022 at 17:24):Contrast with https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#abbreviations
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.
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.
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).
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?
Paolo Giarrusso (May 30 2022 at 12:28):filed https://github.com/coq/coq/issues/16103 for the latter
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: Oct 13 2024 at 01:02 UTC