From 5530d5a69728f3f538d7ec7f2cc7cc524799d6a4 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Thu, 30 Jan 2025 11:11:49 +0100
Subject: [PATCH] Revert "Move trait methods in cyclic dependencies bundling."

This reverts commit 43829c4f115ae31932a11c7657e48332ef2f2f45.
---
 engine/lib/dependencies.ml                    |  5 --
 .../toolchain__cyclic-modules into-fstar.snap | 50 -------------------
 tests/cyclic-modules/src/lib.rs               | 17 -------
 3 files changed, 72 deletions(-)

diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 1b458e189..e314571a1 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -561,11 +561,6 @@ 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 3c32e55a4..e3ef061c7 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap	
@@ -259,56 +259,6 @@ include Cyclic_modules.M1.Cyclic_bundle_892895908 {b as b}
 
 include Cyclic_modules.M1.Cyclic_bundle_892895908 {c as c}
 '''
-"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 cb45f7b82..216a54812 100644
--- a/tests/cyclic-modules/src/lib.rs
+++ b/tests/cyclic-modules/src/lib.rs
@@ -178,20 +178,3 @@ pub mod late_skip_b {
         super::late_skip_a::f()
     }
 }
-
-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()
-        }
-    }
-}