From 514da75df458316840d5c9615be1aa34402dd3f7 Mon Sep 17 00:00:00 2001 From: Kanghee Park Date: Tue, 21 Jul 2026 05:24:19 +0000 Subject: [PATCH 1/5] Add module-object substitution characterization tests --- .../modules/ModuleObjectSubstitutionChain.v | 206 ++++++++++++++++++ .../unit-tests/kernel/mod_subst_test.ml | 175 +++++++++++++++ 2 files changed, 381 insertions(+) create mode 100644 test-suite/modules/ModuleObjectSubstitutionChain.v create mode 100644 test-suite/unit-tests/kernel/mod_subst_test.ml diff --git a/test-suite/modules/ModuleObjectSubstitutionChain.v b/test-suite/modules/ModuleObjectSubstitutionChain.v new file mode 100644 index 000000000000..3dea9e3699fd --- /dev/null +++ b/test-suite/modules/ModuleObjectSubstitutionChain.v @@ -0,0 +1,206 @@ +(* Regression coverage for substitution of algebraic module objects. + + The combined module type below deliberately retains references to many + component module types. Loading it as a functor parameter therefore drives + [Declaremods.subst_aobjs] through [Libobject.Ref] nodes and composes their + substitutions with [Mod_subst.join]. The body of [Probe] is empty so the + test isolates parameter loading from subsequent elaboration. *) + +Module Type S00. Parameter t00 : Type. End S00. +Module Type S01. Parameter t01 : Type. End S01. +Module Type S02. Parameter t02 : Type. End S02. +Module Type S03. Parameter t03 : Type. End S03. +Module Type S04. Parameter t04 : Type. End S04. +Module Type S05. Parameter t05 : Type. End S05. +Module Type S06. Parameter t06 : Type. End S06. +Module Type S07. Parameter t07 : Type. End S07. +Module Type S08. Parameter t08 : Type. End S08. +Module Type S09. Parameter t09 : Type. End S09. +Module Type S10. Parameter t10 : Type. End S10. +Module Type S11. Parameter t11 : Type. End S11. +Module Type S12. Parameter t12 : Type. End S12. +Module Type S13. Parameter t13 : Type. End S13. +Module Type S14. Parameter t14 : Type. End S14. +Module Type S15. Parameter t15 : Type. End S15. +Module Type S16. Parameter t16 : Type. End S16. +Module Type S17. Parameter t17 : Type. End S17. +Module Type S18. Parameter t18 : Type. End S18. +Module Type S19. Parameter t19 : Type. End S19. +Module Type S20. Parameter t20 : Type. End S20. +Module Type S21. Parameter t21 : Type. End S21. +Module Type S22. Parameter t22 : Type. End S22. +Module Type S23. Parameter t23 : Type. End S23. +Module Type S24. Parameter t24 : Type. End S24. +Module Type S25. Parameter t25 : Type. End S25. +Module Type S26. Parameter t26 : Type. End S26. +Module Type S27. Parameter t27 : Type. End S27. +Module Type S28. Parameter t28 : Type. End S28. +Module Type S29. Parameter t29 : Type. End S29. +Module Type S30. Parameter t30 : Type. End S30. +Module Type S31. Parameter t31 : Type. End S31. +Module Type S32. Parameter t32 : Type. End S32. +Module Type S33. Parameter t33 : Type. End S33. +Module Type S34. Parameter t34 : Type. End S34. +Module Type S35. Parameter t35 : Type. End S35. +Module Type S36. Parameter t36 : Type. End S36. +Module Type S37. Parameter t37 : Type. End S37. +Module Type S38. Parameter t38 : Type. End S38. +Module Type S39. Parameter t39 : Type. End S39. + +Module Type Nested. + Parameter carrier : Type. + Parameter value : carrier. +End Nested. + +Module Type Structured. + Inductive wrapped : Type := Wrap : nat -> wrapped. + Declare Module Inner : Nested. + Definition unwrap (x : wrapped) : nat := + match x with Wrap n => n end. +End Structured. + +Module Type WithNested. + Declare Module N : Nested. +End WithNested. + +Module ConcreteNested. + Definition carrier := nat. + Definition value := 0. +End ConcreteNested. + +Module ObjectSource. + Definition value := 0. + Abbreviation object_zero := value. +End ObjectSource. + +(* Module aliases retain substitutive object references. Keeping many of them + under one component makes parameter loading exercise repeated [Ref] + composition without relying on an external plugin. *) +Module Type AliasObjects. + Module Alias00 := ObjectSource. + Module Alias01 := ObjectSource. + Module Alias02 := ObjectSource. + Module Alias03 := ObjectSource. + Module Alias04 := ObjectSource. + Module Alias05 := ObjectSource. + Module Alias06 := ObjectSource. + Module Alias07 := ObjectSource. + Module Alias08 := ObjectSource. + Module Alias09 := ObjectSource. + Module Alias10 := ObjectSource. + Module Alias11 := ObjectSource. + Module Alias12 := ObjectSource. + Module Alias13 := ObjectSource. + Module Alias14 := ObjectSource. + Module Alias15 := ObjectSource. + Module Alias16 := ObjectSource. + Module Alias17 := ObjectSource. + Module Alias18 := ObjectSource. + Module Alias19 := ObjectSource. + Module Alias20 := ObjectSource. + Module Alias21 := ObjectSource. + Module Alias22 := ObjectSource. + Module Alias23 := ObjectSource. +End AliasObjects. + +Module Type ConstrainedNested := + WithNested with Module N := ConcreteNested. + +Module Type Args := + S00 <+ S01 <+ S02 <+ S03 <+ S04 <+ S05 <+ S06 <+ S07 <+ S08 <+ S09 <+ + S10 <+ S11 <+ S12 <+ S13 <+ S14 <+ S15 <+ S16 <+ S17 <+ S18 <+ S19 <+ + S20 <+ S21 <+ S22 <+ S23 <+ S24 <+ S25 <+ S26 <+ S27 <+ S28 <+ S29 <+ + S30 <+ S31 <+ S32 <+ S33 <+ S34 <+ S35 <+ S36 <+ S37 <+ S38 <+ S39 <+ + Structured <+ ConstrainedNested <+ AliasObjects. + +Module Type Probe (args : Args). +End Probe. + +(* Replaying parameter loading after rollback must preserve the same result. *) +Module Type ProbeReplay (args : Args). +End ProbeReplay. +Reset ProbeReplay. +Module Type ProbeReplay (args : Args). +End ProbeReplay. + +(* Applied functors and includes exercise the same composed substitution after + the parameter has been accepted. *) +Module UseArgs (args : Args). + Include args. + Definition witness : t00 -> t00 := fun x => x. +End UseArgs. + +Module ConcreteArgs <: Args. + Definition t00 := nat. + Definition t01 := nat. + Definition t02 := nat. + Definition t03 := nat. + Definition t04 := nat. + Definition t05 := nat. + Definition t06 := nat. + Definition t07 := nat. + Definition t08 := nat. + Definition t09 := nat. + Definition t10 := nat. + Definition t11 := nat. + Definition t12 := nat. + Definition t13 := nat. + Definition t14 := nat. + Definition t15 := nat. + Definition t16 := nat. + Definition t17 := nat. + Definition t18 := nat. + Definition t19 := nat. + Definition t20 := nat. + Definition t21 := nat. + Definition t22 := nat. + Definition t23 := nat. + Definition t24 := nat. + Definition t25 := nat. + Definition t26 := nat. + Definition t27 := nat. + Definition t28 := nat. + Definition t29 := nat. + Definition t30 := nat. + Definition t31 := nat. + Definition t32 := nat. + Definition t33 := nat. + Definition t34 := nat. + Definition t35 := nat. + Definition t36 := nat. + Definition t37 := nat. + Definition t38 := nat. + Definition t39 := nat. + Inductive wrapped : Type := Wrap : nat -> wrapped. + Module Inner := ConcreteNested. + Definition unwrap (x : wrapped) : nat := + match x with Wrap n => n end. + Module N := ConcreteNested. + Module Alias00 := ObjectSource. + Module Alias01 := ObjectSource. + Module Alias02 := ObjectSource. + Module Alias03 := ObjectSource. + Module Alias04 := ObjectSource. + Module Alias05 := ObjectSource. + Module Alias06 := ObjectSource. + Module Alias07 := ObjectSource. + Module Alias08 := ObjectSource. + Module Alias09 := ObjectSource. + Module Alias10 := ObjectSource. + Module Alias11 := ObjectSource. + Module Alias12 := ObjectSource. + Module Alias13 := ObjectSource. + Module Alias14 := ObjectSource. + Module Alias15 := ObjectSource. + Module Alias16 := ObjectSource. + Module Alias17 := ObjectSource. + Module Alias18 := ObjectSource. + Module Alias19 := ObjectSource. + Module Alias20 := ObjectSource. + Module Alias21 := ObjectSource. + Module Alias22 := ObjectSource. + Module Alias23 := ObjectSource. +End ConcreteArgs. + +Module Applied := UseArgs ConcreteArgs. +Check Applied.witness. diff --git a/test-suite/unit-tests/kernel/mod_subst_test.ml b/test-suite/unit-tests/kernel/mod_subst_test.ml new file mode 100644 index 000000000000..d42ff47ddbae --- /dev/null +++ b/test-suite/unit-tests/kernel/mod_subst_test.ml @@ -0,0 +1,175 @@ +open OUnit +open Utest +open Names +open Mod_subst + +let tests = ref [] +let add_test name test = tests := mk_test name (TestCase test) :: !tests + +let id = Id.of_string +let mp name = ModPath.MPfile (DirPath.make [id name]) +let dot path name = ModPath.MPdot (path, id name) +let kn path name = KerName.make path (id name) + +let assert_mp ?msg expected actual = + assert_equal ?msg ~cmp:ModPath.equal ~printer:ModPath.to_string expected actual + +let assert_kn ?msg expected actual = + assert_equal ?msg ~cmp:KerName.equal ~printer:KerName.to_string expected actual + +let assert_constant ?msg expected actual = + let cmp x y = + KerName.equal (Constant.user x) (Constant.user y) && + KerName.equal (Constant.canonical x) (Constant.canonical y) + in + assert_equal ?msg ~cmp ~printer:Constant.debug_to_string expected actual + +let assert_delta ?msg expected actual = + assert_equal ?msg ~printer:(fun x -> x) + (debug_string_of_delta expected) (debug_string_of_delta actual) + +let empty_map from_ to_ = map_mp from_ to_ (empty_delta_resolver to_) + +let sequential_mp subst1 subst2 path = subst_mp subst2 (subst_mp subst1 path) + +let () = add_test "join preserves sequential module-path substitution" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let subst1 = empty_map a b in + let subst2 = empty_map b c in + let subst = join subst1 subst2 in + List.iter (fun path -> + assert_mp (sequential_mp subst1 subst2 path) (subst_mp subst path)) + [a; dot a "Inner"; dot (dot a "Inner") "Nested"]; + assert_mp c (subst_mp subst a); + assert_mp (dot c "Inner") (subst_mp subst (dot a "Inner"))) + +let () = add_test "join handles empty and disjoint substitutions" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" and d = mp "D" in + let subst1 = empty_map a b in + let subst2 = empty_map c d in + let joined = join subst1 subst2 in + assert_mp b (subst_mp joined a); + assert_mp d (subst_mp joined c); + assert_mp b (subst_mp (join subst1 empty_subst) a); + assert_mp b (subst_mp (join empty_subst subst1) a)) + +let () = add_test "join resolves overlapping prefixes in order" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let b_inner = dot b "Inner" in + let subst1 = empty_map a b in + let subst2 = empty_map b_inner c in + let joined = join subst1 subst2 in + assert_mp c (subst_mp joined (dot a "Inner")); + assert_mp (dot c "Leaf") (subst_mp joined (dot (dot a "Inner") "Leaf"))) + +let () = add_test "join preserves unchanged module-path identity" (fun () -> + let a = mp "A" and b = mp "B" in + let untouched = dot (mp "Unchanged") "Inner" in + let joined = join (empty_map a b) (empty_map b (mp "C")) in + assert_bool "an unchanged path must retain pointer identity" + (subst_mp joined untouched == untouched)) + +let () = add_test "join substitutes bound module paths sequentially" (fun () -> + let a = mp "A" and b = mp "B" in + let mbid = MBId.make DirPath.empty (id "Arg") in + let subst1 = map_mbid mbid a (empty_delta_resolver a) in + let subst2 = empty_map a b in + let joined = join subst1 subst2 in + assert_mp b (subst_mp joined (ModPath.MPbound mbid)); + assert_mp (dot b "Field") + (subst_mp joined (dot (ModPath.MPbound mbid) "Field"))) + +let () = add_test "join preserves kernel-name and constant substitution" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let subst1 = empty_map a b in + let subst2 = empty_map b c in + let joined = join subst1 subst2 in + let name = kn a "value" in + assert_kn (subst_kn subst2 (subst_kn subst1 name)) (subst_kn joined name); + let constant = Constant.make1 name in + let sequential = subst_constant subst2 (subst_constant subst1 constant) in + assert_constant sequential (subst_constant joined constant)) + +let () = add_test "join substitutes inline bodies after expansion" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let value_a = kn a "value" and value_b = kn b "value" in + let body_b = Constant.make2 b (id "body") in + let body = { + UVars.univ_abstracted_value = + Constr.mkConstU (body_b, UVars.Instance.empty); + univ_abstracted_binder = UVars.AbstractContext.empty; + } in + let resolver1 = + empty_delta_resolver b + |> add_inline_delta_resolver value_b (0, Some body) + in + let subst1 = map_mp a b resolver1 in + let subst2 = empty_map b c in + let joined = join subst1 subst2 in + let constant = Constant.make1 value_a in + let _, joined_body = subst_con joined constant in + let _, first_body = subst_con subst1 constant in + let sequential_body = + Option.map (UVars.map_univ_abstracted (subst_mps subst2)) first_body + in + match sequential_body, joined_body with + | Some expected, Some actual -> + assert_bool "joined inline body differs from sequential application" + (Constr.equal expected.UVars.univ_abstracted_value + actual.UVars.univ_abstracted_value) + | None, None -> assert_failure "the inline hint was not exercised" + | _ -> assert_failure "join changed whether the constant is inlined") + +let () = add_test "joined substitutions act sequentially on resolver domains" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let resolver = + empty_delta_resolver a + |> add_mp_delta_resolver (dot a "Inner") (dot a "Canonical") + |> add_kn_delta_resolver (kn a "value") (kn (dot a "Canonical") "value") + in + let subst1 = empty_map a b in + let subst2 = empty_map b c in + let expected = + resolver + |> subst_dom_delta_resolver subst1 + |> subst_dom_delta_resolver subst2 + in + assert_delta expected (subst_dom_delta_resolver (join subst1 subst2) resolver)) + +let () = add_test "joined substitutions act sequentially on resolver codomains" (fun () -> + let root = mp "Root" and a = mp "A" and b = mp "B" and c = mp "C" in + let resolver = + empty_delta_resolver root + |> add_mp_delta_resolver (dot root "Inner") (dot a "Canonical") + |> add_kn_delta_resolver (kn root "value") (kn a "value") + in + let subst1 = empty_map a b in + let subst2 = empty_map b c in + let expected = + resolver + |> subst_codom_delta_resolver subst1 + |> subst_codom_delta_resolver subst2 + in + assert_delta expected (subst_codom_delta_resolver (join subst1 subst2) resolver)) + +let () = add_test "joined substitutions survive marshal round trips" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let joined = join (empty_map a b) (empty_map b c) in + let serialized = Marshal.to_string joined [] in + let restored : substitution = Marshal.from_string serialized 0 in + assert_mp c (subst_mp restored a); + assert_mp (dot c "Inner") (subst_mp restored (dot a "Inner"))) + +let () = add_test "long join chains preserve sequential behavior" (fun () -> + let rec build index current subst = + if Int.equal index 200 then current, subst + else + let next = mp ("M" ^ string_of_int (index + 1)) in + build (index + 1) next (join subst (empty_map current next)) + in + let start = mp "M0" in + let expected, subst = build 0 start empty_subst in + assert_mp expected (subst_mp subst start); + assert_mp (dot expected "Field") (subst_mp subst (dot start "Field"))) + +let () = run_tests __FILE__ (open_log_out_ch __FILE__) (List.rev !tests) From 4f9b551b2c5b49f5cfcff97d94b37438faa8641a Mon Sep 17 00:00:00 2001 From: Kanghee Park Date: Tue, 21 Jul 2026 05:39:20 +0000 Subject: [PATCH 2/5] Defer module substitution composition --- kernel/mod_subst.ml | 316 +++++++++++++----- kernel/mod_subst.mli | 4 + .../unit-tests/kernel/mod_subst_test.ml | 77 ++++- 3 files changed, 304 insertions(+), 93 deletions(-) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 88088010629c..8940d5ce3cc8 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -152,11 +152,32 @@ module Umap : let join map1 map2 = fold add_mp map1 map2 end -type substitution = delta_resolver Umap.t - -let empty_subst = Umap.empty - -let is_empty_subst = Umap.is_empty +type flat_substitution = delta_resolver Umap.t + +(* Substitutions are kept as a bounded sequence of flat maps. + [Compose (left, right)] means that [left] is applied before [right]. + The representation is deliberately made only of serializable values: module + substitutive objects retain substitutions in compiled files. *) +type substitution = + | Flat of flat_substitution + | Compose of { + left : substitution; + right : substitution; + leaves : int; + } + +let empty_subst = Flat Umap.empty + +let is_empty_subst = function + | Flat subst -> Umap.is_empty subst + | Compose _ -> false + +let rec fold_substitution f subst accu = + match subst with + | Flat subst -> f subst accu + | Compose { left; right; _ } -> + let accu = fold_substitution f left accu in + fold_substitution f right accu (* *) @@ -178,7 +199,8 @@ let debug_string_of_delta resolve = let list_contents subst = let one_pair reso = (ModPath.to_string (Deltamap.root reso), debug_string_of_delta reso) in let mp_one_pair mp0 p l = (ModPath.to_string mp0, one_pair p)::l in - Umap.fold mp_one_pair subst [] + let flat_contents subst l = Umap.fold mp_one_pair subst l in + fold_substitution flat_contents subst [] let debug_string_of_subst subst = let l = List.map (fun (s1,(s2,s3)) -> s1^"|->"^s2^"["^s3^"]") @@ -208,18 +230,17 @@ let add_kn_delta_resolver kn kn' = let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 -(** Extending a [substitution] without sequential composition *) - -let add_mbid mbid mp resolve s = +let map_mbid_flat mbid mp resolve = let () = assert (ModPath.equal mp (Deltamap.root resolve)) in - Umap.add_mbi mbid resolve s -let add_mp mp1 mp2 resolve s = + Umap.add_mbi mbid resolve Umap.empty + +let map_mp_flat mp1 mp2 resolve = let () = assert (ModPath.equal mp2 (Deltamap.root resolve)) in - Umap.add_mp mp1 resolve s + Umap.add_mp mp1 resolve Umap.empty + +let map_mbid mbid mp resolve = Flat (map_mbid_flat mbid mp resolve) -let map_mbid mbid mp resolve = - add_mbid mbid mp resolve empty_subst -let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst +let map_mp mp1 mp2 resolve = Flat (map_mp_flat mp1 mp2 resolve) let mp_in_delta mp = Deltamap.mem_mp mp @@ -288,7 +309,7 @@ let search_delta_inline resolve kn1 kn2 = try find kn2 with Not_found -> None -let subst_mp_opt subst mp = (* 's like subst *) +let subst_mp_opt_flat subst mp = (* 's like subst *) let repr r = Deltamap.root r, r in let rec aux mp = match mp with | MPfile _ | MPbound _ -> repr @@ Umap.find mp subst @@ -302,31 +323,31 @@ let subst_mp_opt subst mp = (* 's like subst *) in try Some (aux mp) with Not_found -> None -let subst_mp subst mp = - match subst_mp_opt subst mp with +let subst_mp_flat subst mp = + match subst_mp_opt_flat subst mp with None -> mp | Some (mp',_) -> mp' -let subst_kn_delta subst kn = +let subst_kn_delta_flat subst kn = let mp,l = KerName.repr kn in - match subst_mp_opt subst mp with + match subst_mp_opt_flat subst mp with Some (mp',resolve) -> solve_delta_kn resolve (KerName.make mp' l) | None -> Equiv kn -let subst_kn subst kn = +let subst_kn_flat subst kn = let mp,l = KerName.repr kn in - match subst_mp_opt subst mp with + match subst_mp_opt_flat subst mp with Some (mp',_) -> (KerName.make mp' l) | None -> kn exception No_subst -let subst_dual_mp subst mp1 mp2 = - let o1 = subst_mp_opt subst mp1 in - let o2 = if mp1 == mp2 then o1 else subst_mp_opt subst mp2 in +let subst_dual_mp_flat subst mp1 mp2 = + let o1 = subst_mp_opt_flat subst mp1 in + let o2 = if mp1 == mp2 then o1 else subst_mp_opt_flat subst mp2 in match o1, o2 with | None, None -> raise No_subst | Some (mp1',resolve), None -> mp1', mp2, resolve, true @@ -337,11 +358,11 @@ let progress f x ~orelse = let y = f x in if y != x then y else orelse -let subst_mind subst mind = +let subst_mind_flat subst mind = let mpu,l = KerName.repr (MutInd.user mind) in let mpc = KerName.modpath (MutInd.canonical mind) in try - let mpu,mpc,resolve,user = subst_dual_mp subst mpu mpc in + let mpu,mpc,resolve,user = subst_dual_mp_flat subst mpu mpc in let knu = KerName.make mpu l in let knc = if mpu == mpc then knu else KerName.make mpc l in let knc' = @@ -350,22 +371,22 @@ let subst_mind subst mind = MutInd.make knu knc' with No_subst -> mind -let subst_ind subst (ind,i as indi) = - let ind' = subst_mind subst ind in +let subst_ind_flat subst (ind,i as indi) = + let ind' = subst_mind_flat subst ind in if ind' == ind then indi else ind',i -let subst_constructor subst (ind,j as ref) = - let ind' = subst_ind subst ind in +let subst_constructor_flat subst (ind,j as ref) = + let ind' = subst_ind_flat subst ind in if ind==ind' then ref else (ind',j) -let subst_pind subst (ind,u) = - (subst_ind subst ind, u) +let subst_pind_flat subst (ind,u) = + (subst_ind_flat subst ind, u) -let subst_con0 subst cst = +let subst_con0_flat subst cst = let mpu,l = KerName.repr (Constant.user cst) in let mpc = KerName.modpath (Constant.canonical cst) in - let mpu,mpc,resolve,user = subst_dual_mp subst mpu mpc in + let mpu,mpc,resolve,user = subst_dual_mp_flat subst mpu mpc in let knu = KerName.make mpu l in let knc = if mpu == mpc then knu else KerName.make mpc l in let knc' = @@ -373,35 +394,14 @@ let subst_con0 subst cst = let cst' = Constant.make knu knc' in cst', search_delta_inline resolve knu knc -let subst_con subst cst = - try subst_con0 subst cst +let subst_con_flat subst cst = + try subst_con0_flat subst cst with No_subst -> cst, None -let subst_pcon subst (con,u as pcon) = - try let con', _can = subst_con0 subst con in - con',u - with No_subst -> pcon - -let subst_constant subst con = - try fst (subst_con0 subst con) +let subst_constant_flat subst con = + try fst (subst_con0_flat subst con) with No_subst -> con -let subst_proj_repr subst p = - Projection.Repr.map (subst_mind subst) p - -let subst_proj subst p = - Projection.map (subst_mind subst) p - -let subst_retro_action subst action = - let open Retroknowledge in - match action with - | Register_ind(prim,ind) -> - let ind' = subst_ind subst ind in - if ind == ind' then action else Register_ind(prim, ind') - | Register_type(prim,c) -> - let c' = subst_constant subst c in - if c == c' then action else Register_type(prim, c') - let rec map_kn f f' c = let func = map_kn f f' in match kind c with @@ -479,22 +479,80 @@ let rec map_kn f f' c = else mkCoFix (ln,(lna,tl',bl')) | _ -> c -let subst_mps subst c = +let subst_mps_flat subst c = let subst_pcon_term subst (con,u) = - let con', can = subst_con0 subst con in + let con', can = subst_con0_flat subst con in match can with | None -> mkConstU (con',u) | Some t -> Vars.univ_instantiate_constr u t in - if is_empty_subst subst then c - else map_kn (subst_mind subst) (subst_pcon_term subst) c + if Umap.is_empty subst then c + else map_kn (subst_mind_flat subst) (subst_pcon_term subst) c + +let subst_mp subst mp = + fold_substitution (fun subst mp -> subst_mp_flat subst mp) subst mp + +let subst_kn subst kn = + fold_substitution (fun subst kn -> subst_kn_flat subst kn) subst kn + +let subst_mind subst mind = + fold_substitution (fun subst mind -> subst_mind_flat subst mind) subst mind + +let subst_ind subst ind = + fold_substitution (fun subst ind -> subst_ind_flat subst ind) subst ind + +let subst_constructor subst cstr = + fold_substitution + (fun subst cstr -> subst_constructor_flat subst cstr) subst cstr + +let subst_pind subst pind = + fold_substitution (fun subst pind -> subst_pind_flat subst pind) subst pind + +let subst_con subst con = + let apply subst (con, body) = + match body with + | None -> subst_con_flat subst con + | Some body -> + let con = subst_constant_flat subst con in + let body = UVars.map_univ_abstracted (subst_mps_flat subst) body in + con, Some body + in + fold_substitution apply subst (con, None) + +let subst_pcon subst (con, u as pcon) = + let con' = fold_substitution + (fun subst con -> subst_constant_flat subst con) subst con + in + if con' == con then pcon else con', u + +let subst_constant subst con = + fold_substitution + (fun subst con -> subst_constant_flat subst con) subst con + +let subst_proj_repr subst p = + Projection.Repr.map (subst_mind subst) p + +let subst_proj subst p = + Projection.map (subst_mind subst) p + +let subst_retro_action subst action = + let open Retroknowledge in + match action with + | Register_ind (prim, ind) -> + let ind' = subst_ind subst ind in + if ind == ind' then action else Register_ind (prim, ind') + | Register_type (prim, c) -> + let c' = subst_constant subst c in + if c == c' then action else Register_type (prim, c') + +let subst_mps subst c = + fold_substitution (fun subst c -> subst_mps_flat subst c) subst c let subst_mps_aux subst = function | Inl (con, u) -> - begin match subst_con0 subst con with + begin match subst_con subst con with | con', None -> Inl (con', u) | _, Some t -> Inr (Vars.univ_instantiate_constr u t) - | exception No_subst -> Inl (con, u) end | Inr t -> Inr (subst_mps subst t) @@ -553,46 +611,62 @@ let subset_prefixed_by mp resolver = in Deltamap.fold mp_prefix kn_prefix resolver (empty_delta_resolver mp) -let subst_dom_delta_resolver subst resolver = +let subst_dom_delta_resolver_flat subst resolver = let mp_apply_subst mkey mequ rslv = - Deltamap.add_mp (subst_mp subst mkey) mequ rslv + Deltamap.add_mp (subst_mp_flat subst mkey) mequ rslv in let kn_apply_subst kkey hint rslv = - Deltamap.add_kn (subst_kn subst kkey) hint rslv + Deltamap.add_kn (subst_kn_flat subst kkey) hint rslv in - let root = subst_mp subst (Deltamap.root resolver) in + let root = subst_mp_flat subst (Deltamap.root resolver) in Deltamap.fold mp_apply_subst kn_apply_subst resolver (empty_delta_resolver root) -let subst_mp_delta subst mp mkey = - match subst_mp_opt subst mp with +let subst_mp_delta_flat subst mp mkey = + match subst_mp_opt_flat subst mp with None -> empty_delta_resolver mp, mp | Some (mp',resolve) -> (* root(resolve) ⊆ mp' *) let mp1 = find_prefix resolve mp' in let resolve1 = subset_prefixed_by mp1 resolve in - (subst_dom_delta_resolver - (map_mp mp1 mkey (empty_delta_resolver mkey)) resolve1), mp1 + (subst_dom_delta_resolver_flat + (map_mp_flat mp1 mkey (empty_delta_resolver mkey)) resolve1), mp1 -let gen_subst_delta_resolver dom subst resolver = +let gen_subst_delta_resolver_flat dom subst resolver = let mp_apply_subst mkey mequ rslv = - let mkey' = if dom then subst_mp subst mkey else mkey in - let rslv',mequ' = subst_mp_delta subst mequ mkey' in + let mkey' = if dom then subst_mp_flat subst mkey else mkey in + let rslv',mequ' = subst_mp_delta_flat subst mequ mkey' in Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv) in let kn_apply_subst kkey hint rslv = - let kkey' = if dom then subst_kn subst kkey else kkey in + let kkey' = if dom then subst_kn_flat subst kkey else kkey in let hint' = match hint with - | Equiv kequ -> subst_kn_delta subst kequ - | Inline (lev,Some t) -> Inline (lev,Some (UVars.map_univ_abstracted (subst_mps subst) t)) + | Equiv kequ -> subst_kn_delta_flat subst kequ + | Inline (lev,Some t) -> + Inline (lev,Some (UVars.map_univ_abstracted (subst_mps_flat subst) t)) | Inline (_,None) -> hint in Deltamap.add_kn kkey' hint' rslv in - let root = if dom then subst_mp subst (Deltamap.root resolver) else Deltamap.root resolver in + let root = + if dom then subst_mp_flat subst (Deltamap.root resolver) + else Deltamap.root resolver + in Deltamap.fold mp_apply_subst kn_apply_subst resolver (empty_delta_resolver root) -let subst_codom_delta_resolver = gen_subst_delta_resolver false -let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true +let subst_dom_delta_resolver subst resolver = + fold_substitution + (fun subst resolver -> subst_dom_delta_resolver_flat subst resolver) + subst resolver + +let subst_codom_delta_resolver subst resolver = + fold_substitution + (fun subst resolver -> gen_subst_delta_resolver_flat false subst resolver) + subst resolver + +let subst_dom_codom_delta_resolver subst resolver = + fold_substitution + (fun subst resolver -> gen_subst_delta_resolver_flat true subst resolver) + subst resolver let update_delta_resolver resolver1 resolver2 = let mp_apply_rslv mkey mequ rslv = @@ -618,34 +692,92 @@ let add_delta_resolver resolver1 resolver2 = in update_delta_resolver resolver1 resolver2 -let substitution_prefixed_by k mp subst = +let substitution_prefixed_by_flat k mp subst = let mp_prefixmp kmp reso subst = if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then let new_key = replace_mp_in_mp mp k kmp in Umap.add_mp new_key reso subst else subst in - Umap.fold mp_prefixmp subst empty_subst - -let join subst1 subst2 = + Umap.fold mp_prefixmp subst Umap.empty + +(* Eager composition is retained as the normalization oracle. It is used only + when a bounded composition is compacted or an API operation explicitly + requires a flat map. *) +let join_flat subst1 subst2 = + if Umap.is_empty subst1 then subst2 + else if Umap.is_empty subst2 then subst1 + else let apply_subst mpk resolve res = let mp = Deltamap.root resolve in - let mp', resolve' = match subst_mp_opt subst2 mp with + let mp', resolve' = match subst_mp_opt_flat subst2 mp with | None -> - let resolve' = subst_codom_delta_resolver subst2 resolve in + let resolve' = gen_subst_delta_resolver_flat false subst2 resolve in mp, resolve' | Some (mp', resolve') -> (* root(resolve') ⊆ mp' = subst2(mp) = root(subst_dom_codom_delta_resolver subst2 resolve) *) let resolve' = add_delta_resolver - (subst_dom_codom_delta_resolver subst2 resolve) resolve' + (gen_subst_delta_resolver_flat true subst2 resolve) resolve' in (* We need to reroot, as in general we only have root(resolve'') ⊆ mp' *) let resolve' = Deltamap.reroot mp' resolve' in mp', resolve' in - let prefixed_subst = substitution_prefixed_by mpk mp' subst2 in + let prefixed_subst = substitution_prefixed_by_flat mpk mp' subst2 in Umap.join prefixed_subst (Umap.add_mp mpk resolve' res) in - let subst = Umap.fold apply_subst subst1 empty_subst in + let subst = Umap.fold apply_subst subst1 Umap.empty in Umap.join subst2 subst + +let substitution_leaves = function + | Flat subst -> if Umap.is_empty subst then 0 else 1 + | Compose { leaves; _ } -> leaves + +let compose left right = + let leaves = substitution_leaves left + substitution_leaves right in + Compose { left; right; leaves } + +let rec flat_substitutions subst tail = + match subst with + | Flat subst -> if Umap.is_empty subst then tail else subst :: tail + | Compose { left; right; _ } -> + flat_substitutions left (flat_substitutions right tail) + +let rec compose_pairs accu = function + | [] -> List.rev accu + | [subst] -> List.rev (subst :: accu) + | subst1 :: subst2 :: rest -> + compose_pairs (join_flat subst1 subst2 :: accu) rest + +let rec normalize_substitutions = function + | [] -> Umap.empty + | [subst] -> subst + | substs -> normalize_substitutions (compose_pairs [] substs) + +let flatten_substitution subst = + normalize_substitutions (flat_substitutions subst []) + +(* Keeping at most this many flat leaves bounds lookup and term traversal while + allowing the common [Libobject.Ref] path to record composition without + eagerly traversing resolver maps. Compaction combines pairs of maps in + rounds instead of repeatedly rebuilding one ever-growing map. *) +let max_composition_leaves = 64 + +let join subst1 subst2 = + if is_empty_subst subst1 then subst2 + else if is_empty_subst subst2 then subst1 + else + let subst = compose subst1 subst2 in + if substitution_leaves subst <= max_composition_leaves then subst + else Flat (flatten_substitution subst) + +(** Extending a [substitution] without sequential composition requires a flat + map because the new binding overrides the composed map's domain directly. *) +let add_mbid mbid mp resolve subst = + let () = assert (ModPath.equal mp (Deltamap.root resolve)) in + Flat (Umap.add_mbi mbid resolve (flatten_substitution subst)) + +let add_mp mp1 mp2 resolve subst = + let () = assert (ModPath.equal mp2 (Deltamap.root resolve)) in + Flat (Umap.add_mp mp1 resolve (flatten_substitution subst)) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 6ec4ff53c82e..f3d6688af2ab 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -90,6 +90,10 @@ val map_mp : (** sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] + + Composition is recorded persistently and normalized after a bounded number + of components, so callers should use [join] rather than eagerly combining + resolver maps. *) val join : substitution -> substitution -> substitution diff --git a/test-suite/unit-tests/kernel/mod_subst_test.ml b/test-suite/unit-tests/kernel/mod_subst_test.ml index d42ff47ddbae..a0596c0419cb 100644 --- a/test-suite/unit-tests/kernel/mod_subst_test.ml +++ b/test-suite/unit-tests/kernel/mod_subst_test.ml @@ -152,6 +152,35 @@ let () = add_test "joined substitutions act sequentially on resolver codomains" in assert_delta expected (subst_codom_delta_resolver (join subst1 subst2) resolver)) +let () = add_test "joined substitutions act sequentially on resolver domains and codomains" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let resolver = + empty_delta_resolver a + |> add_mp_delta_resolver (dot a "Inner") (dot a "Canonical") + |> add_kn_delta_resolver (kn a "value") (kn (dot a "Canonical") "value") + in + let subst1 = empty_map a b in + let subst2 = empty_map b c in + let expected = + resolver + |> subst_dom_codom_delta_resolver subst1 + |> subst_dom_codom_delta_resolver subst2 + in + assert_delta expected + (subst_dom_codom_delta_resolver (join subst1 subst2) resolver)) + +let () = add_test "direct extensions preserve an already composed substitution" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let d = mp "D" and e = mp "E" in + let composed = join (empty_map a b) (empty_map b c) in + let extended = add_mp d e (empty_delta_resolver e) composed in + assert_mp c (subst_mp extended a); + assert_mp e (subst_mp extended d); + let mbid = MBId.make DirPath.empty (id "Arg") in + let extended = add_mbid mbid d (empty_delta_resolver d) composed in + assert_mp c (subst_mp extended a); + assert_mp d (subst_mp extended (ModPath.MPbound mbid))) + let () = add_test "joined substitutions survive marshal round trips" (fun () -> let a = mp "A" and b = mp "B" and c = mp "C" in let joined = join (empty_map a b) (empty_map b c) in @@ -162,7 +191,7 @@ let () = add_test "joined substitutions survive marshal round trips" (fun () -> let () = add_test "long join chains preserve sequential behavior" (fun () -> let rec build index current subst = - if Int.equal index 200 then current, subst + if Int.equal index 10000 then current, subst else let next = mp ("M" ^ string_of_int (index + 1)) in build (index + 1) next (join subst (empty_map current next)) @@ -172,4 +201,50 @@ let () = add_test "long join chains preserve sequential behavior" (fun () -> assert_mp expected (subst_mp subst start); assert_mp (dot expected "Field") (subst_mp subst (dot start "Field"))) +let () = add_test "right-associated join chains preserve sequential behavior" (fun () -> + let rec build index = + if Int.equal index 256 then empty_subst + else + let current = mp ("R" ^ string_of_int index) in + let next = mp ("R" ^ string_of_int (index + 1)) in + join (empty_map current next) (build (index + 1)) + in + let start = mp "R0" and expected = mp "R256" in + let subst = build 0 in + assert_mp expected (subst_mp subst start); + assert_mp (dot expected "Field") (subst_mp subst (dot start "Field"))) + +let () = add_test "bounded normalization preserves inline resolver semantics" (fun () -> + let first = mp "N0" and second = mp "N1" in + let source_name = kn first "value" and mapped_name = kn second "value" in + let body_constant = Constant.make2 second (id "body") in + let body = { + UVars.univ_abstracted_value = + Constr.mkConstU (body_constant, UVars.Instance.empty); + univ_abstracted_binder = UVars.AbstractContext.empty; + } in + let first_resolver = + empty_delta_resolver second + |> add_inline_delta_resolver mapped_name (0, Some body) + in + let rec extend index subst = + if Int.equal index 65 then subst + else + let current = mp ("N" ^ string_of_int index) in + let next = mp ("N" ^ string_of_int (index + 1)) in + extend (index + 1) (join subst (empty_map current next)) + in + let subst = extend 1 (map_mp first second first_resolver) in + let expected_path = mp "N65" in + let _, inline_body = subst_con subst (Constant.make1 source_name) in + match inline_body with + | None -> assert_failure "normalization discarded an inline resolver hint" + | Some body -> + let expected = + Constr.mkConstU + (Constant.make2 expected_path (id "body"), UVars.Instance.empty) + in + assert_bool "normalization did not substitute the inline body" + (Constr.equal expected body.UVars.univ_abstracted_value)) + let () = run_tests __FILE__ (open_log_out_ch __FILE__) (List.rev !tests) From 32024ec2139cda34d45f63c5a9a5ace885455b59 Mon Sep 17 00:00:00 2001 From: Kanghee Park Date: Tue, 21 Jul 2026 06:30:34 +0000 Subject: [PATCH 3/5] Validate composed substitution persistence --- checker/values.ml | 7 ++- ...-module-object-substitution-perf-Fixed.rst | 6 +++ .../unit-tests/kernel/mod_subst_test.ml | 54 +++++++++++++++++++ 3 files changed, 66 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/01-kernel/00000-module-object-substitution-perf-Fixed.rst diff --git a/checker/values.ml b/checker/values.ml index 412fd3c8ee6e..a0b7780742f4 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -306,7 +306,12 @@ let v_resolver = v_hmap v_kn v_delta_hint|] let v_subst = - v_annot_c ("substitution", v_map v_mp v_resolver) + fix (fun v_subst -> + v_annot_c + ("substitution", + v_sum "substitution_repr" 0 + [|[|v_map v_mp v_resolver|]; + [|v_subst; v_subst; v_int|]|])) (** kernel/lazyconstr *) diff --git a/doc/changelog/01-kernel/00000-module-object-substitution-perf-Fixed.rst b/doc/changelog/01-kernel/00000-module-object-substitution-perf-Fixed.rst new file mode 100644 index 000000000000..aa4cf4dc5b20 --- /dev/null +++ b/doc/changelog/01-kernel/00000-module-object-substitution-perf-Fixed.rst @@ -0,0 +1,6 @@ +- **Fixed:** + loading module parameters with many substitutive objects no longer repeatedly + rebuilds delta-resolver maps while composing substitutions. Sequential + compositions are recorded in a bounded persistent representation and + normalized only after a bounded number of components, substantially reducing + the time and memory needed for large module signatures. diff --git a/test-suite/unit-tests/kernel/mod_subst_test.ml b/test-suite/unit-tests/kernel/mod_subst_test.ml index a0596c0419cb..2317a90d775c 100644 --- a/test-suite/unit-tests/kernel/mod_subst_test.ml +++ b/test-suite/unit-tests/kernel/mod_subst_test.ml @@ -24,6 +24,28 @@ let assert_constant ?msg expected actual = in assert_equal ?msg ~cmp ~printer:Constant.debug_to_string expected actual +let assert_mind ?msg expected actual = + assert_equal ?msg ~cmp:MutInd.CanOrd.equal ~printer:MutInd.debug_to_string + expected actual + +let assert_ind ?msg expected actual = + let printer (mind, index) = + MutInd.debug_to_string mind ^ "," ^ string_of_int index + in + assert_equal ?msg ~cmp:Ind.CanOrd.equal ~printer expected actual + +let assert_constructor ?msg expected actual = + let printer ((mind, ind_index), cstr_index) = + MutInd.debug_to_string mind ^ "," ^ string_of_int ind_index ^ "," ^ + string_of_int cstr_index + in + assert_equal ?msg ~cmp:Construct.CanOrd.equal ~printer expected actual + +let assert_projection ?msg expected actual = + assert_equal ?msg ~cmp:Projection.CanOrd.equal + ~printer:Projection.debug_to_string + expected actual + let assert_delta ?msg expected actual = assert_equal ?msg ~printer:(fun x -> x) (debug_string_of_delta expected) (debug_string_of_delta actual) @@ -90,6 +112,38 @@ let () = add_test "join preserves kernel-name and constant substitution" (fun () let sequential = subst_constant subst2 (subst_constant subst1 constant) in assert_constant sequential (subst_constant joined constant)) +let () = add_test "join preserves inductive, projection, and term substitution" (fun () -> + let a = mp "A" and b = mp "B" and c = mp "C" in + let subst1 = empty_map a b in + let subst2 = empty_map b c in + let joined = join subst1 subst2 in + let mind = + MutInd.make (kn a "record") (kn (dot a "Canonical") "record") + in + let ind = mind, 0 in + let cstr = ind, 1 in + let projection = + Projection.Repr.make ind ~proj_npars:0 ~proj_arg:0 (id "field") + |> fun repr -> Projection.make repr false + in + let term = Constr.mkIndU (ind, UVars.Instance.empty) in + assert_mind + (subst_mind subst2 (subst_mind subst1 mind)) + (subst_mind joined mind); + assert_ind + (subst_ind subst2 (subst_ind subst1 ind)) + (subst_ind joined ind); + assert_constructor + (subst_constructor subst2 (subst_constructor subst1 cstr)) + (subst_constructor joined cstr); + assert_projection + (subst_proj subst2 (subst_proj subst1 projection)) + (subst_proj joined projection); + assert_bool "joined term substitution differs from sequential application" + (Constr.equal + (subst_mps subst2 (subst_mps subst1 term)) + (subst_mps joined term))) + let () = add_test "join substitutes inline bodies after expansion" (fun () -> let a = mp "A" and b = mp "B" and c = mp "C" in let value_a = kn a "value" and value_b = kn b "value" in From 1de45c08c796c20678fc0c0a6d92d8b2ca0df9b6 Mon Sep 17 00:00:00 2001 From: Kanghee Park Date: Tue, 21 Jul 2026 06:34:51 +0000 Subject: [PATCH 4/5] Link module substitution changelog --- ...-Fixed.rst => 2-module-object-substitution-perf-Fixed.rst} | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) rename doc/changelog/01-kernel/{00000-module-object-substitution-perf-Fixed.rst => 2-module-object-substitution-perf-Fixed.rst} (70%) diff --git a/doc/changelog/01-kernel/00000-module-object-substitution-perf-Fixed.rst b/doc/changelog/01-kernel/2-module-object-substitution-perf-Fixed.rst similarity index 70% rename from doc/changelog/01-kernel/00000-module-object-substitution-perf-Fixed.rst rename to doc/changelog/01-kernel/2-module-object-substitution-perf-Fixed.rst index aa4cf4dc5b20..90aa22bfb5d7 100644 --- a/doc/changelog/01-kernel/00000-module-object-substitution-perf-Fixed.rst +++ b/doc/changelog/01-kernel/2-module-object-substitution-perf-Fixed.rst @@ -3,4 +3,6 @@ rebuilds delta-resolver maps while composing substitutions. Sequential compositions are recorded in a bounded persistent representation and normalized only after a bounded number of components, substantially reducing - the time and memory needed for large module signatures. + the time and memory needed for large module signatures + (`#2 `_, + by Kanghee Park). From da2df15474784e3fd7fdd407eb65c74a10ea56a4 Mon Sep 17 00:00:00 2001 From: Kanghee Park Date: Wed, 22 Jul 2026 00:22:56 +0000 Subject: [PATCH 5/5] Remove module substitution changelog --- .../01-kernel/2-module-object-substitution-perf-Fixed.rst | 8 -------- 1 file changed, 8 deletions(-) delete mode 100644 doc/changelog/01-kernel/2-module-object-substitution-perf-Fixed.rst diff --git a/doc/changelog/01-kernel/2-module-object-substitution-perf-Fixed.rst b/doc/changelog/01-kernel/2-module-object-substitution-perf-Fixed.rst deleted file mode 100644 index 90aa22bfb5d7..000000000000 --- a/doc/changelog/01-kernel/2-module-object-substitution-perf-Fixed.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - loading module parameters with many substitutive objects no longer repeatedly - rebuilds delta-resolver maps while composing substitutions. Sequential - compositions are recorded in a bounded persistent representation and - normalized only after a bounded number of components, substantially reducing - the time and memory needed for large module signatures - (`#2 `_, - by Kanghee Park).