Move trait methods in cyclic dependencies bundling.

hacspec · Oct 30, 2024 · 0a8b2d4 · 0a8b2d4
1 parent cd66c7c
commit 0a8b2d4
Show file tree

Hide file tree

Showing 3 changed files with 72 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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()
+        }
+    }
+}