Merge PR #13265: Add support for general non-necessarily-recursive binders in notations

Reviewed-by: ejgallego
Ack-by: Zimmi48
Ack-by: jfehrle

2 files changed, 14 insertions, 21 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index efe4e17d0b..ad6ac8d3f3 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -249,6 +249,7 @@ type (_, _) entry =
 | TTName : ('self, lname) entry
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, string) entry
+| TTBinder : bool -> ('self, kinded_cases_pattern_expr) entry
 | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -364,6 +365,8 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
 | TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
 | TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
+| TTBinder true -> MayRecNo (Pcoq.Symbol.nterm Constr.one_open_binder)
+| TTBinder false -> MayRecNo (Pcoq.Symbol.nterm Constr.one_closed_binder)
 | TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders)
 | TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat)
 | TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
@@ -372,6 +375,7 @@ let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
+| ETProdOneBinder o -> TTAny (TTBinder o)
 | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
 | ETProdPattern p -> TTAny (TTPattern p)
 | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
@@ -385,7 +389,7 @@ let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
-  binders : cases_pattern_expr list;
+  binders : kinded_cases_pattern_expr list;
   binderlists : local_binder_expr list list;
 }
 
@@ -396,14 +400,15 @@ match e with
 | TTConstr _ -> push_constr subst v
 | TTName ->
   begin match forpat with
-  | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders }
+  | ForConstr -> { subst with binders = (cases_pattern_expr_of_name v, Glob_term.Explicit) :: subst.binders }
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
 | TTPattern _ ->
   begin match forpat with
-  | ForConstr -> { subst with binders = v :: subst.binders }
+  | ForConstr -> { subst with binders = (v, Glob_term.Explicit) :: subst.binders }
   | ForPattern -> push_constr subst v
   end
+| TTBinder o -> { subst with binders = v :: subst.binders }
 | TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
 | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
 | TTBigint ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index dc2b2e889e..8759798331 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -342,12 +342,10 @@ let unparsing_metavar i from typs =
   match x with
   | ETConstr _ | ETGlobal | ETBigint ->
      UnpMetaVar (prec,side)
-  | ETPattern _ ->
-     UnpBinderMetaVar prec
-  | ETIdent ->
-     UnpBinderMetaVar prec
-  | ETBinder isopen ->
-     assert false
+  | ETPattern _ | ETIdent ->
+     UnpBinderMetaVar (prec,NotQuotedPattern)
+  | ETBinder _ ->
+     UnpBinderMetaVar (prec,QuotedPattern)
 
 (* Heuristics for building default printing rules *)
 
@@ -636,7 +634,7 @@ let prod_entry_type = function
   | ETIdent -> ETProdName
   | ETGlobal -> ETProdReference
   | ETBigint -> ETProdBigint
-  | ETBinder _ -> assert false (* See check_binder_type *)
+  | ETBinder o -> ETProdOneBinder o
   | ETConstr (s,_,p) -> ETProdConstr (s,p)
   | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
 
@@ -970,15 +968,6 @@ let check_useless_entry_types recvars mainvars etyps =
                   (Id.print x ++ str " is unbound in the notation.")
   | _ -> ()
 
-let check_binder_type recvars etyps =
-  let l1,l2 = List.split recvars in
-  let l = l1@l2 in
-  List.iter (function
-    | (x,ETBinder b) when not (List.mem x l) ->
-       CErrors.user_err (str (if b then "binder" else "closed binder") ++
-                 strbrk " is only for use in recursive notations for binders.")
-    | _ -> ()) etyps
-
 let interp_non_syntax_modifiers mods =
   let set modif (only_parsing,only_printing,entry) = match modif with
     | SetOnlyParsing -> Some (true,only_printing,entry)
@@ -1058,7 +1047,7 @@ let make_interpretation_type isrec isonlybinding default_if_binding = function
   | ETBigint | ETGlobal -> NtnTypeConstr
   | ETBinder _ ->
      if isrec then NtnTypeBinderList
-     else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
+     else NtnTypeBinder NtnParsedAsBinder
 
 let subentry_of_constr_prod_entry from_level = function
   (* Specific 8.2 approximation *)
@@ -1297,7 +1286,6 @@ let compute_syntax_data ~local deprecation df modifiers =
   let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
   let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
   let _ = check_useless_entry_types recvars mainvars mods.etyps in
-  let _ = check_binder_type recvars mods.etyps in
 
   (* Notations for interp and grammar  *)
   let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in