Stream: Coq devs & plugin devs

Topic: Number notation and custom entries?


view this post on Zulip Jason Gross (Aug 04 2023 at 17:55):

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 )

view this post on Zulip Hugo Herbelin (Aug 07 2023 at 11:47):

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.

view this post on Zulip Gregory Malecha (Aug 07 2023 at 15:34):

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)?

view this post on Zulip Hugo Herbelin (Aug 07 2023 at 16:55):

@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).)

view this post on Zulip Gregory Malecha (Aug 07 2023 at 17:01):

Thanks!

view this post on Zulip Jason Gross (Aug 07 2023 at 17:01):

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),

view this post on Zulip Jason Gross (Aug 07 2023 at 17:04):

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

view this post on Zulip Hugo Herbelin (Aug 09 2023 at 14:28):

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: Jul 13 2024 at 02:02 UTC