inspect: explicitly store added goals

This commit is contained in:
lcnr 2023-09-14 10:41:36 +02:00
parent a3f9530b30
commit 1b141b6d73
5 changed files with 21 additions and 1 deletions

View File

@ -72,6 +72,7 @@ impl Debug for Probe<'_> {
#[derive(Eq, PartialEq)]
pub enum ProbeStep<'tcx> {
AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
EvaluateGoals(AddedGoalsEvaluation<'tcx>),
NestedProbe(Probe<'tcx>),
}

View File

@ -120,6 +120,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
self.nested(|this| {
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)?,
}

View File

@ -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)]

View File

@ -118,6 +118,7 @@ impl<'tcx> WipProbe<'tcx> {
#[derive(Eq, PartialEq, Debug)]
pub enum WipProbeStep<'tcx> {
AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
NestedProbe(WipProbe<'tcx>),
}
@ -125,6 +126,7 @@ pub enum WipProbeStep<'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()),
}
@ -370,6 +372,21 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
}
}
pub fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
if let Some(this) = self.as_mut() {
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) {

View File

@ -228,6 +228,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);
}