From a582892560265cee0a18cc5783e4a98073cda2fc Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Wed, 30 Oct 2024 17:40:52 +0100
Subject: [PATCH] Rename trait methods in bundles for all backends, but include
 them only for fstar (hack).

---
 engine/backends/fstar/fstar_backend.ml |  3 +++
 engine/lib/dependencies.ml             | 28 ++++++++++++++++++++------
 engine/lib/dependencies.mli            |  4 ++++
 3 files changed, 29 insertions(+), 6 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 96f97da8e..0c4fa54a9 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -1806,6 +1806,9 @@ let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) :
     (* else *)
     items
   in
+  (* This is a hack that should be removed
+     (see https://github.com/hacspec/hax/issues/1078) *)
+  Dependencies.includes_for_bundled_trait_methods := true;
   let items =
     TransformToInputLanguage.ditems items
     |> List.map ~f:unsize_as_identity
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index b0345fed5..22852a9c4 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -1,5 +1,9 @@
 open! Prelude
 
+(** This is a hack that should be removed
+    (see https://github.com/hacspec/hax/issues/1078) *)
+let includes_for_bundled_trait_methods = ref false
+
 module Make (F : Features.T) = struct
   module AST = Ast.Make (F)
   module U = Ast_utils.Make (F)
@@ -453,7 +457,8 @@ module Make (F : Features.T) = struct
                     ( name,
                       Concrete_ident.Create.move_under ~new_parent:new_name name
                     )))
-        | Some { v = Trait { items; _ }; _ } ->
+        | Some { v = Trait { items; _ }; _ }
+          when !includes_for_bundled_trait_methods ->
             List.map items ~f:(fun { ti_ident; _ } ->
                 ( ti_ident,
                   Concrete_ident.Create.move_under ~new_parent:new_name ti_ident
@@ -463,11 +468,22 @@ module Make (F : Features.T) = struct
       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 );
-               ])
+               let trait_methods_renamings =
+                 match from_ident old_name with
+                 | Some { v = Trait { items; _ }; _ }
+                   when not !includes_for_bundled_trait_methods ->
+                     List.map items ~f:(fun { ti_ident; _ } ->
+                         ( ti_ident,
+                           Concrete_ident.Create.move_under ~new_parent:new_name
+                             ti_ident ))
+                 | _ -> []
+               in
+               trait_methods_renamings
+               @ [
+                   (old_name, new_name);
+                   ( Concrete_ident.Create.constructor old_name,
+                     Concrete_ident.Create.constructor new_name );
+                 ])
       in
       let renamings =
         Map.of_alist_exn
diff --git a/engine/lib/dependencies.mli b/engine/lib/dependencies.mli
index 5c39773de..ab708e8b0 100644
--- a/engine/lib/dependencies.mli
+++ b/engine/lib/dependencies.mli
@@ -9,3 +9,7 @@ module Make (F : Features.T) : sig
   val filter_by_inclusion_clauses :
     Types.inclusion_clause list -> AST.item list -> AST.item list
 end
+
+val includes_for_bundled_trait_methods : bool ref
+(** This is a hack that should be removed
+    (see https://github.com/hacspec/hax/issues/1078) *)