Only accept SELF on the left for left-associative levels

[ia0]

This PR is a follow-up of the discussion in #21072, initially started by #21029. This can also be seen as the continuation of the work started in #17876. In particular, this PR provides proper support for non-associativity and fixes leniency in right-associativity (namely that the left component recognizes the non-recursive part of the same level instead of the next level only).

Depends on: #21244 (merged)

Overlays (to be merged before the current PR)

• Adapt to https://github.com/rocq-prover/rocq/pull/21126 math-comp/math-comp#1490
• Adapt to https://github.com/rocq-prover/rocq/pull/21126 stdlib#222

Overlays (to be merged in sync with the current PR)

• Adapt to https://github.com/rocq-prover/rocq/pull/21126 uds-psl/autosubst-ocaml#31
• Adapt to https://github.com/rocq-prover/rocq/pull/21126 rocq-community/rocq-lsp#1063

[ia0]

I completely broke associativity... i.e. atom1 op12 atom2 op12 atom2 and atom1 op10 atom1 op10 atom0. I'll take a look when I get time.

[ia0]

Closing this draft because @proux01 fixed it, see #21072 (comment).

[ia0]

Actually I don't think this was buggy (it passes the same tests as the commit from @proux01). The output/Notations4.v test case is buggy.

Print Custom Grammar expr gives:

Entry custom:expr is
[ "2" RIGHTA
  [ SELF; "+"; NEXT ]
| "1" LEFTA
  [ SELF; NEXT ]
| "0" RIGHTA
  [ "{"; term LEVEL "200"; "}"
  | "("; custom:expr LEVEL "2"; ")"
  | NUMBER "1"
  | identref ] ]

Level 2 written like that makes no sense. It essentially means + is non-associative since SELF on the left of RIGHTA is NEXT.

[proux01]

Indeed, this seems to work, let's reopen.
The only advantage I can see to proux01@4fdb719 is that warning seem better located (on the left of right assoc).
Yes, a few output tests will need an update.

[ia0]

The only advantage I can see to proux01@4fdb719 is that warning seem better located (on the left of right assoc).

I don't know about the warnings. I already don't find them correct on master.

Regarding the diff between both commits, in my opinion the biggest difference is the approach. In your case you reject a recovery on a wrong level after running the suffix tree, while in my case I restrict the range of levels to continue which won't even try running the suffix tree for the wrong level if not gstate.recover.

Another minor (but semantically significant in my opinion) difference is that you check lev.assoc = RightA while I believe the correct check is lev.assoc <> LeftA. This recovery mechanism is only meant for left-associativity, so it's normal to disable it for the other cases (right-associativity and non-associativity).

Yes, a few output tests will need an update.

Should I give it a go? (I'm not convinced I should produce a PR if there's too much OCaml involved.)

[proux01]

The only advantage I can see to proux01@4fdb719 is that warning seem better located (on the left of right assoc).

I don't know about the warnings. I already don't find them correct on master.

Maybe the wording could be improved? These warnings are kinda important since they are the main tool for users to adapt to the future change.

Regarding the diff between both commits, in my opinion the biggest difference is the approach. In your case you reject a recovery on a wrong level after running the suffix tree, while in my case I restrict the range of levels to continue which won't even try running the suffix tree for the wrong level if not gstate.recover.

No opinion on which implem is better. I just think that it is important for the warning to be precisely located (in this case, indicating at which character position the user can add parentheses).

Another minor (but semantically significant in my opinion) difference is that you check lev.assoc = RightA while I believe the correct check is lev.assoc <> LeftA. This recovery mechanism is only meant for left-associativity, so it's normal to disable it for the other cases (right-associativity and non-associativity).

Indeed, you're right

Yes, a few output tests will need an update.

Should I give it a go?

Feel free to

(I'm not convinced I should produce a PR if there's too much OCaml involved.)

Well, this repo is essentially OCaml code, so PRs are essentially OCaml.

