aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/03-notations/12163-fix-12159.rst11
-rw-r--r--interp/constrextern.ml11
-rw-r--r--interp/notation.ml88
-rw-r--r--interp/notation.mli4
-rw-r--r--plugins/ssr/ssrparser.mlg4
-rw-r--r--test-suite/output/bug_12159.out28
-rw-r--r--test-suite/output/bug_12159.v39
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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:15:16 +0000