Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(engine) Fix naming bundle regression #1286

Merged
merged 6 commits into from
Feb 5, 2025
Merged

fix(engine) Fix naming bundle regression #1286

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9a633b2
Remove aliases for struct fields.
maximebuyse Feb 3, 2025
bacca2e
Adapt some core lib names to nbew naming.
maximebuyse Feb 3, 2025
72c8a92
Filter out more problematic aliases.
maximebuyse Feb 3, 2025
0f1fc51
Test snapshot with no field include from bundle.
maximebuyse Feb 3, 2025
fe4e1e0
Keep aliases for trait methods.
maximebuyse Feb 4, 2025
1a045fb
Use %matches instead of pattern matching.
maximebuyse Feb 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions engine/lib/dependencies.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -527,7 +527,21 @@ 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 match List.last (Concrete_ident.to_view from_id).rel_path with
| Some (`Field _) -> true
| _ -> false ->
None
(* We don't need aliases for methods of trait impls. *)
| Impl _
when match List.last (Concrete_ident.to_view from_id).rel_path with
| Some (`AssociatedItem _) -> true
| _ -> false ->
None
maximebuyse marked this conversation as resolved.
Show resolved Hide resolved
| 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 =
Expand Down
2 changes: 1 addition & 1 deletion proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions proof-libs/fstar/core/Core.Core_arch.X86.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
22 changes: 0 additions & 22 deletions test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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}
Expand All @@ -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" = '''
Expand Down Expand Up @@ -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
Expand All @@ -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}
Expand All @@ -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
Expand All @@ -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}
Expand Down