Rename trait methods in bundles for all backends, but include them on…

…ly for fstar (hack).
hacspec · Oct 30, 2024 · a582892 · a582892
1 parent 7f34b86
commit a582892
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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) *)