diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index e367d7037..c5bebf76f 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -630,6 +630,10 @@ module Create = struct in let path = List.drop_last_exn old.def_id.path @ [ last ] in { old with def_id = { old.def_id with path } } + + let constructor name = + let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in + { name with def_id = { name.def_id with path } } end let lookup_raw_impl_info (impl : t) : Types.impl_infos option = diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index 8a5e413eb..e87f71b22 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/engine/lib/concrete_ident/concrete_ident.mli @@ -30,6 +30,10 @@ module Create : sig val fresh_module : from:t list -> t val move_under : new_parent:t -> t -> t + val constructor : t -> t + (** [constructor ident] adds a [Ctor] to [ident] + this allows to build a constructor from a variant name. *) + val map_last : f:(string -> string) -> t -> t (** [map_last f ident] applies [f] on the last chunk of [ident]'s path if it holds a string *) diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 2cbe2a32e..7d5570673 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -450,11 +450,19 @@ module Make (F : Features.T) = struct ))) | _ -> [] in - + let variant_and_constructors_renamings = + List.concat_map ~f:variants_renamings renamings + |> List.concat_map ~f:(fun (old_name, new_name) -> + [ + (old_name, new_name); + ( Concrete_ident.Create.constructor old_name, + Concrete_ident.Create.constructor new_name ); + ]) + in let renamings = Map.of_alist_exn (module Concrete_ident) - (renamings @ List.concat_map ~f:variants_renamings renamings) + (renamings @ variant_and_constructors_renamings) in let rename = let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap index 2b4320887..b1eaee72a 100644 --- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -32,7 +32,7 @@ module Cyclic_modules.B open Core open FStar.Mul -include Cyclic_modules.Rec_bundle_805309848 {g as g} +include Cyclic_modules.Rec_bundle_696247411 {g as g} ''' "Cyclic_modules.C.fst" = ''' module Cyclic_modules.C @@ -272,8 +272,8 @@ open FStar.Mul include Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 {f91805216 as f} ''' -"Cyclic_modules.Rec_bundle_805309848.fst" = ''' -module Cyclic_modules.Rec_bundle_805309848 +"Cyclic_modules.Rec_bundle_696247411.fst" = ''' +module Cyclic_modules.Rec_bundle_696247411 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -350,49 +350,94 @@ include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T2Rec as t_T2Rec} include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T2Rec_T2 as T2Rec_T2} ''' +"Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539.fst" = ''' +module Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_Context = + | Context_A : i32 -> t_Context + | Context_B : i32 -> t_Context + +let test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context = + Core.Option.impl__map #i32 #t_Context x Context_A + +let h (_: Prims.unit) : t_Context = Context_A 1l <: t_Context + +let f (_: Prims.unit) : t_Context = h () +''' +"Cyclic_modules.Variant_constructor_a.fst" = ''' +module Cyclic_modules.Variant_constructor_a +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {t_Context as t_Context} + +include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {Context_A as Context_A} + +include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {Context_B as Context_B} + +include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {test as impl__Context__test} + +include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {f as f} +''' +"Cyclic_modules.Variant_constructor_b.fst" = ''' +module Cyclic_modules.Variant_constructor_b +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {h as h} +''' "Cyclic_modules.fst" = ''' module Cyclic_modules #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -include Cyclic_modules.Rec_bundle_805309848 {b as b} +include Cyclic_modules.Rec_bundle_696247411 {b as b} + +include Cyclic_modules.Rec_bundle_696247411 {c as c} + +include Cyclic_modules.Rec_bundle_696247411 {d as d} -include Cyclic_modules.Rec_bundle_805309848 {c as c} +include Cyclic_modules.Rec_bundle_696247411 {de as de} -include Cyclic_modules.Rec_bundle_805309848 {d as d} +include Cyclic_modules.Rec_bundle_696247411 {disjoint_cycle_a as disjoint_cycle_a} -include Cyclic_modules.Rec_bundle_805309848 {de as de} +include Cyclic_modules.Rec_bundle_696247411 {disjoint_cycle_b as disjoint_cycle_b} -include Cyclic_modules.Rec_bundle_805309848 {disjoint_cycle_a as disjoint_cycle_a} +include Cyclic_modules.Rec_bundle_696247411 {e as e} -include Cyclic_modules.Rec_bundle_805309848 {disjoint_cycle_b as disjoint_cycle_b} +include Cyclic_modules.Rec_bundle_696247411 {enums_a as enums_a} -include Cyclic_modules.Rec_bundle_805309848 {e as e} +include Cyclic_modules.Rec_bundle_696247411 {enums_b as enums_b} -include Cyclic_modules.Rec_bundle_805309848 {enums_a as enums_a} +include Cyclic_modules.Rec_bundle_696247411 {m1 as m1} -include Cyclic_modules.Rec_bundle_805309848 {enums_b as enums_b} +include Cyclic_modules.Rec_bundle_696247411 {m2 as m2} -include Cyclic_modules.Rec_bundle_805309848 {m1 as m1} +include Cyclic_modules.Rec_bundle_696247411 {v_rec as v_rec} -include Cyclic_modules.Rec_bundle_805309848 {m2 as m2} +include Cyclic_modules.Rec_bundle_696247411 {rec1_same_name as rec1_same_name} -include Cyclic_modules.Rec_bundle_805309848 {v_rec as v_rec} +include Cyclic_modules.Rec_bundle_696247411 {rec2_same_name as rec2_same_name} -include Cyclic_modules.Rec_bundle_805309848 {rec1_same_name as rec1_same_name} +include Cyclic_modules.Rec_bundle_696247411 {std as std} -include Cyclic_modules.Rec_bundle_805309848 {rec2_same_name as rec2_same_name} +include Cyclic_modules.Rec_bundle_696247411 {typ_a as typ_a} -include Cyclic_modules.Rec_bundle_805309848 {std as std} +include Cyclic_modules.Rec_bundle_696247411 {typ_b as typ_b} -include Cyclic_modules.Rec_bundle_805309848 {typ_a as typ_a} +include Cyclic_modules.Rec_bundle_696247411 {variant_constructor_a as variant_constructor_a} -include Cyclic_modules.Rec_bundle_805309848 {typ_b as typ_b} +include Cyclic_modules.Rec_bundle_696247411 {variant_constructor_b as variant_constructor_b} -include Cyclic_modules.Rec_bundle_805309848 {f as f} +include Cyclic_modules.Rec_bundle_696247411 {f as f} -include Cyclic_modules.Rec_bundle_805309848 {h as h} +include Cyclic_modules.Rec_bundle_696247411 {h as h} -include Cyclic_modules.Rec_bundle_805309848 {h2 as h2} +include Cyclic_modules.Rec_bundle_696247411 {h2 as h2} ''' diff --git a/tests/cyclic-modules/src/lib.rs b/tests/cyclic-modules/src/lib.rs index 781a1e156..b59be2d80 100644 --- a/tests/cyclic-modules/src/lib.rs +++ b/tests/cyclic-modules/src/lib.rs @@ -146,3 +146,23 @@ pub mod disjoint_cycle_b { super::disjoint_cycle_a::g() } } + +pub mod variant_constructor_a { + pub enum Context { + A(i32), + B(i32), + } + pub fn f() -> Context { + super::variant_constructor_b::h() + } + impl Context { + pub fn test(x: Option) -> Option { + x.map(Self::A) + } + } +} +pub mod variant_constructor_b { + pub fn h() -> super::variant_constructor_a::Context { + super::variant_constructor_a::Context::A(1) + } +}