Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple scopes for the same inductive)

7 files changed, 147 insertions, 38 deletions

diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst
new file mode 100644
index 0000000000..978ed561dd
--- /dev/null
+++ b/doc/changelog/03-notations/12163-fix-12159.rst
@@ -0,0 +1,11 @@
+- **Fixed:**
+  Numeral Notations now play better with multiple scopes for the same
+  inductive type. Previously, when multiple numeral notations were defined
+  for the same inductive, only the last one was considered for
+  printing. Now, among the notations that are usable for printing and either
+  have a scope delimiter or are open, the selection is made according
+  to the order of open scopes, or according to the last defined
+  notation if no appropriate scope is open
+  (`#12163 <https://github.com/coq/coq/pull/12163>`_,
+  fixes `#12159 <https://github.com/coq/coq/pull/12159>`_,
+  by Pierre Roux, review by Hugo Herbelin and Jason Gross).
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a37bac3275..d5a5bde616 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -435,13 +435,10 @@ let extern_record_pattern cstrsp args =
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
     if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
-    let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
+    let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
     match availability_of_entry_coercion custom InConstrEntrySomeLevel with
       | None -> raise No_match
       | Some coercion ->
-    match availability_of_prim_token p sc scopes with
-      | None -> raise No_match
-      | Some key ->
         let loc = cases_pattern_loc pat in
         insert_pat_coercion ?loc coercion
           (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
@@ -848,13 +845,11 @@ let same_binder_type ty nal c =
 (* one with no delimiter if possible)                                 *)
 
 let extern_possible_prim_token (custom,scopes) r =
-   let (sc,n) = uninterp_prim_token r in
+   let (n,key) = uninterp_prim_token r scopes in
    match availability_of_entry_coercion custom InConstrEntrySomeLevel with
    | None -> raise No_match
    | Some coercion ->
-   match availability_of_prim_token n sc scopes with
-   | None -> raise No_match
-   | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+      insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
 
 let filter_enough_applied nargs l =
   match nargs with
diff --git a/interp/notation.ml b/interp/notation.ml
index 0afbb9cd62..7761606f11 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -932,7 +932,7 @@ let prim_token_interp_infos =
 (* Table from global_reference to backtrack-able informations about
    prim_token uninterpretation (in particular uninterpreter unique id). *)
 let prim_token_uninterp_infos =
-  ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t)
+  ref (GlobRef.Map.empty : ((scope_name * (prim_token_interp_info * bool)) list) GlobRef.Map.t)
 
 let hashtbl_check_and_set allow_overwrite uid f h eq =
   match Hashtbl.find h uid with
@@ -968,10 +968,13 @@ let cache_prim_token_interpretation (_,infos) =
   check_scope ~tolerant:true sc;
   prim_token_interp_infos :=
     String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
-  List.iter (fun r -> prim_token_uninterp_infos :=
-                        GlobRef.Map.add r (sc,ptii,infos.pt_in_match)
-                          !prim_token_uninterp_infos)
-            infos.pt_refs
+  let add_uninterp r =
+    let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in
+    let l = List.remove_assoc_f String.equal sc l in
+    prim_token_uninterp_infos :=
+      GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l)
+        !prim_token_uninterp_infos in
+  List.iter add_uninterp infos.pt_refs
 
 let subst_prim_token_interpretation (subs,infos) =
   { infos with
@@ -1324,27 +1327,6 @@ let entry_has_ident = function
   | InCustomEntryLevel (s,n) ->
      try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
 
-let uninterp_prim_token c =
-  match glob_prim_constr_key c with
-  | None -> raise Notation_ops.No_match
-  | Some r ->
-     try
-       let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
-       let uninterp = match info with
-         | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
-         | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
-         | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
-       in
-       match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
-       | None -> raise Notation_ops.No_match
-       | Some n -> (sc,n)
-     with Not_found -> raise Notation_ops.No_match
-
-let uninterp_prim_token_cases_pattern c =
-  match glob_constr_of_closed_cases_pattern (Global.env()) c with
-  | exception Not_found -> raise Notation_ops.No_match
-  | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
-
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
     try
@@ -1366,6 +1348,60 @@ let availability_of_prim_token n printer_scope local_scopes =
   let scopes = make_current_scopes local_scopes in
   Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes)
 
