From 46271b2c5fb97bbcf1bd2c2fe7051faa356f28b8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 16 Jan 2025 14:58:39 +0100 Subject: [PATCH] Add more info to `ImplExprAtom::Builtin` --- engine/lib/import_thir.ml | 2 +- frontend/exporter/src/traits.rs | 14 ++- frontend/exporter/src/traits/resolution.rs | 86 +++++++++++++++++-- .../toolchain__traits into-fstar.snap | 10 +-- 4 files changed, 97 insertions(+), 15 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 646e43d9e..2a47901ac 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1147,7 +1147,7 @@ end) : EXPR = struct List.fold ~init ~f:browse_path path | Dyn -> Dyn | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path - | Builtin { trait } -> Builtin (c_trait_ref span trait.value) + | Builtin { trait; _ } -> Builtin (c_trait_ref span trait.value) | Error str -> failwith @@ "impl_expr_atom: Error " ^ str and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 2b0804ea2..6cf6d99e1 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -92,8 +92,18 @@ pub enum ImplExprAtom { /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that /// built-in implementation. Dyn, - /// A built-in trait whose implementation is computed by the compiler, such as `Sync`. - Builtin { r#trait: Binder }, + /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This + /// morally points to an invisible `impl` block; as such it contains the information we may + /// need from one. + Builtin { + r#trait: Binder, + /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration. + /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T: + /// FnOnce`. + impl_exprs: Vec, + /// The values of the associated types for this trait. + types: Vec<(DefId, Ty)>, + }, /// An error happened while resolving traits. Error(String), } diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index fb949eb1c..8da38c203 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -73,8 +73,18 @@ pub enum ImplExprAtom<'tcx> { /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that /// built-in implementation. Dyn, - /// A built-in trait whose implementation is computed by the compiler, such as `Sync`. - Builtin { r#trait: PolyTraitRef<'tcx> }, + /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This + /// morally points to an invisible `impl` block; as such it contains the information we may + /// need from one. + Builtin { + r#trait: PolyTraitRef<'tcx>, + /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration. + /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T: + /// FnOnce`. + impl_exprs: Vec>, + /// The values of the associated types for this trait. + types: Vec<(DefId, Ty<'tcx>)>, + }, /// An error happened while resolving traits. Error(String), } @@ -290,7 +300,7 @@ impl<'tcx> PredicateSearcher<'tcx> { // Resolve predicates required to mention the item. let nested_impl_exprs = - self.resolve_item_predicates(alias_ty.def_id, alias_ty.args, warn)?; + self.resolve_item_required_predicates(alias_ty.def_id, alias_ty.args, warn)?; // Add all the bounds on the corresponding associated item. self.extend(item_bounds.map(|(index, pred)| { @@ -367,7 +377,8 @@ impl<'tcx> PredicateSearcher<'tcx> { .. })) => { // Resolve the predicates required by the impl. - let impl_exprs = self.resolve_item_predicates(impl_def_id, generics, warn)?; + let impl_exprs = + self.resolve_item_required_predicates(impl_def_id, generics, warn)?; ImplExprAtom::Concrete { def_id: impl_def_id, generics, @@ -401,7 +412,43 @@ impl<'tcx> PredicateSearcher<'tcx> { } } Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn, - Ok(ImplSource::Builtin(_, _)) => ImplExprAtom::Builtin { r#trait: *tref }, + Ok(ImplSource::Builtin(_, _)) => { + // Resolve the predicates implied by the trait. + let trait_def_id = erased_tref.skip_binder().def_id; + // If we wanted to not skip this binder, we'd have to instantiate the bound + // regions, solve, then wrap the result in a binder. And track higher-kinded + // clauses better all over. + let impl_exprs = self.resolve_item_implied_predicates( + trait_def_id, + erased_tref.skip_binder().args, + warn, + )?; + let types = tcx + .associated_items(trait_def_id) + .in_definition_order() + .filter(|assoc| matches!(assoc.kind, AssocKind::Type)) + .filter_map(|assoc| { + let ty = AliasTy::new(tcx, assoc.def_id, erased_tref.skip_binder().args) + .to_ty(tcx); + let ty = erase_and_norm(tcx, self.param_env, ty); + if let TyKind::Alias(_, alias_ty) = ty.kind() { + if alias_ty.def_id == assoc.def_id { + warn(&format!("Failed to compute associated type {ty}")); + // We can't return the unnormalized associated type as that would + // make the trait ref contain itself, which would make hax's + // `sinto` infrastructure loop. + return None; + } + } + Some((assoc.def_id, ty)) + }) + .collect(); + ImplExprAtom::Builtin { + r#trait: *tref, + impl_exprs, + types, + } + } Err(e) => { let msg = format!( "Could not find a clause for `{tref:?}` in the current context: `{e:?}`" @@ -418,7 +465,19 @@ impl<'tcx> PredicateSearcher<'tcx> { } /// Resolve the predicates required by the given item. - pub fn resolve_item_predicates( + pub fn resolve_item_required_predicates( + &mut self, + def_id: DefId, + generics: GenericArgsRef<'tcx>, + // Call back into hax-related code to display a nice warning. + warn: &impl Fn(&str), + ) -> Result>, String> { + let tcx = self.tcx; + self.resolve_predicates(generics, required_predicates(tcx, def_id), warn) + } + + /// Resolve the predicates implied by the given item. + pub fn resolve_item_implied_predicates( &mut self, def_id: DefId, generics: GenericArgsRef<'tcx>, @@ -426,7 +485,20 @@ impl<'tcx> PredicateSearcher<'tcx> { warn: &impl Fn(&str), ) -> Result>, String> { let tcx = self.tcx; - required_predicates(tcx, def_id) + self.resolve_predicates(generics, implied_predicates(tcx, def_id), warn) + } + + /// Apply the given generics to the provided clauses and resolve the trait references in the + /// current context. + pub fn resolve_predicates( + &mut self, + generics: GenericArgsRef<'tcx>, + predicates: GenericPredicates<'tcx>, + // Call back into hax-related code to display a nice warning. + warn: &impl Fn(&str), + ) -> Result>, String> { + let tcx = self.tcx; + predicates .predicates .iter() .map(|(clause, _span)| *clause) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 9e505d3a1..6ae14d007 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_16210070100893052778:t_Bar v_Self f_U; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_13496126865352171029:t_Bar v_Self f_U; f_U:Type0 } ''' @@ -408,7 +408,7 @@ class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { v_TypeArg v_ConstArg; f_AssocType:Type0; - f_AssocType_7414800425644916102:t_Trait f_AssocType v_TypeArg v_ConstArg + f_AssocType_13704321474071752218:t_Trait f_AssocType v_TypeArg v_ConstArg } ''' "Traits.Interlaced_consts_types.fst" = ''' @@ -485,7 +485,7 @@ open FStar.Mul class t_Trait1 (v_Self: Type0) = { f_T:Type0; - f_T_2328060197809802853:t_Trait1 f_T + f_T_2186006717281159153:t_Trait1 f_T } class t_Trait2 (v_Self: Type0) = { @@ -630,7 +630,7 @@ let use_impl_trait (_: Prims.unit) : Prims.unit = class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_12248650268031145847:t_SuperTrait f_AssocType; + f_AssocType_16668910951696008497:t_SuperTrait f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> Type0; f_assoc_f_post:Prims.unit -> Prims.unit -> Type0; @@ -667,7 +667,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_12248650268031145847 = FStar.Tactics.Typeclasses.solve; + f_AssocType_16668910951696008497 = 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);