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 a54e28eeb..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,16 +457,33 @@ module Make (F : Features.T) = struct ( name, Concrete_ident.Create.move_under ~new_parent:new_name name ))) + | 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 + )) | _ -> [] in 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) *) 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 3edbdc730..1fc4b3c7a 100644 --- 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 index b59be2d80..4cf4d9486 100644 --- 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() + } + } +}