From b6933c10980edc7cbb831b36791b646520d46ac1 Mon Sep 17 00:00:00 2001 From: Maxime Buyse 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 +++ .../toolchain__cyclic-modules into-fstar.snap | 34 +++++++++---------- 4 files changed, 46 insertions(+), 23 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 7ca56bcb6..aab94fca5 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1851,6 +1851,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 c4e3ab804..631959a0e 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) @@ -455,7 +459,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 @@ -465,11 +470,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 = match 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) *) 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 aa12360f2..54114bfa0 100644 --- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -259,18 +259,8 @@ include Cyclic_modules.M1.Cyclic_bundle_892895908 {d as d} include Cyclic_modules.M1.Cyclic_bundle_892895908 {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 +"Cyclic_modules.Moved_trait.Cyclic_bundle_202498800.fst" = ''' +module Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -293,21 +283,31 @@ let impl: v_Tr t_St = let g (x: t_St) : Prims.unit = f_f #t_St #FStar.Tactics.Typeclasses.solve x ''' +"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.Cyclic_bundle_202498800 {t_St as t_St} + +include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {g as g} +''' "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.Cyclic_bundle_202498800 {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.Cyclic_bundle_202498800 {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.Cyclic_bundle_202498800 {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.Cyclic_bundle_202498800 {f_f as f_f} -include Cyclic_modules.Moved_trait.Rec_bundle_963167032 {impl as impl} +include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {impl as impl} ''' "Cyclic_modules.Rec.fst" = ''' module Cyclic_modules.Rec