Only accept SELF on the left for left-associative levels

dev/ci/user-overlays/21126-ia0-assoc.sh

@@ -0,0 +1,2 @@
+overlay coq_lsp https://github.com/proux01/coq-lsp rocq21126 21126
+overlay autosubst_ocaml https://github.com/proux01/autosubst-ocaml rocq21126 21126

doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst

@@ -1587,7 +1587,7 @@ dependently-typed style:
 
 .. rocqtop:: in
 
-   Notation " t --> t' " := (arrow t t') (at level 20, t' at next level).
+   Notation " t --> t' " := (arrow t t') (at level 20, right associativity).
 
 .. rocqtop:: in
 
@@ -1597,7 +1597,7 @@ dependently-typed style:
 
 .. rocqtop:: in
 
-   Notation " G , tau " := (snoc G tau) (at level 20, tau at next level).
+   Notation " G , tau " := (snoc G tau) (at level 21, left associativity).
 
 .. rocqtop:: in
 
@@ -1609,7 +1609,7 @@ dependently-typed style:
 
 .. rocqtop:: in
 
-   Notation " G ; D " := (conc G D) (at level 20).
+   Notation " G ; D " := (conc G D) (at level 21).
 
 .. rocqtop:: in
 

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -1262,11 +1262,11 @@ Custom entries
       | Add : Expr -> Expr -> Expr.
 
       Declare Custom Entry expr.
-      Notation "[ e ]" := e (e custom expr at level 2).
+      Notation "[ e ]" := e (e custom expr at level 3).
       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, x at level 2).
+      Notation "( x )" := x (in custom expr, x at level 3).
       Notation "{ x }" := x (in custom expr, x constr).
       Notation "x" := x (in custom expr at level 0, x ident).
 
@@ -1329,9 +1329,9 @@ main grammar, or from another custom entry as is the case in
 
 .. rocqtop:: in
 
-   Notation "[ e ]" := e (e custom expr at level 2).
+   Notation "[ e ]" := e (e custom expr at level 3).
 
-to indicate that ``e`` has to be parsed at level ``2`` of the grammar
+to indicate that ``e`` has to be parsed at level ``3`` of the grammar
 associated with the custom entry ``expr``. The level can be omitted, as in
 
 .. rocqdoc::
@@ -1361,7 +1361,7 @@ right-hand side, as it is the case above for
 
 .. rocqtop:: in
 
-   Notation "( x )" := x (in custom expr at level 0, x at level 2).
+   Notation "( x )" := x (in custom expr at level 0, x at level 3).
 
 and
 
@@ -1376,10 +1376,10 @@ in another grammar or in another level of the current grammar. For instance,
 
 .. rocqtop:: in
 
-   Notation "( x )" := x (in custom expr at level 0, x at level 2).
+   Notation "( x )" := x (in custom expr at level 0, x at level 3).
 
 tells that parentheses can be inserted to parse or print an expression
-declared at level ``2`` of ``expr`` whenever this expression is
+declared at level ``3`` of ``expr`` whenever this expression is
 expected to be used as a subterm at level 0 or 1.  This allows for
 instance to parse and print :g:`Add x y` as a subterm of :g:`Mul (Add
 x y) z` using the syntax ``(x + y) z``. Similarly,

doc/tools/docgram/common.edit_mlg

