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

3 files changed, 67 insertions, 36 deletions

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