diff --git a/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst new file mode 100644 index 000000000000..c5a2172005e6 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst @@ -0,0 +1,6 @@ +- **Changed:** + Improve the :cmd:`Coercion` command to reduce the number of ambiguous paths to + report. A pair of multiple inheritance paths that can be reduced to smaller + adjoining pairs will not be reported as ambiguous paths anymore. + (`#13909 `_, + by Kazuhiko Sakaguchi). diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index 274dbfd7ed38..8b864b4dd3c8 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -30,10 +30,6 @@ type cl_typ = | CL_IND of inductive | CL_PROJ of Projection.Repr.t -type cl_info_typ = { - cl_param : int -} - let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 @@ -56,9 +52,17 @@ struct if Int.equal c 0 then cl_typ_ord j1 j2 else c end +module ClTypSet = Set.Make(ClTyp) module ClTypMap = Map.Make(ClTyp) module ClPairMap = Map.Make(ClPairOrd) +type cl_info_typ = { + cl_param : int; + cl_reachable_from : ClTypSet.t; + cl_reachable_to : ClTypSet.t; + cl_repr : cl_typ; +} + type coe_typ = GlobRef.t module CoeTypMap = GlobRef.Map_env @@ -73,18 +77,18 @@ type coe_info_typ = { coe_param : int; } -let coe_info_typ_equal c1 c2 = - GlobRef.equal c1.coe_value c2.coe_value && - c1.coe_local == c2.coe_local && - c1.coe_is_identity == c2.coe_is_identity && - c1.coe_is_projection == c2.coe_is_projection && - Int.equal c1.coe_param c2.coe_param - type inheritance_path = coe_info_typ list let init_class_tab = let open ClTypMap in - add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty) + let cl_info params cl = + let cl_singleton = ClTypSet.singleton cl in + { cl_param = params; + cl_reachable_from = cl_singleton; + cl_reachable_to = cl_singleton; + cl_repr = cl } + in + add CL_FUN (cl_info 0 CL_FUN) (add CL_SORT (cl_info 0 CL_SORT) empty) let class_tab = Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t) @@ -98,8 +102,7 @@ let inheritance_graph = (* ajout de nouveaux "objets" *) let add_new_class cl s = - if not (ClTypMap.mem cl !class_tab) then - class_tab := ClTypMap.add cl s !class_tab + class_tab := ClTypMap.add cl s !class_tab let add_new_coercion coe s = coercion_tab := CoeTypMap.add coe s !coercion_tab @@ -283,54 +286,80 @@ let different_class_params env ci = | _ -> false let add_coercion_in_graph env sigma ic = + let source = ic.coe_source in + let target = ic.coe_target in + let source_info = class_info source in + let target_info = class_info target in let old_inheritance_graph = !inheritance_graph in let ambig_paths : ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref = ref [] in + let check_coherence (i, j as ij) p q = + let i_info = class_info i in + let j_info = class_info j in + let between_ij = ClTypSet.inter i_info.cl_reachable_from j_info.cl_reachable_to in + if cl_typ_eq i_info.cl_repr i && + cl_typ_eq j_info.cl_repr j && + ClTypSet.is_empty + (ClTypSet.diff (ClTypSet.inter between_ij source_info.cl_reachable_to) + i_info.cl_reachable_to) && + ClTypSet.is_empty + (ClTypSet.diff + (ClTypSet.inter between_ij target_info.cl_reachable_from) + j_info.cl_reachable_from) && + not (compare_path env sigma i p q) + then + ambig_paths := (ij, p, q) :: !ambig_paths + in let try_add_new_path (i,j as ij) p = - (* If p is a cycle, we check whether p is definitionally an identity - function or not. If it is not, we report p as an ambiguous inheritance - path. *) - if cl_typ_eq i j && not (compare_path env sigma i p []) then - ambig_paths := (ij,p,[])::!ambig_paths; + if cl_typ_eq i j then check_coherence ij p []; if not (cl_typ_eq i j) || different_class_params env i then match lookup_path_between_class ij with - | q -> - (* p has the same source and target classes as an existing path q. We - report them as ambiguous inheritance paths if - 1. p and q have no common element, and - 2. p and q are not convertible. - If 1 does not hold, say p = p1 @ [c] @ p2 and q = q1 @ [c] @ q2, - convertibility of p1 and q1, also, p2 and q2 should be checked; thus, - checking the ambiguity of p and q is redundant with them. *) - if not (List.exists (fun c -> List.exists (coe_info_typ_equal c) q) p || - compare_path env sigma i p q) then - ambig_paths := (ij,p,q)::!ambig_paths; - false - | exception Not_found -> (add_new_path ij p; true) + | q -> (if not (cl_typ_eq i j) then check_coherence ij p q); false + | exception Not_found -> add_new_path ij p; true else false in let try_add_new_path1 ij p = let _ = try_add_new_path ij p in () in - if try_add_new_path (ic.coe_source, ic.coe_target) [ic] then begin + if try_add_new_path (source, target) [ic] then begin ClPairMap.iter (fun (s,t) p -> if not (cl_typ_eq s t) then begin - if cl_typ_eq t ic.coe_source then begin - try_add_new_path1 (s, ic.coe_target) (p@[ic]); + if cl_typ_eq t source then begin + try_add_new_path1 (s, target) (p@[ic]); ClPairMap.iter (fun (u,v) q -> - if not (cl_typ_eq u v) && cl_typ_eq u ic.coe_target then + if not (cl_typ_eq u v) && cl_typ_eq u target then try_add_new_path1 (s,v) (p@[ic]@q)) old_inheritance_graph end; - if cl_typ_eq s ic.coe_target then - try_add_new_path1 (ic.coe_source, t) (ic::p) + if cl_typ_eq s target then try_add_new_path1 (source, t) (ic::p) end) old_inheritance_graph end; + class_tab := ClTypMap.mapi (fun k k_info -> + let reachable_k_source = ClTypSet.mem k source_info.cl_reachable_to in + let reachable_target_k = ClTypSet.mem k target_info.cl_reachable_from in + { k_info with + cl_reachable_from = + if reachable_k_source then + ClTypSet.union + k_info.cl_reachable_from target_info.cl_reachable_from + else + k_info.cl_reachable_from; + cl_reachable_to = + if reachable_target_k then + ClTypSet.union k_info.cl_reachable_to source_info.cl_reachable_to + else + k_info.cl_reachable_to; + cl_repr = + if reachable_k_source && reachable_target_k then + target_info.cl_repr + else + k_info.cl_repr + }) !class_tab; match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths let subst_coercion subst c = @@ -365,7 +394,13 @@ let class_params env sigma = function (* add_class : cl_typ -> locality_flag option -> bool -> unit *) let add_class env sigma cl = - add_new_class cl { cl_param = class_params env sigma cl } + if not (class_exists cl) then + let cl_singleton = ClTypSet.singleton cl in + add_new_class cl { + cl_param = class_params env sigma cl; + cl_reachable_from = cl_singleton; + cl_reachable_to = cl_singleton; + cl_repr = cl } let declare_coercion env sigma c = let () = add_class env sigma c.coe_source in diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index fb5621dd3a59..9236167021c4 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -31,9 +31,19 @@ val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ (** Comparison of [cl_typ] *) val cl_typ_ord : cl_typ -> cl_typ -> int +module ClTypSet : Set.S with type elt = cl_typ + (** This is the type of infos for declared classes *) type cl_info_typ = { - cl_param : int } + (* The number of parameters of the coercion class. *) + cl_param : int; + (* The sets of coercion classes respectively reachable from and to the + coercion class. *) + cl_reachable_from : ClTypSet.t; + cl_reachable_to : ClTypSet.t; + (* The representative class of the strongly connected component. *) + cl_repr : cl_typ; +} (** This is the type of coercion kinds *) type coe_typ = GlobRef.t diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index 48368c7ede90..6bf03d30d3d8 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -1,13 +1,24 @@ -File "stdin", line 10, characters 0-28: +File "stdin", line 13, characters 0-29: Warning: -New coercion path [ac; cd] : A >-> D is ambiguous with existing -[ab; bd] : A >-> D. [ambiguous-paths,typechecker] -[ab] : A >-> B -[ac] : A >-> C -[ab; bd] : A >-> D -[bd] : B >-> D -[cd] : C >-> D -File "stdin", line 26, characters 0-28: +New coercion path [g1; f2] : A >-> B' is ambiguous with existing +[f1; g2] : A >-> B'. [ambiguous-paths,typechecker] +File "stdin", line 14, characters 0-29: +Warning: +New coercion path [h1; f3] : B >-> C' is ambiguous with existing +[f2; h2] : B >-> C'. [ambiguous-paths,typechecker] +[f1] : A >-> A' +[g1] : A >-> B +[f1; g2] : A >-> B' +[g1; h1] : A >-> C +[f1; g2; h2] : A >-> C' +[g2] : A' >-> B' +[g2; h2] : A' >-> C' +[f2] : B >-> B' +[h1] : B >-> C +[f2; h2] : B >-> C' +[h2] : B' >-> C' +[f3] : C >-> C' +File "stdin", line 33, characters 0-28: Warning: New coercion path [ab; bc] : A >-> C is ambiguous with existing [ac] : A >-> C. [ambiguous-paths,typechecker] @@ -17,6 +28,19 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing [bc] : B >-> C [bc; cd] : B >-> D [cd] : C >-> D +File "stdin", line 50, characters 0-28: +Warning: +New coercion path [ab; bc] : A >-> C is ambiguous with existing +[ac] : A >-> C. [ambiguous-paths,typechecker] +File "stdin", line 51, characters 0-28: +Warning: +New coercion path [ba; ab] : B >-> B is not definitionally an identity function. +New coercion path [ab; ba] : A >-> A is not definitionally an identity function. +[ambiguous-paths,typechecker] +[ab] : A >-> B +[ac] : A >-> C +[ba] : B >-> A +[bc] : B >-> C [B_A] : B >-> A [C_A] : C >-> A [D_A] : D >-> A @@ -31,7 +55,7 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing [D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C -File "stdin", line 121, characters 0-86: +File "stdin", line 147, characters 0-86: Warning: New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker] @@ -44,15 +68,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing [D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C -File "stdin", line 130, characters 0-47: +File "stdin", line 156, characters 0-47: Warning: New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function. [ambiguous-paths,typechecker] -File "stdin", line 131, characters 0-64: +File "stdin", line 157, characters 0-64: Warning: New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function. [ambiguous-paths,typechecker] -File "stdin", line 132, characters 0-51: +File "stdin", line 158, characters 0-51: Warning: New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function. [ambiguous-paths,typechecker] diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v index 41322045f2b3..182e155273fb 100644 --- a/test-suite/output/relaxed_ambiguous_paths.v +++ b/test-suite/output/relaxed_ambiguous_paths.v @@ -1,13 +1,20 @@ Module test1. Section test1. -Variable (A B C D : Type). -Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D). - -Local Coercion ab : A >-> B. -Local Coercion bd : B >-> D. -Local Coercion ac : A >-> C. -Local Coercion cd : C >-> D. +Variable (A B C A' B' C' : Type). +Variable (f1 : A -> A') (f2 : B -> B') (f3 : C -> C'). +Variable (g1 : A -> B) (g2 : A' -> B') (h1 : B -> C) (h2 : B' -> C'). + +Local Coercion g1 : A >-> B. +Local Coercion g2 : A' >-> B'. +Local Coercion h1 : B >-> C. +Local Coercion h2 : B' >-> C'. +Local Coercion f1 : A >-> A'. +Local Coercion f2 : B >-> B'. +Local Coercion f3 : C >-> C'. +(* [g1; h1; f3], [f1; g2; h2] : A >-> C' should not be reported as ambiguous *) +(* paths because they are redundant with `[g1; f2], [f1; g2] : A >-> B'` and *) +(* `[h1; f3], [f2; h2] : B >-> C'`. *) Print Graph. @@ -24,8 +31,8 @@ Local Coercion ac : A >-> C. Local Coercion cd : C >-> D. Local Coercion ab : A >-> B. Local Coercion bc : B >-> C. -(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths *) -(* here because they are redundant with `[ab; bc], [ac] : A >-> C`. *) +(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be reported as ambiguous *) +(* paths because they are redundant with `[ab; bc], [ac] : A >-> C`. *) Print Graph. @@ -34,6 +41,25 @@ End test2. Module test3. Section test3. + +Variable (A B C : Type). +Variable (ab : A -> B) (ba : B -> A) (ac : A -> C) (bc : B -> C). + +Local Coercion ac : A >-> C. +Local Coercion bc : B >-> C. +Local Coercion ab : A >-> B. +Local Coercion ba : B >-> A. +(* `[ba; ac], [bc] : B >-> C` should not be reported as ambiguous paths *) +(* because they are redundant with `[ab; bc], [ac] : A >-> C` and *) +(* `[ba; ab] : B >-> B`. *) + +Print Graph. + +End test3. +End test3. + +Module test4. +Section test4. Variable (A : Type) (P Q : A -> Prop). Record B := { @@ -57,11 +83,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d). Print Graph. -End test3. -End test3. +End test4. +End test4. -Module test4. -Section test4. +Module test5. +Section test5. Variable (A : Type) (P Q : A -> Prop). @@ -89,11 +115,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d). Print Graph. -End test4. -End test4. +End test5. +End test5. -Module test5. -Section test5. +Module test6. +Section test6. Variable (A : Type) (P Q : A -> Prop). @@ -123,18 +149,18 @@ Local Coercion D_C (d : D) : C true := Print Graph. -End test5. -End test5. +End test6. +End test6. -Module test6. +Module test7. Record > NAT := wrap_nat { unwrap_nat :> nat }. Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }. Record > TYPE := wrap_Type { unwrap_Type :> Type }. -End test6. +End test7. -Module test7. +Module test8. Set Primitive Projections. Record > NAT_prim := wrap_nat { unwrap_nat :> nat }. Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }. Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }. -End test7. +End test8.