From 27270870ea75e77808d8e1b4af4998c0b57255ae Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 10 Mar 2021 13:07:58 +0900 Subject: [PATCH 1/2] Minimize the set of multiple inheritance paths to check for conversion The table of coercion classes (`class_tab`) has been extended with information about reachability. The conversion checking of a pair of multiple inheritance paths (of coercions) will be skipped if these paths can be reduced to smaller adjoining pairs of multiple inheritance paths, and this reduction will be determined based on that reachability information. --- .../13909-reduce-ambiguous-paths.rst | 6 + pretyping/coercionops.ml | 113 ++++++++++++------ pretyping/coercionops.mli | 12 +- test-suite/output/relaxed_ambiguous_paths.out | 50 ++++++-- test-suite/output/relaxed_ambiguous_paths.v | 72 +++++++---- 5 files changed, 177 insertions(+), 76 deletions(-) create mode 100644 doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst 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. From f71129454d2c4ecde10e2a2e4284d6a576ee39ca Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 26 Mar 2021 00:24:37 +0900 Subject: [PATCH 2/2] Expose less interface in coercionops.mli --- pretyping/coercionops.ml | 6 ++++++ pretyping/coercionops.mli | 16 +--------------- pretyping/pretyping.ml | 2 +- 3 files changed, 8 insertions(+), 16 deletions(-) diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index 8b864b4dd3c8..9b25d636405b 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -57,9 +57,13 @@ module ClTypMap = Map.Make(ClTyp) module ClPairMap = Map.Make(ClPairOrd) type cl_info_typ = { + (* 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; } @@ -114,6 +118,8 @@ let add_new_path x y = let class_info cl = ClTypMap.find cl !class_tab +let class_nparams cl = (class_info cl).cl_param + let class_exists cl = ClTypMap.mem cl !class_tab let coercion_info coe = CoeTypMap.find coe !coercion_tab diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 9236167021c4..af91dd1d0e90 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -31,20 +31,6 @@ 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 = { - (* 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 @@ -67,7 +53,7 @@ type inheritance_path = coe_info_typ list val class_exists : cl_typ -> bool (** @raise Not_found if this type is not a class *) -val class_info : cl_typ -> cl_info_typ +val class_nparams : cl_typ -> int (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3ccc6ea12588..4f9283e999b4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1423,7 +1423,7 @@ let path_convertible env sigma cl p q = p' | [] -> (* identity function for the class [i]. *) - let params = (class_info cl).cl_param in + let params = class_nparams cl in let clty = match cl with | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})