Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding notations in patterns

Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: LasseBlaauwbroek

5 files changed, 29 insertions, 19 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 269e20c16e..c150ae7abb 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 fe874cd01d..24b5dfce29 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