dnrops
/
rust
mirror of https://github.com/rust-lang/rust.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

remove proof tree formatter, make em shallow

This commit is contained in:
lcnr 2024-05-24 18:23:24 +00:00
parent 213ad10c8f
commit ebd9f355e2
16 changed files with 135 additions and 505 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
compiler/rustc_interface/src/tests.rs
View File

@ -799,10 +799,7 @@ fn test_unstable_options_tracking_hash() {
tracked!(mir_opt_level, Some(4));
tracked!(move_size_limit, Some(4096));
tracked!(mutable_noalias, false);
tracked!(
next_solver,
Some(NextSolverConfig { coherence: true, globally: false, dump_tree: Default::default() })
);
tracked!(next_solver, Some(NextSolverConfig { coherence: true, globally: false }));
tracked!(no_generate_arange_section, true);
tracked!(no_jump_tables, true);
tracked!(no_link, true);

5
compiler/rustc_middle/src/arena.rs
View File

@ -61,7 +61,10 @@ macro_rules! arena_types {
[] dtorck_constraint: rustc_middle::traits::query::DropckConstraint<'tcx>,
[] candidate_step: rustc_middle::traits::query::CandidateStep<'tcx>,
[] autoderef_bad_ty: rustc_middle::traits::query::MethodAutoderefBadTy<'tcx>,
[] canonical_goal_evaluation: rustc_next_trait_solver::solve::inspect::GoalEvaluationStep<rustc_middle::ty::TyCtxt<'tcx>>,
[] canonical_goal_evaluation:
rustc_next_trait_solver::solve::inspect::CanonicalGoalEvaluationStep<
rustc_middle::ty::TyCtxt<'tcx>
>,
[] query_region_constraints: rustc_middle::infer::canonical::QueryRegionConstraints<'tcx>,
[] type_op_subtype:
rustc_middle::infer::canonical::Canonical<'tcx,

6
compiler/rustc_middle/src/traits/solve/cache.rs
View File

@ -17,7 +17,7 @@ pub struct EvaluationCache<'tcx> {
#[derive(Debug, PartialEq, Eq)]
pub struct CacheData<'tcx> {
pub result: QueryResult<'tcx>,
pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
pub additional_depth: usize,
pub encountered_overflow: bool,
}
@ -28,7 +28,7 @@ impl<'tcx> EvaluationCache<'tcx> {
&self,
tcx: TyCtxt<'tcx>,
key: CanonicalInput<'tcx>,
proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
additional_depth: usize,
encountered_overflow: bool,
cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
@ -107,7 +107,7 @@ struct Success<'tcx> {
#[derive(Clone, Copy)]
pub struct QueryData<'tcx> {
pub result: QueryResult<'tcx>,
pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
}
/// The cache entry for a goal `CanonicalInput`.

3
compiler/rustc_middle/src/ty/context.rs
View File

@ -103,7 +103,8 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
type PredefinedOpaques = solve::PredefinedOpaques<'tcx>;
type DefiningOpaqueTypes = &'tcx ty::List<LocalDefId>;
type ExternalConstraints = ExternalConstraints<'tcx>;
type GoalEvaluationSteps = &'tcx [solve::inspect::GoalEvaluationStep<TyCtxt<'tcx>>];
type CanonicalGoalEvaluationStepRef =
&'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>;
type Ty = Ty<'tcx>;
type Tys = &'tcx List<Ty<'tcx>>;

10
compiler/rustc_session/src/config.rs
View File

@ -796,16 +796,6 @@ pub struct NextSolverConfig {
/// Whether the new trait solver should be enabled everywhere.
/// This is only `true` if `coherence` is also enabled.
pub globally: bool,
/// Whether to dump proof trees after computing a proof tree.
pub dump_tree: DumpSolverProofTree,
}
#[derive(Default, Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum DumpSolverProofTree {
Always,
OnError,
#[default]
Never,
}
#[derive(Clone)]

26
compiler/rustc_session/src/options.rs
View File

