Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)

1 files changed, 34 insertions, 15 deletions

diff --git a/intf/extend.ml b/intf/extend.ml
index 5552bed559..78f0aa1178 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -29,29 +29,48 @@ type production_level =
   | NextLevel
   | NumLevel of int
 
-type ('lev,'pos) constr_entry_key_gen =
-  | ETName | ETReference | ETBigint
-  | ETBinder of bool
-  | ETConstr of ('lev * 'pos)
-  | ETPattern
+type constr_as_binder_kind =
+  | AsIdent
+  | AsIdentOrPattern
+  | AsStrictPattern
+
+(** User-level types used to tell how to parse or interpret of the non-terminal *)
+
+type 'a constr_entry_key_gen =
+  | ETName
+  | ETReference
+  | ETBigint
+  | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
+  | ETConstr of 'a
+  | ETConstrAsBinder of constr_as_binder_kind * 'a
+  | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
   | ETOther of string * string
-  | ETConstrList of ('lev * 'pos) * Tok.t list
-  | ETBinderList of bool * Tok.t list
 
-(** Entries level (left-hand-side of grammar rules) *)
+(** Entries level (left-hand side of grammar rules) *)
 
 type constr_entry_key =
-    (int,unit) constr_entry_key_gen
-
-(** Entries used in productions (in right-hand-side of grammar rules) *)
-
-type constr_prod_entry_key =
-    (production_level,production_position) constr_entry_key_gen
+    (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,unit) constr_entry_key_gen
+    production_level option 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 Tok.t 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 (production_level * production_position) (* Parsed as constr or pattern *)
+  | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
+  | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
+  | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
+  | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
 
 (** {5 AST for user-provided entries} *)