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.
As a fix, you replace
Notation “‘unit’” with
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.
I’m sure that’s not what you meant, but that is the effect.
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.
Uh, what’s the error?
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
Yes, it is an abbreviation, but those take modifiers as well according to the manual…
It’s not clear if abbreviations in custom entries are supported cc @Hugo Herbelin , but I’d expect them to be?
I'm using Coq 8.13.2 by the way
To have them used, you probably need
Notation "x" := x (in custom expr at level 0, x ident).
Ah, I was using the manual for 8.15.
I don’t recall if custom entries were usable back then, not an expert but they matured pretty recently
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
Contrast with https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#abbreviations
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.
I agree the manual needs improvements there; the problem is that it tries to hide the implementation.
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).
IIUC, avoiding global keywords is WONTFIX-level hard (without scannerless parsers), but abbreviations in custom entries seems _much_ easier and maybe easy?
filed https://github.com/coq/coq/issues/16103 for the latter
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