@@ -2486,7 +2486,7 @@ RENAME: [
 | ltac2_expr6 ltac2_expr
 | starredidentref starred_ident_ref
 | constr_pattern one_pattern
-| hints_path hints_regexp
+| hints_path_entry hints_regexp
 | clause_dft_concl occurrences
 | in_clause goal_occurrences
 | unfold_occ reference_occs

doc/tools/docgram/fullGrammar

@@ -639,7 +639,7 @@ command: [
 | "Declare" "Equivalent" "Keys" constr constr
 | "Print" "Equivalent" "Keys"
 | "infoH" tactic
-| "Hint" "Cut" "[" hints_path "]" opthints
+| "Hint" "Cut" "[" hints_path_entry "]" opthints
 | "Typeclasses" "Transparent" LIST1 reference
 | "Typeclasses" "Opaque" LIST1 reference
 | "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural
@@ -2112,15 +2112,23 @@ auto_using: [
 |
 ]
 
-hints_path: [
-| "(" hints_path ")"
-| hints_path "*"
+hints_path_entry: [
+| hints_path1
+]
+
+hints_path1: [
+| hints_path1 "*"
+| hints_path1 "|" hints_path0
+| hints_path1 hints_path0
+| hints_path0
+]
+
+hints_path0: [
+| "(" hints_path1 ")"
 | "emp"
 | "eps"
-| hints_path "|" hints_path
 | LIST1 global
 | "_"
-| hints_path hints_path
 ]
 
 opthints: [

doc/tools/docgram/orderedGrammar

@@ -1297,14 +1297,22 @@ number_string_via: [
 ]
 
 hints_regexp: [
-| LIST1 qualid
-| "_"
-| hints_regexp "|" hints_regexp
-| hints_regexp hints_regexp
-| hints_regexp "*"
+| hints_path1
+]
+
+hints_path1: [
+| hints_path1 "*"
+| hints_path1 "|" hints_path0
+| hints_path1 hints_path0
+| hints_path0
+]
+
+hints_path0: [
+| "(" hints_path1 ")"
 | "emp"
 | "eps"
-| "(" hints_regexp ")"
+| LIST1 qualid
+| "_"
 ]
 
 coercion_class: [

gramlib/gramext.ml

@@ -8,9 +8,20 @@ type position =
   | Before of string
   | After of string
 
-type g_assoc = NonA | RightA | LeftA
+type g_assoc = NonA | RightA | LeftA | BothA
 
 let pr_assoc = function
+  | BothA -> Pp.str "multi associativity"
   | LeftA -> Pp.str "left associativity"
   | RightA -> Pp.str "right associativity"
   | NonA -> Pp.str "no associativity"
+
+(** Returns whether SELF means SELF, respectively on the left and on the right. *)
+let split_assoc = function
+  | BothA -> (true, true)
+  | LeftA -> (true, false)
+  | RightA -> (false, true)
+  | NonA -> (false, false)
+
+let self_on_the_left assoc = fst (split_assoc assoc)
+let self_on_the_right assoc = snd (split_assoc assoc)

gramlib/gramext.mli

@@ -8,7 +8,13 @@ type position =
   | Before of string
   | After of string
 
-type g_assoc = NonA | RightA | LeftA
+type g_assoc = NonA | RightA | LeftA | BothA
 
 val pr_assoc : g_assoc -> Pp.t
 (** Prints a [g_assoc] value. *)
+
+val self_on_the_left : g_assoc -> bool
+(** Returns whether SELF means SELF on the left. *)
+
+val self_on_the_right : g_assoc -> bool
+(** Returns whether SELF means SELF on the right. *)

gramlib/grammar.ml

@@ -870,7 +870,8 @@ let print_levels ppf elev =
          | None -> ()
        end;
        begin match lev.assoc with
-           LeftA -> fprintf ppf "LEFTA"
+           BothA -> fprintf ppf "BOTHA"
+         | LeftA -> fprintf ppf "LEFTA"
          | RightA -> fprintf ppf "RIGHTA"
          | NonA -> fprintf ppf "NONA"
        end;
@@ -1047,25 +1048,34 @@ let top_tree : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> (s, tr, a) ty_tr
 let warn_tolerance =
   CWarnings.(create_in (create_warning ~name:"level-tolerance"
                           ~from:[CoreCategories.parsing; Deprecation.Version.v9_2] ())
-    Pp.(fun (e, msg) ->
+    ~quickfix:(fun ~loc (_, _, qf) -> qf)
+    Pp.(fun (e, msg, _) ->
         strbrk "In " ++ str e ++ str ", tolerating this expression at" ++
-        strbrk " a higher level than expected." ++
-        pr_opt (fun m -> strbrk (" " ^ m)) msg ++
+        strbrk " a higher level than expected " ++ strbrk msg ++ str "." ++
         strbrk " This tolerance will be eventually removed." ++
         strbrk " Insert parentheses or try to lower the level at which the top symbol of this expression is parsed."))
 
-let warn_recover ename bp strm__ =
-  let ep = LStream.count strm__ in
+let warn_recover_qf ename bp ?ep strm__ msg =
+  let has_ep = Option.has_some ep in
+  let ep = Option.default (LStream.count strm__) ep in
   let loc = LStream.interval_loc bp ep strm__ in
-  warn_tolerance ~loc (ename, None)
+  let qf =
+    let paren_enames = ["term"; "pattern"; "ltac_expr"] in
+    if not (has_ep && List.mem ename paren_enames) then [] else
+      let qf le s = Quickfix.make ~loc:(le loc 0 0) (Pp.str s) in
+      [qf Loc.sub "("; qf Loc.after ")"] in
+  warn_tolerance ~loc (ename, msg, qf)
 
-let warn_recover_continuation ename bp ep strm__ =
-  let loc = LStream.interval_loc bp ep strm__ in
-  warn_tolerance ~loc (ename, None)
+let warn_recover ename bp ?ep strm__ =
+  warn_recover_qf ename bp ?ep strm__ "by the notation started on the left"
+
+let warn_recover_continuation ename bp ep strm__ strict =
+  let msg = "by the notation continuing on the right"
+    ^ if not strict then "" else " (which is not left-associative)" in
+  warn_recover_qf ename bp ~ep strm__ msg
 
 let warn_recover_last_start ename bp ep strm__ =
-  let loc = LStream.interval_loc bp ep strm__ in
-  warn_tolerance ~loc (ename, Some "(there is no next level of last level)")
+  warn_recover_qf ename bp ~ep strm__ "(there is no next level of last level)"
 
 let empty_entry ename levn strm =
   raise (ParseError ("entry [" ^ ename ^ "] is empty"))
@@ -1165,9 +1175,10 @@ and parser_cont : type s tr tr' a r.
           let* s' = entry_of_symb entry s in
           continue_parser_of_entry gstate s' None 0 bp a0 strm__
         in
+        let ep = LStream.count strm__ in
         let a = or_fail a0 a in
         let act = or_fail a (p1 gstate strm__) in
-        warn_recover entry.ename bp strm__;
+        warn_recover entry.ename bp ~ep strm__;
         Ok (act a)
 
 (** [parser_of_token_list] attempts to look-ahead an arbitrary-long
@@ -1389,11 +1400,7 @@ let rec start_parser_of_levels entry clevn =
       match lev.lprefix with
         DeadEnd -> p1
       | tree ->
-          let alevn =
-            match lev.assoc with
-              LeftA | NonA -> succ clevn
-            | RightA -> clevn
-          in
+          let alevn = if self_on_the_right lev.assoc then clevn else succ clevn in
           let p2 = parser_of_tree entry (succ clevn) alevn tree in
           match levs with
             [] ->
@@ -1445,18 +1452,19 @@ let rec continue_parser_of_levels entry clevn =
       match lev.lsuffix with
         DeadEnd -> p1
       | tree ->
-          let alevn =
-            match lev.assoc with
-              LeftA | NonA -> succ clevn
-            | RightA -> clevn
-          in
+          let alevn = if self_on_the_right lev.assoc then clevn else succ clevn in
           let p2 = parser_of_tree entry (succ clevn) alevn tree in
           fun gstate levfrom levn bp a strm ->
+            let tolerance = match levfrom with
+              | Some levfrom when levfrom = clevn && not (self_on_the_left lev.assoc) -> Some true
+              | Some levfrom when levfrom < clevn -> Some false
+              | _ -> None
+            in
             (* Apply the lsuffix continuation if the level is in the interval [levn;levfrom] *)
             if levn > clevn then
               (* Skip rules before [levn] *)
               p1 gstate levfrom levn bp a strm
-            else if (not gstate.recover && match levfrom with Some levfrom -> levfrom < clevn | None -> false) then
+            else if (not gstate.recover && Option.has_some tolerance) then
               Error ()
             else
               let (strm__ : _ LStream.t) = strm in
@@ -1472,11 +1480,7 @@ let rec continue_parser_of_levels entry clevn =
                       continue_parser_of_entry gstate entry (Some (clevn-1)) levn bp a strm
                   else
                     continue_parser_of_entry gstate entry (Some clevn) levn bp a strm in
-              let () = match levfrom with
-                | Some levfrom when levfrom < clevn ->
-                  warn_recover_continuation entry.ename bp ep strm__
-                | _ -> ()
-              in
+              let () = Option.iter (warn_recover_continuation entry.ename bp ep strm__) tolerance in
               c
 
 let make_continue_parser_of_entry entry = function

plugins/ltac/g_auto.mlg

@@ -12,6 +12,7 @@
 
 open Pp
 open Stdarg
+open Procq
 open Procq.Prim
 open Procq.Constr
 open Pltac
@@ -162,19 +163,31 @@ END
 
 let pr_pre_hints_path c = Hints.pp_hints_path_gen Libnames.pr_qualid c
 
+let hints_path = Entry.make "hints_path"
+
 }
 
-VERNAC ARGUMENT EXTEND hints_path
+VERNAC ARGUMENT EXTEND hints_path_entry
 PRINTED BY { pr_pre_hints_path }
-
-| [ "(" hints_path(p) ")"  ] -> { p }
-| [ hints_path(p) "*" ] -> { Hints.PathStar p }
-| [ "emp" ] -> { Hints.PathEmpty }
-| [ "eps" ] -> { Hints.PathEpsilon }
-| [ hints_path(p) "|" hints_path(q) ] -> { Hints.PathOr (p, q) }
-| [ ne_global_list(g) ] -> { Hints.PathAtom (Hints.PathHints g) }
-| [ "_" ] -> { Hints.PathAtom Hints.PathAny }
-| [ hints_path(p) hints_path(q) ] -> { Hints.PathSeq (p, q) }
+| [ hints_path(p) ] -> { p }
+END
+
+GRAMMAR EXTEND Gram
+  GLOBAL: hints_path;
+  hints_path:
+    [ "1" LEFTA
+      [ p = hints_path; "*" -> { Hints.PathStar p }
+      | p = hints_path; "|"; q = hints_path LEVEL "0" -> { Hints.PathOr (p, q) }
+      | p = hints_path; q = hints_path LEVEL "0" -> { Hints.PathSeq (p, q) }
+      ]
+    | "0" NONA
+      [ "("; p = hints_path; ")" -> { p }
+      | IDENT "emp" -> { Hints.PathEmpty }
+      | IDENT "eps" -> { Hints.PathEpsilon }
+      | g = LIST1 global -> { Hints.PathAtom (Hints.PathHints g) }
+      | "_" -> { Hints.PathAtom Hints.PathAny }
+      ]
+    ];
 END
 
 ARGUMENT EXTEND opthints
@@ -185,7 +198,7 @@ ARGUMENT EXTEND opthints
 END
 
 VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| #[ locality = Attributes.hint_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
+| #[ locality = Attributes.hint_locality; ] [ "Hint" "Cut" "[" hints_path_entry(p) "]" opthints(dbnames) ] -> {
   let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
   Hints.add_hints ~locality
     (match dbnames with None -> ["core"] | Some l -> l) entry;

plugins/ltac/g_auto.mli

@@ -21,7 +21,7 @@ val wit_auto_using :
 
 val auto_using : Constrexpr.constr_expr list Procq.Entry.t
 
-val wit_hints_path :
+val wit_hints_path_entry :
   Libnames.qualid Hints.hints_path_gen Genarg.vernac_genarg_type
 
 val hints_path : Libnames.qualid Hints.hints_path_gen Procq.Entry.t

plugins/ltac2/g_ltac2.mlg

@@ -146,7 +146,7 @@ GRAMMAR EXTEND Gram
   GLOBAL: ltac2_expr ltac2_type tac2def_val tac2def_typ tac2def_ext tac2def_syn tac2abbrev_syn
           tac2def_mut tac2expr_in_env ltac2_atom;
   tac2pat:
-    [ "3" NONA
+    [ "3" LEFTA
       [ p = tac2pat; "|"; pl = LIST1 tac2pat LEVEL "2" SEP "|" ->
         { let pl = p :: pl in
           CAst.make ~loc @@ CPatOr pl }