Merge pull request #1286 from cryspen/fix-naming-bundle-regression

fix(engine) Fix naming bundle regression

Author: maximebuyse

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 =

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

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

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

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

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}