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

6 files changed, 59 insertions, 31 deletions

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index fbf9e248ab..c598287943 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -46,7 +46,7 @@ type prim_token =
 type instance_expr = Misctypes.glob_level list
 
 type cases_pattern_expr_r =
-  | CPatAlias of cases_pattern_expr * Id.t
+  | CPatAlias of cases_pattern_expr * Name.t Loc.located
   | CPatCstr  of reference
     * cases_pattern_expr list option * cases_pattern_expr list
   (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
@@ -70,8 +70,8 @@ and constr_expr_r =
   | CRef     of reference * instance_expr option
   | CFix     of Id.t Loc.located * fix_expr list
   | CCoFix   of Id.t Loc.located * cofix_expr list
-  | CProdN   of binder_expr list * constr_expr
-  | CLambdaN of binder_expr list * constr_expr
+  | CProdN   of local_binder_expr list * constr_expr
+  | CLambdaN of local_binder_expr list * constr_expr
   | CLetIn   of Name.t Loc.located * constr_expr * constr_expr option * constr_expr
   | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
   | CApp     of (proj_flag * constr_expr) *
@@ -107,9 +107,6 @@ and case_expr = constr_expr                 (* expression that is being matched
 and branch_expr =
   (cases_pattern_expr list list * constr_expr) Loc.located
 
-and binder_expr =
-  Name.t Loc.located list * binder_kind * constr_expr
-
 and fix_expr =
     Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) *
       local_binder_expr list * constr_expr * constr_expr
@@ -131,7 +128,8 @@ and local_binder_expr =
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
     constr_expr list list * (** for recursive notations *)
-    local_binder_expr list list (** for binders subexpressions *)
+    cases_pattern_expr list *   (** for binders *)
+    local_binder_expr list list (** for binder lists (recursive notations) *)
 
 type constr_pattern_expr = constr_expr
 
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} *)
 
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 61bbe2c264..3f48fa5479 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -105,7 +105,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g
 type 'a extended_glob_local_binder_r =
   | GLocalAssum   of Name.t * binding_kind * 'a glob_constr_g
   | GLocalDef     of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option
-  | GLocalPattern of ('a cases_pattern_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g
+  | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g
 and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t
 
 type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g
diff --git a/intf/intf.mllib b/intf/intf.mllib
index 38a2a71cc0..2b8960d3f2 100644
--- a/intf/intf.mllib
+++ b/intf/intf.mllib
@@ -2,9 +2,9 @@ Constrexpr
 Evar_kinds
 Genredexpr
 Locus
+Extend
 Notation_term
 Decl_kinds
-Extend
 Glob_term
 Misctypes
 Pattern
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index cad6f4b821..86f5adbd78 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -25,11 +25,11 @@ type notation_constr =
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
-  | NList of Id.t * Id.t * notation_constr * notation_constr * bool
+  | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   (** Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
   | NProd of Name.t * notation_constr * notation_constr
-  | NBinderList of Id.t * Id.t * notation_constr * notation_constr
+  | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
   | NCases of Constr.case_style * notation_constr option *
       (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
@@ -60,21 +60,31 @@ type subscopes = tmp_scope_name option * scope_name list
 
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
+
+type notation_binder_source =
+  (* This accepts only pattern *)
+  (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
+  | NtnParsedAsPattern of bool
+  (* This accepts only ident *)
+  | NtnParsedAsIdent
+  (* This accepts ident, or pattern, or both *)
+  | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
+
 type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList
+  | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
 
-(** Type of variables when interpreting a constr_expr as an notation_constr:
+(** Type of variables when interpreting a constr_expr as a notation_constr:
     in a recursive pattern x..y, both x and y carry the individual type
     of each element of the list x..y *)
 type notation_var_internalization_type =
-  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
+  | NtnInternTypeAny | NtnInternTypeOnlyBinder
 
 (** This characterizes to what a notation is interpreted to *)
 type interpretation =
     (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
 
-type reversibility_flag = bool
+type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
 
 type notation_interp_env = {
   ninterp_var_type : notation_var_internalization_type Id.Map.t;
@@ -95,7 +105,7 @@ type precedence = int
 type parenRelation = L | E | Any | Prec of precedence
 type tolerability = precedence * parenRelation
 
-type level = precedence * tolerability list * notation_var_internalization_type list
+type level = precedence * tolerability list * Extend.constr_entry_key list
 
 (** Grammar rules for a notation *)
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 8e0fe54c55..d16c9bb802 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -214,6 +214,7 @@ type proof_expr =
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
+  | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option
   | SetLevel of int
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key