diff options
| -rw-r--r-- | compiler/rustc_interface/src/passes.rs | 3 | ||||
| -rw-r--r-- | compiler/rustc_middle/src/arena.rs | 1 | ||||
| -rw-r--r-- | compiler/rustc_middle/src/query/erase.rs | 5 | ||||
| -rw-r--r-- | compiler/rustc_middle/src/query/mod.rs | 10 | ||||
| -rw-r--r-- | compiler/rustc_middle/src/ty/context.rs | 15 | ||||
| -rw-r--r-- | compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs | 47 | ||||
| -rw-r--r-- | compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs | 151 | ||||
| -rw-r--r-- | compiler/rustc_next_trait_solver/src/solve/inspect/build.rs | 399 | ||||
| -rw-r--r-- | compiler/rustc_next_trait_solver/src/solve/mod.rs | 11 | ||||
| -rw-r--r-- | compiler/rustc_next_trait_solver/src/solve/search_graph.rs | 14 | ||||
| -rw-r--r-- | compiler/rustc_trait_selection/src/solve.rs | 16 | ||||
| -rw-r--r-- | compiler/rustc_trait_selection/src/solve/inspect/analyse.rs | 18 | ||||
| -rw-r--r-- | compiler/rustc_type_ir/src/interner.rs | 11 | ||||
| -rw-r--r-- | compiler/rustc_type_ir/src/search_graph/mod.rs | 42 | ||||
| -rw-r--r-- | compiler/rustc_type_ir/src/solve/inspect.rs | 29 |
15 files changed, 331 insertions, 441 deletions
diff --git a/compiler/rustc_interface/src/passes.rs b/compiler/rustc_interface/src/passes.rs index bc5ef04079e..ca8c10311fb 100644 --- a/compiler/rustc_interface/src/passes.rs +++ b/compiler/rustc_interface/src/passes.rs @@ -41,7 +41,7 @@ use rustc_span::{ Symbol, sym, }; use rustc_target::spec::PanicStrategy; -use rustc_trait_selection::traits; +use rustc_trait_selection::{solve, traits}; use tracing::{info, instrument}; use crate::interface::Compiler; @@ -895,6 +895,7 @@ pub static DEFAULT_QUERY_PROVIDERS: LazyLock<Providers> = LazyLock::new(|| { rustc_hir_typeck::provide(providers); ty::provide(providers); traits::provide(providers); + solve::provide(providers); rustc_passes::provide(providers); rustc_traits::provide(providers); rustc_ty_utils::provide(providers); diff --git a/compiler/rustc_middle/src/arena.rs b/compiler/rustc_middle/src/arena.rs index 4b6e38cd52d..52fbe19c9f2 100644 --- a/compiler/rustc_middle/src/arena.rs +++ b/compiler/rustc_middle/src/arena.rs @@ -80,6 +80,7 @@ macro_rules! arena_types { rustc_middle::infer::canonical::Canonical<'tcx, rustc_middle::infer::canonical::QueryResponse<'tcx, rustc_middle::ty::Ty<'tcx>> >, + [] inspect_probe: rustc_middle::traits::solve::inspect::Probe<rustc_middle::ty::TyCtxt<'tcx>>, [] effective_visibilities: rustc_middle::middle::privacy::EffectiveVisibilities, [] upvars_mentioned: rustc_data_structures::fx::FxIndexMap<rustc_hir::HirId, rustc_hir::Upvar>, [] dyn_compatibility_violations: rustc_middle::traits::DynCompatibilityViolation, diff --git a/compiler/rustc_middle/src/query/erase.rs b/compiler/rustc_middle/src/query/erase.rs index ea62461ebeb..bea2191c560 100644 --- a/compiler/rustc_middle/src/query/erase.rs +++ b/compiler/rustc_middle/src/query/erase.rs @@ -6,6 +6,7 @@ use rustc_span::ErrorGuaranteed; use crate::mir::interpret::EvalToValTreeResult; use crate::query::CyclePlaceholder; +use crate::traits::solve; use crate::ty::adjustment::CoerceUnsizedInfo; use crate::ty::{self, Ty, TyCtxt}; use crate::{mir, traits}; @@ -219,6 +220,10 @@ impl<T0, T1> EraseType for (&'_ T0, &'_ T1) { type Result = [u8; size_of::<(&'static (), &'static ())>()]; } +impl<T0> EraseType for (solve::QueryResult<'_>, &'_ T0) { + type Result = [u8; size_of::<(solve::QueryResult<'static>, &'static ())>()]; +} + impl<T0, T1> EraseType for (&'_ T0, &'_ [T1]) { type Result = [u8; size_of::<(&'static (), &'static [()])>()]; } diff --git a/compiler/rustc_middle/src/query/mod.rs b/compiler/rustc_middle/src/query/mod.rs index 8ce70f75c67..874cee54c7c 100644 --- a/compiler/rustc_middle/src/query/mod.rs +++ b/compiler/rustc_middle/src/query/mod.rs @@ -131,7 +131,7 @@ use crate::traits::query::{ }; use crate::traits::{ CodegenObligationError, DynCompatibilityViolation, EvaluationResult, ImplSource, - ObligationCause, OverflowError, WellFormedLoc, specialization_graph, + ObligationCause, OverflowError, WellFormedLoc, solve, specialization_graph, }; use crate::ty::fast_reject::SimplifiedType; use crate::ty::layout::ValidityRequirement; @@ -2563,6 +2563,14 @@ rustc_queries! { desc { "computing autoderef types for `{}`", goal.canonical.value.value } } + /// Used by `-Znext-solver` to compute proof trees. + query evaluate_root_goal_for_proof_tree_raw( + goal: solve::CanonicalInput<'tcx>, + ) -> (solve::QueryResult<'tcx>, &'tcx solve::inspect::Probe<TyCtxt<'tcx>>) { + no_hash + desc { "computing proof tree for `{}`", goal.canonical.value.goal.predicate } + } + /// Returns the Rust target features for the current target. These are not always the same as LLVM target features! query rust_target_features(_: CrateNum) -> &'tcx UnordMap<String, rustc_target::target_features::Stability> { arena_cache diff --git a/compiler/rustc_middle/src/ty/context.rs b/compiler/rustc_middle/src/ty/context.rs index 5dbbc7297ab..72ab6ac612c 100644 --- a/compiler/rustc_middle/src/ty/context.rs +++ b/compiler/rustc_middle/src/ty/context.rs @@ -72,9 +72,9 @@ use crate::query::plumbing::QuerySystem; use crate::query::{IntoQueryParam, LocalCrate, Providers, TyCtxtAt}; use crate::thir::Thir; use crate::traits; -use crate::traits::solve; use crate::traits::solve::{ - ExternalConstraints, ExternalConstraintsData, PredefinedOpaques, PredefinedOpaquesData, + self, CanonicalInput, ExternalConstraints, ExternalConstraintsData, PredefinedOpaques, + PredefinedOpaquesData, QueryResult, inspect, }; use crate::ty::predicate::ExistentialPredicateStableCmpExt as _; use crate::ty::{ @@ -737,6 +737,17 @@ impl<'tcx> Interner for TyCtxt<'tcx> { self.opaque_types_defined_by(defining_anchor).iter().chain(coroutines_defined_by), ) } + + type ProbeRef = &'tcx inspect::Probe<TyCtxt<'tcx>>; + fn mk_probe_ref(self, probe: inspect::Probe<Self>) -> &'tcx inspect::Probe<TyCtxt<'tcx>> { + self.arena.alloc(probe) + } + fn evaluate_root_goal_for_proof_tree_raw( + self, + canonical_goal: CanonicalInput<'tcx>, + ) -> (QueryResult<'tcx>, &'tcx inspect::Probe<TyCtxt<'tcx>>) { + self.evaluate_root_goal_for_proof_tree_raw(canonical_goal) + } } macro_rules! bidirectional_lang_item_map { diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs index 4644b145b18..6f9f4067384 100644 --- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs +++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs @@ -56,22 +56,23 @@ where /// /// This expects `goal` and `opaque_types` to be eager resolved. pub(super) fn canonicalize_goal( - &self, + delegate: &D, goal: Goal<I, I::Predicate>, opaque_types: Vec<(ty::OpaqueTypeKey<I>, I::Ty)>, ) -> (Vec<I::GenericArg>, CanonicalInput<I, I::Predicate>) { let mut orig_values = Default::default(); let canonical = Canonicalizer::canonicalize_input( - self.delegate, + delegate, &mut orig_values, QueryInput { goal, - predefined_opaques_in_body: self + predefined_opaques_in_body: delegate .cx() .mk_predefined_opaques_in_body(PredefinedOpaquesData { opaque_types }), }, ); - let query_input = ty::CanonicalQueryInput { canonical, typing_mode: self.typing_mode() }; + let query_input = + ty::CanonicalQueryInput { canonical, typing_mode: delegate.typing_mode() }; (orig_values, query_input) } @@ -271,28 +272,23 @@ where /// - we apply the `external_constraints` returned by the query, returning /// the `normalization_nested_goals` pub(super) fn instantiate_and_apply_query_response( - &mut self, + delegate: &D, param_env: I::ParamEnv, original_values: &[I::GenericArg], response: CanonicalResponse<I>, + span: I::Span, ) -> (NestedNormalizationGoals<I>, Certainty) { let instantiation = Self::compute_query_response_instantiation_values( - self.delegate, + delegate, &original_values, &response, - self.origin_span, + span, ); let Response { var_values, external_constraints, certainty } = - self.delegate.instantiate_canonical(response, instantiation); + delegate.instantiate_canonical(response, instantiation); - Self::unify_query_var_values( - self.delegate, - param_env, - &original_values, - var_values, - self.origin_span, - ); + Self::unify_query_var_values(delegate, param_env, &original_values, var_values, span); let ExternalConstraintsData { region_constraints, @@ -300,8 +296,8 @@ where normalization_nested_goals, } = &*external_constraints; - self.register_region_constraints(region_constraints); - self.register_new_opaque_types(opaque_types); + Self::register_region_constraints(delegate, region_constraints, span); + Self::register_new_opaque_types(delegate, opaque_types, span); (normalization_nested_goals.clone(), certainty) } @@ -424,21 +420,26 @@ where } fn register_region_constraints( - &mut self, + delegate: &D, outlives: &[ty::OutlivesPredicate<I, I::GenericArg>], + span: I::Span, ) { for &ty::OutlivesPredicate(lhs, rhs) in outlives { match lhs.kind() { - ty::GenericArgKind::Lifetime(lhs) => self.register_region_outlives(lhs, rhs), - ty::GenericArgKind::Type(lhs) => self.register_ty_outlives(lhs, rhs), + ty::GenericArgKind::Lifetime(lhs) => delegate.sub_regions(rhs, lhs, span), + ty::GenericArgKind::Type(lhs) => delegate.register_ty_outlives(lhs, rhs, span), ty::GenericArgKind::Const(_) => panic!("const outlives: {lhs:?}: {rhs:?}"), } } } - fn register_new_opaque_types(&mut self, opaque_types: &[(ty::OpaqueTypeKey<I>, I::Ty)]) { + fn register_new_opaque_types( + delegate: &D, + opaque_types: &[(ty::OpaqueTypeKey<I>, I::Ty)], + span: I::Span, + ) { for &(key, ty) in opaque_types { - let prev = self.delegate.register_hidden_type_in_storage(key, ty, self.origin_span); + let prev = delegate.register_hidden_type_in_storage(key, ty, span); // We eagerly resolve inference variables when computing the query response. // This can cause previously distinct opaque type keys to now be structurally equal. // @@ -447,7 +448,7 @@ where // types here. However, doing so is difficult as it may result in nested goals and // any errors may make it harder to track the control flow for diagnostics. if let Some(prev) = prev { - self.delegate.add_duplicate_opaque_type(key, prev, self.origin_span); + delegate.add_duplicate_opaque_type(key, prev, span); } } } diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs index 4f87902e46e..31106a74527 100644 --- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs +++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs @@ -20,13 +20,12 @@ use crate::coherence; use crate::delegate::SolverDelegate; use crate::placeholder::BoundVarReplacer; use crate::resolve::eager_resolve_vars; -use crate::solve::inspect::{self, ProofTreeBuilder}; use crate::solve::search_graph::SearchGraph; use crate::solve::ty::may_use_unstable_feature; use crate::solve::{ - CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluation, GoalEvaluationKind, - GoalSource, GoalStalledOn, HasChanged, NestedNormalizationGoals, NoSolution, QueryInput, - QueryResult, + CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluation, GoalSource, + GoalStalledOn, HasChanged, NestedNormalizationGoals, NoSolution, QueryInput, QueryResult, + inspect, }; pub(super) mod canonical; @@ -130,7 +129,7 @@ where // evaluation code. tainted: Result<(), NoSolution>, - pub(super) inspect: ProofTreeBuilder<D>, + pub(super) inspect: inspect::EvaluationStepBuilder<D>, } #[derive(PartialEq, Eq, Debug, Hash, Clone, Copy)] @@ -172,10 +171,7 @@ pub trait SolverDelegateEvalExt: SolverDelegate { goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, span: <Self::Interner as Interner>::Span, ) -> ( - Result< - (NestedNormalizationGoals<Self::Interner>, GoalEvaluation<Self::Interner>), - NoSolution, - >, + Result<NestedNormalizationGoals<Self::Interner>, NoSolution>, inspect::GoalEvaluation<Self::Interner>, ); } @@ -192,14 +188,9 @@ where span: I::Span, stalled_on: Option<GoalStalledOn<I>>, ) -> Result<GoalEvaluation<I>, NoSolution> { - EvalCtxt::enter_root( - self, - self.cx().recursion_limit(), - GenerateProofTree::No, - span, - |ecx| ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal, stalled_on), - ) - .0 + EvalCtxt::enter_root(self, self.cx().recursion_limit(), span, |ecx| { + ecx.evaluate_goal(GoalSource::Misc, goal, stalled_on) + }) } fn root_goal_may_hold_with_depth( @@ -208,10 +199,9 @@ where goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, ) -> bool { self.probe(|| { - EvalCtxt::enter_root(self, root_depth, GenerateProofTree::No, I::Span::dummy(), |ecx| { - ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal, None) + EvalCtxt::enter_root(self, root_depth, I::Span::dummy(), |ecx| { + ecx.evaluate_goal(GoalSource::Misc, goal, None) }) - .0 }) .is_ok() } @@ -221,18 +211,8 @@ where &self, goal: Goal<I, I::Predicate>, span: I::Span, - ) -> ( - Result<(NestedNormalizationGoals<I>, GoalEvaluation<I>), NoSolution>, - inspect::GoalEvaluation<I>, - ) { - let (result, proof_tree) = EvalCtxt::enter_root( - self, - self.cx().recursion_limit(), - GenerateProofTree::Yes, - span, - |ecx| ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Misc, goal, None), - ); - (result, proof_tree.unwrap()) + ) -> (Result<NestedNormalizationGoals<I>, NoSolution>, inspect::GoalEvaluation<I>) { + evaluate_root_goal_for_proof_tree(self, goal, span) } } @@ -301,17 +281,16 @@ where pub(super) fn enter_root<R>( delegate: &D, root_depth: usize, - generate_proof_tree: GenerateProofTree, origin_span: I::Span, f: impl FnOnce(&mut EvalCtxt<'_, D>) -> R, - ) -> (R, Option<inspect::GoalEvaluation<I>>) { + ) -> R { let mut search_graph = SearchGraph::new(root_depth); let mut ecx = EvalCtxt { delegate, search_graph: &mut search_graph, nested_goals: Default::default(), - inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree), + inspect: inspect::EvaluationStepBuilder::new_noop(), // Only relevant when canonicalizing the response, // which we don't do within this evaluation context. @@ -324,15 +303,12 @@ where tainted: Ok(()), }; let result = f(&mut ecx); - - let proof_tree = ecx.inspect.finalize(); assert!( ecx.nested_goals.is_empty(), "root `EvalCtxt` should not have any goals added to it" ); - assert!(search_graph.is_empty()); - (result, proof_tree) + result } /// Creates a nested evaluation context that shares the same search graph as the @@ -346,11 +322,10 @@ where cx: I, search_graph: &'a mut SearchGraph<D>, canonical_input: CanonicalInput<I>, - canonical_goal_evaluation: &mut ProofTreeBuilder<D>, + proof_tree_builder: &mut inspect::ProofTreeBuilder<D>, f: impl FnOnce(&mut EvalCtxt<'_, D>, Goal<I, I::Predicate>) -> R, ) -> R { let (ref delegate, input, var_values) = D::build_with_canonical(cx, &canonical_input); - for &(key, ty) in &input.predefined_opaques_in_body.opaque_types { let prev = delegate.register_hidden_type_in_storage(key, ty, I::Span::dummy()); // It may be possible that two entries in the opaque type storage end up @@ -381,12 +356,12 @@ where nested_goals: Default::default(), origin_span: I::Span::dummy(), tainted: Ok(()), - inspect: canonical_goal_evaluation.new_goal_evaluation_step(var_values), + inspect: proof_tree_builder.new_evaluation_step(var_values), }; let result = f(&mut ecx, input.goal); ecx.inspect.probe_final_state(ecx.delegate, ecx.max_input_universe); - canonical_goal_evaluation.goal_evaluation_step(ecx.inspect); + proof_tree_builder.finish_evaluation_step(ecx.inspect); // When creating a query response we clone the opaque type constraints // instead of taking them. This would cause an ICE here, since we have @@ -406,13 +381,12 @@ where /// been constrained and the certainty of the result. fn evaluate_goal( &mut self, - goal_evaluation_kind: GoalEvaluationKind, source: GoalSource, goal: Goal<I, I::Predicate>, stalled_on: Option<GoalStalledOn<I>>, ) -> Result<GoalEvaluation<I>, NoSolution> { let (normalization_nested_goals, goal_evaluation) = - self.evaluate_goal_raw(goal_evaluation_kind, source, goal, stalled_on)?; + self.evaluate_goal_raw(source, goal, stalled_on)?; assert!(normalization_nested_goals.is_empty()); Ok(goal_evaluation) } @@ -426,7 +400,6 @@ where /// storage. pub(super) fn evaluate_goal_raw( &mut self, - goal_evaluation_kind: GoalEvaluationKind, source: GoalSource, goal: Goal<I, I::Predicate>, stalled_on: Option<GoalStalledOn<I>>, @@ -458,17 +431,14 @@ where let opaque_types = self.delegate.clone_opaque_types_lookup_table(); let (goal, opaque_types) = eager_resolve_vars(self.delegate, (goal, opaque_types)); - let (orig_values, canonical_goal) = self.canonicalize_goal(goal, opaque_types); - let mut goal_evaluation = - self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind); + let (orig_values, canonical_goal) = + Self::canonicalize_goal(self.delegate, goal, opaque_types); let canonical_result = self.search_graph.evaluate_goal( self.cx(), canonical_goal, self.step_kind_for_source(source), - &mut goal_evaluation, + &mut inspect::ProofTreeBuilder::new_noop(), ); - goal_evaluation.query_result(canonical_result); - self.inspect.goal_evaluation(goal_evaluation); let response = match canonical_result { Err(e) => return Err(e), Ok(response) => response, @@ -477,8 +447,13 @@ where let has_changed = if !has_only_region_constraints(response) { HasChanged::Yes } else { HasChanged::No }; - let (normalization_nested_goals, certainty) = - self.instantiate_and_apply_query_response(goal.param_env, &orig_values, response); + let (normalization_nested_goals, certainty) = Self::instantiate_and_apply_query_response( + self.delegate, + goal.param_env, + &orig_values, + response, + self.origin_span, + ); // FIXME: We previously had an assert here that checked that recomputing // a goal after applying its constraints did not change its response. @@ -676,12 +651,7 @@ where let ( NestedNormalizationGoals(nested_goals), GoalEvaluation { goal, certainty, stalled_on, has_changed: _ }, - ) = self.evaluate_goal_raw( - GoalEvaluationKind::Nested, - source, - unconstrained_goal, - stalled_on, - )?; + ) = self.evaluate_goal_raw(source, unconstrained_goal, stalled_on)?; // Add the nested goals from normalization to our own nested goals. trace!(?nested_goals); self.nested_goals.extend(nested_goals.into_iter().map(|(s, g)| (s, g, None))); @@ -734,7 +704,7 @@ where } } else { let GoalEvaluation { goal, certainty, has_changed, stalled_on } = - self.evaluate_goal(GoalEvaluationKind::Nested, source, goal, stalled_on)?; + self.evaluate_goal(source, goal, stalled_on)?; if has_changed == HasChanged::Yes { unchanged_certainty = None; } @@ -1297,3 +1267,62 @@ where if predicate.allow_normalization() { predicate.super_fold_with(self) } else { predicate } } } + +/// Do not call this directly, use the `tcx` query instead. +pub fn evaluate_root_goal_for_proof_tree_raw_provider< + D: SolverDelegate<Interner = I>, + I: Interner, +>( + cx: I, + canonical_goal: CanonicalInput<I>, +) -> (QueryResult<I>, I::ProbeRef) { + let mut inspect = inspect::ProofTreeBuilder::new(); + let canonical_result = SearchGraph::<D>::evaluate_root_goal_for_proof_tree( + cx, + cx.recursion_limit(), + canonical_goal, + &mut inspect, + ); + let final_revision = inspect.unwrap(); + (canonical_result, cx.mk_probe_ref(final_revision)) +} + +/// Evaluate a goal to build a proof tree. +/// +/// This is a copy of [EvalCtxt::evaluate_goal_raw] which avoids relying on the +/// [EvalCtxt] and uses a separate cache. +pub(super) fn evaluate_root_goal_for_proof_tree<D: SolverDelegate<Interner = I>, I: Interner>( + delegate: &D, + goal: Goal<I, I::Predicate>, + origin_span: I::Span, +) -> (Result<NestedNormalizationGoals<I>, NoSolution>, inspect::GoalEvaluation<I>) { + let opaque_types = delegate.clone_opaque_types_lookup_table(); + let (goal, opaque_types) = eager_resolve_vars(delegate, (goal, opaque_types)); + + let (orig_values, canonical_goal) = EvalCtxt::canonicalize_goal(delegate, goal, opaque_types); + + let (canonical_result, final_revision) = + delegate.cx().evaluate_root_goal_for_proof_tree_raw(canonical_goal); + + let proof_tree = inspect::GoalEvaluation { + uncanonicalized_goal: goal, + orig_values, + final_revision, + result: canonical_result, + }; + + let response = match canonical_result { + Err(e) => return (Err(e), proof_tree), + Ok(response) => response, + }; + + let (normalization_nested_goals, _certainty) = EvalCtxt::instantiate_and_apply_query_response( + delegate, + goal.param_env, + &proof_tree.orig_values, + response, + origin_span, + ); + + (Ok(normalization_nested_goals), proof_tree) +} diff --git a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs index fc56b006d94..2675ed0d0da 100644 --- a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs +++ b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs @@ -12,96 +12,86 @@ use rustc_type_ir::{self as ty, Interner}; use crate::delegate::SolverDelegate; use crate::solve::eval_ctxt::canonical; -use crate::solve::{ - Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource, QueryResult, inspect, -}; +use crate::solve::{Certainty, Goal, GoalSource, QueryResult, inspect}; -/// The core data structure when building proof trees. +/// We need to know whether to build a prove tree while evaluating. We +/// pass a `ProofTreeBuilder` with `state: Some(None)` into the search +/// graph which then causes the initial `EvalCtxt::compute_goal` to actually +/// build a proof tree which then gets written into the `state`. /// -/// In case the current evaluation does not generate a proof -/// tree, `state` is simply `None` and we avoid any work. -/// -/// The possible states of the solver are represented via -/// variants of [DebugSolver]. For any nested computation we call -/// `ProofTreeBuilder::new_nested_computation_kind` which -/// creates a new `ProofTreeBuilder` to temporarily replace the -/// current one. Once that nested computation is done, -/// `ProofTreeBuilder::nested_computation_kind` is called -/// to add the finished nested evaluation to the parent. -/// -/// We provide additional information to the current state -/// by calling methods such as `ProofTreeBuilder::probe_kind`. -/// -/// The actual structure closely mirrors the finished proof -/// trees. At the end of trait solving `ProofTreeBuilder::finalize` -/// is called to recursively convert the whole structure to a -/// finished proof tree. +/// Building the proof tree for a single evaluation step happens via the +/// [EvaluationStepBuilder] which is updated by the `EvalCtxt` when +/// appropriate. pub(crate) struct ProofTreeBuilder<D, I = <D as SolverDelegate>::Interner> where D: SolverDelegate<Interner = I>, I: Interner, { + state: Option<Box<Option<inspect::Probe<I>>>>, _infcx: PhantomData<D>, - state: Option<Box<DebugSolver<I>>>, } -/// The current state of the proof tree builder, at most places -/// in the code, only one or two variants are actually possible. -/// -/// We simply ICE in case that assumption is broken. -#[derive_where(Debug; I: Interner)] -enum DebugSolver<I: Interner> { - Root, - GoalEvaluation(WipGoalEvaluation<I>), - CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>), -} +impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> { + pub(crate) fn new() -> ProofTreeBuilder<D> { + ProofTreeBuilder { state: Some(Box::new(None)), _infcx: PhantomData } + } -impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> { - fn from(g: WipGoalEvaluation<I>) -> DebugSolver<I> { - DebugSolver::GoalEvaluation(g) + pub(crate) fn new_noop() -> ProofTreeBuilder<D> { + ProofTreeBuilder { state: None, _infcx: PhantomData } } -} -impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> { - fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> { - DebugSolver::CanonicalGoalEvaluationStep(g) + pub(crate) fn is_noop(&self) -> bool { + self.state.is_none() } -} -#[derive_where(PartialEq, Debug; I: Interner)] -struct WipGoalEvaluation<I: Interner> { - pub uncanonicalized_goal: Goal<I, I::Predicate>, - pub orig_values: Vec<I::GenericArg>, - pub encountered_overflow: bool, - /// After we finished evaluating this is moved into `kind`. - pub final_revision: Option<WipCanonicalGoalEvaluationStep<I>>, - pub result: Option<QueryResult<I>>, -} + pub(crate) fn new_evaluation_step( + &mut self, + var_values: ty::CanonicalVarValues<I>, + ) -> EvaluationStepBuilder<D> { + if self.is_noop() { + EvaluationStepBuilder { state: None, _infcx: PhantomData } + } else { + EvaluationStepBuilder { + state: Some(Box::new(WipEvaluationStep { + var_values: var_values.var_values.to_vec(), + evaluation: WipProbe { + initial_num_var_values: var_values.len(), + steps: vec![], + kind: None, + final_state: None, + }, + probe_depth: 0, + })), + _infcx: PhantomData, + } + } + } -impl<I: Interner> Eq for WipGoalEvaluation<I> {} - -impl<I: Interner> WipGoalEvaluation<I> { - fn finalize(self) -> inspect::GoalEvaluation<I> { - inspect::GoalEvaluation { - uncanonicalized_goal: self.uncanonicalized_goal, - orig_values: self.orig_values, - kind: if self.encountered_overflow { - assert!(self.final_revision.is_none()); - inspect::GoalEvaluationKind::Overflow - } else { - let final_revision = self.final_revision.unwrap().finalize(); - inspect::GoalEvaluationKind::Evaluation { final_revision } - }, - result: self.result.unwrap(), + pub(crate) fn finish_evaluation_step( + &mut self, + goal_evaluation_step: EvaluationStepBuilder<D>, + ) { + if let Some(this) = self.state.as_deref_mut() { + *this = Some(goal_evaluation_step.state.unwrap().finalize()); } } + + pub(crate) fn unwrap(self) -> inspect::Probe<I> { + self.state.unwrap().unwrap() + } } -/// This only exists during proof tree building and does not have -/// a corresponding struct in `inspect`. We need this to track a -/// bunch of metadata about the current evaluation. -#[derive_where(PartialEq, Debug; I: Interner)] -struct WipCanonicalGoalEvaluationStep<I: Interner> { +pub(crate) struct EvaluationStepBuilder<D, I = <D as SolverDelegate>::Interner> +where + D: SolverDelegate<Interner = I>, + I: Interner, +{ + state: Option<Box<WipEvaluationStep<I>>>, + _infcx: PhantomData<D>, +} + +#[derive_where(PartialEq, Eq, Debug; I: Interner)] +struct WipEvaluationStep<I: Interner> { /// Unlike `EvalCtxt::var_values`, we append a new /// generic arg here whenever we create a new inference /// variable. @@ -113,9 +103,7 @@ struct WipCanonicalGoalEvaluationStep<I: Interner> { evaluation: WipProbe<I>, } -impl<I: Interner> Eq for WipCanonicalGoalEvaluationStep<I> {} - -impl<I: Interner> WipCanonicalGoalEvaluationStep<I> { +impl<I: Interner> WipEvaluationStep<I> { fn current_evaluation_scope(&mut self) -> &mut WipProbe<I> { let mut current = &mut self.evaluation; for _ in 0..self.probe_depth { @@ -181,169 +169,48 @@ impl<I: Interner> WipProbeStep<I> { } } -impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> { - fn new(state: impl Into<DebugSolver<I>>) -> ProofTreeBuilder<D> { - ProofTreeBuilder { state: Some(Box::new(state.into())), _infcx: PhantomData } - } - - fn opt_nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> Option<T>) -> Self { - ProofTreeBuilder { - state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new), - _infcx: PhantomData, - } +impl<D: SolverDelegate<Interner = I>, I: Interner> EvaluationStepBuilder<D> { + pub(crate) fn new_noop() -> EvaluationStepBuilder<D> { + EvaluationStepBuilder { state: None, _infcx: PhantomData } } - fn nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> T) -> Self { - ProofTreeBuilder { - state: self.state.as_ref().map(|_| Box::new(state().into())), - _infcx: PhantomData, - } + pub(crate) fn is_noop(&self) -> bool { + self.state.is_none() } - fn as_mut(&mut self) -> Option<&mut DebugSolver<I>> { + fn as_mut(&mut self) -> Option<&mut WipEvaluationStep<I>> { self.state.as_deref_mut() } - pub(crate) fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<D> { - let mut nested = ProofTreeBuilder { state: self.state.take(), _infcx: PhantomData }; + pub(crate) fn take_and_enter_probe(&mut self) -> EvaluationStepBuilder<D> { + let mut nested = EvaluationStepBuilder { state: self.state.take(), _infcx: PhantomData }; nested.enter_probe(); nested } - pub(crate) fn finalize(self) -> Option<inspect::GoalEvaluation<I>> { - match *self.state? { - DebugSolver::GoalEvaluation(wip_goal_evaluation) => { - Some(wip_goal_evaluation.finalize()) - } - root => unreachable!("unexpected proof tree builder root node: {:?}", root), - } - } - - pub(crate) fn new_maybe_root(generate_proof_tree: GenerateProofTree) -> ProofTreeBuilder<D> { - match generate_proof_tree { - GenerateProofTree::No => ProofTreeBuilder::new_noop(), - GenerateProofTree::Yes => ProofTreeBuilder::new_root(), - } - } - - fn new_root() -> ProofTreeBuilder<D> { - ProofTreeBuilder::new(DebugSolver::Root) - } - - fn new_noop() -> ProofTreeBuilder<D> { - ProofTreeBuilder { state: None, _infcx: PhantomData } - } - - pub(crate) fn is_noop(&self) -> bool { - self.state.is_none() - } - - pub(in crate::solve) fn new_goal_evaluation( - &mut self, - uncanonicalized_goal: Goal<I, I::Predicate>, - orig_values: &[I::GenericArg], - kind: GoalEvaluationKind, - ) -> ProofTreeBuilder<D> { - self.opt_nested(|| match kind { - GoalEvaluationKind::Root => Some(WipGoalEvaluation { - uncanonicalized_goal, - orig_values: orig_values.to_vec(), - encountered_overflow: false, - final_revision: None, - result: None, - }), - GoalEvaluationKind::Nested => None, - }) - } - - pub(crate) fn canonical_goal_evaluation_overflow(&mut self) { + pub(crate) fn add_var_value<T: Into<I::GenericArg>>(&mut self, arg: T) { if let Some(this) = self.as_mut() { - match this { - DebugSolver::GoalEvaluation(goal_evaluation) => { - goal_evaluation.encountered_overflow = true; - } - _ => unreachable!(), - }; + this.var_values.push(arg.into()); } } - pub(crate) fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<D>) { + fn enter_probe(&mut self) { if let Some(this) = self.as_mut() { - match this { - DebugSolver::Root => *this = *goal_evaluation.state.unwrap(), - DebugSolver::CanonicalGoalEvaluationStep(_) => { - assert!(goal_evaluation.state.is_none()) - } - _ => unreachable!(), - } - } - } - - pub(crate) fn new_goal_evaluation_step( - &mut self, - var_values: ty::CanonicalVarValues<I>, - ) -> ProofTreeBuilder<D> { - self.nested(|| WipCanonicalGoalEvaluationStep { - var_values: var_values.var_values.to_vec(), - evaluation: WipProbe { - initial_num_var_values: var_values.len(), + let initial_num_var_values = this.var_values.len(); + this.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe { + initial_num_var_values, steps: vec![], kind: None, final_state: None, - }, - probe_depth: 0, - }) - } - - pub(crate) fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<D>) { - if let Some(this) = self.as_mut() { - match (this, *goal_evaluation_step.state.unwrap()) { - ( - DebugSolver::GoalEvaluation(goal_evaluation), - DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step), - ) => { - goal_evaluation.final_revision = Some(goal_evaluation_step); - } - _ => unreachable!(), - } - } - } - - pub(crate) fn add_var_value<T: Into<I::GenericArg>>(&mut self, arg: T) { - match self.as_mut() { - None => {} - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - state.var_values.push(arg.into()); - } - Some(s) => panic!("tried to add var values to {s:?}"), - } - } - - fn enter_probe(&mut self) { - match self.as_mut() { - None => {} - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - let initial_num_var_values = state.var_values.len(); - state.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe { - initial_num_var_values, - steps: vec![], - kind: None, - final_state: None, - })); - state.probe_depth += 1; - } - Some(s) => panic!("tried to start probe to {s:?}"), + })); + this.probe_depth += 1; } } pub(crate) fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<I>) { - match self.as_mut() { - None => {} - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - let prev = state.current_evaluation_scope().kind.replace(probe_kind); - assert_eq!(prev, None); - } - _ => panic!(), + if let Some(this) = self.as_mut() { + let prev = this.current_evaluation_scope().kind.replace(probe_kind); + assert_eq!(prev, None); } } @@ -352,19 +219,11 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> { delegate: &D, max_input_universe: ty::UniverseIndex, ) { - match self.as_mut() { - None => {} - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - let final_state = canonical::make_canonical_state( - delegate, - &state.var_values, - max_input_universe, - (), - ); - let prev = state.current_evaluation_scope().final_state.replace(final_state); - assert_eq!(prev, None); - } - _ => panic!(), + if let Some(this) = self.as_mut() { + let final_state = + canonical::make_canonical_state(delegate, &this.var_values, max_input_universe, ()); + let prev = this.current_evaluation_scope().final_state.replace(final_state); + assert_eq!(prev, None); } } @@ -375,18 +234,14 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> { source: GoalSource, goal: Goal<I, I::Predicate>, ) { - match self.as_mut() { - None => {} - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - let goal = canonical::make_canonical_state( - delegate, - &state.var_values, - max_input_universe, - goal, - ); - state.current_evaluation_scope().steps.push(WipProbeStep::AddGoal(source, goal)) - } - _ => panic!(), + if let Some(this) = self.as_mut() { + let goal = canonical::make_canonical_state( + delegate, + &this.var_values, + max_input_universe, + goal, + ); + this.current_evaluation_scope().steps.push(WipProbeStep::AddGoal(source, goal)) } } @@ -396,47 +251,31 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> { max_input_universe: ty::UniverseIndex, impl_args: I::GenericArgs, ) { - match self.as_mut() { - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - let impl_args = canonical::make_canonical_state( - delegate, - &state.var_values, - max_input_universe, - impl_args, - ); - state - .current_evaluation_scope() - .steps - .push(WipProbeStep::RecordImplArgs { impl_args }); - } - None => {} - _ => panic!(), + if let Some(this) = self.as_mut() { + let impl_args = canonical::make_canonical_state( + delegate, + &this.var_values, + max_input_universe, + impl_args, + ); + this.current_evaluation_scope().steps.push(WipProbeStep::RecordImplArgs { impl_args }); } } pub(crate) fn make_canonical_response(&mut self, shallow_certainty: Certainty) { - match self.as_mut() { - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - state - .current_evaluation_scope() - .steps - .push(WipProbeStep::MakeCanonicalResponse { shallow_certainty }); - } - None => {} - _ => panic!(), + if let Some(this) = self.as_mut() { + this.current_evaluation_scope() + .steps + .push(WipProbeStep::MakeCanonicalResponse { shallow_certainty }); } } - pub(crate) fn finish_probe(mut self) -> ProofTreeBuilder<D> { - match self.as_mut() { - None => {} - Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => { - assert_ne!(state.probe_depth, 0); - let num_var_values = state.current_evaluation_scope().initial_num_var_values; - state.var_values.truncate(num_var_values); - state.probe_depth -= 1; - } - _ => panic!(), + pub(crate) fn finish_probe(mut self) -> EvaluationStepBuilder<D> { + if let Some(this) = self.as_mut() { + assert_ne!(this.probe_depth, 0); + let num_var_values = this.current_evaluation_scope().initial_num_var_values; + this.var_values.truncate(num_var_values); + this.probe_depth -= 1; } self @@ -444,21 +283,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> { pub(crate) fn query_result(&mut self, result: QueryResult<I>) { if let Some(this) = self.as_mut() { - match this { - DebugSolver::GoalEvaluation(goal_evaluation) => { - assert_eq!(goal_evaluation.result.replace(result), None); - } - DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => { - assert_eq!( - evaluation_step - .evaluation - .kind - .replace(inspect::ProbeKind::Root { result }), - None - ); - } - _ => unreachable!(), - } + assert_eq!(this.evaluation.kind.replace(inspect::ProbeKind::Root { result }), None); } } } diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs index 710b59f662a..85f9d852d95 100644 --- a/compiler/rustc_next_trait_solver/src/solve/mod.rs +++ b/compiler/rustc_next_trait_solver/src/solve/mod.rs @@ -27,7 +27,10 @@ pub use rustc_type_ir::solve::*; use rustc_type_ir::{self as ty, Interner, TypingMode}; use tracing::instrument; -pub use self::eval_ctxt::{EvalCtxt, GenerateProofTree, SolverDelegateEvalExt}; +pub use self::eval_ctxt::{ + EvalCtxt, GenerateProofTree, SolverDelegateEvalExt, + evaluate_root_goal_for_proof_tree_raw_provider, +}; use crate::delegate::SolverDelegate; use crate::solve::assembly::Candidate; @@ -42,12 +45,6 @@ use crate::solve::assembly::Candidate; /// recursion limit again. However, this feels very unlikely. const FIXPOINT_STEP_LIMIT: usize = 8; -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -enum GoalEvaluationKind { - Root, - Nested, -} - /// Whether evaluating this goal ended up changing the /// inference state. #[derive(PartialEq, Eq, Debug, Hash, Clone, Copy)] diff --git a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs index 84f8eda4f8d..f0342e0523f 100644 --- a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs +++ b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs @@ -7,8 +7,9 @@ use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult}; use rustc_type_ir::{Interner, TypingMode}; use crate::delegate::SolverDelegate; -use crate::solve::inspect::ProofTreeBuilder; -use crate::solve::{EvalCtxt, FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints}; +use crate::solve::{ + EvalCtxt, FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints, inspect, +}; /// This type is never constructed. We only use it to implement `search_graph::Delegate` /// for all types which impl `SolverDelegate` and doing it directly fails in coherence. @@ -34,7 +35,7 @@ where const FIXPOINT_STEP_LIMIT: usize = FIXPOINT_STEP_LIMIT; - type ProofTreeBuilder = ProofTreeBuilder<D>; + type ProofTreeBuilder = inspect::ProofTreeBuilder<D>; fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool { inspect.is_noop() } @@ -81,12 +82,7 @@ where Self::initial_provisional_result(cx, kind, input) == result } - fn on_stack_overflow( - cx: I, - input: CanonicalInput<I>, - inspect: &mut ProofTreeBuilder<D>, - ) -> QueryResult<I> { - inspect.canonical_goal_evaluation_overflow(); + fn on_stack_overflow(cx: I, input: CanonicalInput<I>) -> QueryResult<I> { response_no_constraints(cx, input, Certainty::overflow(true)) } diff --git a/compiler/rustc_trait_selection/src/solve.rs b/compiler/rustc_trait_selection/src/solve.rs index f58961683a9..5d200c4d340 100644 --- a/compiler/rustc_trait_selection/src/solve.rs +++ b/compiler/rustc_trait_selection/src/solve.rs @@ -13,4 +13,20 @@ pub use normalize::{ deeply_normalize, deeply_normalize_with_skipped_universes, deeply_normalize_with_skipped_universes_and_ambiguous_coroutine_goals, }; +use rustc_middle::query::Providers; +use rustc_middle::ty::TyCtxt; pub use select::InferCtxtSelectExt; + +fn evaluate_root_goal_for_proof_tree_raw<'tcx>( + tcx: TyCtxt<'tcx>, + canonical_input: CanonicalInput<TyCtxt<'tcx>>, +) -> (QueryResult<TyCtxt<'tcx>>, &'tcx inspect::Probe<TyCtxt<'tcx>>) { + evaluate_root_goal_for_proof_tree_raw_provider::<SolverDelegate<'tcx>, TyCtxt<'tcx>>( + tcx, + canonical_input, + ) +} + +pub fn provide(providers: &mut Providers) { + *providers = Providers { evaluate_root_goal_for_proof_tree_raw, ..*providers }; +} diff --git a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs index 308486811e6..342d7121fc3 100644 --- a/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs +++ b/compiler/rustc_trait_selection/src/solve/inspect/analyse.rs @@ -37,7 +37,7 @@ pub struct InspectGoal<'a, 'tcx> { orig_values: Vec<ty::GenericArg<'tcx>>, goal: Goal<'tcx, ty::Predicate<'tcx>>, result: Result<Certainty, NoSolution>, - evaluation_kind: inspect::GoalEvaluationKind<TyCtxt<'tcx>>, + final_revision: &'tcx inspect::Probe<TyCtxt<'tcx>>, normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>, source: GoalSource, } @@ -249,7 +249,7 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> { // `InspectGoal::new` so that the goal has the right result (and maintains // the impression that we don't do this normalizes-to infer hack at all). let (nested, proof_tree) = infcx.evaluate_root_goal_for_proof_tree(goal, span); - let nested_goals_result = nested.and_then(|(nested, _)| { + let nested_goals_result = nested.and_then(|nested| { normalizes_to_term_hack.constrain_and( infcx, span, @@ -391,15 +391,8 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> { pub fn candidates(&'a self) -> Vec<InspectCandidate<'a, 'tcx>> { let mut candidates = vec![]; - let last_eval_step = match &self.evaluation_kind { - // An annoying edge case in case the recursion limit is 0. - inspect::GoalEvaluationKind::Overflow => return vec![], - inspect::GoalEvaluationKind::Evaluation { final_revision } => final_revision, - }; - let mut nested_goals = vec![]; - self.candidates_recur(&mut candidates, &mut nested_goals, &last_eval_step); - + self.candidates_recur(&mut candidates, &mut nested_goals, &self.final_revision); candidates } @@ -426,7 +419,8 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> { ) -> Self { let infcx = <&SolverDelegate<'tcx>>::from(infcx); - let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, kind, result } = root; + let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, final_revision, result } = + root; // If there's a normalizes-to goal, AND the evaluation result with the result of // constraining the normalizes-to RHS and computing the nested goals. let result = result.and_then(|ok| { @@ -441,7 +435,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> { orig_values, goal: eager_resolve_vars(infcx, uncanonicalized_goal), result, - evaluation_kind: kind, + final_revision, normalizes_to_term_hack: term_hack_and_nested_certainty.map(|(n, _)| n), source, } diff --git a/compiler/rustc_type_ir/src/interner.rs b/compiler/rustc_type_ir/src/interner.rs index 21fe7879b29..f5448baf8c0 100644 --- a/compiler/rustc_type_ir/src/interner.rs +++ b/compiler/rustc_type_ir/src/interner.rs @@ -10,7 +10,9 @@ use crate::inherent::*; use crate::ir_print::IrPrint; use crate::lang_items::{SolverLangItem, SolverTraitLangItem}; use crate::relate::Relate; -use crate::solve::{CanonicalInput, ExternalConstraintsData, PredefinedOpaquesData, QueryResult}; +use crate::solve::{ + CanonicalInput, ExternalConstraintsData, PredefinedOpaquesData, QueryResult, inspect, +}; use crate::visit::{Flags, TypeVisitable}; use crate::{self as ty, CanonicalParamEnvCacheEntry, search_graph}; @@ -380,6 +382,13 @@ pub trait Interner: self, defining_anchor: Self::LocalDefId, ) -> Self::LocalDefIds; + + type ProbeRef: Copy + Debug + Hash + Eq + Deref<Target = inspect::Probe<Self>>; + fn mk_probe_ref(self, probe: inspect::Probe<Self>) -> Self::ProbeRef; + fn evaluate_root_goal_for_proof_tree_raw( + self, + canonical_goal: CanonicalInput<Self>, + ) -> (QueryResult<Self>, Self::ProbeRef); } /// Imagine you have a function `F: FnOnce(&[T]) -> R`, plus an iterator `iter` diff --git a/compiler/rustc_type_ir/src/search_graph/mod.rs b/compiler/rustc_type_ir/src/search_graph/mod.rs index 348178a527f..dbbc0c217d7 100644 --- a/compiler/rustc_type_ir/src/search_graph/mod.rs +++ b/compiler/rustc_type_ir/src/search_graph/mod.rs @@ -92,11 +92,7 @@ pub trait Delegate: Sized { input: <Self::Cx as Cx>::Input, result: <Self::Cx as Cx>::Result, ) -> bool; - fn on_stack_overflow( - cx: Self::Cx, - input: <Self::Cx as Cx>::Input, - inspect: &mut Self::ProofTreeBuilder, - ) -> <Self::Cx as Cx>::Result; + fn on_stack_overflow(cx: Self::Cx, input: <Self::Cx as Cx>::Input) -> <Self::Cx as Cx>::Result; fn on_fixpoint_overflow( cx: Self::Cx, input: <Self::Cx as Cx>::Input, @@ -703,6 +699,31 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> { } } + pub fn evaluate_root_goal_for_proof_tree( + cx: X, + root_depth: usize, + input: X::Input, + inspect: &mut D::ProofTreeBuilder, + ) -> X::Result { + let mut this = SearchGraph::<D>::new(root_depth); + let available_depth = AvailableDepth(root_depth); + let step_kind_from_parent = PathKind::Inductive; // is never used + this.stack.push(StackEntry { + input, + step_kind_from_parent, + available_depth, + provisional_result: None, + required_depth: 0, + heads: Default::default(), + encountered_overflow: false, + usages: None, + candidate_usages: None, + nested_goals: Default::default(), + }); + let evaluation_result = this.evaluate_goal_in_task(cx, input, inspect); + evaluation_result.result + } + /// Probably the most involved method of the whole solver. /// /// While goals get computed via `D::compute_goal`, this function handles @@ -718,7 +739,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> { let Some(available_depth) = AvailableDepth::allowed_depth_for_nested::<D>(self.root_depth, &self.stack) else { - return self.handle_overflow(cx, input, inspect); + return self.handle_overflow(cx, input); }; // We check the provisional cache before checking the global cache. This simplifies @@ -833,12 +854,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> { result } - fn handle_overflow( - &mut self, - cx: X, - input: X::Input, - inspect: &mut D::ProofTreeBuilder, - ) -> X::Result { + fn handle_overflow(&mut self, cx: X, input: X::Input) -> X::Result { if let Some(last) = self.stack.last_mut() { last.encountered_overflow = true; // If computing a goal `B` depends on another goal `A` and @@ -853,7 +869,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> { } debug!("encountered stack overflow"); - D::on_stack_overflow(cx, input, inspect) + D::on_stack_overflow(cx, input) } /// When reevaluating a goal with a changed provisional result, all provisional cache entry diff --git a/compiler/rustc_type_ir/src/solve/inspect.rs b/compiler/rustc_type_ir/src/solve/inspect.rs index afb4043648f..5452ac44158 100644 --- a/compiler/rustc_type_ir/src/solve/inspect.rs +++ b/compiler/rustc_type_ir/src/solve/inspect.rs @@ -45,31 +45,18 @@ pub type CanonicalState<I, T> = Canonical<I, State<I, T>>; /// for the `CanonicalVarValues` of the canonicalized goal. /// We use this to map any [CanonicalState] from the local `InferCtxt` /// of the solver query to the `InferCtxt` of the caller. -#[derive_where(PartialEq, Hash; I: Interner)] +#[derive_where(PartialEq, Eq, Hash; I: Interner)] pub struct GoalEvaluation<I: Interner> { pub uncanonicalized_goal: Goal<I, I::Predicate>, pub orig_values: Vec<I::GenericArg>, - pub kind: GoalEvaluationKind<I>, + pub final_revision: I::ProbeRef, pub result: QueryResult<I>, } -impl<I: Interner> Eq for GoalEvaluation<I> {} - -#[derive_where(PartialEq, Hash, Debug; I: Interner)] -pub enum GoalEvaluationKind<I: Interner> { - Overflow, - Evaluation { - /// This is always `ProbeKind::Root`. - final_revision: Probe<I>, - }, -} - -impl<I: Interner> Eq for GoalEvaluationKind<I> {} - /// A self-contained computation during trait solving. This either /// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation /// of a goal. -#[derive_where(PartialEq, Hash, Debug; I: Interner)] +#[derive_where(PartialEq, Eq, Hash, Debug; I: Interner)] pub struct Probe<I: Interner> { /// What happened inside of this probe in chronological order. pub steps: Vec<ProbeStep<I>>, @@ -77,9 +64,7 @@ pub struct Probe<I: Interner> { pub final_state: CanonicalState<I, ()>, } -impl<I: Interner> Eq for Probe<I> {} - -#[derive_where(PartialEq, Hash, Debug; I: Interner)] +#[derive_where(PartialEq, Eq, Hash, Debug; I: Interner)] pub enum ProbeStep<I: Interner> { /// We added a goal to the `EvalCtxt` which will get proven /// the next time `EvalCtxt::try_evaluate_added_goals` is called. @@ -98,12 +83,10 @@ pub enum ProbeStep<I: Interner> { MakeCanonicalResponse { shallow_certainty: Certainty }, } -impl<I: Interner> Eq for ProbeStep<I> {} - /// What kind of probe we're in. In case the probe represents a candidate, or /// the final result of the current goal - via [ProbeKind::Root] - we also /// store the [QueryResult]. -#[derive_where(Clone, Copy, PartialEq, Hash, Debug; I: Interner)] +#[derive_where(Clone, Copy, PartialEq, Eq, Hash, Debug; I: Interner)] #[derive(TypeVisitable_Generic, TypeFoldable_Generic)] pub enum ProbeKind<I: Interner> { /// The root inference context while proving a goal. @@ -128,5 +111,3 @@ pub enum ProbeKind<I: Interner> { /// Checking that a rigid alias is well-formed. RigidAlias { result: QueryResult<I> }, } - -impl<I: Interner> Eq for ProbeKind<I> {} |