Merge PR #12984: [printing] Order notations by matching precision first, and then by last imported

Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares

1 files changed, 29 insertions, 18 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 1a361dc1a6..286ece6cb6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -345,11 +345,23 @@ 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 adjust_application c1 c2 =
+  match c1, c2 with
+  | NApp (t1, a1), (NList (_,_,NApp (_, a2),_,_) | NApp (_, a2)) when List.length a1 >= List.length a2 ->
+      NApp (t1, List.firstn (List.length a2) a1)
+  | NApp (t1, a1), _ ->
+      t1
+  | _ -> c1
+
+let strictly_finer_interpretation_than (_,(_,(vars1,c1),_)) (_,(_,(vars2,c2),_)) =
+  let c1 = adjust_application c1 c2 in
+  Notation_ops.strictly_finer_notation_constr (List.map fst vars1, List.map fst vars2) c1 c2
+
 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 (also_cases_notation_rule_eq interp) old with Not_found -> old in
-  KeyMap.add key (interp :: old) map
+  (* strictly finer interpretation are kept in front *)
+  let strictly_finer, rest = List.partition (fun c -> strictly_finer_interpretation_than c interp) old in
+  KeyMap.add key (strictly_finer @ interp :: rest) map
 
 let keymap_remove key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
@@ -1419,12 +1431,12 @@ let check_parsing_override (scopt,ntn) data = function
   | OnlyParsingData (_,old_data) ->
     let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
     warn_override_if_needed (scopt,ntn) overridden data old_data;
-    None, not overridden
+    None
   | ParsingAndPrintingData (_,on_printing,old_data) ->
     let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
     warn_override_if_needed (scopt,ntn) overridden data old_data;
-    (if on_printing then Some old_data.not_interp else None), not overridden
-  | NoParsingData -> None, false
+    if on_printing then Some old_data.not_interp else None
+  | NoParsingData -> None
 
 let check_printing_override (scopt,ntn) data parsingdata printingdata =
   let parsing_update = match parsingdata with
@@ -1453,15 +1465,15 @@ let update_notation_data (scopt,ntn) use data table =
     try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in
   match use with
   | OnlyParsing ->
-    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
-    NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists
+    let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update
   | ParsingAndPrinting ->
-    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
-    NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists
+    let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update
   | OnlyPrinting ->
     let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in
     let printingdata = if exists then printingdata else (true,data) :: printingdata in
-    NotationMap.add ntn (parsingdata, printingdata) table, None, exists
+    NotationMap.add ntn (parsingdata, printingdata) table, None
 
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
@@ -1734,23 +1746,22 @@ let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecat
     not_location = df;
     not_deprecation = deprecation;
   } in
-  let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in
-  if not exists then
-    let sc = { sc with notations = notation_update } in
-    scope_map := String.Map.add scope sc !scope_map;
+  let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in
+  let sc = { sc with notations = notation_update } in
+  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)) also_in_cases_pattern pat
   | None -> ()
   end;
-  if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
+  if 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
+  begin match scopt with
   | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
   | NotationInScope _ -> ()
   end;
   (* Declare a possible coercion *)
-  if not exists then begin match coe with
+  begin match coe with
    | Some (IsEntryCoercion entry) ->
      let (_,level,_) = level_of_notation ntn in
      let level = match fst ntn with