Fixing printing part of #13078 (anomaly with binding notations in patterns).

We prevent notations involving binders (i.e. names or patterns) to be
used for printing in "match" patterns. The computation is done in
"has_no_binders_type", controlling uninterpretation.

7 files changed, 57 insertions, 25 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index d57c4f3abf..e6258a2791 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -341,22 +341,27 @@ type notation_rule = interp_rule * interpretation * notation_applicative_status
 let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) =
   x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2)
 
+let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) =
+  (* No need in principle to compare also_cases as it is inferred *)
+  also_cases1 = also_cases2 && notation_rule_eq rule1 rule2
+
 let keymap_add key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
   (* In case of re-import, no need to keep the previous copy *)
-  let old = try List.remove_first (notation_rule_eq interp) old with Not_found -> old in
+  let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in
   KeyMap.add key (interp :: old) map
 
 let keymap_remove key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
-  KeyMap.add key (List.remove_first (notation_rule_eq interp) old) map
+  KeyMap.add key (List.remove_first (also_cases_notation_rule_eq interp) old) map
 
 let keymap_find key map =
   try KeyMap.find key map
   with Not_found -> []
 
 (* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
+(* Boolean = for cases pattern also *)
+let notations_key_table = ref (KeyMap.empty : (bool * notation_rule) list KeyMap.t)
 
 let glob_prim_constr_key c = match DAst.get c with
   | GRef (ref, _) -> Some (canonical_gr ref)
@@ -1333,13 +1338,13 @@ let check_printing_override (scopt,ntn) data parsingdata printingdata =
     exists) printingdata in
   parsing_update, exists
 
-let remove_uninterpretation rule (metas,c as pat) =
+let remove_uninterpretation rule also_in_cases_pattern (metas,c as pat) =
   let (key,n) = notation_constr_key c in
-  notations_key_table := keymap_remove key (rule,pat,n) !notations_key_table
+  notations_key_table := keymap_remove key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table
 
-let declare_uninterpretation rule (metas,c as pat) =
+let declare_uninterpretation ?(also_in_cases_pattern=true) rule (metas,c as pat) =
   let (key,n) = notation_constr_key c in
-  notations_key_table := keymap_add key (rule,pat,n) !notations_key_table
+  notations_key_table := keymap_add key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table
 
 let update_notation_data (scopt,ntn) use data table =
   let (parsingdata,printingdata) =
@@ -1448,14 +1453,17 @@ let interp_notation ?loc ntn local_scopes =
       (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
 let uninterp_notations c =
-  List.map_append (fun key -> keymap_find key !notations_key_table)
+  List.map_append (fun key -> List.map snd (keymap_find key !notations_key_table))
     (glob_constr_keys c)
 
+let filter_also_for_pattern =
+  List.map_filter (function (true,x) -> Some x | _ -> None)
+
 let uninterp_cases_pattern_notations c =
-  keymap_find (cases_pattern_key c) !notations_key_table
+  filter_also_for_pattern (keymap_find (cases_pattern_key c) !notations_key_table)
 
 let uninterp_ind_pattern_notations ind =
-  keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table
+  filter_also_for_pattern (keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table)
 
 let has_active_parsing_rule_in_scope ntn sc =
   try
@@ -1615,7 +1623,7 @@ type entry_coercion_kind =
   | IsEntryGlobal of string * int
   | IsEntryIdent of string * int
 
-let declare_notation (scopt,ntn) pat df ~use coe deprecation =
+let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecation =
   (* Register the interpretation *)
   let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in
   let sc = find_scope scope in
@@ -1630,10 +1638,10 @@ let declare_notation (scopt,ntn) pat df ~use coe deprecation =
     scope_map := String.Map.add scope sc !scope_map;
   (* Update the uninterpretation cache *)
   begin match printing_update with
-  | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) pat
+  | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat
   | None -> ()
   end;
-  if not exists && use <> OnlyParsing then declare_uninterpretation (NotationRule (scopt,ntn)) pat;
+  if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
   (* Register visibility of lonely notations *)
   if not exists then begin match scopt with
   | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
diff --git a/interp/notation.mli b/interp/notation.mli
index d744ff41d9..4d6d640a2d 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -234,7 +234,7 @@ type notation_use =
   | OnlyParsing
   | ParsingAndPrinting
 
-val declare_uninterpretation : interp_rule -> interpretation -> unit
+val declare_uninterpretation : ?also_in_cases_pattern:bool -> interp_rule -> interpretation -> unit
 
 type entry_coercion_kind =
   | IsEntryCoercion of notation_entry_level
@@ -243,6 +243,7 @@ type entry_coercion_kind =
 
 val declare_notation : notation_with_optional_scope * notation ->
   interpretation -> notation_location -> use:notation_use ->
+  also_in_cases_pattern:bool ->
   entry_coercion_kind option ->
   Deprecation.t option -> unit
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 354809252e..3ea3f3ccff 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1436,9 +1436,8 @@ let reorder_canonically_substitution terms termlists metas =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
     match typ with
       | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
-      | NtnTypeBinder _ -> assert false
       | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
-      | NtnTypeBinderList -> assert false)
+      | NtnTypeBinder _ | NtnTypeBinderList -> anomaly (str "Unexpected binder in pattern notation."))
     metas ([],[])
 
 let match_notation_constr_cases_pattern c (metas,pat) =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index bd3e234a91..f3ad3546ff 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -22,6 +22,7 @@ type syndef =
   { syndef_pattern : interpretation;
     syndef_onlyparsing : bool;
     syndef_deprecation : Deprecation.t option;
+    syndef_also_in_cases_pattern : bool;
   }
 
 let syntax_table =