@ -399,7 +399,8 @@ mod desc {
pub const parse_instrument_xray: &str = "either a boolean (`yes`, `no`, `on`, `off`, etc), or a comma separated list of settings: `always` or `never` (mutually exclusive), `ignore-loops`, `instruction-threshold=N`, `skip-entry`, `skip-exit`";
pub const parse_unpretty: &str = "`string` or `string=string`";
pub const parse_treat_err_as_bug: &str = "either no value or a non-negative number";
pub const parse_next_solver_config: &str = "a comma separated list of solver configurations: `globally` (default), `coherence`, `dump-tree`, `dump-tree-on-error";
pub const parse_next_solver_config: &str =
"a comma separated list of solver configurations: `globally` (default), and `coherence`";
pub const parse_lto: &str =
"either a boolean (`yes`, `no`, `on`, `off`, etc), `thin`, `fat`, or omitted";
pub const parse_linker_plugin_lto: &str =
@ -1058,7 +1059,6 @@ mod parse {
if let Some(config) = v {
let mut coherence = false;
let mut globally = true;
let mut dump_tree = None;
for c in config.split(',') {
match c {
"globally" => globally = true,
@ -1066,31 +1066,13 @@ mod parse {
globally = false;
coherence = true;
}
"dump-tree" => {
if dump_tree.replace(DumpSolverProofTree::Always).is_some() {
return false;
}
}
"dump-tree-on-error" => {
if dump_tree.replace(DumpSolverProofTree::OnError).is_some() {
return false;
}
}
_ => return false,
}
}
*slot = Some(NextSolverConfig {
coherence: coherence || globally,
globally,
dump_tree: dump_tree.unwrap_or_default(),
});
*slot = Some(NextSolverConfig { coherence: coherence || globally, globally });
} else {
*slot = Some(NextSolverConfig {
coherence: true,
globally: true,
dump_tree: Default::default(),
});
*slot = Some(NextSolverConfig { coherence: true, globally: true });
}
true

27
compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
View File

@ -1,6 +1,3 @@
use std::io::Write;
use std::ops::ControlFlow;
use rustc_data_structures::stack::ensure_sufficient_stack;
use rustc_hir::def_id::DefId;
use rustc_infer::infer::at::ToTrace;
@ -20,10 +17,10 @@ use rustc_middle::ty::{
self, InferCtxtLike, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable,
TypeVisitable, TypeVisitableExt, TypeVisitor,
};
use rustc_session::config::DumpSolverProofTree;
use rustc_span::DUMMY_SP;
use rustc_type_ir::{self as ir, CanonicalVarValues, Interner};
use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
use std::ops::ControlFlow;
use crate::traits::coherence;
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
@ -135,8 +132,7 @@ impl<I: Interner> NestedGoals<I> {
#[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
pub enum GenerateProofTree {
Yes,
IfEnabled,
Never,
No,
}
#[extension(pub trait InferCtxtEvalExt<'tcx>)]
@ -182,7 +178,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
infcx,
search_graph: &mut search_graph,
nested_goals: NestedGoals::new(),
inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),
// Only relevant when canonicalizing the response,
// which we don't do within this evaluation context.
@ -197,23 +193,14 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
};
let result = f(&mut ecx);
let tree = ecx.inspect.finalize();
if let (Some(tree), DumpSolverProofTree::Always) = (
&tree,
infcx.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default(),
) {
let mut lock = std::io::stdout().lock();
let _ = lock.write_fmt(format_args!("{tree:?}\n"));
let _ = lock.flush();
}
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, tree)
(result, proof_tree)
}
/// Creates a nested evaluation context that shares the same search graph as the
@ -483,7 +470,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
// the certainty of all the goals.
#[instrument(level = "trace", skip(self))]
pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
self.inspect.start_evaluate_added_goals();
let mut response = Ok(Certainty::overflow(false));
for _ in 0..FIXPOINT_STEP_LIMIT {
// FIXME: This match is a bit ugly, it might be nice to change the inspect
@ -501,8 +487,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
}
}
self.inspect.evaluate_added_goals_result(response);
if response.is_err() {
self.tainted = Err(NoSolution);
}
@ -515,7 +499,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
/// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
let tcx = self.tcx();
self.inspect.start_evaluate_added_goals_step();
let mut goals = core::mem::take(&mut self.nested_goals);
// If this loop did not result in any progress, what's our final certainty.

6
compiler/rustc_trait_selection/src/solve/fulfill.rs
View File

