Adding support for parsing subterms of a notation as "pattern".

This allows in particular to define notations with 'pat style binders.

E.g.:

A non-trivial change in this commit is storing binders and patterns
separately from terms.

This is not strictly necessary but has some advantages.

However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).

So, it is as simple to always store idents (and eventually patterns)
as terms.

4 files changed, 13 insertions, 10 deletions

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 2575b71ea..c59828794 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 *)
@@ -128,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 79bbbd376..5258ef56b 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -37,13 +37,13 @@ type ('lev,'pos) constr_entry_key_gen =
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of ('lev * 'pos)
-  | ETPattern
+  | ETPattern of int
   | ETOther of string * string
 
-(** 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
+    (production_level,production_position) constr_entry_key_gen
 
 (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
 
@@ -54,12 +54,14 @@ type simple_constr_prod_entry_key =
 
 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                  (* Parsed as pattern (as subpart of a constr) *)
+  | 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 *)
diff --git a/intf/intf.mllib b/intf/intf.mllib
index 38a2a71cc..2b8960d3f 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 52fd0f368..83cc454f4 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -61,13 +61,13 @@ 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_var_instance_type =
-  | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList
+  | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList
 
 (** 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 =
@@ -95,7 +95,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 *)