From aedaffb46945c590e97154d75235208c6fcb1062 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 18 Nov 2024 15:53:28 +0100 Subject: [PATCH 1/8] Partially copy `rustc_target::Abi` --- frontend/exporter/src/types/hir.rs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs index 4287fb190..307120076 100644 --- a/frontend/exporter/src/types/hir.rs +++ b/frontend/exporter/src/types/hir.rs @@ -144,7 +144,18 @@ pub struct FnHeader { pub abi: Abi, } -sinto_todo!(rustc_target::spec::abi, Abi); +/// Reflects [`rustc_target::spec::abi::Abi`] +#[derive_group(Serializers)] +#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] +#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_target::spec::abi::Abi, state: S as s)] +pub enum Abi { + Rust, + C { + unwind: bool, + }, + #[todo] + Other(String), +} /// Function definition #[derive_group(Serializers)] From e1e4ab40f601c2b79b612b64fee519f83b5c554e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 18 Nov 2024 15:56:40 +0100 Subject: [PATCH 2/8] Simplify `get_function_from_operand` a bit --- frontend/exporter/src/types/mir.rs | 44 +++++++----------------------- 1 file changed, 10 insertions(+), 34 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index ecc4d9d72..fd1f45e3e 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -390,7 +390,7 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: BaseState<'tcx> + H let impl_expr = self_clause_for_item(s, &assoc, generics).unwrap(); // Return only the method generics; the trait generics are included in `impl_expr`. let method_generics = &generics[num_container_generics..]; - (method_generics.sinto(s), Option::Some(impl_expr)) + (method_generics.sinto(s), Some(impl_expr)) } rustc_middle::ty::AssocItemContainer::ImplContainer => { // Solve the trait constraints of the impl block. @@ -399,12 +399,12 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: BaseState<'tcx> + H let container_trait_refs = solve_item_required_traits(s, container_def_id, container_generics); trait_refs.extend(container_trait_refs); - (generics.sinto(s), Option::None) + (generics.sinto(s), None) } } } else { // Regular function call - (generics.sinto(s), Option::None) + (generics.sinto(s), None) }; (def_id.sinto(s), generics, trait_refs, source) @@ -420,44 +420,20 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>( s: &S, func: &rustc_middle::mir::Operand<'tcx>, ) -> (FunOperand, Vec, Vec, Option) { - use std::ops::Deref; // Match on the func operand: it should be a constant as we don't support // closures for now. - use rustc_middle::mir::{Const, Operand}; + use rustc_middle::mir::Operand; use rustc_middle::ty::TyKind; match func { Operand::Constant(c) => { - // Regular function case - let c = c.deref(); - let (def_id, generics) = match &c.const_ { - Const::Ty(c_ty, _c) => { - // The type of the constant should be a FnDef, allowing - // us to retrieve the function's identifier and instantiation. - assert!(c_ty.is_fn()); - match c_ty.kind() { - TyKind::FnDef(def_id, generics) => (*def_id, *generics), - _ => { - unreachable!(); - } - } - } - Const::Val(_, c_ty) => { - // Same as for the `Ty` case above - assert!(c_ty.is_fn()); - match c_ty.kind() { - TyKind::FnDef(def_id, generics) => (*def_id, *generics), - _ => { - unreachable!(); - } - } - } - Const::Unevaluated(_, _) => { - unimplemented!(); - } + let c_ty = c.const_.ty(); + // The type of the constant should be a FnDef, allowing us to retrieve the function's + // identifier and instantiation. + let TyKind::FnDef(def_id, generics) = c_ty.kind() else { + unreachable!(); }; - let (fun_id, generics, trait_refs, trait_info) = - get_function_from_def_id_and_generics(s, def_id, generics); + get_function_from_def_id_and_generics(s, *def_id, *generics); (FunOperand::Id(fun_id), generics, trait_refs, trait_info) } Operand::Move(place) => { From 6719e5001148be47c60a2fc42f11ac58b51a7dd5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 19 Nov 2024 16:28:41 +0100 Subject: [PATCH 3/8] Expose `Ty::new` --- frontend/exporter/src/types/ty.rs | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index c254bb0b7..9dfad01de 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -743,6 +743,15 @@ pub struct Ty { } impl Ty { + #[cfg(feature = "rustc")] + pub fn new<'tcx, S: BaseState<'tcx>>(s: &S, kind: TyKind) -> Self { + s.with_global_cache(|cache| { + let table_session = &mut cache.id_table_session; + let kind = id_table::Node::new(kind, table_session); + Ty { kind } + }) + } + pub fn inner(&self) -> &Arc { self.kind.inner() } @@ -758,15 +767,12 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_middle::ty::Ty<'tcx> if let Some(ty) = s.with_cache(|cache| cache.tys.get(self).cloned()) { return ty; } - let ty_kind: TyKind = self.kind().sinto(s); - s.with_global_cache(|cache| { - let table_session = &mut cache.id_table_session; - let cache = cache.per_item.entry(s.owner_id()).or_default(); - let kind = id_table::Node::new(ty_kind, table_session); - let ty = Ty { kind }; + let kind: TyKind = self.kind().sinto(s); + let ty = Ty::new(s, kind); + s.with_cache(|cache| { cache.tys.insert(*self, ty.clone()); - ty - }) + }); + ty } } From c47610f1898dafc3225bf3d79d448ab5e3647cdb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 19 Nov 2024 17:24:14 +0100 Subject: [PATCH 4/8] Mini clarification --- frontend/exporter/src/types/mir.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index fd1f45e3e..fa04da2b2 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -954,13 +954,13 @@ pub enum AggregateKind { let closure = generics.as_closure(); let sig = closure.sig().sinto(s); - // Solve the predicates from the parent (i.e., the function which calls the closure). + // Solve the predicates from the parent (i.e., the item which defines the closure). let tcx = s.base().tcx; let parent_generics = closure.parent_args(); - let generics = tcx.mk_args(parent_generics); + let parent_generics_ref = tcx.mk_args(parent_generics); // TODO: does this handle nested closures? let parent = tcx.generics_of(rust_id).parent.unwrap(); - let trait_refs = solve_item_required_traits(s, parent, generics); + let trait_refs = solve_item_required_traits(s, parent, parent_generics_ref); AggregateKind::Closure(def_id, parent_generics.sinto(s), trait_refs, sig) })] From 9f6c8343261c785687451fe167ede3810439ef85 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 19 Nov 2024 17:53:13 +0100 Subject: [PATCH 5/8] Improve translation of MIR calls --- frontend/exporter/src/types/mir.rs | 45 +++++++++++------------------- 1 file changed, 17 insertions(+), 28 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index fa04da2b2..db5839bc9 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -410,51 +410,40 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: BaseState<'tcx> + H (def_id.sinto(s), generics, trait_refs, source) } +/// Get a `FunOperand` from an `Operand` used in a function call. /// Return the [DefId] of the function referenced by an operand, with the /// parameters substitution. /// The [Operand] comes from a [TerminatorKind::Call]. -/// Only supports calls to top-level functions (which are considered as constants -/// by rustc); doesn't support closures for now. #[cfg(feature = "rustc")] fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>( s: &S, - func: &rustc_middle::mir::Operand<'tcx>, + op: &rustc_middle::mir::Operand<'tcx>, ) -> (FunOperand, Vec, Vec, Option) { // Match on the func operand: it should be a constant as we don't support // closures for now. use rustc_middle::mir::Operand; use rustc_middle::ty::TyKind; - match func { - Operand::Constant(c) => { - let c_ty = c.const_.ty(); - // The type of the constant should be a FnDef, allowing us to retrieve the function's - // identifier and instantiation. - let TyKind::FnDef(def_id, generics) = c_ty.kind() else { - unreachable!(); - }; - let (fun_id, generics, trait_refs, trait_info) = - get_function_from_def_id_and_generics(s, *def_id, *generics); - (FunOperand::Id(fun_id), generics, trait_refs, trait_info) + let ty = op.ty(&s.mir().local_decls, s.base().tcx); + trace!("type: {:?}", ty); + // If the type of the value is one of the singleton types that corresponds to each function, + // that's enough information. + if let TyKind::FnDef(def_id, generics) = ty.kind() { + let (fun_id, generics, trait_refs, trait_info) = + get_function_from_def_id_and_generics(s, *def_id, *generics); + return (FunOperand::Id(fun_id), generics, trait_refs, trait_info); + } + match op { + Operand::Constant(_) => { + unimplemented!("{:?}", op); } Operand::Move(place) => { - // Closure case. - // The closure can not have bound variables nor trait references, - // so we don't need to extract generics, trait refs, etc. - let body = s.mir(); - let ty = func.ty(&body.local_decls, s.base().tcx); - trace!("type: {:?}", ty); - trace!("type kind: {:?}", ty.kind()); - let sig = match ty.kind() { - rustc_middle::ty::TyKind::FnPtr(sig, ..) => sig, - _ => unreachable!(), - }; - trace!("FnPtr: {:?}", sig); + // Function pointer. A fn pointer cannot have bound variables or trait references, so + // we don't need to extract generics, trait refs, etc. let place = place.sinto(s); - (FunOperand::Move(place), Vec::new(), Vec::new(), None) } Operand::Copy(_place) => { - unimplemented!("{:?}", func); + unimplemented!("{:?}", op); } } } From d83c24a47a87129d44daf675df6dd22ff99464e7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 19 Nov 2024 17:25:08 +0100 Subject: [PATCH 6/8] Add more info to `FullDefKind::Ctor` --- frontend/exporter/src/traits/resolution.rs | 2 +- frontend/exporter/src/types/new/full_def.rs | 39 +++++++++++++++++++-- frontend/exporter/src/types/ty.rs | 9 +++-- 3 files changed, 42 insertions(+), 8 deletions(-) diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index f7c67a86b..53379a6a5 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -121,7 +121,7 @@ fn initial_search_predicates<'tcx>( use DefKind::*; match tcx.def_kind(def_id) { // These inherit some predicates from their parent. - AssocTy | AssocFn | AssocConst | Closure => { + AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant => { let parent = tcx.parent(def_id); acc_predicates(tcx, parent, predicates, pred_id); } diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index eabdde186..cacd983e4 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -350,8 +350,15 @@ pub enum FullDefKind { // ADT parts /// Refers to the variant definition, [`DefKind::Ctor`] refers to its constructor if it exists. Variant, - /// Refers to the struct or enum variant's constructor. - Ctor(CtorOf, CtorKind), + /// The constructor function of a tuple/unit struct or tuple/unit enum variant. + #[custom_arm(RDefKind::Ctor(ctor_of, _) => get_ctor_contents(s, ctor_of.sinto(s)),)] + Ctor { + adt_def_id: DefId, + ctor_of: CtorOf, + variant_id: VariantIdx, + fields: IndexVec, + output_ty: Ty, + }, /// A field in a struct, enum or union. e.g. /// - `bar` in `struct Foo { bar: u8 }` /// - `Foo::Bar::0` in `enum Foo { Bar(u8) }` @@ -762,6 +769,34 @@ where } } +#[cfg(feature = "rustc")] +fn get_ctor_contents<'tcx, S, Body>(s: &S, ctor_of: CtorOf) -> FullDefKind +where + S: UnderOwnerState<'tcx>, + Body: IsBody + TypeMappable, +{ + let tcx = s.base().tcx; + let def_id = s.owner_id(); + + // The def_id of the adt this ctor belongs to. + let adt_def_id = match ctor_of { + CtorOf::Struct => tcx.parent(def_id), + CtorOf::Variant => tcx.parent(tcx.parent(def_id)), + }; + let adt_def = tcx.adt_def(adt_def_id); + let variant_id = adt_def.variant_index_with_ctor_id(def_id); + let fields = adt_def.variant(variant_id).fields.sinto(s); + let generic_args = ty::GenericArgs::identity_for_item(tcx, adt_def_id); + let output_ty = ty::Ty::new_adt(tcx, adt_def, generic_args).sinto(s); + FullDefKind::Ctor { + adt_def_id: adt_def_id.sinto(s), + ctor_of, + variant_id: variant_id.sinto(s), + fields, + output_ty, + } +} + /// This normalizes trait clauses before calling `sinto` on them. This is a bit of a hack required /// by charon for now. We can't normalize all clauses as this would lose region information in /// outlives clauses. diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 9dfad01de..457f8193c 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -341,11 +341,10 @@ pub struct VariantDef { pub name: Symbol, pub discr_def: DiscriminantDefinition, pub discr_val: DiscriminantValue, - /// The definitions of the fields on this variant. In case of - /// [tuple - /// structs](https://doc.rust-lang.org/book/ch05-01-defining-structs.html#using-tuple-structs-without-named-fields-to-create-different-types), + /// The definitions of the fields on this variant. In case of [tuple + /// structs/variants](https://doc.rust-lang.org/book/ch05-01-defining-structs.html#using-tuple-structs-without-named-fields-to-create-different-types), /// the fields are anonymous, otherwise fields are named. - pub fields: Vec, + pub fields: IndexVec, /// Span of the definition of the variant pub span: Span, } @@ -363,7 +362,7 @@ impl VariantDef { name: def.name.sinto(s), discr_def: def.discr.sinto(s), discr_val: discr_val.sinto(s), - fields: def.fields.raw.sinto(s), + fields: def.fields.sinto(s), span: s.base().tcx.def_span(def.def_id).sinto(s), } } From 494c76afe41dc510f743375e92c93942492bc20a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 20 Nov 2024 15:33:20 +0100 Subject: [PATCH 7/8] Reorder some defs --- frontend/exporter/src/types/ty.rs | 98 +++++++++++++++---------------- 1 file changed, 49 insertions(+), 49 deletions(-) diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 457f8193c..6aa480c64 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -1316,39 +1316,6 @@ pub enum PredicateKind { NormalizesTo(NormalizesTo), } -#[cfg(feature = "rustc")] -fn get_container_for_assoc_item<'tcx, S: BaseState<'tcx>>( - s: &S, - item: &ty::AssocItem, -) -> AssocItemContainer { - let tcx = s.base().tcx; - let container_id = item.container_id(tcx); - match item.container { - ty::AssocItemContainer::TraitContainer => AssocItemContainer::TraitContainer { - trait_id: container_id.sinto(s), - }, - ty::AssocItemContainer::ImplContainer => { - if let Some(implemented_trait_item) = item.trait_item_def_id { - // The trait ref that is being implemented by this `impl` block. - let implemented_trait_ref = tcx - .impl_trait_ref(container_id) - .unwrap() - .instantiate_identity(); - AssocItemContainer::TraitImplContainer { - impl_id: container_id.sinto(s), - implemented_trait: implemented_trait_ref.def_id.sinto(s), - implemented_trait_item: implemented_trait_item.sinto(s), - overrides_default: tcx.defaultness(implemented_trait_item).has_value(), - } - } else { - AssocItemContainer::InherentImplContainer { - impl_id: container_id.sinto(s), - } - } - } - } -} - /// Reflects [`ty::AssocItem`] #[derive(AdtInto)] #[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocItem, state: S as s)] @@ -1368,19 +1335,15 @@ pub struct AssocItem { pub opt_rpitit_info: Option, } -/// Reflects [`ty::ImplTraitInTraitData`] +/// Reflects [`ty::AssocKind`] #[derive(AdtInto)] -#[args(<'tcx, S: BaseState<'tcx>>, from: ty::ImplTraitInTraitData, state: S as _s)] +#[args(, from: ty::AssocKind, state: S as _tcx)] #[derive_group(Serializers)] #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub enum ImplTraitInTraitData { - Trait { - fn_def_id: DefId, - opaque_def_id: DefId, - }, - Impl { - fn_def_id: DefId, - }, +pub enum AssocKind { + Const, + Fn, + Type, } #[derive_group(Serializers)] @@ -1402,13 +1365,50 @@ pub enum AssocItemContainer { }, } -/// Reflects [`ty::AssocKind`] +#[cfg(feature = "rustc")] +fn get_container_for_assoc_item<'tcx, S: BaseState<'tcx>>( + s: &S, + item: &ty::AssocItem, +) -> AssocItemContainer { + let tcx = s.base().tcx; + let container_id = item.container_id(tcx); + match item.container { + ty::AssocItemContainer::TraitContainer => AssocItemContainer::TraitContainer { + trait_id: container_id.sinto(s), + }, + ty::AssocItemContainer::ImplContainer => { + if let Some(implemented_trait_item) = item.trait_item_def_id { + // The trait ref that is being implemented by this `impl` block. + let implemented_trait_ref = tcx + .impl_trait_ref(container_id) + .unwrap() + .instantiate_identity(); + AssocItemContainer::TraitImplContainer { + impl_id: container_id.sinto(s), + implemented_trait: implemented_trait_ref.def_id.sinto(s), + implemented_trait_item: implemented_trait_item.sinto(s), + overrides_default: tcx.defaultness(implemented_trait_item).has_value(), + } + } else { + AssocItemContainer::InherentImplContainer { + impl_id: container_id.sinto(s), + } + } + } + } +} + +/// Reflects [`ty::ImplTraitInTraitData`] #[derive(AdtInto)] -#[args(, from: ty::AssocKind, state: S as _tcx)] +#[args(<'tcx, S: BaseState<'tcx>>, from: ty::ImplTraitInTraitData, state: S as _s)] #[derive_group(Serializers)] #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub enum AssocKind { - Const, - Fn, - Type, +pub enum ImplTraitInTraitData { + Trait { + fn_def_id: DefId, + opaque_def_id: DefId, + }, + Impl { + fn_def_id: DefId, + }, } From a8dfb6ff4971633c0245ec0f51510b2d474907e5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 20 Nov 2024 15:58:27 +0100 Subject: [PATCH 8/8] Get parent generics in `AssocItem` --- frontend/exporter/src/types/ty.rs | 28 ++++++++++++++----- .../toolchain__traits into-fstar.snap | 12 ++++---- 2 files changed, 27 insertions(+), 13 deletions(-) diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 6aa480c64..c0b12fd4d 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -1350,11 +1350,18 @@ pub enum AssocKind { #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] pub enum AssocItemContainer { TraitContainer { - trait_id: DefId, + trait_ref: TraitRef, }, TraitImplContainer { + /// The def_id of the impl block. impl_id: DefId, - implemented_trait: DefId, + /// The generics applied to the impl block (that's just the identity generics). + impl_generics: Vec, + /// The impl exprs applied to the impl block (again the identity). + impl_required_impl_exprs: Vec, + /// The trait ref implemented by the impl block. + implemented_trait_ref: TraitRef, + /// The def_id of the associated item (in the trait declaration) that is being implemented. implemented_trait_item: DefId, /// Whether the corresponding trait item had a default (and therefore this one overrides /// it). @@ -1371,21 +1378,28 @@ fn get_container_for_assoc_item<'tcx, S: BaseState<'tcx>>( item: &ty::AssocItem, ) -> AssocItemContainer { let tcx = s.base().tcx; + // We want to solve traits in the context of this item. + let state_with_id = &with_owner_id(s.base(), (), (), item.def_id); let container_id = item.container_id(tcx); match item.container { - ty::AssocItemContainer::TraitContainer => AssocItemContainer::TraitContainer { - trait_id: container_id.sinto(s), - }, + ty::AssocItemContainer::TraitContainer => { + let trait_ref = ty::TraitRef::identity(tcx, container_id).sinto(state_with_id); + AssocItemContainer::TraitContainer { trait_ref } + } ty::AssocItemContainer::ImplContainer => { if let Some(implemented_trait_item) = item.trait_item_def_id { - // The trait ref that is being implemented by this `impl` block. + let impl_generics = ty::GenericArgs::identity_for_item(tcx, container_id); + let impl_required_impl_exprs = + solve_item_required_traits(state_with_id, container_id, impl_generics); let implemented_trait_ref = tcx .impl_trait_ref(container_id) .unwrap() .instantiate_identity(); AssocItemContainer::TraitImplContainer { impl_id: container_id.sinto(s), - implemented_trait: implemented_trait_ref.def_id.sinto(s), + impl_generics: impl_generics.sinto(state_with_id), + impl_required_impl_exprs, + implemented_trait_ref: implemented_trait_ref.sinto(state_with_id), implemented_trait_item: implemented_trait_item.sinto(s), overrides_default: tcx.defaultness(implemented_trait_item).has_value(), } diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 3ada99292..fcc166dc9 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -55,7 +55,7 @@ open FStar.Mul class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit } class t_Foo (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_12056653545434731362:t_Bar v_Self f_U; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_5461126672499050919:t_Bar v_Self f_U; f_U:Type0 } ''' @@ -391,7 +391,7 @@ class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { v_TypeArg v_ConstArg; f_AssocType:Type0; - f_AssocType_10469511598065652520:t_Trait f_AssocType v_TypeArg v_ConstArg + f_AssocType_5566993444404141271:t_Trait f_AssocType v_TypeArg v_ConstArg } ''' "Traits.Interlaced_consts_types.fst" = ''' @@ -468,7 +468,7 @@ open FStar.Mul class t_Trait1 (v_Self: Type0) = { f_T:Type0; - f_T_1640036513185240095:t_Trait1 f_T + f_T_7805326132379548775:t_Trait1 f_T } class t_Trait2 (v_Self: Type0) = { @@ -613,8 +613,8 @@ let use_impl_trait (_: Prims.unit) : Prims.unit = class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_15525962639250476383:t_SuperTrait f_AssocType; - f_AssocType_17265963849229885182:Core.Clone.t_Clone f_AssocType; + f_AssocType_15012754260415912210:t_SuperTrait f_AssocType; + f_AssocType_3242921639065184873:Core.Clone.t_Clone f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> Type0; f_assoc_f_post:Prims.unit -> Prims.unit -> Type0; @@ -651,7 +651,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; - f_AssocType_15525962639250476383 = FStar.Tactics.Typeclasses.solve; + f_AssocType_15012754260415912210 = FStar.Tactics.Typeclasses.solve; f_N = sz 32; f_assoc_f_pre = (fun (_: Prims.unit) -> true); f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);