+let rec find_uninterpretation need_delim def find = function
+  | [] ->
+      List.find_map
+        (fun (sc,_,_) -> try Some (find need_delim sc) with Not_found -> None)
+        def
+  | OpenScopeItem scope :: scopes ->
+      (try find need_delim scope
+       with Not_found -> find_uninterpretation need_delim def find scopes)  (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *)
+  | LonelyNotationItem ntn::scopes ->
+      find_uninterpretation (ntn::need_delim) def find scopes
+
+let uninterp_prim_token c local_scopes =
+  match glob_prim_constr_key c with
+  | None -> raise Notation_ops.No_match
+  | Some r ->
+     let uninterp (sc,(info,_)) =
+       try
+         let uninterp = match info with
+           | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
+           | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+           | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
+         in
+         match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
+         | None -> None
+         | Some n -> Some (sc,n)
+       with Not_found -> None in
+     let add_key (sc,n) =
+       Option.map (fun k -> sc,n,k) (availability_of_prim_token n sc local_scopes) in
+     let l =
+       try GlobRef.Map.find r !prim_token_uninterp_infos
+       with Not_found -> raise Notation_ops.No_match in
+     let l = List.map_filter uninterp l in
+     let l = List.map_filter add_key l in
+     let find need_delim sc =
+       let _,n,k = List.find (fun (sc',_,_) -> String.equal sc' sc) l in
+       if k <> None then n,k else
+         let hidden =
+           List.exists
+             (fun n' -> notation_eq n' (notation_of_prim_token n))
+             need_delim in
+         if not hidden then n,k else
+           match (String.Map.find sc !scope_map).delimiters with
+           | Some k -> n,Some k
+           | None -> raise Not_found
+     in
+     let scopes = make_current_scopes local_scopes in
+     try find_uninterpretation [] l find scopes
+     with Not_found -> match l with (_,n,k)::_ -> n,k | [] -> raise Notation_ops.No_match
+
+let uninterp_prim_token_cases_pattern c local_scopes =
+  match glob_constr_of_closed_cases_pattern (Global.env()) c with
+  | exception Not_found -> raise Notation_ops.No_match
+  | na,c -> let (sc,n) = uninterp_prim_token c local_scopes in (na,sc,n)
+
 (* Miscellaneous *)
 
 let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
diff --git a/interp/notation.mli b/interp/notation.mli
index 892eba8d11..842f2b1458 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -206,9 +206,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) ->
    raise [No_match] if no such token *)
 
 val uninterp_prim_token :
-  'a glob_constr_g -> scope_name * prim_token
+  'a glob_constr_g -> subscopes -> prim_token * delimiters option
 val uninterp_prim_token_cases_pattern :
-  'a cases_pattern_g -> Name.t * scope_name * prim_token
+  'a cases_pattern_g -> subscopes -> Name.t * prim_token * delimiters option
 
 val availability_of_prim_token :
   prim_token -> scope_name -> subscopes -> delimiters option option
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0307728819..60af804c1b 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -349,8 +349,8 @@ let interp_index ist gl idx =
         begin match Tacinterp.Value.to_constr v with
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
-          begin match Notation.uninterp_prim_token rc with
-          | _, Constrexpr.Numeral n when NumTok.Signed.is_int n ->
+          begin match Notation.uninterp_prim_token rc (None, []) with
+          | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n ->
             int_of_string (NumTok.Signed.to_string n)
           | _ -> raise Not_found
           end
diff --git a/test-suite/output/bug_12159.out b/test-suite/output/bug_12159.out
new file mode 100644
index 0000000000..7f47c47e32
--- /dev/null
+++ b/test-suite/output/bug_12159.out
@@ -0,0 +1,28 @@
+f 1%B
+     : unit
+f 0
+     : unit
+1%B
+     : unit
+0
+     : unit
+1%B
+     : unit
+1
+     : unit
+1
+     : unit
+0
+     : unit
+1
+     : unit
+0%A
+     : unit
+1
+     : unit
+0%A
+     : unit
+0
+     : unit
+0
+     : unit
diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v
new file mode 100644
index 0000000000..91d66f7f4c
--- /dev/null
+++ b/test-suite/output/bug_12159.v
@@ -0,0 +1,39 @@
+Declare Scope A.
+Declare Scope B.
+Delimit Scope A with A.
+Delimit Scope B with B.
+Definition to_unit (v : Decimal.uint) : option unit
+  := match Nat.of_uint v with O => Some tt | _ => None end.
+Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1.
+Numeral Notation unit to_unit of_unit : A.
+Numeral Notation unit to_unit of_unit' : B.
+Definition f x : unit := x.
+Check f tt.
+Arguments f x%A.
+Check f tt.
+Check tt.
+Open Scope A.
+Check tt.
+Close Scope A.
+Check tt.
+Open Scope B.
+Check tt.
+Undelimit Scope B.
+Check tt.
+Open Scope A.
+Check tt.
+Close Scope A.
+Check tt.
+Close Scope B.
+Check tt.
+Open Scope B.
+Check tt.
+Notation "1" := true.
+Check tt.
+Open Scope A.
+Check tt.
+Declare Scope C.
+Notation "0" := false : C.
+Open Scope C.
+Check tt.  (* gives 0 but should now be 0%A *)