diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index b743b4dc6..91aa2da1a 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -513,6 +513,9 @@ module Make (F : Features.T) = struct (idents_of item)) in let aliases = + let inspect_view_last id = + List.last (Concrete_ident.to_view id).rel_path + in List.filter_map renamings ~f:(fun (origin_item, (from_id, to_id)) -> let attrs = List.filter @@ -527,7 +530,18 @@ module Make (F : Features.T) = struct when List.for_all variants ~f:(fun variant -> variant.is_record) && Concrete_ident.is_constructor from_id -> None + (* We don't need aliases for fields of types. *) + | Type _ when [%matches? Some (`Field _)] (inspect_view_last from_id) + -> + None + (* We don't need aliases for methods of trait impls. *) + | Impl _ + when [%matches? Some (`AssociatedItem _)] + (inspect_view_last from_id) -> + None | Quote _ -> None + (* This is temporary: see https://github.com/cryspen/hax/issues/1285 *) + | Trait { name; _ } when [%equal: concrete_ident] name from_id -> None | _ -> Some { attrs; span = origin_item.span; ident = from_id; v }) in let rename = diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti index b249cb49a..ddb9222be 100644 --- a/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti +++ b/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti @@ -1,3 +1,3 @@ module Core.Core_arch.X86.Pclmulqdq -val v__mm_clmulepi64_si128 : Rust_primitives.Integers.i32 -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i +val e_mm_clmulepi64_si128 : Rust_primitives.Integers.i32 -> Core.Core_arch.X86.t_e_ee_m128i -> Core.Core_arch.X86.t_e_ee_m128i -> Core.Core_arch.X86.t_e_ee_m128i diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti index 9e2419879..549a82f82 100644 --- a/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti +++ b/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti @@ -1,3 +1,3 @@ module Core.Core_arch.X86.Sse2 -val v__mm_set_epi64x: Rust_primitives.Integers.i64 -> Rust_primitives.Integers.i64 -> Core.Core_arch.X86.t____m128i +val e_mm_set_epi64x: Rust_primitives.Integers.i64 -> Rust_primitives.Integers.i64 -> Core.Core_arch.X86.t_e_ee_m128i diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.fsti index 5056e0e34..2305bd249 100644 --- a/proof-libs/fstar/core/Core.Core_arch.X86.fsti +++ b/proof-libs/fstar/core/Core.Core_arch.X86.fsti @@ -1,5 +1,5 @@ module Core.Core_arch.X86 -val t____m128i:Type0 +val t_e_ee_m128i:Type0 -val t____m256i:Type0 +val t_e_ee_m256i:Type0 diff --git a/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti b/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti index 48fbe8e42..a04253e2c 100644 --- a/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti +++ b/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti @@ -1,3 +1,3 @@ module Core.Core_arch.X86_64_.Sse2 -val v__mm_cvtsi128_si64: Core.Core_arch.X86.t____m128i -> Rust_primitives.Integers.i64 +val e_mm_cvtsi128_si64: Core.Core_arch.X86.t_e_ee_m128i -> Rust_primitives.Integers.i64 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 d0f4a2af0..eed36bb37 100644 --- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -247,11 +247,7 @@ include Cyclic_modules.Bundle_enums_a {T_B__from__enums_a as T_B} include Cyclic_modules.Bundle_enums_a {T_C__from__enums_a as T_C} -include Cyclic_modules.Bundle_enums_a {_0 as _0} - include Cyclic_modules.Bundle_enums_a {T_D as T_D} - -include Cyclic_modules.Bundle_enums_a {_0 as _0} ''' "Cyclic_modules.Enums_b.fst" = ''' module Cyclic_modules.Enums_b @@ -267,8 +263,6 @@ include Cyclic_modules.Bundle_enums_a {U_B as U_B} include Cyclic_modules.Bundle_enums_a {U_C as U_C} -include Cyclic_modules.Bundle_enums_a {_0 as _0} - include Cyclic_modules.Bundle_enums_a {t_T__from__enums_b as t_T} include Cyclic_modules.Bundle_enums_a {T_A as T_A} @@ -277,8 +271,6 @@ include Cyclic_modules.Bundle_enums_a {T_B as T_B} include Cyclic_modules.Bundle_enums_a {T_C as T_C} -include Cyclic_modules.Bundle_enums_a {_0 as _0} - include Cyclic_modules.Bundle_enums_a {f as f} ''' "Cyclic_modules.Late_skip_a.fst" = ''' @@ -373,15 +365,11 @@ include Cyclic_modules.Bundle_typ_a {t_TRec as t_TRec} include Cyclic_modules.Bundle_typ_a {TRec_T as TRec_T} -include Cyclic_modules.Bundle_typ_a {_0 as _0} - include Cyclic_modules.Bundle_typ_a {TRec_Empty as TRec_Empty} include Cyclic_modules.Bundle_typ_a {t_T as t_T} include Cyclic_modules.Bundle_typ_a {T_T as T_T} - -include Cyclic_modules.Bundle_typ_a {_0 as _0} ''' "Cyclic_modules.Typ_b.fst" = ''' module Cyclic_modules.Typ_b @@ -393,14 +381,10 @@ include Cyclic_modules.Bundle_typ_a {t_T1Rec as t_T1Rec} include Cyclic_modules.Bundle_typ_a {T1Rec_T1 as T1Rec_T1} -include Cyclic_modules.Bundle_typ_a {_0 as _0} - include Cyclic_modules.Bundle_typ_a {t_T2Rec as t_T2Rec} include Cyclic_modules.Bundle_typ_a {T2Rec_T2 as T2Rec_T2} -include Cyclic_modules.Bundle_typ_a {_0 as _0} - include Cyclic_modules.Bundle_typ_a {t_T1_cast_to_repr as t_T1_cast_to_repr} include Cyclic_modules.Bundle_typ_a {t_T1 as t_T1} @@ -410,8 +394,6 @@ include Cyclic_modules.Bundle_typ_a {T1_T1 as T1_T1} include Cyclic_modules.Bundle_typ_a {t_T2 as t_T2} include Cyclic_modules.Bundle_typ_a {T2_T2 as T2_T2} - -include Cyclic_modules.Bundle_typ_a {_0 as _0} ''' "Cyclic_modules.Variant_constructor_a.fst" = ''' module Cyclic_modules.Variant_constructor_a @@ -423,12 +405,8 @@ include Cyclic_modules.Bundle_variant_constructor_a {t_Context as t_Context} include Cyclic_modules.Bundle_variant_constructor_a {Context_A as Context_A} -include Cyclic_modules.Bundle_variant_constructor_a {_0 as _0} - include Cyclic_modules.Bundle_variant_constructor_a {Context_B as Context_B} -include Cyclic_modules.Bundle_variant_constructor_a {_0 as _0} - include Cyclic_modules.Bundle_variant_constructor_a {f as f} include Cyclic_modules.Bundle_variant_constructor_a {impl__test as impl_Context__test}