diff --git a/checker/values.ml b/checker/values.ml index cc2ccfd65307..88f2a6a5d842 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -300,9 +300,11 @@ let v_univ_abstracted v = v_tuple "univ_abstracted" [|v;v_abs_context|] let v_delta_hint = v_sum "delta_hint" 0 [|[|v_int; v_opt (v_univ_abstracted v_constr)|];[|v_kn|]|] +let v_mp_hint = v_sum "mp_hint" 1 [|[|v_mp|]|] + let v_resolver = v_tuple "delta_resolver" - [|v_mp; v_map v_mp v_mp; + [|v_mp; v_map v_mp v_mp_hint; v_hmap v_kn v_delta_hint|] let v_subst = diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 821bd5e7176a..c9eb382cce91 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -20,10 +20,17 @@ open Util open Names open Constr +(* The modpath part of a resolver holds two kinds of statements. + - [p ↦ MPequiv q] states that [q] is the canonical name of [p]. + - [p ↦ MPlift] states that [p] is a bound name that should be left untouched + by substitution. *) +type mp_hint = +| MPequiv of ModPath.t (** the canonical form of the key *) +| MPlift (** the prefix rule stops here *) + (* For Inline, the int is an inlining level, and the constr (if present) is the term into which we should inline. Equiv gives the canonical name in the given context. *) - type delta_hint = | Inline of int * constr UVars.univ_abstracted option | Equiv of KerName.t @@ -35,7 +42,7 @@ module Deltamap = struct type t = { root : ModPath.t; (** Common root of all keys in the deltamap *) - mmap : ModPath.t ModPath.Map.t; + mmap : mp_hint ModPath.Map.t; (** All bindings [mp ↦ _] must satisfy [mp ⊆ root] *) kmap : delta_hint KerName.Map.t; (** All bindings [kn ↦ _] must satisfy [modpath(kn) ⊆ root] *) @@ -53,16 +60,19 @@ module Deltamap = struct let () = assert (ModPath.subpath reso.root (KerName.modpath kn)) in { reso with kmap = KerName.Map.add kn hint reso.kmap } - let add_mp mp mp' reso = + let add_mp_hint mp hint reso = let () = assert (ModPath.subpath reso.root mp) in - { reso with mmap = ModPath.Map.add mp mp' reso.mmap } + { reso with mmap = ModPath.Map.add mp hint reso.mmap } - let find_mp mp reso = ModPath.Map.find mp reso.mmap + let add_mp mp mp' reso = add_mp_hint mp (MPequiv mp') reso + let lift_mp mp reso = add_mp_hint mp MPlift reso + + let find_mp_opt mp reso = ModPath.Map.find_opt mp reso.mmap let find_kn kn reso = KerName.Map.find kn reso.kmap let fold_kn f reso i = KerName.Map.fold f reso.kmap i let fold fmp fkn reso accu = ModPath.Map.fold fmp reso.mmap (KerName.Map.fold fkn reso.kmap accu) - let join map1 map2 = fold add_mp add_kn map1 map2 + let join map1 map2 = fold add_mp_hint add_kn map1 map2 (** if mp0 ⊆ root, we can see a resolver on root as a resolver on mp *) let upcast mp0 reso = @@ -87,8 +97,8 @@ module Deltamap = struct path in mm above root, as find_prefix will always return this one without considering the less precise ones. *) let glb = match glb with - | None -> Some mp - | Some glb -> if ModPath.subpath glb mp then Some mp else Some glb + | None -> Some (mp, data) + | Some (g, _) as old -> if ModPath.subpath g mp then Some (mp, data) else old in glb, accu else @@ -98,21 +108,23 @@ module Deltamap = struct let glb, mm' = ModPath.Map.fold fold_mp mm (None, ModPath.Map.empty) in let mm' = match glb with | None -> mm' - | Some glb -> + | Some (glb, data) -> if ModPath.Map.mem root mm then mm' else (* Add root to the resolver and map it to what find_prefix would have returned on root *) - let rec diff accu mp = - if ModPath.equal mp glb then accu - else match mp with - | MPdot (mp, l) -> diff (l :: accu) mp - | MPbound _ | MPfile _ -> assert false - in - let diff = diff [] root in - let data = ModPath.Map.get glb mm in - let data' = List.fold_left (fun accu l -> MPdot (accu, l)) data diff in - ModPath.Map.add root data' mm' + match data with + | MPlift -> ModPath.Map.add root MPlift mm' + | MPequiv data -> + let rec diff accu mp = + if ModPath.equal mp glb then accu + else match mp with + | MPdot (mp, l) -> diff (l :: accu) mp + | MPbound _ | MPfile _ -> assert false + in + let diff = diff [] root in + let data' = List.fold_left (fun accu l -> MPdot (accu, l)) data diff in + ModPath.Map.add root (MPequiv data') mm' in (* filter the kernames *) let filter_kn kn _ = ModPath.subpath root (KerName.modpath kn) in @@ -166,12 +178,16 @@ let string_of_hint pr = function | Inline (lvl, None) -> str "inline[" ++ int lvl ++ str "]" | Equiv kn -> str "equiv(" ++ KerName.print kn ++ str ")" +let debug_pr_mp_hint = function +| MPequiv mp -> ModPath.print mp +| MPlift -> str "" + let debug_pr_delta pr resolve = let kn_to_string kn hint l = hov 2 (KerName.print kn ++ str " =>" ++ spc() ++ string_of_hint pr hint) :: l in - let mp_to_string mp mp' l = - hov 2 (ModPath.print mp ++ str " =>" ++ spc() ++ ModPath.print mp') :: l + let mp_to_string mp hint l = + hov 2 (ModPath.print mp ++ str " =>" ++ spc() ++ debug_pr_mp_hint hint) :: l in let l = Deltamap.fold mp_to_string kn_to_string resolve [] in v 0 @@ prlist_with_sep pr_comma (fun p -> p) (List.rev l) @@ -207,7 +223,11 @@ let add_kn_delta_resolver kn kn' = assert (Id.equal (KerName.label kn) (KerName.label kn')); Deltamap.add_kn kn (Equiv kn') -let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 +let add_mp_delta_resolver mp1 mp2 = + let () = assert (not (ModPath.equal mp1 mp2)) in + Deltamap.add_mp mp1 mp2 + +let lift_mp_delta_resolver mp = Deltamap.lift_mp mp (** Extending a [substitution] without sequential composition *) @@ -223,13 +243,19 @@ let map_mbid mbid mp resolve = let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst let find_prefix resolve mp = - let rec sub_mp = function - | MPdot(mp,l) as mp_sup -> - (try Deltamap.find_mp mp_sup resolve - with Not_found -> MPdot(sub_mp mp,l)) - | p -> Deltamap.find_mp p resolve + let rec sub_mp mp = match Deltamap.find_mp_opt mp resolve with + | Some (MPequiv mp') -> mp' + | Some MPlift -> mp + | None -> + match mp with + | MPdot (mp1, l) -> + (* Preserving sharing is not an optimisation: [progress] in [subst_con0] + and [subst_mind] tests with [!=]. This should be fixed at some point. *) + let mp1' = sub_mp mp1 in + if mp1' == mp1 then mp else MPdot (mp1', l) + | MPbound _ | MPfile _ -> mp in - try sub_mp mp with Not_found -> mp + sub_mp mp (* TODO: remove the indirection at some point *) let mp_of_delta = find_prefix @@ -543,8 +569,8 @@ let replace_mp_in_kn mpfrom mpto kn = let mp_in_mp = ModPath.subpath let subset_prefixed_by mp resolver = - let mp_prefix mkey mequ rslv = - if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv + let mp_prefix mkey hint rslv = + if mp_in_mp mp mkey then Deltamap.add_mp_hint mkey hint rslv else rslv in let kn_prefix kn hint rslv = match hint with @@ -557,8 +583,8 @@ let subset_prefixed_by mp resolver = let subst_dom_delta_resolver mp_from mp_to resolver = let () = assert (ModPath.equal mp_from resolver.Deltamap.root) in let subst = map_mp mp_from mp_to (empty_delta_resolver mp_to) in - let mp_apply_subst mkey mequ rslv = - Deltamap.add_mp (subst_mp subst mkey) mequ rslv + let mp_apply_subst mkey hint rslv = + Deltamap.add_mp_hint (subst_mp subst mkey) hint rslv in let kn_apply_subst kkey hint rslv = Deltamap.add_kn (subst_kn subst kkey) hint rslv @@ -594,10 +620,13 @@ let subst_mp_delta subst mp mkey = reso, mp1 let gen_subst_delta_resolver dom subst resolver = - let mp_apply_subst mkey mequ rslv = + let mp_apply_subst mkey hint rslv = let mkey' = if dom then subst_mp subst mkey else mkey in - let rslv',mequ' = subst_mp_delta subst mequ mkey' in - Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv) + match hint with + | MPlift -> Deltamap.add_mp_hint mkey' MPlift rslv + | MPequiv mequ -> + let rslv', mequ' = subst_mp_delta subst mequ mkey' in + Deltamap.join rslv' (Deltamap.add_mp_hint mkey' (MPequiv mequ') rslv) in let kn_apply_subst kkey hint rslv = let kkey' = if dom then subst_kn subst kkey else kkey in @@ -615,8 +644,10 @@ let subst_codom_delta_resolver = gen_subst_delta_resolver false let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true let update_delta_resolver resolver1 resolver2 = - let mp_apply_rslv mkey mequ rslv = - Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv + let mp_apply_rslv mkey hint rslv = match hint with + | MPlift -> Deltamap.add_mp_hint mkey MPlift rslv + | MPequiv mequ -> + Deltamap.add_mp_hint mkey (MPequiv (find_prefix resolver2 mequ)) rslv in let kn_apply_rslv kkey hint1 rslv = let hint = match hint1 with diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 57bf52f36107..d7d07c19a50d 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -25,10 +25,16 @@ val empty_delta_resolver : ModPath.t -> delta_resolver val has_root_delta_resolver : ModPath.t -> delta_resolver -> bool -(** [add_mp_delta_resolver mp v reso] assumes that root(reso) ⊆ mp. *) +(** [add_mp_delta_resolver mp v reso] assumes that root(reso) ⊆ mp and mp ≠ v. *) val add_mp_delta_resolver : ModPath.t -> ModPath.t -> delta_resolver -> delta_resolver +(** [lift_mp_delta_resolver mp reso] marks [mp] as being a bound name that must + be left untouched by substitution. This is the semantics of delayed + resolvers for functors and module types. Assumes that root(reso) ⊆ mp. *) +val lift_mp_delta_resolver : + ModPath.t -> delta_resolver -> delta_resolver + (** [add_kn_delta_resolver kn v reso] assumes that root(reso) ⊆ modpath(kn). *) val add_kn_delta_resolver : KerName.t -> KerName.t -> delta_resolver -> delta_resolver diff --git a/kernel/modops.ml b/kernel/modops.ml index e0423d48c294..172ad020d8d3 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -293,7 +293,7 @@ let rec strengthen_module mp mb = match mod_type mb with if mp_is_alias delta_mb mp then mb (* already strengthened *) else let reso, struc' = strengthen_signature mp struc delta_mb in - let reso = add_mp_delta_resolver mp mp (add_delta_resolver delta_mb reso) in + let reso = lift_mp_delta_resolver mp (add_delta_resolver delta_mb reso) in strengthen_module_body ~src:mp (NoFunctor struc') reso mb | MoreFunctor _ -> mb @@ -307,7 +307,7 @@ and strengthen_signature mp struc reso0 = let reso = match mod_global_delta mb with | None -> (* See {!strengthen_and_subst_module} *) - add_mp_delta_resolver mp' mp' reso + lift_mp_delta_resolver mp' reso | Some delta -> add_delta_resolver delta reso in @@ -324,7 +324,7 @@ let strengthen mtb mp = match mod_type mtb with if mp_is_alias delta_mtb mp then mtb else let reso', struc' = strengthen_signature mp struc delta_mtb in - let reso' = add_delta_resolver delta_mtb (add_mp_delta_resolver mp mp reso') in + let reso' = add_delta_resolver delta_mtb (lift_mp_delta_resolver mp reso') in strengthen_module_type struc' reso' mtb | MoreFunctor _ -> mtb @@ -408,7 +408,7 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = semantic for functor this should be changed.*) begin match mod_global_delta mb' with | None -> (* functor case *) - add_mp_delta_resolver mp_to' mp_to' reso', item' + lift_mp_delta_resolver mp_to' reso', item' | Some delta -> add_delta_resolver delta reso', item' end @@ -418,7 +418,7 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso = let subst' = add_mp mp_from' mp_to' (empty_delta_resolver mp_to') subst in let mty' = subst_modtype subst_dom_codom subst' mp_from' mty in let item' = if mty' == mty then item else (l, SFBmodtype mty') in - add_mp_delta_resolver mp_to' mp_to' reso', item' + lift_mp_delta_resolver mp_to' reso', item' in List.Smart.fold_left_map strengthen_and_subst_field (empty_delta_resolver mp_to) struc @@ -449,7 +449,7 @@ let expand_self_delta mp sign reso = let self = mp_of_delta reso mp in (* [mp] is only equivalent to itself, it stops the prefix rule from reaching the fields the includer will get later. *) - let reso0 = add_mp_delta_resolver mp mp reso in + let reso0 = lift_mp_delta_resolver mp reso in let expand accu (l, item) = match item with | SFBconst _ | SFBmind _ | SFBrules _ -> let kn = KerName.make mp l in @@ -465,7 +465,7 @@ let expand_self_delta mp sign reso = | SFBmodtype _ -> (* as in [strengthen_and_subst_struct], module types are only equivalent to themselves *) - add_mp_delta_resolver (MPdot (mp, l)) (MPdot (mp, l)) accu + lift_mp_delta_resolver (MPdot (mp, l)) accu in List.fold_left expand reso0 (struct_of_signature sign) diff --git a/test-suite/modules/resolver_prefix_marker.v b/test-suite/modules/resolver_prefix_marker.v new file mode 100644 index 000000000000..fe6b8481410f --- /dev/null +++ b/test-suite/modules/resolver_prefix_marker.v @@ -0,0 +1,69 @@ +(* A delta-resolver binding on a modpath records either the canonical form of + that path, or a marker saying that the prefix rule must not be extrapolated + into it ([Mod_subst.lift_mp_delta_resolver], recorded by + [Modops.strengthen_and_subst_struct] for every functor field and every module + type field of the module it builds). + + The two transport differently -- a canonical name is left alone, a marker + travels with its key -- and while both were spelled [p -> p] they were + indistinguishable, so α-renaming a resolver turned a marker into a genuine + alias to the source. The two directions of the equivalence check that + [Subtyping.check_signatures] runs on a module type field then disagreed on + the canonical name of the inductive declared inside it, and the sealing below + was rejected with an error that could not even be printed. *) + +Module Type HasS. Module Type S. Inductive I := c. End S. End HasS. +Module Type T. Declare Module M : HasS. End T. + +Module B. + Module Type S. Inductive I := c. End S. +End B. + +Module C := B. (* first hop: marks C.S *) + +Module D : T. + Module M := C. (* second hop: used to lose the mark *) +End D. + +(* The same shape with a functor field rather than a module type field, the + other kind of field [strengthen_and_subst_struct] marks. It takes a + [with Module] to make the parameter type's [M] be [B'] itself, so that the + two sides of the check compare the resolver of [B'] with the ambient one; + sealing against a module type that merely declares a functor field of the + same shape gives them nothing in common to disagree about. The parameter type + of [Fn] must have content, for the same reason. + + On its own this no longer trips anything -- the [subst_mp_delta] fix of + #22445 is enough for it -- so it is kept as a guard on the marker of a + functor field, not as a reproducer. *) + +Module Type Any. End Any. +Module Type TAny. Declare Module M : Any. End TAny. + +Module Type WithI. Inductive I := c. End WithI. + +Module B'. + Module Fn (X : WithI) := X. +End B'. + +Module D' : TAny with Module M := B'. + Module M := B'. +End D'. + +(* Another funky test. *) + +Module Other. + +Module A. + Module E. Definition n := false. End E. + Module B. + Module P. Include A.E. End P. + End B. + Include B. +End A. + +Include A. + +Definition p := P.n. + +End Other.