mirror of
https://github.com/rust-lang/rust.git
synced 2024-11-25 16:24:46 +00:00
Rollup merge of #115838 - lcnr:added-goals, r=compiler-errors
inspect: closer to proof trees for coherence a continuation of #115751. Now explicitly store the added goals r? ```@compiler-errors```
This commit is contained in:
commit
944c4134d2
@ -14,10 +14,16 @@ pub enum CacheHit {
|
||||
Global,
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub enum GoalEvaluationKind {
|
||||
Root,
|
||||
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub struct GoalEvaluation<'tcx> {
|
||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
pub is_normalizes_to_hack: IsNormalizesToHack,
|
||||
pub kind: GoalEvaluationKind,
|
||||
pub evaluation: CanonicalGoalEvaluation<'tcx>,
|
||||
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||
}
|
||||
@ -25,12 +31,12 @@ pub struct GoalEvaluation<'tcx> {
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub struct CanonicalGoalEvaluation<'tcx> {
|
||||
pub goal: CanonicalInput<'tcx>,
|
||||
pub kind: GoalEvaluationKind<'tcx>,
|
||||
pub kind: CanonicalGoalEvaluationKind<'tcx>,
|
||||
pub result: QueryResult<'tcx>,
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub enum GoalEvaluationKind<'tcx> {
|
||||
pub enum CanonicalGoalEvaluationKind<'tcx> {
|
||||
Overflow,
|
||||
CacheHit(CacheHit),
|
||||
Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
|
||||
@ -52,22 +58,31 @@ pub struct GoalEvaluationStep<'tcx> {
|
||||
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
||||
|
||||
/// The actual evaluation of the goal, always `ProbeKind::Root`.
|
||||
pub evaluation: GoalCandidate<'tcx>,
|
||||
pub evaluation: Probe<'tcx>,
|
||||
}
|
||||
|
||||
/// A self-contained computation during trait solving. This either
|
||||
/// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation
|
||||
/// of a goal.
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub struct GoalCandidate<'tcx> {
|
||||
pub added_goals_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
|
||||
pub candidates: Vec<GoalCandidate<'tcx>>,
|
||||
pub struct Probe<'tcx> {
|
||||
pub steps: Vec<ProbeStep<'tcx>>,
|
||||
pub kind: ProbeKind<'tcx>,
|
||||
}
|
||||
|
||||
impl Debug for GoalCandidate<'_> {
|
||||
impl Debug for Probe<'_> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
ProofTreeFormatter::new(f).format_candidate(self)
|
||||
ProofTreeFormatter::new(f).format_probe(self)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub enum ProbeStep<'tcx> {
|
||||
AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
|
||||
EvaluateGoals(AddedGoalsEvaluation<'tcx>),
|
||||
NestedProbe(Probe<'tcx>),
|
||||
}
|
||||
|
||||
#[derive(Debug, PartialEq, Eq)]
|
||||
pub enum ProbeKind<'tcx> {
|
||||
/// The root inference context while proving a goal.
|
||||
|
@ -40,9 +40,12 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||
}
|
||||
|
||||
pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
|
||||
let goal_text = match eval.is_normalizes_to_hack {
|
||||
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
|
||||
IsNormalizesToHack::No => "GOAL",
|
||||
let goal_text = match eval.kind {
|
||||
GoalEvaluationKind::Root => "ROOT GOAL",
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack } => match is_normalizes_to_hack {
|
||||
IsNormalizesToHack::No => "GOAL",
|
||||
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
|
||||
},
|
||||
};
|
||||
writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
|
||||
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
|
||||
@ -68,16 +71,16 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||
writeln!(self.f, "GOAL: {:?}", eval.goal)?;
|
||||
|
||||
match &eval.kind {
|
||||
GoalEvaluationKind::Overflow => {
|
||||
CanonicalGoalEvaluationKind::Overflow => {
|
||||
writeln!(self.f, "OVERFLOW: {:?}", eval.result)
|
||||
}
|
||||
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
|
||||
CanonicalGoalEvaluationKind::CacheHit(CacheHit::Global) => {
|
||||
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
|
||||
}
|
||||
GoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
|
||||
CanonicalGoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
|
||||
writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
|
||||
}
|
||||
GoalEvaluationKind::Uncached { revisions } => {
|
||||
CanonicalGoalEvaluationKind::Uncached { revisions } => {
|
||||
for (n, step) in revisions.iter().enumerate() {
|
||||
writeln!(self.f, "REVISION {n}")?;
|
||||
self.nested(|this| this.format_evaluation_step(step))?;
|
||||
@ -92,11 +95,11 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||
evaluation_step: &GoalEvaluationStep<'_>,
|
||||
) -> std::fmt::Result {
|
||||
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
|
||||
self.format_candidate(&evaluation_step.evaluation)
|
||||
self.format_probe(&evaluation_step.evaluation)
|
||||
}
|
||||
|
||||
pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
|
||||
match &candidate.kind {
|
||||
pub(super) fn format_probe(&mut self, probe: &Probe<'_>) -> std::fmt::Result {
|
||||
match &probe.kind {
|
||||
ProbeKind::Root { result } => {
|
||||
writeln!(self.f, "ROOT RESULT: {result:?}")
|
||||
}
|
||||
@ -118,11 +121,12 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||
}?;
|
||||
|
||||
self.nested(|this| {
|
||||
for candidate in &candidate.candidates {
|
||||
this.format_candidate(candidate)?;
|
||||
}
|
||||
for nested in &candidate.added_goals_evaluations {
|
||||
this.format_added_goals_evaluation(nested)?;
|
||||
for step in &probe.steps {
|
||||
match step {
|
||||
ProbeStep::AddGoal(goal) => writeln!(this.f, "ADDED GOAL: {goal:?}")?,
|
||||
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
|
||||
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
})
|
||||
|
@ -28,8 +28,8 @@ use std::ops::ControlFlow;
|
||||
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
|
||||
|
||||
use super::inspect::ProofTreeBuilder;
|
||||
use super::search_graph;
|
||||
use super::SolverMode;
|
||||
use super::{search_graph, GoalEvaluationKind};
|
||||
use super::{search_graph::SearchGraph, Goal};
|
||||
pub use select::InferCtxtSelectExt;
|
||||
|
||||
@ -85,7 +85,7 @@ pub struct EvalCtxt<'a, 'tcx> {
|
||||
// evaluation code.
|
||||
tainted: Result<(), NoSolution>,
|
||||
|
||||
inspect: ProofTreeBuilder<'tcx>,
|
||||
pub(super) inspect: ProofTreeBuilder<'tcx>,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
@ -164,7 +164,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
|
||||
Option<inspect::GoalEvaluation<'tcx>>,
|
||||
) {
|
||||
EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
|
||||
ecx.evaluate_goal(IsNormalizesToHack::No, goal)
|
||||
ecx.evaluate_goal(GoalEvaluationKind::Root, goal)
|
||||
})
|
||||
}
|
||||
}
|
||||
@ -340,11 +340,11 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
/// been constrained and the certainty of the result.
|
||||
fn evaluate_goal(
|
||||
&mut self,
|
||||
is_normalizes_to_hack: IsNormalizesToHack,
|
||||
goal_evaluation_kind: GoalEvaluationKind,
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
|
||||
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
||||
let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, is_normalizes_to_hack);
|
||||
let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, goal_evaluation_kind);
|
||||
let encountered_overflow = self.search_graph.encountered_overflow();
|
||||
let canonical_response = EvalCtxt::evaluate_canonical_goal(
|
||||
self.tcx(),
|
||||
@ -389,7 +389,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
// solver cycle.
|
||||
if cfg!(debug_assertions)
|
||||
&& has_changed
|
||||
&& is_normalizes_to_hack == IsNormalizesToHack::No
|
||||
&& !matches!(
|
||||
goal_evaluation_kind,
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes }
|
||||
)
|
||||
&& !self.search_graph.in_cycle()
|
||||
{
|
||||
// The nested evaluation has to happen with the original state
|
||||
@ -561,8 +564,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
},
|
||||
);
|
||||
|
||||
let (_, certainty, instantiate_goals) =
|
||||
self.evaluate_goal(IsNormalizesToHack::Yes, unconstrained_goal)?;
|
||||
let (_, certainty, instantiate_goals) = self.evaluate_goal(
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
|
||||
unconstrained_goal,
|
||||
)?;
|
||||
self.add_goals(instantiate_goals);
|
||||
|
||||
// Finally, equate the goal's RHS with the unconstrained var.
|
||||
@ -596,8 +601,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
}
|
||||
|
||||
for goal in goals.goals.drain(..) {
|
||||
let (has_changed, certainty, instantiate_goals) =
|
||||
self.evaluate_goal(IsNormalizesToHack::No, goal)?;
|
||||
let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
|
||||
goal,
|
||||
)?;
|
||||
self.add_goals(instantiate_goals);
|
||||
if has_changed {
|
||||
unchanged_certainty = None;
|
||||
|
@ -24,13 +24,13 @@ where
|
||||
search_graph: outer_ecx.search_graph,
|
||||
nested_goals: outer_ecx.nested_goals.clone(),
|
||||
tainted: outer_ecx.tainted,
|
||||
inspect: outer_ecx.inspect.new_goal_candidate(),
|
||||
inspect: outer_ecx.inspect.new_probe(),
|
||||
};
|
||||
let r = nested_ecx.infcx.probe(|_| f(&mut nested_ecx));
|
||||
if !outer_ecx.inspect.is_noop() {
|
||||
let probe_kind = probe_kind(&r);
|
||||
nested_ecx.inspect.probe_kind(probe_kind);
|
||||
outer_ecx.inspect.goal_candidate(nested_ecx.inspect);
|
||||
outer_ecx.inspect.finish_probe(nested_ecx.inspect);
|
||||
}
|
||||
r
|
||||
}
|
||||
|
@ -7,13 +7,13 @@ use rustc_middle::ty::{self, TyCtxt};
|
||||
use rustc_session::config::DumpSolverProofTree;
|
||||
|
||||
use super::eval_ctxt::UseGlobalCache;
|
||||
use super::GenerateProofTree;
|
||||
use super::{GenerateProofTree, GoalEvaluationKind};
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipGoalEvaluation<'tcx> {
|
||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
pub kind: WipGoalEvaluationKind,
|
||||
pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
|
||||
pub is_normalizes_to_hack: IsNormalizesToHack,
|
||||
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||
}
|
||||
|
||||
@ -21,8 +21,13 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
|
||||
pub fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
|
||||
inspect::GoalEvaluation {
|
||||
uncanonicalized_goal: self.uncanonicalized_goal,
|
||||
kind: match self.kind {
|
||||
WipGoalEvaluationKind::Root => inspect::GoalEvaluationKind::Root,
|
||||
WipGoalEvaluationKind::Nested { is_normalizes_to_hack } => {
|
||||
inspect::GoalEvaluationKind::Nested { is_normalizes_to_hack }
|
||||
}
|
||||
},
|
||||
evaluation: self.evaluation.unwrap().finalize(),
|
||||
is_normalizes_to_hack: self.is_normalizes_to_hack,
|
||||
returned_goals: self.returned_goals,
|
||||
}
|
||||
}
|
||||
@ -30,6 +35,12 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub enum WipGoalEvaluationKind {
|
||||
Root,
|
||||
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub enum WipCanonicalGoalEvaluationKind {
|
||||
Overflow,
|
||||
CacheHit(CacheHit),
|
||||
}
|
||||
@ -37,7 +48,7 @@ pub enum WipGoalEvaluationKind {
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipCanonicalGoalEvaluation<'tcx> {
|
||||
pub goal: CanonicalInput<'tcx>,
|
||||
pub kind: Option<WipGoalEvaluationKind>,
|
||||
pub kind: Option<WipCanonicalGoalEvaluationKind>,
|
||||
pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
|
||||
pub result: Option<QueryResult<'tcx>>,
|
||||
}
|
||||
@ -45,11 +56,13 @@ pub struct WipCanonicalGoalEvaluation<'tcx> {
|
||||
impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
|
||||
pub fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
|
||||
let kind = match self.kind {
|
||||
Some(WipGoalEvaluationKind::Overflow) => inspect::GoalEvaluationKind::Overflow,
|
||||
Some(WipGoalEvaluationKind::CacheHit(hit)) => {
|
||||
inspect::GoalEvaluationKind::CacheHit(hit)
|
||||
Some(WipCanonicalGoalEvaluationKind::Overflow) => {
|
||||
inspect::CanonicalGoalEvaluationKind::Overflow
|
||||
}
|
||||
None => inspect::GoalEvaluationKind::Uncached {
|
||||
Some(WipCanonicalGoalEvaluationKind::CacheHit(hit)) => {
|
||||
inspect::CanonicalGoalEvaluationKind::CacheHit(hit)
|
||||
}
|
||||
None => inspect::CanonicalGoalEvaluationKind::Uncached {
|
||||
revisions: self
|
||||
.revisions
|
||||
.into_iter()
|
||||
@ -87,7 +100,7 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
|
||||
pub struct WipGoalEvaluationStep<'tcx> {
|
||||
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
||||
|
||||
pub evaluation: WipGoalCandidate<'tcx>,
|
||||
pub evaluation: WipProbe<'tcx>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
||||
@ -102,26 +115,37 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipGoalCandidate<'tcx> {
|
||||
pub added_goals_evaluations: Vec<WipAddedGoalsEvaluation<'tcx>>,
|
||||
pub candidates: Vec<WipGoalCandidate<'tcx>>,
|
||||
pub struct WipProbe<'tcx> {
|
||||
pub steps: Vec<WipProbeStep<'tcx>>,
|
||||
pub kind: Option<ProbeKind<'tcx>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipGoalCandidate<'tcx> {
|
||||
pub fn finalize(self) -> inspect::GoalCandidate<'tcx> {
|
||||
inspect::GoalCandidate {
|
||||
added_goals_evaluations: self
|
||||
.added_goals_evaluations
|
||||
.into_iter()
|
||||
.map(WipAddedGoalsEvaluation::finalize)
|
||||
.collect(),
|
||||
candidates: self.candidates.into_iter().map(WipGoalCandidate::finalize).collect(),
|
||||
impl<'tcx> WipProbe<'tcx> {
|
||||
pub fn finalize(self) -> inspect::Probe<'tcx> {
|
||||
inspect::Probe {
|
||||
steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
|
||||
kind: self.kind.unwrap(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub enum WipProbeStep<'tcx> {
|
||||
AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
|
||||
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
|
||||
NestedProbe(WipProbe<'tcx>),
|
||||
}
|
||||
|
||||
impl<'tcx> WipProbeStep<'tcx> {
|
||||
pub fn finalize(self) -> inspect::ProbeStep<'tcx> {
|
||||
match self {
|
||||
WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
|
||||
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
||||
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug)]
|
||||
pub enum DebugSolver<'tcx> {
|
||||
Root,
|
||||
@ -129,7 +153,7 @@ pub enum DebugSolver<'tcx> {
|
||||
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<'tcx>),
|
||||
AddedGoalsEvaluation(WipAddedGoalsEvaluation<'tcx>),
|
||||
GoalEvaluationStep(WipGoalEvaluationStep<'tcx>),
|
||||
GoalCandidate(WipGoalCandidate<'tcx>),
|
||||
Probe(WipProbe<'tcx>),
|
||||
}
|
||||
|
||||
impl<'tcx> From<WipGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
|
||||
@ -156,9 +180,9 @@ impl<'tcx> From<WipGoalEvaluationStep<'tcx>> for DebugSolver<'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> From<WipGoalCandidate<'tcx>> for DebugSolver<'tcx> {
|
||||
fn from(g: WipGoalCandidate<'tcx>) -> DebugSolver<'tcx> {
|
||||
DebugSolver::GoalCandidate(g)
|
||||
impl<'tcx> From<WipProbe<'tcx>> for DebugSolver<'tcx> {
|
||||
fn from(p: WipProbe<'tcx>) -> DebugSolver<'tcx> {
|
||||
DebugSolver::Probe(p)
|
||||
}
|
||||
}
|
||||
|
||||
@ -249,15 +273,20 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
self.state.is_none()
|
||||
}
|
||||
|
||||
pub fn new_goal_evaluation(
|
||||
pub(super) fn new_goal_evaluation(
|
||||
&mut self,
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
is_normalizes_to_hack: IsNormalizesToHack,
|
||||
kind: GoalEvaluationKind,
|
||||
) -> ProofTreeBuilder<'tcx> {
|
||||
self.nested(|| WipGoalEvaluation {
|
||||
uncanonicalized_goal: goal,
|
||||
kind: match kind {
|
||||
GoalEvaluationKind::Root => WipGoalEvaluationKind::Root,
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
|
||||
WipGoalEvaluationKind::Nested { is_normalizes_to_hack }
|
||||
}
|
||||
},
|
||||
evaluation: None,
|
||||
is_normalizes_to_hack,
|
||||
returned_goals: vec![],
|
||||
})
|
||||
}
|
||||
@ -286,7 +315,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn goal_evaluation_kind(&mut self, kind: WipGoalEvaluationKind) {
|
||||
pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match this {
|
||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||
@ -329,11 +358,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
) -> ProofTreeBuilder<'tcx> {
|
||||
self.nested(|| WipGoalEvaluationStep {
|
||||
instantiated_goal,
|
||||
evaluation: WipGoalCandidate {
|
||||
added_goals_evaluations: vec![],
|
||||
candidates: vec![],
|
||||
kind: None,
|
||||
},
|
||||
evaluation: WipProbe { steps: vec![], kind: None },
|
||||
})
|
||||
}
|
||||
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
|
||||
@ -350,18 +375,14 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn new_goal_candidate(&mut self) -> ProofTreeBuilder<'tcx> {
|
||||
self.nested(|| WipGoalCandidate {
|
||||
added_goals_evaluations: vec![],
|
||||
candidates: vec![],
|
||||
kind: None,
|
||||
})
|
||||
pub fn new_probe(&mut self) -> ProofTreeBuilder<'tcx> {
|
||||
self.nested(|| WipProbe { steps: vec![], kind: None })
|
||||
}
|
||||
|
||||
pub fn probe_kind(&mut self, probe_kind: ProbeKind<'tcx>) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match this {
|
||||
DebugSolver::GoalCandidate(this) => {
|
||||
DebugSolver::Probe(this) => {
|
||||
assert_eq!(this.kind.replace(probe_kind), None)
|
||||
}
|
||||
_ => unreachable!(),
|
||||
@ -369,17 +390,32 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn goal_candidate(&mut self, candidate: ProofTreeBuilder<'tcx>) {
|
||||
pub fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match (this, candidate.state.unwrap().tree) {
|
||||
match this {
|
||||
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||
evaluation: WipProbe { steps, .. },
|
||||
..
|
||||
})
|
||||
| DebugSolver::Probe(WipProbe { steps, .. }) => {
|
||||
steps.push(WipProbeStep::AddGoal(goal))
|
||||
}
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub fn finish_probe(&mut self, probe: ProofTreeBuilder<'tcx>) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match (this, probe.state.unwrap().tree) {
|
||||
(
|
||||
DebugSolver::GoalCandidate(WipGoalCandidate { candidates, .. })
|
||||
DebugSolver::Probe(WipProbe { steps, .. })
|
||||
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||
evaluation: WipGoalCandidate { candidates, .. },
|
||||
evaluation: WipProbe { steps, .. },
|
||||
..
|
||||
}),
|
||||
DebugSolver::GoalCandidate(candidate),
|
||||
) => candidates.push(candidate),
|
||||
DebugSolver::Probe(probe),
|
||||
) => steps.push(WipProbeStep::NestedProbe(probe)),
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
@ -416,14 +452,12 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
match (this, added_goals_evaluation.state.unwrap().tree) {
|
||||
(
|
||||
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||
evaluation: WipGoalCandidate { added_goals_evaluations, .. },
|
||||
evaluation: WipProbe { steps, .. },
|
||||
..
|
||||
})
|
||||
| DebugSolver::GoalCandidate(WipGoalCandidate {
|
||||
added_goals_evaluations, ..
|
||||
}),
|
||||
| DebugSolver::Probe(WipProbe { steps, .. }),
|
||||
DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
|
||||
) => added_goals_evaluations.push(added_goals_evaluation),
|
||||
) => steps.push(WipProbeStep::EvaluateGoals(added_goals_evaluation)),
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
@ -19,7 +19,8 @@ use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
|
||||
use rustc_infer::traits::query::NoSolution;
|
||||
use rustc_middle::infer::canonical::CanonicalVarInfos;
|
||||
use rustc_middle::traits::solve::{
|
||||
CanonicalResponse, Certainty, ExternalConstraintsData, Goal, QueryResult, Response,
|
||||
CanonicalResponse, Certainty, ExternalConstraintsData, Goal, IsNormalizesToHack, QueryResult,
|
||||
Response,
|
||||
};
|
||||
use rustc_middle::ty::{self, Ty, TyCtxt, UniverseIndex};
|
||||
use rustc_middle::ty::{
|
||||
@ -59,6 +60,12 @@ enum SolverMode {
|
||||
Coherence,
|
||||
}
|
||||
|
||||
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
|
||||
enum GoalEvaluationKind {
|
||||
Root,
|
||||
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||
}
|
||||
|
||||
trait CanonicalResponseExt {
|
||||
fn has_no_inference_or_external_constraints(&self) -> bool;
|
||||
|
||||
@ -228,6 +235,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
|
||||
#[instrument(level = "debug", skip(self))]
|
||||
fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
|
||||
self.inspect.add_goal(goal);
|
||||
self.nested_goals.goals.push(goal);
|
||||
}
|
||||
|
||||
|
@ -187,7 +187,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||
last.encountered_overflow = true;
|
||||
}
|
||||
|
||||
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::Overflow);
|
||||
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
|
||||
return Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
|
||||
};
|
||||
|
||||
@ -203,7 +203,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||
available_depth,
|
||||
)
|
||||
{
|
||||
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
|
||||
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CacheHit(
|
||||
CacheHit::Global,
|
||||
));
|
||||
self.on_cache_hit(reached_depth, encountered_overflow);
|
||||
@ -240,7 +240,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||
// Finally we can return either the provisional response for that goal if we have a
|
||||
// coinductive cycle or an ambiguous result if the cycle is inductive.
|
||||
Entry::Occupied(entry_index) => {
|
||||
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
|
||||
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CacheHit(
|
||||
CacheHit::Provisional,
|
||||
));
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user