Skip to content

Commit c26cc9c

Browse files
W95PspW95Psp
authored
Merge pull request #1510 from cryspen/fun-ty-fix
Fix following merges changing the frontend AST
2 parents b3e7fcd + 5a5fc86 commit c26cc9c

File tree

3 files changed

+13
-13
lines changed

3 files changed

+13
-13
lines changed

‎frontend/exporter/src/types/new/full_def.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ pub enum FullDefKind<Body> {
277277
TraitAlias {
278278
#[value(get_param_env(s, s.owner_id()))]
279279
param_env: ParamEnv,
280-
#[value(implied_predicates(s.base().tcx, s.owner_id()).sinto(s))]
280+
#[value(implied_predicates(s.base().tcx, s.owner_id(), s.base().options.resolve_drop_bounds).sinto(s))]
281281
implied_predicates: GenericPredicates,
282282
/// The special `Self: Trait` clause.
283283
#[value(get_self_predicate(s))]

‎test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ class t_T (v_Self: Type0) = {
133133
val impl_T_for_u8:t_T u8
134134

135135
class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
136-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_1848985618546216515:Core.Clone.t_Clone v_U;
136+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_17366758704172627538:Core.Clone.t_Clone v_U;
137137
f_f_pre:v_U -> Type0;
138138
f_f_post:v_U -> v_Self -> Type0;
139139
f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)

‎test-harness/src/snapshots/toolchain__traits into-fstar.snap‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -35,11 +35,11 @@ open FStar.Mul
3535
class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
3636

3737
class t_ParBlocksSizeUser (v_Self: Type0) = {
38-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_3159012011946225137:t_BlockSizeUser v_Self
38+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_17815885805992953905:t_BlockSizeUser v_Self
3939
}
4040

4141
class t_BlockBackend (v_Self: Type0) = {
42-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_16388660322355014604:t_ParBlocksSizeUser v_Self;
42+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_3870134778723684320:t_ParBlocksSizeUser v_Self;
4343
f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
4444
f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
4545
f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global
@@ -55,7 +55,7 @@ open FStar.Mul
5555
class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
5656

5757
class t_Foo (v_Self: Type0) = {
58-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_5411500213814698936:t_Bar v_Self f_U;
58+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_13934332861551154312:t_Bar v_Self f_U;
5959
f_U:Type0
6060
}
6161
'''
@@ -425,11 +425,11 @@ let associated_function_caller
425425
()
426426

427427
class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
428-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_11151200176018912690:t_Trait v_Self
428+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_17329518651521910487:t_Trait v_Self
429429
v_TypeArg
430430
v_ConstArg;
431431
f_AssocType:Type0;
432-
f_AssocType_119499091631403638:t_Trait f_AssocType v_TypeArg v_ConstArg
432+
f_AssocType_14861369404924822957:t_Trait f_AssocType v_TypeArg v_ConstArg
433433
}
434434
'''
435435
"Traits.Interlaced_consts_types.fst" = '''
@@ -506,11 +506,11 @@ open FStar.Mul
506506

507507
class t_Trait1 (v_Self: Type0) = {
508508
f_T:Type0;
509-
f_T_4710375119464455744:t_Trait1 f_T
509+
f_T_8448309519961512781:t_Trait1 f_T
510510
}
511511

512512
class t_Trait2 (v_Self: Type0) = {
513-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_1575596395930652292:t_Trait1 v_Self;
513+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_6349185720639908215:t_Trait1 v_Self;
514514
f_U:Type0
515515
}
516516
'''
@@ -567,7 +567,7 @@ open Core
567567
open FStar.Mul
568568

569569
class t_SuperTrait (v_Self: Type0) = {
570-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_13802182059387893012:Core.Clone.t_Clone v_Self;
570+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_3462755511828336413:Core.Clone.t_Clone v_Self;
571571
f_function_of_super_trait_pre:v_Self -> Type0;
572572
f_function_of_super_trait_post:v_Self -> u32 -> Type0;
573573
f_function_of_super_trait:x0: v_Self
@@ -579,7 +579,7 @@ class t_SuperTrait (v_Self: Type0) = {
579579
[@@ FStar.Tactics.Typeclasses.tcinstance]
580580
let impl: t_SuperTrait i32 =
581581
{
582-
_super_13802182059387893012 = FStar.Tactics.Typeclasses.solve;
582+
_super_3462755511828336413 = FStar.Tactics.Typeclasses.solve;
583583
f_function_of_super_trait_pre = (fun (self: i32) -> true);
584584
f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true);
585585
f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl_i32__abs self <: i32) <: u32
@@ -651,7 +651,7 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit =
651651

652652
class t_Foo (v_Self: Type0) = {
653653
f_AssocType:Type0;
654-
f_AssocType_2403979284550981955:t_SuperTrait f_AssocType;
654+
f_AssocType_16748852984889271376:t_SuperTrait f_AssocType;
655655
f_N:usize;
656656
f_assoc_f_pre:Prims.unit -> Type0;
657657
f_assoc_f_post:Prims.unit -> Prims.unit -> Type0;
@@ -688,7 +688,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
688688
let impl_Foo_for_tuple_: t_Foo Prims.unit =
689689
{
690690
f_AssocType = i32;
691-
f_AssocType_2403979284550981955 = FStar.Tactics.Typeclasses.solve;
691+
f_AssocType_16748852984889271376 = FStar.Tactics.Typeclasses.solve;
692692
f_N = mk_usize 32;
693693
f_assoc_f_pre = (fun (_: Prims.unit) -> true);
694694
f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);

0 commit comments

Comments
 (0)