normalizes-to change from '1' to '0 to inf' steps

This commit is contained in:
lcnr
2024-04-02 15:12:20 +02:00
parent d99c775feb
commit 92b280ce81
12 changed files with 148 additions and 296 deletions

View File

@@ -130,17 +130,14 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
self.candidates_recur(candidates, nested_goals, probe);
nested_goals.truncate(num_goals);
}
inspect::ProbeStep::EvaluateGoals(_)
| inspect::ProbeStep::CommitIfOkStart
| inspect::ProbeStep::CommitIfOkSuccess => (),
inspect::ProbeStep::EvaluateGoals(_) => (),
}
}
match probe.kind {
inspect::ProbeKind::NormalizedSelfTyAssembly
| inspect::ProbeKind::UnsizeAssembly
| inspect::ProbeKind::UpcastProjectionCompatibility
| inspect::ProbeKind::CommitIfOk => (),
| inspect::ProbeKind::UpcastProjectionCompatibility => (),
// We add a candidate for the root evaluation if there
// is only one way to prove a given goal, e.g. for `WellFormed`.
//
@@ -157,7 +154,8 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
});
}
}
inspect::ProbeKind::MiscCandidate { name: _, result }
inspect::ProbeKind::TryNormalizeNonRigid { result }
| inspect::ProbeKind::MiscCandidate { name: _, result }
| inspect::ProbeKind::TraitCandidate { source: _, result } => {
candidates.push(InspectCandidate {
goal: self,

View File

@@ -220,8 +220,6 @@ enum WipProbeStep<'tcx> {
AddGoal(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
NestedProbe(WipProbe<'tcx>),
CommitIfOkStart,
CommitIfOkSuccess,
}
impl<'tcx> WipProbeStep<'tcx> {
@@ -230,8 +228,6 @@ impl<'tcx> WipProbeStep<'tcx> {
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::CommitIfOkStart => inspect::ProbeStep::CommitIfOkStart,
WipProbeStep::CommitIfOkSuccess => inspect::ProbeStep::CommitIfOkSuccess,
}
}
}
@@ -467,29 +463,6 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
}
}
/// Used by `EvalCtxt::commit_if_ok` to flatten the work done inside
/// of the probe into the parent.
pub fn integrate_snapshot(&mut self, probe: ProofTreeBuilder<'tcx>) {
if let Some(this) = self.as_mut() {
match (this, *probe.state.unwrap()) {
(
DebugSolver::Probe(WipProbe { steps, .. })
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
evaluation: WipProbe { steps, .. },
..
}),
DebugSolver::Probe(probe),
) => {
steps.push(WipProbeStep::CommitIfOkStart);
assert_eq!(probe.kind, None);
steps.extend(probe.steps);
steps.push(WipProbeStep::CommitIfOkSuccess);
}
_ => unreachable!(),
}
}
}
pub fn new_evaluate_added_goals(&mut self) -> ProofTreeBuilder<'tcx> {
self.nested(|| WipAddedGoalsEvaluation { evaluations: vec![], result: None })
}