@@ -52,7 +53,7 @@ let open_syntax_constant i ((sp,kn),(_local,syndef)) =
     if not syndef.syndef_onlyparsing then
       (* Redeclare it to be used as (short) name in case an other (distfix)
          notation was declared in between *)
-      Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+      Notation.declare_uninterpretation ~also_in_cases_pattern:syndef.syndef_also_in_cases_pattern (Notation.SynDefRule kn) pat
   end
 
 let cache_syntax_constant d =
@@ -81,11 +82,12 @@ let in_syntax_constant : (bool * syndef) -> obj =
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
-let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
+let declare_syntactic_definition ~local ?(also_in_cases_pattern=true) deprecation id ~onlyparsing pat =
   let syndef =
     { syndef_pattern = pat;
       syndef_onlyparsing = onlyparsing;
       syndef_deprecation = deprecation;
+      syndef_also_in_cases_pattern = also_in_cases_pattern;
     }
   in
   let _ = add_leaf id (in_syntax_constant (local,syndef)) in ()
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 66a3132f2a..31f685152c 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,7 +13,7 @@ open Notation_term
 
 (** Syntactic definitions. *)
 
-val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
+val declare_syntactic_definition : local:bool -> ?also_in_cases_pattern:bool -> Deprecation.t option -> Id.t ->
   onlyparsing:bool -> interpretation -> unit
 
 val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation
diff --git a/test-suite/bugs/closed/bug_13078.v b/test-suite/bugs/closed/bug_13078.v
new file mode 100644
index 0000000000..1bd32d0576
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13078.v
@@ -0,0 +1,8 @@
+(* Check that rules with patterns are not registered for cases patterns *)
+Module PrintingTest.
+Declare Custom Entry test.
+Notation "& x" := (Some x) (in custom test at level 0, x pattern).
+Check fun x => match x with | None => None | Some tt => Some tt end.
+Notation "& x" := (Some x) (at level 0, x pattern).
+Check fun x => match x with | None => None | Some tt => Some tt end.
+End PrintingTest.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8ce59c40c3..684036bc11 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1042,6 +1042,13 @@ let interp_non_syntax_modifiers mods =
   in
   List.fold_left (fun st modif -> Option.bind st @@ set modif) (Some (false,false,InConstrEntry)) mods
 
+(* Check if an interpretation can be used for printing a cases printing *)
+let has_no_binders_type =
+  List.for_all (fun (_,(_,typ)) ->
+  match typ with
+  | NtnTypeBinder _ | NtnTypeBinderList -> false
+  | NtnTypeConstr | NtnTypeConstrList -> true)
+
 (* Compute precedences from modifiers (or find default ones) *)
 
 let set_entry_type from n etyps (x,typ) =
@@ -1416,6 +1423,7 @@ type notation_obj = {
   notobj_deprecation : Deprecation.t option;
   notobj_notation : notation * notation_location;
   notobj_specific_pp_rules : syntax_printing_extension option;
+  notobj_also_in_cases_pattern : bool;
 }
 
 let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
@@ -1438,9 +1446,10 @@ let open_notation i (_, nobj) =
     let pat = nobj.notobj_interp in
     let deprecation = nobj.notobj_deprecation in
     let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+    let also_in_cases_pattern = nobj.notobj_also_in_cases_pattern in
     (* Declare the notation *)
     (match nobj.notobj_use with
-    | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation
+    | Some use -> Notation.declare_notation (scope,ntn) pat df ~use ~also_in_cases_pattern nobj.notobj_coercion deprecation
     | None -> ());
     (* Declare specific format if any *)
     (match nobj.notobj_specific_pp_rules with
@@ -1621,19 +1630,21 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
   let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
   let interp = make_interpretation_vars sd.recvars (pi2 sd.level) acvars (fst sd.pa_syntax_data) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
+  let vars = List.map_filter map i_vars in (* Order of elements is important here! *)
+  let also_in_cases_pattern = has_no_binders_type vars in
   let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in
   let notation, location = sd.info in
   let use = make_use true onlyparse sd.only_printing in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
-    notobj_interp = (List.map_filter map i_vars, ac);
-    (* Order is important here! *)
     notobj_use = use;
+    notobj_interp = (vars, ac);
     notobj_coercion = coe;
     notobj_deprecation = sd.deprecation;
     notobj_notation = (notation, location);
     notobj_specific_pp_rules = sy_pp_rules;
+    notobj_also_in_cases_pattern = also_in_cases_pattern;
   } in
   (* Ready to change the global state *)
   List.iter (fun f -> f ()) sd.msgs;
@@ -1665,18 +1676,20 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
   let plevel = match level with Some (from,level,l) -> level | None (* numeral: irrelevant )*) -> 0 in
   let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
+  let vars = List.map_filter map i_vars in (* Order of elements is important here! *)
+  let also_in_cases_pattern = has_no_binders_type vars in
   let onlyparse,coe = printability level i_typs onlyparse reversibility ac in
   let use = make_use false onlyparse onlyprint in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
-    notobj_interp = (List.map_filter map i_vars, ac);
-    (* Order is important here! *)
     notobj_use = use;
+    notobj_interp = (vars, ac);
     notobj_coercion = coe;
     notobj_deprecation = deprecation;
     notobj_notation = df';
     notobj_specific_pp_rules = pp_sy;
+    notobj_also_in_cases_pattern = also_in_cases_pattern;
   } in
   Lib.add_anonymous_leaf (inNotation notation);
   df'
@@ -1850,8 +1863,9 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
   let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in
   let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] 0 acvars (List.map in_pat vars) in
   let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
+  let also_in_cases_pattern = has_no_binders_type vars in
   let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in
-  Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
+  Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat)
 
 (**********************************************************************)
 (* Declaration of custom entry                                        *)