ssreflect pollutes notation precedence space for colon

[andrew-appel]

Version

8.7

Operating system

All

Description of the problem

I have an "only printing" notation that uses the colon : at level 26. This works fine in Coq 8.6.1. Apparently in Coq 8.7, I cannot use the colon at level 26, because ssreflect (which I do not want to use) reserves it at precedence level 100. If it is true that the colon's precedence level is fixed at 100 because of something in a nonstandard library, I consider that a bug. Especially that my notation is "only printing", so it can't have any effect on parsing!

See also
PrincetonUniversity/VST#111
PrincetonUniversity/VST#112

[ejgallego]

If I understand the issue currently, you are indeed loading ssreflect in some of your dependencies, so even if you don't plan to use it, it is loaded.

If that is the case, I think it will hard to fix soon [unless ssreflect already has some special flag to help with this], the reason being how parsing rules are handled.

[ejgallego]

By the way, I think the problem should exist in Coq 8.6.0 + ssreflect, but need to double-check.

[gares]

From: http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.ssreflect.html

 Allow overloading of the cast (x : T) syntax, put whitespace around the    
 ":" symbol to avoid lexical clashes (and for consistency with the parsing  
 precedence of the notation, which binds less tightly than application),    
 and put printing boxes that print the type of a long definition on a       
 separate line rather than force-fit it at the right margin.

Notation "x : T" := (x : T)
  (at level 100, right associativity,
   format "'[hv' x '/ ' : T ']'") : core_scope.

I'm not very competent on notations, but i think application is at level 10, so both 100 and 26 should be fine.

Let me ping @ggonthier, @amahboubi and @CohenCyril to see if someone recalls why 100 exactly, and knows if lowering the level (e.g. to 26) would cause any issues in mathcomp. At the same time,
@andrew-appel, I could not find (in the two issues you linked) the reason why : is at level 26 and if raising its level to 100 would be an option.

The fact that that a notation/operator has a global level is clearly a problem (and maybe @ejgallego has an answer to that in his parsing-tables branch).
But while we wait for a better notation infrastructure, putting : at a level that works for both mathcomp and VST is probably doable. Also, moving the notation from ssreflect.v to ssrfun.v looks like another viable option to me (i.e. the offending notation would not be loaded by VST, that only requires ssreflect.v AFAICT).

[ppedrot]

If I understand the issue currently, you are indeed loading ssreflect in some of your dependencies, so even if you don't plan to use it, it is loaded.

AFAIK, notations that are not imported have no effects, so it's even stronger than that: it means that ssreflect has been imported by one of the dependencies, not merely required. Which seems to me like a bug in the dependencies.

[ppedrot]

I had a look at the notation implementation in Metasyntax, and I think it is easy to tweak the code so that only printing notations do not trigger such level conflicts. I'll write a quick PR to see it this is indeed workable.

[ggonthier]

The initial reason for overriding the cast notation was to enable the other overriding rule in ssreflect.v, for T : Type, which puts T in the %type scope, which gives a slightly more pleasant way of saying A * B : Type (vs. (A * B)%type). The printing rule for the generic cast was more like an added bonus. The intent for both rules was to be consistent with the native level for cast, which was 100 at the time this code was written. I’m surprised it’s ben changed by so much, because it is still documented as 100 in the 8.7 manual (end of section 12.1.3): changing that level requires adapting levels in all the comprehension notations, and since the new level is so low (binding tighter than arithmetic operators) require changing client code as well, e.g., [seq n + 1 | n <- iota 1 5] would require parentheses around the n + 1 expression (alongside spoiling the above mentioned A + B : Type notation). Georges

…

