Would there be much of a difference between having native support for number notation in custom entries vs having a Notation "x" := x%my_custom_scope (in custom blah blah at level n, x constr at level m).
and adding the number notation to my_custom_scope
? (I'm wondering if this would solve https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Custom.20entries.20and.20grammar.20factoring/near/380143140 )
Number notations in custom entries is still a project but blocking (in particular) on how to parse negative numbers. Should it be as one token, with -
attached to the number, and a separator before, so that e.g. f-1
is an error (or a minus if binary -
is available), but f -1
is f
applied to -1
.
Would it be tractable to not parse negative numbers and just have - x
be a notation for N.minus
(I don't recall the function name)?
@Gregory Malecha: this is actually what is done currently, and the reason for negative numbers to be at level 35. (It could be lower, but it should be higher than application at level 10, so that x - 1
is not parsed as x (-1)
.)
Thanks!
I think, at least in custom entries, it should be as two tokens, and (if necessary) an error should be raised at number notation time if prefix "-" has not yet been assigned a level and the source type for parse is signed. This seems most general to me; users wanting f -1
can make -
bind tighter then application.
The only use case this doesn't support is having prefix negation bind less tight than application in general but more tight specifically for literals. In theory a user could solve this by putting the number notation in a custom entry on its own, but I wonder if the parser will be able to handle the fact that -1
is parsable both as "- x"
at level 40 in custom foo, x custom foo at level 40, followed by "x"
in custom foo at level 9, x custom foonum at level 10, followed by 1
in custom numfoo at level 0 (levels picked arbitrarily), or as "x"
in custom foo at level 9, x custom foonum at level 10, followed by "- x"
at level 5 in custom foonum, x custom foonum at level 5, followed by 1
in custom numfoo at level 20 (levels picked arbitrarily),
Alternatively, if this is not general enough, it seems fine to have Number Notation default to the thing currently done for constr
, with an extra option attached to in custom blah
so users can write in custom blah, single token minus
or whatever
Somehow, I was trying to understand if the ad hoc way it is parsed in Coq (i.e. hard-wiring the existence of a notation -
in the interpreter of notations - constrintern.ml
) could be avoided.
Last updated: Oct 13 2024 at 01:02 UTC