Merge PR #12764: A fix and two enhancements of trailing pattern factorization in recursive notations

Reviewed-by: ppedrot

3 files changed, 110 insertions, 18 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index fadfb6c5f4..a6fa6edad5 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -21,6 +21,13 @@ type production_level =
   | NumLevel of int
   | DefaultLevel (** Interpreted differently at the border or inside a rule *)
 
+let production_level_eq lev1 lev2 =
+  match lev1, lev2 with
+  | NextLevel, NextLevel -> true
+  | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+  | DefaultLevel, DefaultLevel -> true
+  | (NextLevel | NumLevel _| DefaultLevel), _ -> false
+
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
@@ -59,19 +66,19 @@ type constr_prod_entry_key =
 (** {5 AST for user-provided entries} *)
 
 type 'a user_symbol =
-| Ulist1 of 'a user_symbol
-| Ulist1sep of 'a user_symbol * string
-| Ulist0 of 'a user_symbol
-| Ulist0sep of 'a user_symbol * string
-| Uopt of 'a user_symbol
-| Uentry of 'a
-| Uentryl of 'a * int
+  | Ulist1 of 'a user_symbol
+  | Ulist1sep of 'a user_symbol * string
+  | Ulist0 of 'a user_symbol
+  | Ulist0sep of 'a user_symbol * string
+  | Uopt of 'a user_symbol
+  | Uentry of 'a
+  | Uentryl of 'a * int
 
 type ('a,'b,'c) ty_user_symbol =
-| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
-| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
-| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
-| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
+  | TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
+  | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
+  | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
diff --git a/parsing/extend.mli b/parsing/extend.mli
new file mode 100644
index 0000000000..057fdb3841
--- /dev/null
+++ b/parsing/extend.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Entry keys for constr notations *)
+
+type side = Left | Right
+
+type production_position =
+  | BorderProd of side * Gramlib.Gramext.g_assoc option
+  | InternalProd
+
+type production_level =
+  | NextLevel
+  | NumLevel of int
+  | DefaultLevel (** Interpreted differently at the border or inside a rule *)
+
+val production_level_eq : production_level -> production_level -> bool
+
+(** User-level types used to tell how to parse or interpret of the non-terminal *)
+
+type 'a constr_entry_key_gen =
+  | ETIdent
+  | ETGlobal
+  | ETBigint
+  | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
+  | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
+  | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
+
+(** Entries level (left-hand side of grammar rules) *)
+
+type constr_entry_key =
+    (production_level * production_position) constr_entry_key_gen
+
+(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+
+type simple_constr_prod_entry_key =
+    production_level constr_entry_key_gen
+
+(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *)
+
+type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list
+
+type binder_target = ForBinder | ForTerm
+
+type constr_prod_entry_key =
+  | ETProdName            (* Parsed as a name (ident or _) *)
+  | ETProdReference       (* Parsed as a global reference *)
+  | ETProdBigint          (* Parsed as an (unbounded) integer *)
+  | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
+  | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
+  | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
+  | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
+
+(** {5 AST for user-provided entries} *)
+
+type 'a user_symbol =
+  | Ulist1 of 'a user_symbol
+  | Ulist1sep of 'a user_symbol * string
+  | Ulist0 of 'a user_symbol
+  | Ulist0sep of 'a user_symbol * string
+  | Uopt of 'a user_symbol
+  | Uentry of 'a
+  | Uentryl of 'a * int
+
+type ('a,'b,'c) ty_user_symbol =
+  | TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
+  | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
+  | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 6cc48d0e48..0bdcd53c92 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -665,15 +665,21 @@ let expand_list_rule s typ tkl x n p ll =
        aux (i+1) (main :: tks @ hds) ll in
   aux 0 [] ll
 
-let is_constr_typ typ x etyps =
+let is_constr_typ (s,lev) x etyps =
   match List.assoc x etyps with
-  | ETConstr (_,_,typ') -> typ = typ'
+  (* TODO: factorize these rules with the ones computing the effective
+     sublevel sent to camlp5, so as to include the case of
+     DefaultLevel which are valid *)
+  | ETConstr (s',_,(lev',InternalProd | (NumLevel _ | NextLevel as lev'), _)) ->
+    Notation.notation_entry_eq s s' && production_level_eq lev lev'
   | _ -> false
 
 let include_possible_similar_trailing_pattern typ etyps sl l =
   let rec aux n = function
   | Terminal s :: sl, Terminal s'::l' when s = s' -> aux n (sl,l')
   | [], NonTerminal x ::l' when is_constr_typ typ x etyps -> try_aux n l'
+  | Break _ :: sl, l -> aux n (sl,l)
+  | sl, Break _ :: l -> aux n (sl,l)
   | _ -> raise Exit
   and try_aux n l =
     try aux (n+1) (sl,l)
@@ -704,8 +710,8 @@ let make_production etyps symbols =
             | Break _ -> []
             | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
         match List.assoc x etyps with
-        | ETConstr (s,_,typ) ->
-            let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in
+        | ETConstr (s,_,(lev,_ as typ)) ->
+            let p,l' = include_possible_similar_trailing_pattern (s,lev) etyps sl l in
             expand_list_rule s typ tkl x 1 p (aux l')
         | ETBinder o ->
             check_open_binder o sl x;