Le 5 nov. 2017 à 15:13, Enrico ***@***.***> a écrit : From: http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.ssreflect.html <http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.ssreflect.html> Allow overloading of the cast (x : T) syntax, put whitespace around the ":" symbol to avoid lexical clashes (and for consistency with the parsing precedence of the notation, which binds less tightly than application), and put printing boxes that print the type of a long definition on a separate line rather than force-fit it at the right margin. Notation "x : T" := (x : T) (at level 100, right associativity, format "'[hv' x '/ ' : T ']'") : core_scope. I'm not very competent on notations, but i think application is at level 10, so both 100 and 26 should be fine. Let me ping @ggonthier <https://github.com/ggonthier>, @amahboubi <https://github.com/amahboubi> and @CohenCyril <https://github.com/cohencyril> to see if someone recalls why 100 exactly, and knows if lowering the level (e.g. to 26) would cause any issues in mathcomp. At the same time, @andrew-appel <https://github.com/andrew-appel>, I could not find (in the two issues you linked) the reason why : is at level 26 and if raising its level to 100 would be an option. The fact that that a notation/operator has a global level is clearly a problem (and maybe @ejgallego <https://github.com/ejgallego> has an answer to that in his parsing-tables branch). But while we wait for a better notation infrastructure, putting : at a level that works for both mathcomp and VST is probably doable. Also, moving the notation from ssreflect.v to ssrfun.v looks like another viable option to me (i.e. the offending notation would not be loaded by VST, that only requires ssreflect.v AFAICT). — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#6078 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AOhrHUNYFzg3Peu2R526StzzaTUbs1pPks5szcKCgaJpZM4QSYJp>.

[herbelin]

Hi Georges,

The initial reason for overriding the cast notation was to enable the other overriding rule in ssreflect.v, for T : Type, which puts T in the %type scope, which gives a slightly more pleasant way of saying A * B : Type (vs. (A * B)%type).

Is it possible that the other
Notation "T : 'Type'" := (T%type : Type) (at level 100, only parsing) : core_scope.
work also without the overriding of the main cast notation?

The printing rule for the generic cast was more like an added bonus. The intent for both rules was to be consistent with the native level for cast, which was 100 at the time this code was written.

