order added_goals_evaluation
and nested_probes
This commit is contained in:
parent
be9d7e0b94
commit
a3f9530b30
3 changed files with 37 additions and 31 deletions
|
@ -60,8 +60,7 @@ pub struct GoalEvaluationStep<'tcx> {
|
||||||
/// of a goal.
|
/// of a goal.
|
||||||
#[derive(Eq, PartialEq)]
|
#[derive(Eq, PartialEq)]
|
||||||
pub struct Probe<'tcx> {
|
pub struct Probe<'tcx> {
|
||||||
pub added_goals_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
|
pub steps: Vec<ProbeStep<'tcx>>,
|
||||||
pub nested_probes: Vec<Probe<'tcx>>,
|
|
||||||
pub kind: ProbeKind<'tcx>,
|
pub kind: ProbeKind<'tcx>,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -71,6 +70,12 @@ impl Debug for Probe<'_> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Eq, PartialEq)]
|
||||||
|
pub enum ProbeStep<'tcx> {
|
||||||
|
EvaluateGoals(AddedGoalsEvaluation<'tcx>),
|
||||||
|
NestedProbe(Probe<'tcx>),
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Debug, PartialEq, Eq)]
|
#[derive(Debug, PartialEq, Eq)]
|
||||||
pub enum ProbeKind<'tcx> {
|
pub enum ProbeKind<'tcx> {
|
||||||
/// The root inference context while proving a goal.
|
/// The root inference context while proving a goal.
|
||||||
|
|
|
@ -118,11 +118,11 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||||
}?;
|
}?;
|
||||||
|
|
||||||
self.nested(|this| {
|
self.nested(|this| {
|
||||||
for probe in &probe.nested_probes {
|
for step in &probe.steps {
|
||||||
this.format_probe(probe)?;
|
match step {
|
||||||
|
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
|
||||||
|
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
|
||||||
}
|
}
|
||||||
for nested in &probe.added_goals_evaluations {
|
|
||||||
this.format_added_goals_evaluation(nested)?;
|
|
||||||
}
|
}
|
||||||
Ok(())
|
Ok(())
|
||||||
})
|
})
|
||||||
|
|
|
@ -103,25 +103,34 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(Eq, PartialEq, Debug)]
|
||||||
pub struct WipProbe<'tcx> {
|
pub struct WipProbe<'tcx> {
|
||||||
pub added_goals_evaluations: Vec<WipAddedGoalsEvaluation<'tcx>>,
|
pub steps: Vec<WipProbeStep<'tcx>>,
|
||||||
pub nested_probes: Vec<WipProbe<'tcx>>,
|
|
||||||
pub kind: Option<ProbeKind<'tcx>>,
|
pub kind: Option<ProbeKind<'tcx>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipProbe<'tcx> {
|
impl<'tcx> WipProbe<'tcx> {
|
||||||
pub fn finalize(self) -> inspect::Probe<'tcx> {
|
pub fn finalize(self) -> inspect::Probe<'tcx> {
|
||||||
inspect::Probe {
|
inspect::Probe {
|
||||||
added_goals_evaluations: self
|
steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
|
||||||
.added_goals_evaluations
|
|
||||||
.into_iter()
|
|
||||||
.map(WipAddedGoalsEvaluation::finalize)
|
|
||||||
.collect(),
|
|
||||||
nested_probes: self.nested_probes.into_iter().map(WipProbe::finalize).collect(),
|
|
||||||
kind: self.kind.unwrap(),
|
kind: self.kind.unwrap(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Eq, PartialEq, Debug)]
|
||||||
|
pub enum WipProbeStep<'tcx> {
|
||||||
|
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
|
||||||
|
NestedProbe(WipProbe<'tcx>),
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'tcx> WipProbeStep<'tcx> {
|
||||||
|
pub fn finalize(self) -> inspect::ProbeStep<'tcx> {
|
||||||
|
match self {
|
||||||
|
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
||||||
|
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Debug)]
|
#[derive(Debug)]
|
||||||
pub enum DebugSolver<'tcx> {
|
pub enum DebugSolver<'tcx> {
|
||||||
Root,
|
Root,
|
||||||
|
@ -329,11 +338,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<'tcx> {
|
||||||
self.nested(|| WipGoalEvaluationStep {
|
self.nested(|| WipGoalEvaluationStep {
|
||||||
instantiated_goal,
|
instantiated_goal,
|
||||||
evaluation: WipProbe {
|
evaluation: WipProbe { steps: vec![], kind: None },
|
||||||
added_goals_evaluations: vec![],
|
|
||||||
nested_probes: vec![],
|
|
||||||
kind: None,
|
|
||||||
},
|
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
|
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
|
||||||
|
@ -351,11 +356,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn new_probe(&mut self) -> ProofTreeBuilder<'tcx> {
|
pub fn new_probe(&mut self) -> ProofTreeBuilder<'tcx> {
|
||||||
self.nested(|| WipProbe {
|
self.nested(|| WipProbe { steps: vec![], kind: None })
|
||||||
added_goals_evaluations: vec![],
|
|
||||||
nested_probes: vec![],
|
|
||||||
kind: None,
|
|
||||||
})
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn probe_kind(&mut self, probe_kind: ProbeKind<'tcx>) {
|
pub fn probe_kind(&mut self, probe_kind: ProbeKind<'tcx>) {
|
||||||
|
@ -373,13 +374,13 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match (this, probe.state.unwrap().tree) {
|
match (this, probe.state.unwrap().tree) {
|
||||||
(
|
(
|
||||||
DebugSolver::Probe(WipProbe { nested_probes, .. })
|
DebugSolver::Probe(WipProbe { steps, .. })
|
||||||
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||||
evaluation: WipProbe { nested_probes, .. },
|
evaluation: WipProbe { steps, .. },
|
||||||
..
|
..
|
||||||
}),
|
}),
|
||||||
DebugSolver::Probe(probe),
|
DebugSolver::Probe(probe),
|
||||||
) => nested_probes.push(probe),
|
) => steps.push(WipProbeStep::NestedProbe(probe)),
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -416,12 +417,12 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
match (this, added_goals_evaluation.state.unwrap().tree) {
|
match (this, added_goals_evaluation.state.unwrap().tree) {
|
||||||
(
|
(
|
||||||
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||||
evaluation: WipProbe { added_goals_evaluations, .. },
|
evaluation: WipProbe { steps, .. },
|
||||||
..
|
..
|
||||||
})
|
})
|
||||||
| DebugSolver::Probe(WipProbe { added_goals_evaluations, .. }),
|
| DebugSolver::Probe(WipProbe { steps, .. }),
|
||||||
DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
|
DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
|
||||||
) => added_goals_evaluations.push(added_goals_evaluation),
|
) => steps.push(WipProbeStep::EvaluateGoals(added_goals_evaluation)),
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue