diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index a54e28eeb..b0345fed5 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -453,6 +453,11 @@ module Make (F : Features.T) = struct ( name, Concrete_ident.Create.move_under ~new_parent:new_name name ))) + | Some { v = Trait { items; _ }; _ } -> + List.map items ~f:(fun { ti_ident; _ } -> + ( ti_ident, + Concrete_ident.Create.move_under ~new_parent:new_name ti_ident + )) | _ -> [] in let variant_and_constructors_renamings = 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 3edbdc730..1fc4b3c7a 100644 --- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -216,6 +216,56 @@ include Cyclic_modules.M2.Rec_bundle_489499412 {d as d} include Cyclic_modules.M2.Rec_bundle_489499412 {b as b} ''' +"Cyclic_modules.Moved_trait.Nested.fst" = ''' +module Cyclic_modules.Moved_trait.Nested +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {t_St as t_St} + +include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {g as g} +''' +"Cyclic_modules.Moved_trait.Rec_bundle_963167032.fst" = ''' +module Cyclic_modules.Moved_trait.Rec_bundle_963167032 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +class v_Tr (v_Self: Type0) = { + f_f_pre:v_Self -> Type0; + f_f_post:v_Self -> Prims.unit -> Type0; + f_f:x0: v_Self -> Prims.Pure Prims.unit (f_f_pre x0) (fun result -> f_f_post x0 result) +} + +type t_St = | St : t_St + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl: v_Tr t_St = + { + f_f_pre = (fun (self: t_St) -> true); + f_f_post = (fun (self: t_St) (out: Prims.unit) -> true); + f_f = fun (self: t_St) -> () + } + +let g (x: t_St) : Prims.unit = f_f #t_St #FStar.Tactics.Typeclasses.solve x +''' +"Cyclic_modules.Moved_trait.fst" = ''' +module Cyclic_modules.Moved_trait +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {v_Tr as v_Tr} + +include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {f_f_pre as f_f_pre} + +include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {f_f_post as f_f_post} + +include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {f_f as f_f} + +include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {impl as impl} +''' "Cyclic_modules.Rec.fst" = ''' module Cyclic_modules.Rec #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/cyclic-modules/src/lib.rs b/tests/cyclic-modules/src/lib.rs index b59be2d80..4cf4d9486 100644 --- a/tests/cyclic-modules/src/lib.rs +++ b/tests/cyclic-modules/src/lib.rs @@ -166,3 +166,20 @@ pub mod variant_constructor_b { super::variant_constructor_a::Context::A(1) } } + +pub mod moved_trait { + impl Tr for nested::St { + fn f(self) {} + } + pub trait Tr { + fn f(self); + } + + pub mod nested { + use super::Tr; + pub struct St {} + fn g(x: St) { + x.f() + } + } +}