The level of the native printing rule for cast is also 100, and associativity is the same, so I suspect that the primary reason for the overwriting was to add a space. The native printer adds spaces around the : since 8.5 (thanks to @gmalecha, see #3936), so could it be that the overwriting made in ssreflect.v is not necessary anymore to achieve this goal and that the rule can be removed without any negative impact on the habits of ssreflect users? (In any case, noone is proposing that 26 becomes the default level for cast.)

As a secondary remark, I like the idea of forcing the interpretation of T in T:some_sort to be done in type_scope. It is not excluded in principle that it introduce some incompatibility but I would be tempted to try to activate it by default (i.e w/o requiring a specific notation) since this is after all the intuitive expectation. At least, we could try to see how our test-suite react to such change, and if it works, that would be a simple but good example of how a good communication with ssreflect developers can serve the general interest of users.

Otherwise, about the VST issue, it is still not excluded, if I understood correctly, that there is an issue in the dependencies of VST in ssreflect or a Coq bug of Require wrt grammars.

As for the enhancement request that several notations with same "key" but different printing rules are supported, it also remains valid.

[herbelin]

PS: In the longer term (8.8), support for stand-alone constr parsers (PR #982, this comment) shall give more flexibility in defining custom syntaxes for formalized languages such as Clight here (no interference with the main syntax on the choice of precedences or associativity).

[ggonthier]

Hi Hugo,

Is it possible that the other Notation "T : 'Type'" := (T%type : Type) (at level 100, only parsing) : core_scope. work also without the overriding of the main cast notation? The printing rule for the generic cast was more like an added bonus. The intent for both rules was to be consistent with the native level for cast, which was 100 at the time this code was written. The level of the native printing rule for cast is also 100, and associativity is the same, so I suspect that the primary reason for the overwriting was to add a space. The native printer adds spaces around the : since 8.5 (thanks to @gmalecha <https://github.com/gmalecha>, see #3936 <#3936>), so could it be that the overwriting made in ssreflect.v is not necessary anymore to achieve this goal and that the rule can be removed without any negative impact on the habits of ssreflect users? (In any case, noone is proposing that 26 becomes the default level for cast.)

It’s quite possible that the two overrides are linked conceptually rather than materially (i.e., once we’d picked up enough motivation to override the cast grammar, we just did both). If the overriding is now redundant, we should by all means remove it. Do note however that the generic cast override also adds a pretty-printing box, and this is much more important as it affects the readability of proof contexts for the reasons cited in the comment.

As a secondary remark, I like the idea of forcing the interpretation of T in T:some_sort to be done in type_scope. It is not excluded in principle that it introduce some incompatibility but I would be tempted to try to activate it by default (i.e w/o requiring a specific notation) since this is after all the intuitive expectation. At least, we could try to see how our test-suite react to such change, and if it works, that would be a simple but good example of how a good communication with ssreflect developers can serve the general interest of users.

By all means do experiment! Also, you could get a better implementation of this functionality while implementing this in system code: - imposing only transient (one-level) rather than deep scope override on T (unless there is now user syntax for that?) - generalising this to all type-bound scopes (so m + n : nat always interprets the + in nat_scope) - generalising this to implied casts, i.e., Definition AxB : Type := A * B does what you’d expect.

Otherwise, about the VST issue, it is still not excluded, if I understood correctly, that there is an issue in the dependencies of VST in ssreflect or a Coq bug of Require wrt grammars.

That seems likely; AFAIK unimproved grammar notations (in contrast to simple notations) have no effect. Perhaps some Import dependency of VST (improperly) exports ssreflect. Cheers, Georges

[herbelin]

Hi Georges,

It’s quite possible that the two overrides are linked conceptually rather than materially (i.e., once we’d picked up enough motivation to override the cast grammar, we just did both). If the overriding is now redundant, we should by all means remove it. Do note however that the generic cast override also adds a pretty-printing box, and this is much more important as it affects the readability of proof contexts for the reasons cited in the comment.

According to git log, there is a box for casts in the native printer since the very beginning of the new syntax (i.e. 8.0). So, "by all means remove it"?

By all means do experiment!

Do you think that it is a good idea to propose @gares to do the experiment? (And if not, I can propose a PR for item 1 below.)

Also, you could get a better implementation of this functionality while implementing this in system code:

• imposing only transient (one-level) rather than deep scope override on T (unless there is now user syntax for that?)

This is the default for those "ad hoc" internal forcing of a scope, so, that shall be easy.

• generalising this to all type-bound scopes (so m + n : nat always interprets the + in nat_scope)

Yes and no. Yes, this is convenient, but if we start in this direction, I don't know where to stop. Why nat and not a _ easily inferable to be nat, why nat and not id nat, etc. I feel that internalize time is not the right place for this kind of feature (compare to pretyping). I'm not opposed but I wonder about what is the general opinion.

Is your motivation aesthetic (i.e compared to (m+n)%nat)? It is not that I find the notation % pretty illuminating, but a cast leaves a trace in the term, so if we want to favor the t : T in place of t%TT when type T is bound to a scope TT, this shall have impact beyond the purely surface language.

• generalising this to implied casts, i.e., Definition AxB : Type := A * B does what you’d expect.

It happens that this is already like this (since 8.5).

Best,

Hugo

[herbelin]

BTW, Georges, you are someone pretty sensitive to syntactic issues, so let me digress a bit. I tried a couple of time to motivate other people to integrate some of your syntax ideas that I find cool, but with little success in getting feedback. For instance, I like n.+1 but I did not perceive a strong will yet at providing it as soon as the initial state. On the other side, if t is pat then u else v seems to have received some support at the last Coq WG (while e.g. my efforts to convince OCaml to propose it failed). I don't think you are pretty motivated yourself with existT, but this is yet another syntax which looks rather ugly to me. Ideally, the most natural to me would be (t,u) but I don't know how to solve the conflict with pair (maybe prod and sigT should be non-generative after all, I think that this is also what @JasonGross suggested, and prod seen as a particular case of sigT). As a short-term plan, it could at least be (t;u) as used by @JasonGross. On another somewhat related question, what do you think about the idea of unifying seq and list? Best, Hugo

[andrew-appel]

Let me clarify, now that @ildyria has explained it better to me:

VST does not import or export ssreflect. But some users of VST want to also use ssreflect, or vice versa. It's only when they are combined that there is a problem.

[ggonthier]

Le 6 nov. 2017 à 16:40, Hugo Herbelin ***@***.***> a écrit : BTW, Georges, you are someone pretty sensitive to syntactic issues, so let me digress a bit. I tried a couple of time to motivate other people to integrate some of your syntax ideas that I find cool, but with little success in getting feedback. For instance, I like n.+1 but I did not perceive a strong will yet at providing it as soon as the initial state. On the other side, if t is pat then u else v seems to have received some support at the last Coq WG (while e.g. my efforts to convince OCaml to propose it failed). I don't think you are pretty motivated yourself with existT, but this is yet another syntax which looks rather ugly to me. Ideally, the most natural to me would be (t,u) but I don't know how to solve the conflict with pair (maybe prod and sigT should be non-generative after all, I think that this is also what @JasonGross <https://github.com/jasongross> suggested, and prod seen as a particular case of sigT). As a short-term plan, it could at least be (t;u) as used by @JasonGross <https://github.com/jasongross>. On another somewhat related question, what do you think about the idea of unifying seq and list? Best, Hugo

Thanks for trying! Regarding existT, math comp gets around some of the ugliness by using aliases for accessors and constructors (tag/tagged/Tagged), and we kind of get by with that because of the limited use we make of the generic sigT type - though I can clearly see how HoTT des might have different needs, and the (i; u) notation might be right (and may help deter users from overloading ‘;’, which wreaks havoc in the rest of the syntax). I still think there’s a big issue with the flow of information in type inference: I’d usually expect (i; u) to be untypeable unless the expected type for the expression is allowed to inform the expected type for u (specifically, provide the T in {i & T i} - indeed, in the Tagged alias i is implicit and T is explicit). I’ve already noted that this is a general problem with type inference of applied constants, and that it would help a lot if users could specify at which point the expected type of a application can be used to synthesise the type of remaining arguments, because the current default (« never ») is not always appropriate. Partly for this we tend not to use the generic sigT type, but define specialised sigT-like (co)inductive types - and we haven’t really found the need for a canonical structure reflecting that correspondance (as subType does for sig) simply because there aren’t enough theorems about sigT that could exploit this (I’ll grant you this may be very different in HoTT). Concerning seq and list: they have long been unified (since 2007 if memory serves well): seq is merely an alias for list.Originally (for the 4 color theorem and in the very early math comp days) the types were different, because I’d used coercion to Funclass to denote list membership, and at the time this meant the argument to seq had to be an eqType structure to satisfy uniform inheritance. We’ve since moved to an explicit membership operator supporting type-based overloading, removing the need for a distinct type (uniform inheritance is sort of going away too). However I’ve found it difficult to replace seq by list, cat by append, size by length, etc, in the names of both auxiliary operations and related lemmas; in particular ‘l’ is a troublesome suffix to use, too easily confused with 1 and I. So, we’ve stuck with those aliases. There is a separate issue with the explicit list syntax: [] are the only ASCII brackets that aren’t reserved by the native Coq grammar, so it’s unreasonable to use them only for list syntax, especially as lists play a much smaller role in formalised theories as compared to functional programming. Our solution is to follow the leading ‘[‘ with a keyword or operator that specifies the kind of construction to follow, using ‘::' for explicit sequences, and ‘seq’ for sequence comprehensions. Perhaps there’s a better solution if one can tweak the parse engine (at least, one should be able to use the same separator for nil and cons terminated lists). Best, Georges