Do not tolerate SELF on the left of right-associative levels

ia0 · ia0 · commit 2273226ed8f4 · 2025-10-13T21:40:02.000+02:00
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
@@ -1452,6 +1452,9 @@ let rec continue_parser_of_levels entry clevn =
           in
           let p2 = parser_of_tree entry (succ clevn) alevn tree in
           fun gstate levfrom levn bp a strm ->
+            (* Adjust levfrom based on its associativity. *)
+            let levfrom = if levfrom = Some clevn && lev.assoc <> LeftA
+                          then Some(clevn - 1) else levfrom in
             (* Apply the lsuffix continuation if the level is in the interval [levn;levfrom] *)
             if levn > clevn then
               (* Skip rules before [levn] *)
diff --git a/test-suite/ltac2/fragile_matching.v b/test-suite/ltac2/fragile_matching.v
@@ -117,10 +117,6 @@ End RealCodeTest.
 Module Parsing.
   (* additional parsing tests not from ocaml *)
 
-  (* the first command should not parse as the second *)
-  Ltac2 Eval fun x => match x with _ :: _ | _ as x => x end.
-  Fail Ltac2 Eval fun x => match x with _ :: _ | (_ as x) => x end.
-
   (* #21045 *)
   Ltac2 Eval match [10; 20; 30; 40] with x :: y :: z => x :: y :: z | _ => [] end.
 
diff --git a/test-suite/output-coqtop/StrictAssociativity.out b/test-suite/output-coqtop/StrictAssociativity.out
@@ -172,8 +172,13 @@ 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]
 
-Rocq < Rocq < Reject 60 (F E)
-     : Parsing
+Rocq < Rocq < Toplevel input, characters 20-25:
+> Check Reject 60 [2 atom2 post12 ].
+>                    ^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Accept 61 (F E)
      : Parsing
@@ -208,8 +213,13 @@ 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]
 
-Rocq < Rocq < Reject 80 (G E E)
-     : Parsing
+Rocq < Rocq < Toplevel input, characters 20-25:
+> Check Reject 80 [3 atom3 op22 atom2 ].
+>                    ^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Toplevel input, characters 30-35:
 > Check Reject 81 [3 atom2 op22 atom3 ].
@@ -230,8 +240,13 @@ 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]
 
-Rocq < Rocq < Reject 90 (G E E)
-     : Parsing
+Rocq < Rocq < Toplevel input, characters 20-25:
+> Check Reject 90 [2 atom2 op12 atom2 ].
+>                    ^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Toplevel input, characters 30-35:
 > Check Reject 91 [2 atom1 op12 atom3 ].
@@ -279,20 +294,40 @@ 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]
 
-Rocq < Rocq < Reject 110 (F (G E E))
-     : Parsing
+Rocq < Rocq < Toplevel input, characters 27-32:
+> Check Reject 110 [2 pre22 atom2 op12 atom2 ].
+>                           ^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
-Rocq < Reject 111 (G (F E) E)
-     : Parsing
+Rocq < Toplevel input, characters 20-31:
+> Check Reject 111 [2 pre21 atom1 op12 atom2 ].
+>                     ^^^^^^^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Accept 112 (F (G E E))
      : Parsing
 
-Rocq < Rocq < Reject 120 (G (F E) E)
-     : Parsing
+Rocq < Rocq < Toplevel input, characters 21-33:
+> Check Reject 120 [2 atom2 post12 op12 atom2 ].
+>                     ^^^^^^^^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
-Rocq < Reject 121 (G (F E) E)
-     : Parsing
+Rocq < Toplevel input, characters 20-32:
+> Check Reject 121 [2 atom1 post12 op12 atom2 ].
+>                     ^^^^^^^^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Accept 122 (G (F E) E)
      : Parsing
@@ -311,8 +346,13 @@ try to lower the level at which the top symbol of this expression is parsed.
 Rocq < Accept 132 (G E (F E))
      : Parsing
 
-Rocq < Rocq < Reject 140 (G E (F E))
-     : Parsing
+Rocq < Rocq < Toplevel input, characters 32-37:
+> Check Reject 140 [2 atom1 op12 atom2 post12 ].
+>                                ^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Accept 141 (G E (F E))
      : Parsing
@@ -383,8 +423,13 @@ the level at which the top symbol of this expression is parsed.
 Rocq < Accept 182 (F (G E E))
      : Parsing
 
-Rocq < Rocq < Reject 190 (G E (G E E))
-     : Parsing
+Rocq < Rocq < Toplevel input, characters 32-37:
+> Check Reject 190 [2 atom1 op12 atom2 op12 atom2 ].
+>                                ^^^^^
+Error: In custom:Top.expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Accept 191 (G E (G E E))
      : Parsing
@@ -849,11 +894,13 @@ where
 ?A : [ |- Type]
 ?Goal : [ |- ?A]
 
-Rocq < Rocq < Reject 1100 ?Goal
-     : Parsing
-where
-?A : [ |- Type]
-?Goal : [ |- ?A]
+Rocq < Rocq < Toplevel input, characters 25-30:
+> Check Reject 1100 ltac:(atom2 + atom2).
+>                         ^^^^^
+Error: In ltac_expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Toplevel input, characters 32-37:
 > Check Reject 1101 ltac:(atom1 + atom3).