@ -79,7 +79,7 @@ impl<'tcx> ObligationStorage<'tcx> {
// change.
self.overflowed.extend(self.pending.extract_if(|o| {
let goal = o.clone().into();
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::Never).0;
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
match result {
Ok((has_changed, _)) => has_changed,
_ => false,
@ -159,7 +159,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
let mut has_changed = false;
for obligation in self.obligations.unstalled_for_select() {
let goal = obligation.clone().into();
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0;
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
self.inspect_evaluated_obligation(infcx, &obligation, &result);
let (changed, certainty) = match result {
Ok(result) => result,
@ -246,7 +246,7 @@ fn fulfillment_error_for_stalled<'tcx>(
root_obligation: PredicateObligation<'tcx>,
) -> FulfillmentError<'tcx> {
let (code, refine_obligation) = infcx.probe(|_| {
match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::Never).0 {
match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::No).0 {
Ok((_, Certainty::Maybe(MaybeCause::Ambiguity))) => {
(FulfillmentErrorCode::Ambiguity { overflow: None }, true)
}

13
compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
View File

@ -317,7 +317,6 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
inspect::ProbeStep::RecordImplArgs { impl_args: i } => {
assert_eq!(impl_args.replace(i), None);
}
inspect::ProbeStep::EvaluateGoals(_) => (),
}
}
@ -359,13 +358,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
warn!("unexpected root evaluation: {:?}", self.evaluation_kind);
return vec![];
}
inspect::CanonicalGoalEvaluationKind::Evaluation { revisions } => {
if let Some(last) = revisions.last() {
last
} else {
return vec![];
}
}
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
};
let mut nested_goals = vec![];
@ -392,9 +385,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
source: GoalSource,
) -> Self {
let inspect::GoalEvaluation { uncanonicalized_goal, kind, evaluation } = root;
let inspect::GoalEvaluationKind::Root { orig_values } = kind else { unreachable!() };
let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, evaluation } = root;
let result = evaluation.result.and_then(|ok| {
if let Some(term_hack) = normalizes_to_term_hack {
infcx

226
compiler/rustc_trait_selection/src/solve/inspect/build.rs
View File

@ -5,20 +5,17 @@
//! see the comment on [ProofTreeBuilder].
use std::mem;
use crate::solve::eval_ctxt::canonical;
use crate::solve::{self, inspect, GenerateProofTree};
use rustc_infer::infer::InferCtxt;
use rustc_middle::bug;
use rustc_middle::infer::canonical::CanonicalVarValues;
use rustc_middle::traits::query::NoSolution;
use rustc_middle::ty::{self, TyCtxt};
use rustc_next_trait_solver::solve::{
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
};
use rustc_session::config::DumpSolverProofTree;
use rustc_type_ir::Interner;
use crate::solve::eval_ctxt::canonical;
use crate::solve::{self, inspect, GenerateProofTree};
/// The core data structure when building proof trees.
///
/// In case the current evaluation does not generate a proof
@ -53,7 +50,7 @@ enum DebugSolver<I: Interner> {
Root,
GoalEvaluation(WipGoalEvaluation<I>),
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<I>),
GoalEvaluationStep(WipGoalEvaluationStep<I>),
CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
}
impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
@ -68,9 +65,9 @@ impl<I: Interner> From<WipCanonicalGoalEvaluation<I>> for DebugSolver<I> {
}
}
impl<I: Interner> From<WipGoalEvaluationStep<I>> for DebugSolver<I> {
fn from(g: WipGoalEvaluationStep<I>) -> DebugSolver<I> {
DebugSolver::GoalEvaluationStep(g)
impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
DebugSolver::CanonicalGoalEvaluationStep(g)
}
}
@ -78,7 +75,7 @@ impl<I: Interner> From<WipGoalEvaluationStep<I>> for DebugSolver<I> {
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
struct WipGoalEvaluation<I: Interner> {
pub uncanonicalized_goal: Goal<I, I::Predicate>,
pub kind: WipGoalEvaluationKind<I>,
pub orig_values: Vec<I::GenericArg>,
pub evaluation: Option<WipCanonicalGoalEvaluation<I>>,
}
@ -86,31 +83,19 @@ impl<I: Interner> WipGoalEvaluation<I> {
fn finalize(self) -> inspect::GoalEvaluation<I> {
inspect::GoalEvaluation {
uncanonicalized_goal: self.uncanonicalized_goal,
kind: match self.kind {
WipGoalEvaluationKind::Root { orig_values } => {
inspect::GoalEvaluationKind::Root { orig_values }
}
WipGoalEvaluationKind::Nested => inspect::GoalEvaluationKind::Nested,
},
orig_values: self.orig_values,
evaluation: self.evaluation.unwrap().finalize(),
}
}
}
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
pub(in crate::solve) enum WipGoalEvaluationKind<I: Interner> {
Root { orig_values: Vec<I::GenericArg> },
Nested,
}
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""))]
pub(in crate::solve) enum WipCanonicalGoalEvaluationKind<I: Interner> {
Overflow,
CycleInStack,
ProvisionalCacheHit,
Interned { revisions: I::GoalEvaluationSteps },
Interned { final_revision: I::CanonicalGoalEvaluationStepRef },
}
impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
@ -119,7 +104,9 @@ impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
Self::Overflow => write!(f, "Overflow"),
Self::CycleInStack => write!(f, "CycleInStack"),
Self::ProvisionalCacheHit => write!(f, "ProvisionalCacheHit"),
Self::Interned { revisions: _ } => f.debug_struct("Interned").finish_non_exhaustive(),
Self::Interned { final_revision: _ } => {
f.debug_struct("Interned").finish_non_exhaustive()
}
}
}
}
@ -131,13 +118,15 @@ struct WipCanonicalGoalEvaluation<I: Interner> {
kind: Option<WipCanonicalGoalEvaluationKind<I>>,
/// Only used for uncached goals. After we finished evaluating
/// the goal, this is interned and moved into `kind`.
revisions: Vec<WipGoalEvaluationStep<I>>,
final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
result: Option<QueryResult<I>>,
}
impl<I: Interner> WipCanonicalGoalEvaluation<I> {
fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
assert!(self.revisions.is_empty());
// We've already interned the final revision in
// `fn finalize_canonical_goal_evaluation`.
assert!(self.final_revision.is_none());
let kind = match self.kind.unwrap() {
WipCanonicalGoalEvaluationKind::Overflow => {
inspect::CanonicalGoalEvaluationKind::Overflow
@ -148,8 +137,8 @@ impl<I: Interner> WipCanonicalGoalEvaluation<I> {
WipCanonicalGoalEvaluationKind::ProvisionalCacheHit => {
inspect::CanonicalGoalEvaluationKind::ProvisionalCacheHit
}
WipCanonicalGoalEvaluationKind::Interned { revisions } => {
inspect::CanonicalGoalEvaluationKind::Evaluation { revisions }
WipCanonicalGoalEvaluationKind::Interned { final_revision } => {
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision }
}
};
@ -159,29 +148,7 @@ impl<I: Interner> WipCanonicalGoalEvaluation<I> {
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
struct WipAddedGoalsEvaluation<I: Interner> {
evaluations: Vec<Vec<WipGoalEvaluation<I>>>,
result: Option<Result<Certainty, NoSolution>>,
}
impl<I: Interner> WipAddedGoalsEvaluation<I> {
fn finalize(self) -> inspect::AddedGoalsEvaluation<I> {
inspect::AddedGoalsEvaluation {
evaluations: self
.evaluations
.into_iter()
.map(|evaluations| {
evaluations.into_iter().map(WipGoalEvaluation::finalize).collect()
})
.collect(),
result: self.result.unwrap(),
}
}
}
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
struct WipGoalEvaluationStep<I: Interner> {
struct WipCanonicalGoalEvaluationStep<I: Interner> {
/// Unlike `EvalCtxt::var_values`, we append a new
/// generic arg here whenever we create a new inference
/// variable.
@ -194,7 +161,7 @@ struct WipGoalEvaluationStep<I: Interner> {
evaluation: WipProbe<I>,
}
impl<I: Interner> WipGoalEvaluationStep<I> {
impl<I: Interner> WipCanonicalGoalEvaluationStep<I> {
fn current_evaluation_scope(&mut self) -> &mut WipProbe<I> {
let mut current = &mut self.evaluation;
for _ in 0..self.probe_depth {
@ -206,24 +173,16 @@ impl<I: Interner> WipGoalEvaluationStep<I> {
current
}
fn added_goals_evaluation(&mut self) -> &mut WipAddedGoalsEvaluation<I> {
let mut current = &mut self.evaluation;
loop {
match current.steps.last_mut() {
Some(WipProbeStep::NestedProbe(p)) => current = p,
Some(WipProbeStep::EvaluateGoals(evaluation)) => return evaluation,
_ => bug!(),
}
}
}
fn finalize(self) -> inspect::GoalEvaluationStep<I> {
fn finalize(self) -> inspect::CanonicalGoalEvaluationStep<I> {
let evaluation = self.evaluation.finalize();
match evaluation.kind {
inspect::ProbeKind::Root { .. } => (),
_ => unreachable!("unexpected root evaluation: {evaluation:?}"),
}
inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
inspect::CanonicalGoalEvaluationStep {
instantiated_goal: self.instantiated_goal,
evaluation,
}
}
}
@ -250,7 +209,6 @@ impl<I: Interner> WipProbe<I> {
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
enum WipProbeStep<I: Interner> {
AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, I::Predicate>>),
EvaluateGoals(WipAddedGoalsEvaluation<I>),
NestedProbe(WipProbe<I>),
MakeCanonicalResponse { shallow_certainty: Certainty },
RecordImplArgs { impl_args: inspect::CanonicalState<I, I::GenericArgs> },
@ -260,7 +218,6 @@ impl<I: Interner> WipProbeStep<I> {
fn finalize(self) -> inspect::ProbeStep<I> {
match self {
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
WipProbeStep::RecordImplArgs { impl_args } => {
inspect::ProbeStep::RecordImplArgs { impl_args }
@ -278,6 +235,15 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
ProofTreeBuilder { state: Some(Box::new(state.into())) }
}
fn opt_nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(
&self,
state: impl FnOnce() -> Option<T>,
) -> Self {
ProofTreeBuilder {
state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
}
}
fn nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(&self, state: impl FnOnce() -> T) -> Self {
ProofTreeBuilder { state: self.state.as_ref().map(|_| Box::new(state().into())) }
}
@ -302,22 +268,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
}
pub fn new_maybe_root(
tcx: TyCtxt<'tcx>,
generate_proof_tree: GenerateProofTree,
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
match generate_proof_tree {
GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
GenerateProofTree::IfEnabled => {
let opts = &tcx.sess.opts.unstable_opts;
match opts.next_solver.map(|c| c.dump_tree).unwrap_or_default() {
DumpSolverProofTree::Always => ProofTreeBuilder::new_root(),
// `OnError` is handled by reevaluating goals in error
// reporting with `GenerateProofTree::Yes`.
DumpSolverProofTree::OnError | DumpSolverProofTree::Never => {
ProofTreeBuilder::new_noop()
}
}
}
GenerateProofTree::No => ProofTreeBuilder::new_noop(),
GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
}
}
@ -340,15 +294,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
orig_values: &[ty::GenericArg<'tcx>],
kind: solve::GoalEvaluationKind,
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
self.nested(|| WipGoalEvaluation {
uncanonicalized_goal: goal,
kind: match kind {
solve::GoalEvaluationKind::Root => {
WipGoalEvaluationKind::Root { orig_values: orig_values.to_vec() }
}
solve::GoalEvaluationKind::Nested => WipGoalEvaluationKind::Nested,
},
evaluation: None,
self.opt_nested(|| match kind {
solve::GoalEvaluationKind::Root => Some(WipGoalEvaluation {
uncanonicalized_goal: goal,
orig_values: orig_values.to_vec(),
evaluation: None,
}),
solve::GoalEvaluationKind::Nested => None,
})
}
@ -359,24 +311,22 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
self.nested(|| WipCanonicalGoalEvaluation {
goal,
kind: None,
revisions: vec![],
final_revision: None,
result: None,
})
}
pub fn finalize_evaluation(
pub fn finalize_canonical_goal_evaluation(
&mut self,
tcx: TyCtxt<'tcx>,
) -> Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]> {
) -> Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>> {
self.as_mut().map(|this| match this {
DebugSolver::CanonicalGoalEvaluation(evaluation) => {
let revisions = mem::take(&mut evaluation.revisions)
.into_iter()
.map(WipGoalEvaluationStep::finalize);
let revisions = &*tcx.arena.alloc_from_iter(revisions);
let kind = WipCanonicalGoalEvaluationKind::Interned { revisions };
let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
let final_revision = &*tcx.arena.alloc(final_revision.finalize());
let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
assert_eq!(evaluation.kind.replace(kind), None);
revisions
final_revision
}
_ => unreachable!(),
})
@ -400,7 +350,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
}
}
pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>) {
pub fn canonical_goal_evaluation_kind(
&mut self,
kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
) {
if let Some(this) = self.as_mut() {
match this {
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
@ -413,17 +366,11 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>) {
if let Some(this) = self.as_mut() {
match (this, *goal_evaluation.state.unwrap()) {
(
DebugSolver::GoalEvaluationStep(state),
DebugSolver::GoalEvaluation(goal_evaluation),
) => state
.added_goals_evaluation()
.evaluations
.last_mut()
.unwrap()
.push(goal_evaluation),
(this @ DebugSolver::Root, goal_evaluation) => *this = goal_evaluation,
match this {
DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
DebugSolver::CanonicalGoalEvaluationStep(_) => {
assert!(goal_evaluation.state.is_none())
}
_ => unreachable!(),
}
}
@ -434,7 +381,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
var_values: CanonicalVarValues<'tcx>,
instantiated_goal: QueryInput<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
self.nested(|| WipGoalEvaluationStep {
self.nested(|| WipCanonicalGoalEvaluationStep {
var_values: var_values.var_values.to_vec(),
instantiated_goal,
evaluation: WipProbe {
@ -452,9 +399,9 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
match (this, *goal_evaluation_step.state.unwrap()) {
(
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
DebugSolver::GoalEvaluationStep(goal_evaluation_step),
DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
) => {
canonical_goal_evaluations.revisions.push(goal_evaluation_step);
canonical_goal_evaluations.final_revision = Some(goal_evaluation_step);
}
_ => unreachable!(),
}
@ -464,7 +411,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
pub fn add_var_value<T: Into<ty::GenericArg<'tcx>>>(&mut self, arg: T) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
state.var_values.push(arg.into());
}
Some(s) => bug!("tried to add var values to {s:?}"),
@ -474,7 +421,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
pub fn enter_probe(&mut self) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
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,
@ -491,7 +438,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<TyCtxt<'tcx>>) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
let prev = state.current_evaluation_scope().kind.replace(probe_kind);
assert_eq!(prev, None);
}
@ -506,7 +453,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
let final_state = canonical::make_canonical_state(
infcx,
&state.var_values,
@ -543,7 +490,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
let goal = canonical::make_canonical_state(
infcx,
&state.var_values,
@ -563,7 +510,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
impl_args: ty::GenericArgsRef<'tcx>,
) {
match self.as_mut() {
Some(DebugSolver::GoalEvaluationStep(state)) => {
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
let impl_args = canonical::make_canonical_state(
infcx,
&state.var_values,
@ -582,7 +529,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
pub fn make_canonical_response(&mut self, shallow_certainty: Certainty) {
match self.as_mut() {
Some(DebugSolver::GoalEvaluationStep(state)) => {
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
state
.current_evaluation_scope()
.steps
@ -596,7 +543,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
pub fn finish_probe(mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
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);
@ -608,46 +555,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
self
}
pub fn start_evaluate_added_goals(&mut self) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
state.current_evaluation_scope().steps.push(WipProbeStep::EvaluateGoals(
WipAddedGoalsEvaluation { evaluations: vec![], result: None },
));
}
_ => bug!(),
}
}
pub fn start_evaluate_added_goals_step(&mut self) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
state.added_goals_evaluation().evaluations.push(vec![]);
}
_ => bug!(),
}
}
pub fn evaluate_added_goals_result(&mut self, result: Result<Certainty, NoSolution>) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
let prev = state.added_goals_evaluation().result.replace(result);
assert_eq!(prev, None);
}
_ => bug!(),
}
}
pub fn query_result(&mut self, result: QueryResult<TyCtxt<'tcx>>) {
if let Some(this) = self.as_mut() {
match this {
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
assert_eq!(canonical_goal_evaluation.result.replace(result), None);
}
DebugSolver::GoalEvaluationStep(evaluation_step) => {
DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
assert_eq!(
evaluation_step
.evaluation

20
compiler/rustc_trait_selection/src/solve/search_graph.rs
View File

@ -274,7 +274,8 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
last.encountered_overflow = true;
}
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
inspect
.canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
return Self::response_no_constraints(tcx, input, Certainty::overflow(true));
};
@ -302,8 +303,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
// We have a nested goal which is already in the provisional cache, use
// its result. We do not provide any usage kind as that should have been
// already set correctly while computing the cache entry.
inspect
.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::ProvisionalCacheHit);
inspect.canonical_goal_evaluation_kind(
inspect::WipCanonicalGoalEvaluationKind::ProvisionalCacheHit,
);
Self::tag_cycle_participants(&mut self.stack, HasBeenUsed::empty(), entry.head);
return entry.result;
} else if let Some(stack_depth) = cache_entry.stack_depth {
@ -314,7 +316,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
//
// Finally we can return either the provisional response or the initial response
// in case we're in the first fixpoint iteration for this goal.
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CycleInStack);
inspect.canonical_goal_evaluation_kind(
inspect::WipCanonicalGoalEvaluationKind::CycleInStack,
);
let is_coinductive_cycle = Self::stack_coinductive_from(tcx, &self.stack, stack_depth);
let usage_kind = if is_coinductive_cycle {
HasBeenUsed::COINDUCTIVE_CYCLE
@ -371,7 +375,7 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
(current_entry, result)
});
let proof_tree = inspect.finalize_evaluation(tcx);
let proof_tree = inspect.finalize_canonical_goal_evaluation(tcx);
// We're now done with this goal. In case this goal is involved in a larger cycle
// do not remove it from the provisional cache and update its provisional result.
@ -433,9 +437,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
// the goal. We simply overwrite the existing entry once we're done,
// caching the proof tree.
if !inspect.is_noop() {
if let Some(revisions) = proof_tree {
let kind = inspect::WipCanonicalGoalEvaluationKind::Interned { revisions };
inspect.goal_evaluation_kind(kind);
if let Some(final_revision) = proof_tree {
let kind = inspect::WipCanonicalGoalEvaluationKind::Interned { final_revision };
inspect.canonical_goal_evaluation_kind(kind);
} else {
return None;
}

17
compiler/rustc_trait_selection/src/traits/error_reporting/mod.rs
View File

@ -7,15 +7,11 @@ pub mod suggestions;
mod type_err_ctxt_ext;
use super::{Obligation, ObligationCause, ObligationCauseCode, PredicateObligation};
use crate::infer::InferCtxt;
use crate::solve::{GenerateProofTree, InferCtxtEvalExt};
use rustc_hir as hir;
use rustc_hir::def_id::DefId;
use rustc_hir::intravisit::Visitor;
use rustc_middle::traits::solve::Goal;
use rustc_middle::ty::{self, Ty, TyCtxt};
use rustc_span::Span;
use std::io::Write;
use std::ops::ControlFlow;
pub use self::infer_ctxt_ext::*;
@ -184,16 +180,3 @@ pub enum DefIdOrName {
DefId(DefId),
Name(&'static str),
}
pub fn dump_proof_tree<'tcx>(o: &Obligation<'tcx, ty::Predicate<'tcx>>, infcx: &InferCtxt<'tcx>) {
infcx.probe(|_| {
let goal = Goal { predicate: o.predicate, param_env: o.param_env };
let tree = infcx
.evaluate_root_goal(goal, GenerateProofTree::Yes)
.1
.expect("proof tree should have been generated");
let mut lock = std::io::stdout().lock();
let _ = lock.write_fmt(format_args!("{tree:?}\n"));
let _ = lock.flush();
});
}

18
compiler/rustc_trait_selection/src/traits/error_reporting/type_err_ctxt_ext.rs
View File

@ -46,7 +46,6 @@ use rustc_middle::ty::{
TypeVisitableExt, Upcast,
};
use rustc_middle::{bug, span_bug};
use rustc_session::config::DumpSolverProofTree;
use rustc_session::Limit;
use rustc_span::def_id::LOCAL_CRATE;
use rustc_span::symbol::sym;
@ -56,8 +55,8 @@ use std::fmt;
use std::iter;
use super::{
dump_proof_tree, ArgKind, CandidateSimilarity, FindExprBySpan, FindTypeParam,
GetSafeTransmuteErrorAndReason, HasNumericInferVisitor, ImplCandidate, UnsatisfiedConst,
ArgKind, CandidateSimilarity, FindExprBySpan, FindTypeParam, GetSafeTransmuteErrorAndReason,
HasNumericInferVisitor, ImplCandidate, UnsatisfiedConst,
};
pub use rustc_infer::traits::error_reporting::*;
@ -369,13 +368,6 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
error: &SelectionError<'tcx>,
) -> ErrorGuaranteed {
let tcx = self.tcx;
if tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default()
== DumpSolverProofTree::OnError
{
dump_proof_tree(root_obligation, self.infcx);
}
let mut span = obligation.cause.span;
let mut err = match *error {
@ -1529,12 +1521,6 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
#[instrument(skip(self), level = "debug")]
fn report_fulfillment_error(&self, error: &FulfillmentError<'tcx>) -> ErrorGuaranteed {
if self.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default()
== DumpSolverProofTree::OnError
{
dump_proof_tree(&error.root_obligation, self.infcx);
}
match error.code {
FulfillmentErrorCode::Select(ref selection_error) => self.report_selection_error(
error.obligation.clone(),

8
compiler/rustc_type_ir/src/interner.rs
View File

@ -5,7 +5,7 @@ use std::ops::Deref;
use crate::inherent::*;
use crate::ir_print::IrPrint;
use crate::solve::inspect::GoalEvaluationStep;
use crate::solve::inspect::CanonicalGoalEvaluationStep;
use crate::visit::{Flags, TypeSuperVisitable, TypeVisitable};
use crate::{
AliasTerm, AliasTermKind, AliasTy, AliasTyKind, CanonicalVarInfo, CoercePredicate,
@ -55,7 +55,11 @@ pub trait Interner:
type PredefinedOpaques: Copy + Debug + Hash + Eq;
type DefiningOpaqueTypes: Copy + Debug + Hash + Default + Eq + TypeVisitable<Self>;
type ExternalConstraints: Copy + Debug + Hash + Eq;
type GoalEvaluationSteps: Copy + Debug + Hash + Eq + Deref<Target = [GoalEvaluationStep<Self>]>;
type CanonicalGoalEvaluationStepRef: Copy
+ Debug
+ Hash
+ Eq
+ Deref<Target = CanonicalGoalEvaluationStep<Self>>;
// Kinds of tys
type Ty: Ty<Self>;

77
compiler/rustc_type_ir/src/solve/inspect.rs
View File

@ -1,36 +1,29 @@
//! Data structure used to inspect trait solver behavior.
//!
//! During trait solving we optionally build "proof trees", the root of
//! which is a [GoalEvaluation] with [GoalEvaluationKind::Root]. These
//! trees are used to improve the debug experience and are also used by
//! the compiler itself to provide necessary context for error messages.
//! which is a [GoalEvaluation]. These trees are used by the compiler
//! to inspect the behavior of the trait solver and to access its internal
//! state, e.g. for diagnostics and when selecting impls during codegen.
//!
//! Because each nested goal in the solver gets [canonicalized] separately
//! and we discard inference progress via "probes", we cannot mechanically
//! use proof trees without somehow "lifting up" data local to the current
//! `InferCtxt`. Any data used mechanically is therefore canonicalized and
//! stored as [CanonicalState]. As printing canonicalized data worsens the
//! debugging dumps, we do not simply canonicalize everything.
//! `InferCtxt`. To use the data from evaluation we therefore canonicalize
//! it and store it as a [CanonicalState].
//!
//! This means proof trees contain inference variables and placeholders
//! local to a different `InferCtxt` which must not be used with the
//! current one.
//! Proof trees are only shallow, we do not compute the proof tree for nested
//! goals. Visiting proof trees instead recomputes nested goals in the parents
//! inference context when necessary.
//!
//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
mod format;
use std::fmt::{Debug, Write};
use std::hash::Hash;
use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
use self::format::ProofTreeFormatter;
use crate::solve::{
CandidateSource, CanonicalInput, Certainty, Goal, GoalSource, NoSolution, QueryInput,
QueryResult,
CandidateSource, CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
};
use crate::{Canonical, CanonicalVarValues, Interner};
use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
use std::fmt::Debug;
use std::hash::Hash;
/// Some `data` together with information about how they relate to the input
/// of the canonical query.
@ -55,23 +48,15 @@ pub struct State<I: Interner, T> {
pub type CanonicalState<I, T> = Canonical<I, State<I, T>>;
/// When evaluating the root goals we also store the
/// original values 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(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
pub enum GoalEvaluationKind<I: Interner> {
Root { orig_values: Vec<I::GenericArg> },
Nested,
}
/// When evaluating a goal we also store the original values
/// 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(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
pub struct GoalEvaluation<I: Interner> {
pub uncanonicalized_goal: Goal<I, I::Predicate>,
pub kind: GoalEvaluationKind<I>,
pub orig_values: Vec<I::GenericArg>,
pub evaluation: CanonicalGoalEvaluation<I>,
}
@ -89,24 +74,12 @@ pub enum CanonicalGoalEvaluationKind<I: Interner> {
Overflow,
CycleInStack,
ProvisionalCacheHit,
Evaluation { revisions: I::GoalEvaluationSteps },
}
impl<I: Interner> Debug for GoalEvaluation<I> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter::new(f).format_goal_evaluation(self)
}
Evaluation { final_revision: I::CanonicalGoalEvaluationStepRef },
}
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
pub struct AddedGoalsEvaluation<I: Interner> {
pub evaluations: Vec<Vec<GoalEvaluation<I>>>,
pub result: Result<Certainty, NoSolution>,
}
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
pub struct GoalEvaluationStep<I: Interner> {
pub struct CanonicalGoalEvaluationStep<I: Interner> {
pub instantiated_goal: QueryInput<I, I::Predicate>,
/// The actual evaluation of the goal, always `ProbeKind::Root`.
@ -117,7 +90,7 @@ pub struct GoalEvaluationStep<I: Interner> {
/// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation
/// of a goal.
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
#[derivative(Debug(bound = ""), PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""))]
pub struct Probe<I: Interner> {
/// What happened inside of this probe in chronological order.
pub steps: Vec<ProbeStep<I>>,
@ -125,23 +98,15 @@ pub struct Probe<I: Interner> {
pub final_state: CanonicalState<I, ()>,
}
impl<I: Interner> Debug for Probe<I> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter::new(f).format_probe(self)
}
}
#[derive(derivative::Derivative)]
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Hash(bound = ""), Debug(bound = ""))]
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.
AddGoal(GoalSource, CanonicalState<I, Goal<I, I::Predicate>>),
/// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
EvaluateGoals(AddedGoalsEvaluation<I>),
/// A call to `probe` while proving the current goal. This is
/// used whenever there are multiple candidates to prove the
/// current goalby .
/// current goal.
NestedProbe(Probe<I>),
/// A trait goal was satisfied by an impl candidate.
RecordImplArgs { impl_args: CanonicalState<I, I::GenericArgs> },

173
compiler/rustc_type_ir/src/solve/inspect/format.rs
View File

@ -1,173 +0,0 @@
use std::marker::PhantomData;
use super::*;
pub(super) struct ProofTreeFormatter<'a, 'b, I> {
f: &'a mut (dyn Write + 'b),
_interner: PhantomData<I>,
}
enum IndentorState {
StartWithNewline,
OnNewline,
Inline,
}
/// A formatter which adds 4 spaces of indentation to its input before
/// passing it on to its nested formatter.
///
/// We can use this for arbitrary levels of indentation by nesting it.
struct Indentor<'a, 'b> {
f: &'a mut (dyn Write + 'b),
state: IndentorState,
}
impl Write for Indentor<'_, '_> {
fn write_str(&mut self, s: &str) -> std::fmt::Result {
for line in s.split_inclusive('\n') {
match self.state {
IndentorState::StartWithNewline => self.f.write_str("\n ")?,
IndentorState::OnNewline => self.f.write_str(" ")?,
IndentorState::Inline => {}
}
self.state =
if line.ends_with('\n') { IndentorState::OnNewline } else { IndentorState::Inline };
self.f.write_str(line)?;
}
Ok(())
}
}
impl<'a, 'b, I: Interner> ProofTreeFormatter<'a, 'b, I> {
pub(super) fn new(f: &'a mut (dyn Write + 'b)) -> Self {
ProofTreeFormatter { f, _interner: PhantomData }
}
fn nested<F>(&mut self, func: F) -> std::fmt::Result
where
F: FnOnce(&mut ProofTreeFormatter<'_, '_, I>) -> std::fmt::Result,
{
write!(self.f, " {{")?;
func(&mut ProofTreeFormatter {
f: &mut Indentor { f: self.f, state: IndentorState::StartWithNewline },
_interner: PhantomData,
})?;
writeln!(self.f, "}}")
}
pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<I>) -> std::fmt::Result {
let goal_text = match eval.kind {
GoalEvaluationKind::Root { orig_values: _ } => "ROOT GOAL",
GoalEvaluationKind::Nested => "GOAL",
};
write!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
}
pub(super) fn format_canonical_goal_evaluation(
&mut self,
eval: &CanonicalGoalEvaluation<I>,
) -> std::fmt::Result {
writeln!(self.f, "GOAL: {:?}", eval.goal)?;
match &eval.kind {
CanonicalGoalEvaluationKind::Overflow => {
writeln!(self.f, "OVERFLOW: {:?}", eval.result)
}
CanonicalGoalEvaluationKind::CycleInStack => {
writeln!(self.f, "CYCLE IN STACK: {:?}", eval.result)
}
CanonicalGoalEvaluationKind::ProvisionalCacheHit => {
writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
}
CanonicalGoalEvaluationKind::Evaluation { revisions } => {
for (n, step) in revisions.iter().enumerate() {
write!(self.f, "REVISION {n}")?;
self.nested(|this| this.format_evaluation_step(step))?;
}
writeln!(self.f, "RESULT: {:?}", eval.result)
}
}
}
pub(super) fn format_evaluation_step(
&mut self,
evaluation_step: &GoalEvaluationStep<I>,
) -> std::fmt::Result {
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
self.format_probe(&evaluation_step.evaluation)
}
pub(super) fn format_probe(&mut self, probe: &Probe<I>) -> std::fmt::Result {
match &probe.kind {
ProbeKind::Root { result } => {
write!(self.f, "ROOT RESULT: {result:?}")
}
ProbeKind::TryNormalizeNonRigid { result } => {
write!(self.f, "TRY NORMALIZE NON-RIGID: {result:?}")
}
ProbeKind::NormalizedSelfTyAssembly => {
write!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
}
ProbeKind::UnsizeAssembly => {
write!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:")
}
ProbeKind::UpcastProjectionCompatibility => {
write!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:")
}
ProbeKind::OpaqueTypeStorageLookup { result } => {
write!(self.f, "PROBING FOR AN EXISTING OPAQUE: {result:?}")
}
ProbeKind::TraitCandidate { source, result } => {
write!(self.f, "CANDIDATE {source:?}: {result:?}")
}
ProbeKind::ShadowedEnvProbing => {
write!(self.f, "PROBING FOR IMPLS SHADOWED BY PARAM-ENV CANDIDATE:")
}
}?;
self.nested(|this| {
for step in &probe.steps {
match step {
ProbeStep::AddGoal(source, goal) => {
let source = match source {
GoalSource::Misc => "misc",
GoalSource::ImplWhereBound => "impl where-bound",
GoalSource::InstantiateHigherRanked => "higher-ranked goal",
};
writeln!(this.f, "ADDED GOAL ({source}): {goal:?}")?
}
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
ProbeStep::MakeCanonicalResponse { shallow_certainty } => {
writeln!(this.f, "EVALUATE GOALS AND MAKE RESPONSE: {shallow_certainty:?}")?
}
ProbeStep::RecordImplArgs { impl_args } => {
writeln!(this.f, "RECORDED IMPL ARGS: {impl_args:?}")?
}
}
}
Ok(())
})
}
pub(super) fn format_added_goals_evaluation(
&mut self,
added_goals_evaluation: &AddedGoalsEvaluation<I>,
) -> std::fmt::Result {
writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", added_goals_evaluation.result)?;
for (n, iterations) in added_goals_evaluation.evaluations.iter().enumerate() {
write!(self.f, "ITERATION {n}")?;
self.nested(|this| {
for goal_evaluation in iterations {
this.format_goal_evaluation(goal_evaluation)?;
}
Ok(())
})?;
}
Ok(())
}
}