[ia0]

Maybe the wording could be improved? These warnings are kinda important since they are the main tool for users to adapt to the future change.

Yes I agree they are important. The problem I'm referring to is not really the formulation, but the levels (and maybe sometime the location? I'll need to find examples). An example that I find confusing for levels is:

Check 0 > ~ 0.

It gives the following warning (on the correct location of ~ 0):

Error: In term, tolerating this expression at level 60 while it is expected to be at level 200. This tolerance
will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this
expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

I would expect level 75 instead of level 200, since that's the most precise level of ~ 0. It is indeed also at level 200 but that seems imprecise and possibly confusing. Although one could argue that the implementation would indeed tolerate anything up to level 200. So yes, maybe it's just the formulation.

[proux01]

Honestly, in my experience as a user, whereas the location is super important, the levels in the warning message aren't very useful: either you decide to add parentheses and you don't care about the levels, or you decide to change some levels which means you need to find where the notations are reserved and you'll then also get their levels. So maybe our best move would just be to get rid of the levels in the message.

[ia0]

I see, makes sense.

[proux01]

I see, makes sense.

C.f. #21166

[proux01]

Rebased to fix the conflict I created with #21166

FTR, this was discussed during yesterday's call, there was a general agreeement we should do it, with the following requests:

• try to get the warning locations right
• which should enable quickfixes (offering to add the extra parentheses)
• fix the issue with the tactic => intro_pattern ssreflect syntax (I'm looking at it)
• have an extra reviewer

[SkySkimmer]

which should enable quickfixes (offering to add the extra parentheses)

Adding parentheses is not always guaranteed to work, in particular custom entries don't have to have a rule with parentheses embedding the top level into the bottom level.

[proux01]

Yes, it's more a best effort that will work in many cases than a 100% foolproof solution.

[ia0]

I've rebased onto master and split into 2 commits: one adding the test file and one with the actual change (which I changed to use the level-tolerance warning such that the error locations are correct). In particular, the .out file in the second commit is exactly the diff of the change and enough to review to check the error locations (which I find correct). If we can have @herbelin reviewing that would be great since this touches level-tolerance.

[proux01]

I think it would be nice to have an indication in the message on whether the issue lies on the left (all warnings prior to the current PR) or on the right (the new warnings from this PR) of the flagged location.
Otherwise LGTM, we still need before merging (potentially in separate PR) to:

• fix the ssreflect _ => _ issue (I'm looking at it)
• try to improve the recovery locations so that we can provide a quickfix suggesting adding parentheses (maybe only on constr were we are sure the parentheses do exist)
• get an extra review

[proux01]

Definitely independent from the current PR but here, I'd rather expect the following location

Suggested change

	> Check Reject 10 [2 atom3 ].
	> ^^^^^^^
	> Check Reject 10 [2 atom3 ].
	> ^^^^^

not sure if this could be reasonably obtained.

[ia0]

Yes, I was also expecting that more narrow error location.

[SkySkimmer]

This creates a warning in the ltac2/custom_entry test. Ltac2 custom entries declare levels to be RIGHTA so that self on the right and on the left always means the current level and leaves associativity to the rule writer, this PR would break that.

IDK if there should be a new associativity that doesn't warn or what but this shouldn't be merged as-is.

[ia0]

Ltac2 custom entries declare levels to be RIGHTA so that self on the right and on the left always means the current level.

This is not what right-associativity means. Right-associativity means that NEXT op SELF.

IDK if there should be a new associativity that doesn't warn.

What you want would be all-associativity defined by SELF op SELF. That's indeed the only missing option of the 4 possibilities:

• no-associativity is NEXT op NEXT
• left-associativity is SELF op NEXT
• right-associativity is NEXT op SELF
• all-associativity is SELF op SELF

Note that all-associativity is ambiguous if no care is taken. The user needs to write their rules (e.g. notations) such that no ambiguity is possible, i.e. NEXT op SELF or SELF op NEXT for each production rule.

I don't think this would be difficult to implement once we have add the ALLA variant to NONEA, LEFTA, and RIGHTA.

However, I wonder how niche this is. Do we have concrete examples of users that need to control associativity for each rule rather than each level?

The examples in ltac2/custom_entry.v are rather artificial. They abuse the fact that you can do left-associativity rules in a right-associative level. Most (if not all) users (see the mathcomp overlay) consider this a hack and would prefer to get a warning to fix it.

[proux01]

This creates a warning in the ltac2/custom_entry test. Ltac2 custom entries declare levels to be RIGHTA so that self on the right and on the left always means the current level and leaves associativity to the rule writer, this PR would break that.

My understanding of this hack is that you use RIGHTA as a way of trying to convince gramlib to "stop trying to handle associativity for me". Note that the ultimate goal of this PR is to ultimately get rid of any associativity notion in gramlib (and have higher levels be the only one to handle it, through proper use of SELF and NEXT). Unfortunately, note that this doesn't perfectly work, when you write

(* we can also do right associative notations *)
Ltac2 Notation x(self) "-" y(self) : mycustom(1) := (x, y).

what you'd really like to write is rather

(* we can also do right associative notations *)
Ltac2 Notation x(next) "-" y(self) : mycustom(1) := (x, y).

but unfortunately this doesn't quite work as the parser doesn't handle it since all levels are righta and you need to write

Ltac2 Notation x(next) "-" y(self) : mycustom(1) := (x, y).
Ltac2 Notation x(next) : mycustom(1) := x.

Not sure what's the best solution. Maybe we should just allocate "correct" associativities rather than the default righta for now (this would restrain a tiny bit the expressivity of ltac2 custom entries (at least as long as gramlib insists on managing them) but probably nothing unacceptable)

[ia0]

I think there's some confusion due to the meaning of SELF and NEXT. There are 3 different meanings:

• The syntax at Rocq level (at next level, x(self), and x(next) for example).
• The syntax at Gramlib level (Sself and Snext).
• The semantics at Gramlib level (what grammar is actually recognized).

I've been using SELF and NEXT with this last meaning, because that's what matters (and that's what SELF means in the title of this PR).

Ideally we could make the Rocq syntax match the Gramlib semantics. But we won't be able to make the Gramlib syntax match its semantics without major changes because of the strong distinction between start and continue trees (which hardcodes the meaning of Sself on the left in the design).

Note that the ultimate goal of this PR is to ultimately get rid of any associativity notion in gramlib (and have higher levels be the only one to handle it, through proper use of SELF and NEXT).

I would say this PR does actually the complete opposite of that. Also this seems to contradict one of your previous comment:

IIRC, the outcome of the discussion was that we absolutely don't want that. Mixing different associativities at the same level would be way to confusing. Associativity is a level thing. The fact that it currently seems attached to rules is an interface defect

So maybe we should try to go back to the blackboard and see what we want to do. I see at least 2 toplevel options:

• Make associativity a level decision in Rocq (as it is the case in Gramlib).
• Make associativity a rule decision in Rocq and Gramlib.

I believe both are possible (ignoring the amount of effort), so the question is what we want. I'll try to give pros and cons, but I'm sure this is non-exhaustive.

Pros of level-based associativity (thus cons of rule-based associativity):

• Minimum changes to Gramlib implementation.

Pros of rule-based associativity (thus cons of level-based associativity):

• Minimum changes to Rocq notations (doesn't need Named notation levels rfcs#106).
• More expressive grammar (I believe).

Ignoring difficulty and sunk-cost fallacy, rule-based associativity seems better. This would align with what both @SkySkimmer and @proux01 seemed to prefer in their last comment. If we want to go that direction, then indeed this PR is completely useless, because we will remove NONEA, LEFTA, and RIGHTA altogether. All levels will have all-associativity (i.e. syntactic SELF on either end means SELF and it's up to the user to avoid ambiguities).

I don't know if I will be able to implement the change to Gramlib but I could take a look if that's the decision. (That would be a much more ambitious project than just fixing Gramlib as this PR is doing.)

[jfehrle]

The term "associative" seems like it's probably misleading. The last time I looked at the parser a couple years ago, there was no way that a OP b OP c could be parsed as a OP (b OP c), ie right associatively in the most common sense. That generally requires a parser stack, which gramlib doesn't have. Gramlib seems to give "associative" a different meaning. Right?

[ia0]

there was no way that a OP b OP c could be parsed as a OP (b OP c), ie right associatively in the most common sense.

I believe this always worked:

Notation "x 'op' y" := (x, y) (at level 60, only parsing, right associativity).
Check I op I op I.
(* (I, (I, I)) : True * (True * True) *)

However, I agree that we use the word associative in a more general meaning than just binary operators. We use associative to describe the meaning of SELF on the left and on the right, regardless of the symbols in-between (there could be 0, 1, or more).

[proux01]

Well, the current PR is essentially just introducing a deprecation warning.
Currently, associativities are managed in multiple ways both by gramlib and higher levels (be it (term) notations or Ltac2 tactic notations). This duplication leads to many bugs / hard to understand behaviors. Once we get rid of the bahavior that is deprecated in the current PR, we can get rid of associativities in gramlib (and other recovery mechanisms) and massively simplify it. Until then, we have plenty of time (at least a year) to discuss on whether we want to keep associativity a level based thing or make it rule based.
So the only "urgent" thing is to get Ltac2 Notation somehow compatible with the new warning, so that we can merge the current PR (it's a bit unfortunate that both get implemented in the same time frame, Ltac2 custom entries would have been much easier to implement with the simplified gramlib, not requiring all those hacks with RightA).

About level/rule based: IIRC, the major argument in favor of level based associativity was to reduce the risk of surprising behavior (what happens when mixing left and right associative notations at the same level). I'd say the major argument for rule based would be increased compatibility between libraries (no more dreaded error "level n is left-assoc in library A and right-assoc in library B"). In any case, I tend to think that interface/user facing arguments should come first before implementation cost.

The term "associative" seems like it's probably misleading. The last time I looked at the parser a couple years ago, there was no way that a OP b OP c could be parsed as a OP (b OP c), ie right associatively in the most common sense. That generally requires a parser stack, which gramlib doesn't have. Gramlib seems to give "associative" a different meaning. Right?

wrong

[ia0]

Once we get rid of the bahavior that is deprecated in the current PR, we can get rid of associativities in gramlib

I'm not able to follow this step. I don't see why we need strict associativity (this PR after deprecation) to get rid of associativities in gramlib. It seems to me we could just straight get rid of them now.

So the only "urgent" thing is to get Ltac2 Notation somehow compatible with the new warning

Ok, then if I find time this week-end I'll try to add the AllA variant and make that the default for Ltac2 custom entries. This AllA would behave the same as RightA today.

it's a bit unfortunate that both get implemented in the same time frame

Ah ok, Ltac2 custom entries is something new. That's why I couldn't find anything in the documentation. I was trying Print Custom Grammar mycustom in ltac2/custom_entry.v without success and had to guess what grammar was generated.

About level/rule based: IIRC, the major argument in favor of level based associativity was to reduce the risk of surprising behavior (what happens when mixing left and right associative notations at the same level). I'd say the major argument for rule based would be increased compatibility between libraries (no more dreaded error "level n is left-assoc in library A and right-assoc in library B").

Ok so it really seems rule-based is better, because it should be possible to avoid surprising behavior with a good syntax to describe production rules.

In any case, I tend to think that interface/user facing arguments should come first before implementation cost.

I totally agree.

[proux01]

Once we get rid of the bahavior that is deprecated in the current PR, we can get rid of associativities in gramlib

I'm not able to follow this step. I don't see why we need strict associativity (this PR after deprecation) to get rid of associativities in gramlib. It seems to me we could just straight get rid of them now.

Don't we need to temporarily keep the associativities, at the very least to trigger the warning?

Ah ok, Ltac2 custom entries is something new. That's why I couldn't find anything in the documentation. I was trying Print Custom Grammar mycustom in ltac2/custom_entry.v without success and had to guess what grammar was generated.

Print Grammar (then looking for mycustom) will tell you. Unfortunately the full name contains a dash which prevents Print Grammar custom-ltac2:custom_entry.mycustom to work (we should probably fix that in a separate PR).

Ok so it really seems rule-based is better, because it should be possible to avoid surprising behavior with a good syntax to describe production rules.

Maybe we should also keep a warning like "using left associativity on level xyz previously only used for right associativity" to limit the risk of confusing behavior? But no strong opinion yet.

[ia0]

Once we get rid of the bahavior that is deprecated in the current PR, we can get rid of associativities in gramlib

I'm not able to follow this step. I don't see why we need strict associativity (this PR after deprecation) to get rid of associativities in gramlib. It seems to me we could just straight get rid of them now.

Don't we need to temporarily keep the associativities, at the very least to trigger the warning?

I'm not sure which warning you're talking about. I'm assuming "we can get rid of associativities in gramlib" means we only implement associativities at Rocq-level. To do this, we just need to make every level RIGHTA because the current semantics of RIGHTA is buggy (this PR is fixing it). It has the semantics of FULLA/ALLA which is the one you want if you had to choose only one (which is equivalent to having both associativities), because that's the most permissive and from that one you can either implement left-associativity or right-associativity (but not no-associativity, see below). That's essentially what ltac2 custom entries is doing. So this PR is not needed for that (actually this PR is bad for that, because it fixes RIGHTA to only be right-associativity and not all-associativity).

Actually, only using RIGHTA is not enough. Gramlib needs to be extended to support annotations when a continuation is after SELF or NEXT. It would be like having 3 trees instead of 2:

• start (for rules that don't start with SELF or NEXT)
• self-continue (for rules that start with SELF)
• next-continue (for rules that start with NEXT)

Otherwise we still have the bug that right-associativity is all-associativity and no-associativity is left-associativity.

This change would actually be the change needed to get rid of associativities in Gramlib (thus have rule-based associativities in Gramlib).

Print Grammar (then looking for mycustom) will tell you.

Thanks, I forgot about that. I don't know why company-coq doesn't complete to it.

Maybe we should also keep a warning like "using left associativity on level xyz previously only used for right associativity" to limit the risk of confusing behavior? But no strong opinion yet.

Yes, we'll most probably need some warnings for the transition. But it's not clear to me yet how this is going to happen. I'll need to learn all the quirks of the translation from Rocq notations to Gramlib syntax.

[ia0]

I've pushed a commit that adds BothA (called multi-associativity) that behaves like RightA before this PR, such that this PR can fix RightA to be right-associativity. I'm also making ltac2 custom entries use BothA instead of RightA, thus restoring the current behavior (no warning).

Also I'm using assert false in a lot of places because only ltac2 custom entries should use BothA. It's not reachable by users (but they can see it in Print Grammar of ltac2 custom entries). But maybe some of those assert false are reachable from ltac2 custom entries, I don't know. If that's the case please provide an example (or feel free to replace the assert false with the correct code).

[proux01]

@coqbot merge now

[coqbot-app]

@proux01: You cannot merge this PR because:

• There is still a needs: fixing label.

[proux01]

@coqbot merge now

[coqbot-app]

@proux01: Please take care of the following overlays:

• 21126-ia0-assoc.sh

[ia0]

I'll send a PR to update docgram and refman to fix #21029 and #21072.