@@ -875,17 +922,21 @@ where
 ?A : [ |- Type]
 ?Goal : [ |- ?A]
 
-Rocq < Rocq < Reject 1110 ?Goal
-     : Parsing
-where
-?A : [ |- Type]
-?Goal : [ |- ?A]
+Rocq < Rocq < Toplevel input, characters 31-36:
+> Check Reject 1110 ltac:(pre22 atom2 + atom2).
+>                               ^^^^^
+Error: In ltac_expr, tolerating this expression at a higher level than
+expected. 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]
 
-Rocq < Reject 1111 ?Goal
-     : Parsing
-where
-?A : [ |- Type]
-?Goal : [ |- ?A]
+Rocq < Toplevel input, characters 24-35:
+> Check Reject 1111 ltac:(pre21 atom1 + atom2).
+>                         ^^^^^^^^^^^
+Error: In ltac_expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Accept 1112 ?Goal
      : Parsing
@@ -899,17 +950,21 @@ where
 ?A : [ |- Type]
 ?Goal : [ |- ?A]
 
-Rocq < Rocq < Reject 1120 ?Goal
-     : Parsing
-where
-?A : [ |- Type]
-?Goal : [ |- ?A]
+Rocq < Rocq < Toplevel input, characters 25-37:
+> Check Reject 1120 ltac:(atom1 post12 + atom2).
+>                         ^^^^^^^^^^^^
+Error: In ltac_expr, tolerating this expression at a higher level than
+expected. 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]
 
-Rocq < Reject 1121 ?Goal
-     : Parsing
-where
-?A : [ |- Type]
-?Goal : [ |- ?A]
+Rocq < Toplevel input, characters 32-37:
+> Check Reject 1121 ltac:(atom1 + atom2 post12).
+>                                 ^^^^^
+Error: In ltac_expr, tolerating this expression at a higher level than
+expected. 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]
 
 Rocq < Accept 1122 ?Goal
      : Parsing
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
@@ -49,10 +49,10 @@ Inductive Expr :=
  | One : Expr.
 
 Declare Custom Entry expr.
+Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
 Notation "[ expr ]" := expr (expr custom expr at level 2).
 Notation "1" := One (in custom expr at level 0).
 Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity).
-Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
 Notation "( x )" := x (in custom expr at level 0, x at level 2).
 Notation "{ x }" := x (in custom expr at level 0, x constr).
 Notation "x" := x (in custom expr at level 0, x ident).
diff --git a/test-suite/output/PrintNotation.out b/test-suite/output/PrintNotation.out
@@ -1,5 +1,10 @@
 Notation "_ $ _" at level 123 with arguments constr at next level, constr
 at next level, no associativity.
+File "./output/PrintNotation.v", line 8, characters 9-14:
+Warning: In term, tolerating this expression at a higher level than expected.
+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]
 bar (bar ?f ?f0) ?f1
      : foo
 where
@@ -8,6 +13,11 @@ where
 ?f1 : [ |- foo]
 Notation "_ $ _" at level 123 with arguments constr at next level, constr
 at next level, no associativity.
+File "./output/PrintNotation.v", line 17, characters 9-14:
+Warning: In term, tolerating this expression at a higher level than expected.
+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]
 bar (bar ?f ?f0) ?f1
      : foo
 where
diff --git a/test-suite/output/ltac2_match.out b/test-suite/output/ltac2_match.out
@@ -1,4 +1,4 @@
-File "./output/ltac2_match.v", line 12, characters 41-42:
+File "./output/ltac2_match.v", line 12, characters 43-44:
 Warning: This pattern is redundant. [redundant-pattern,ltac2,default]
 File "./output/ltac2_match.v", line 34, characters 5-51:
 Warning: This clause is redundant. [redundant-pattern,ltac2,default]
diff --git a/test-suite/output/ltac2_match.v b/test-suite/output/ltac2_match.v
@@ -9,7 +9,7 @@ Ltac2 rec autre x := match x with
 | D,D,_ => 3
 | (D|(F _ _)|(H _)|K _),_,_ => 4
 | (_, (D|I|E _|F _ _|H _|K _), _) => 8
-| (J,J,((C|D) as x |E x|F _ x)) | (J,_,((C|J) as x)) => autre (x,x,x)
+| (J,J,(((C|D) as x) |E x|F _ x)) | (J,_,((C|J) as x)) => autre (x,x,x)
 | (J, J, (I|H _|K _)) => 9
 | I,_,_ => 6
 | E _,_,_ => 7

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-File "./output/ltac2_match.v", line 12, characters 41-42:`
	`1`	`+File "./output/ltac2_match.v", line 12, characters 43-44:`
`2`	`2`	`Warning: This pattern is redundant. [redundant-pattern,ltac2,default]`
`3`	`3`	`File "./output/ltac2_match.v", line 34, characters 5-51:`
`4`	`4`	`Warning: This clause is redundant. [redundant-pattern,ltac2,default]`