dedup GoalEvaluationStep
and GoalCandidate
also handle 2 panics when dumping proof trees for the whole test suite - need to actually tell the proof tree builder about overflow - need to handle a recursion_limit of 0 :<
This commit is contained in:
parent
8225a2e9ec
commit
eac55eec9e
5 changed files with 75 additions and 56 deletions
|
@ -31,6 +31,7 @@ pub struct CanonicalGoalEvaluation<'tcx> {
|
||||||
|
|
||||||
#[derive(Eq, PartialEq)]
|
#[derive(Eq, PartialEq)]
|
||||||
pub enum GoalEvaluationKind<'tcx> {
|
pub enum GoalEvaluationKind<'tcx> {
|
||||||
|
Overflow,
|
||||||
CacheHit(CacheHit),
|
CacheHit(CacheHit),
|
||||||
Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
|
Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
|
||||||
}
|
}
|
||||||
|
@ -50,10 +51,8 @@ pub struct AddedGoalsEvaluation<'tcx> {
|
||||||
pub struct GoalEvaluationStep<'tcx> {
|
pub struct GoalEvaluationStep<'tcx> {
|
||||||
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
||||||
|
|
||||||
pub added_goals_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
|
/// The actual evaluation of the goal, always `ProbeKind::Root`.
|
||||||
pub candidates: Vec<GoalCandidate<'tcx>>,
|
pub evaluation: GoalCandidate<'tcx>,
|
||||||
|
|
||||||
pub result: QueryResult<'tcx>,
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq)]
|
#[derive(Eq, PartialEq)]
|
||||||
|
@ -63,8 +62,16 @@ pub struct GoalCandidate<'tcx> {
|
||||||
pub kind: ProbeKind<'tcx>,
|
pub kind: ProbeKind<'tcx>,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl Debug for GoalCandidate<'_> {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
ProofTreeFormatter::new(f).format_candidate(self)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Debug, PartialEq, Eq)]
|
#[derive(Debug, PartialEq, Eq)]
|
||||||
pub enum ProbeKind<'tcx> {
|
pub enum ProbeKind<'tcx> {
|
||||||
|
/// The root inference context while proving a goal.
|
||||||
|
Root { result: QueryResult<'tcx> },
|
||||||
/// Probe entered when normalizing the self ty during candidate assembly
|
/// Probe entered when normalizing the self ty during candidate assembly
|
||||||
NormalizedSelfTyAssembly,
|
NormalizedSelfTyAssembly,
|
||||||
/// Some candidate to prove the current goal.
|
/// Some candidate to prove the current goal.
|
||||||
|
|
|
@ -68,6 +68,9 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||||
writeln!(self.f, "GOAL: {:?}", eval.goal)?;
|
writeln!(self.f, "GOAL: {:?}", eval.goal)?;
|
||||||
|
|
||||||
match &eval.kind {
|
match &eval.kind {
|
||||||
|
GoalEvaluationKind::Overflow => {
|
||||||
|
writeln!(self.f, "OVERFLOW: {:?}", eval.result)
|
||||||
|
}
|
||||||
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
|
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
|
||||||
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
|
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
|
||||||
}
|
}
|
||||||
|
@ -76,7 +79,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||||
}
|
}
|
||||||
GoalEvaluationKind::Uncached { revisions } => {
|
GoalEvaluationKind::Uncached { revisions } => {
|
||||||
for (n, step) in revisions.iter().enumerate() {
|
for (n, step) in revisions.iter().enumerate() {
|
||||||
writeln!(self.f, "REVISION {n}: {:?}", step.result)?;
|
writeln!(self.f, "REVISION {n}")?;
|
||||||
self.nested(|this| this.format_evaluation_step(step))?;
|
self.nested(|this| this.format_evaluation_step(step))?;
|
||||||
}
|
}
|
||||||
writeln!(self.f, "RESULT: {:?}", eval.result)
|
writeln!(self.f, "RESULT: {:?}", eval.result)
|
||||||
|
@ -89,19 +92,14 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||||
evaluation_step: &GoalEvaluationStep<'_>,
|
evaluation_step: &GoalEvaluationStep<'_>,
|
||||||
) -> std::fmt::Result {
|
) -> std::fmt::Result {
|
||||||
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
|
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
|
||||||
|
self.format_candidate(&evaluation_step.evaluation)
|
||||||
for candidate in &evaluation_step.candidates {
|
|
||||||
self.nested(|this| this.format_candidate(candidate))?;
|
|
||||||
}
|
|
||||||
for nested in &evaluation_step.added_goals_evaluations {
|
|
||||||
self.nested(|this| this.format_added_goals_evaluation(nested))?;
|
|
||||||
}
|
|
||||||
|
|
||||||
Ok(())
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
|
pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
|
||||||
match &candidate.kind {
|
match &candidate.kind {
|
||||||
|
ProbeKind::Root { result } => {
|
||||||
|
writeln!(self.f, "ROOT RESULT: {result:?}")
|
||||||
|
}
|
||||||
ProbeKind::NormalizedSelfTyAssembly => {
|
ProbeKind::NormalizedSelfTyAssembly => {
|
||||||
writeln!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
|
writeln!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
|
||||||
}
|
}
|
||||||
|
|
|
@ -28,28 +28,34 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Eq, PartialEq, Debug)]
|
||||||
|
pub enum WipGoalEvaluationKind {
|
||||||
|
Overflow,
|
||||||
|
CacheHit(CacheHit),
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(Eq, PartialEq, Debug)]
|
||||||
pub struct WipCanonicalGoalEvaluation<'tcx> {
|
pub struct WipCanonicalGoalEvaluation<'tcx> {
|
||||||
pub goal: CanonicalInput<'tcx>,
|
pub goal: CanonicalInput<'tcx>,
|
||||||
pub cache_hit: Option<CacheHit>,
|
pub kind: Option<WipGoalEvaluationKind>,
|
||||||
pub evaluation_steps: Vec<WipGoalEvaluationStep<'tcx>>,
|
pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
|
||||||
pub result: Option<QueryResult<'tcx>>,
|
pub result: Option<QueryResult<'tcx>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
|
impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
|
||||||
pub fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
|
pub fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
|
||||||
let kind = match self.cache_hit {
|
let kind = match self.kind {
|
||||||
Some(hit) => inspect::GoalEvaluationKind::CacheHit(hit),
|
Some(WipGoalEvaluationKind::Overflow) => inspect::GoalEvaluationKind::Overflow,
|
||||||
None => {
|
Some(WipGoalEvaluationKind::CacheHit(hit)) => {
|
||||||
assert!(!self.evaluation_steps.is_empty());
|
inspect::GoalEvaluationKind::CacheHit(hit)
|
||||||
inspect::GoalEvaluationKind::Uncached {
|
}
|
||||||
|
None => inspect::GoalEvaluationKind::Uncached {
|
||||||
revisions: self
|
revisions: self
|
||||||
.evaluation_steps
|
.revisions
|
||||||
.into_iter()
|
.into_iter()
|
||||||
.map(WipGoalEvaluationStep::finalize)
|
.map(WipGoalEvaluationStep::finalize)
|
||||||
.collect(),
|
.collect(),
|
||||||
}
|
},
|
||||||
}
|
|
||||||
};
|
};
|
||||||
|
|
||||||
inspect::CanonicalGoalEvaluation { goal: self.goal, kind, result: self.result.unwrap() }
|
inspect::CanonicalGoalEvaluation { goal: self.goal, kind, result: self.result.unwrap() }
|
||||||
|
@ -81,24 +87,17 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
|
||||||
pub struct WipGoalEvaluationStep<'tcx> {
|
pub struct WipGoalEvaluationStep<'tcx> {
|
||||||
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
||||||
|
|
||||||
pub added_goals_evaluations: Vec<WipAddedGoalsEvaluation<'tcx>>,
|
pub evaluation: WipGoalCandidate<'tcx>,
|
||||||
pub candidates: Vec<WipGoalCandidate<'tcx>>,
|
|
||||||
|
|
||||||
pub result: Option<QueryResult<'tcx>>,
|
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
||||||
pub fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
|
pub fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
|
||||||
inspect::GoalEvaluationStep {
|
let evaluation = self.evaluation.finalize();
|
||||||
instantiated_goal: self.instantiated_goal,
|
match evaluation.kind {
|
||||||
added_goals_evaluations: self
|
ProbeKind::Root { .. } => (),
|
||||||
.added_goals_evaluations
|
_ => unreachable!("unexpected root evaluation: {evaluation:?}"),
|
||||||
.into_iter()
|
|
||||||
.map(WipAddedGoalsEvaluation::finalize)
|
|
||||||
.collect(),
|
|
||||||
candidates: self.candidates.into_iter().map(WipGoalCandidate::finalize).collect(),
|
|
||||||
result: self.result.unwrap(),
|
|
||||||
}
|
}
|
||||||
|
inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -269,8 +268,8 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<'tcx> {
|
||||||
self.nested(|| WipCanonicalGoalEvaluation {
|
self.nested(|| WipCanonicalGoalEvaluation {
|
||||||
goal,
|
goal,
|
||||||
cache_hit: None,
|
kind: None,
|
||||||
evaluation_steps: vec![],
|
revisions: vec![],
|
||||||
result: None,
|
result: None,
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
@ -287,11 +286,11 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn cache_hit(&mut self, cache_hit: CacheHit) {
|
pub fn goal_evaluation_kind(&mut self, kind: WipGoalEvaluationKind) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||||
assert_eq!(canonical_goal_evaluation.cache_hit.replace(cache_hit), None);
|
assert_eq!(canonical_goal_evaluation.kind.replace(kind), None);
|
||||||
}
|
}
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
};
|
};
|
||||||
|
@ -330,9 +329,11 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<'tcx> {
|
||||||
self.nested(|| WipGoalEvaluationStep {
|
self.nested(|| WipGoalEvaluationStep {
|
||||||
instantiated_goal,
|
instantiated_goal,
|
||||||
|
evaluation: WipGoalCandidate {
|
||||||
added_goals_evaluations: vec![],
|
added_goals_evaluations: vec![],
|
||||||
candidates: vec![],
|
candidates: vec![],
|
||||||
result: None,
|
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>) {
|
||||||
|
@ -342,7 +343,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
|
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
|
||||||
DebugSolver::GoalEvaluationStep(goal_evaluation_step),
|
DebugSolver::GoalEvaluationStep(goal_evaluation_step),
|
||||||
) => {
|
) => {
|
||||||
canonical_goal_evaluations.evaluation_steps.push(goal_evaluation_step);
|
canonical_goal_evaluations.revisions.push(goal_evaluation_step);
|
||||||
}
|
}
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
}
|
}
|
||||||
|
@ -373,7 +374,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
match (this, candidate.state.unwrap().tree) {
|
match (this, candidate.state.unwrap().tree) {
|
||||||
(
|
(
|
||||||
DebugSolver::GoalCandidate(WipGoalCandidate { candidates, .. })
|
DebugSolver::GoalCandidate(WipGoalCandidate { candidates, .. })
|
||||||
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep { candidates, .. }),
|
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||||
|
evaluation: WipGoalCandidate { candidates, .. },
|
||||||
|
..
|
||||||
|
}),
|
||||||
DebugSolver::GoalCandidate(candidate),
|
DebugSolver::GoalCandidate(candidate),
|
||||||
) => candidates.push(candidate),
|
) => candidates.push(candidate),
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
|
@ -412,7 +416,7 @@ 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 {
|
||||||
added_goals_evaluations,
|
evaluation: WipGoalCandidate { added_goals_evaluations, .. },
|
||||||
..
|
..
|
||||||
})
|
})
|
||||||
| DebugSolver::GoalCandidate(WipGoalCandidate {
|
| DebugSolver::GoalCandidate(WipGoalCandidate {
|
||||||
|
@ -432,7 +436,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
assert_eq!(canonical_goal_evaluation.result.replace(result), None);
|
assert_eq!(canonical_goal_evaluation.result.replace(result), None);
|
||||||
}
|
}
|
||||||
DebugSolver::GoalEvaluationStep(evaluation_step) => {
|
DebugSolver::GoalEvaluationStep(evaluation_step) => {
|
||||||
assert_eq!(evaluation_step.result.replace(result), None);
|
assert_eq!(
|
||||||
|
evaluation_step.evaluation.kind.replace(ProbeKind::Root { result }),
|
||||||
|
None
|
||||||
|
);
|
||||||
}
|
}
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
}
|
}
|
||||||
|
|
|
@ -233,9 +233,9 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||||
|
|
||||||
#[instrument(level = "debug", skip(self, goals))]
|
#[instrument(level = "debug", skip(self, goals))]
|
||||||
fn add_goals(&mut self, goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>) {
|
fn add_goals(&mut self, goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>) {
|
||||||
let current_len = self.nested_goals.goals.len();
|
for goal in goals {
|
||||||
self.nested_goals.goals.extend(goals);
|
self.add_goal(goal);
|
||||||
debug!("added_goals={:?}", &self.nested_goals.goals[current_len..]);
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Try to merge multiple possible ways to prove a goal, if that is not possible returns `None`.
|
/// Try to merge multiple possible ways to prove a goal, if that is not possible returns `None`.
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
mod cache;
|
mod cache;
|
||||||
|
|
||||||
use self::cache::ProvisionalEntry;
|
use self::cache::ProvisionalEntry;
|
||||||
|
use super::inspect;
|
||||||
use super::inspect::ProofTreeBuilder;
|
use super::inspect::ProofTreeBuilder;
|
||||||
use super::SolverMode;
|
use super::SolverMode;
|
||||||
use cache::ProvisionalCache;
|
use cache::ProvisionalCache;
|
||||||
|
@ -185,6 +186,8 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||||
if let Some(last) = self.stack.raw.last_mut() {
|
if let Some(last) = self.stack.raw.last_mut() {
|
||||||
last.encountered_overflow = true;
|
last.encountered_overflow = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::Overflow);
|
||||||
return Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
|
return Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -200,7 +203,9 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||||
available_depth,
|
available_depth,
|
||||||
)
|
)
|
||||||
{
|
{
|
||||||
inspect.cache_hit(CacheHit::Global);
|
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
|
||||||
|
CacheHit::Global,
|
||||||
|
));
|
||||||
self.on_cache_hit(reached_depth, encountered_overflow);
|
self.on_cache_hit(reached_depth, encountered_overflow);
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
@ -235,7 +240,9 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||||
// Finally we can return either the provisional response for that goal if we have a
|
// 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.
|
// coinductive cycle or an ambiguous result if the cycle is inductive.
|
||||||
Entry::Occupied(entry_index) => {
|
Entry::Occupied(entry_index) => {
|
||||||
inspect.cache_hit(CacheHit::Provisional);
|
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
|
||||||
|
CacheHit::Provisional,
|
||||||
|
));
|
||||||
|
|
||||||
let entry_index = *entry_index.get();
|
let entry_index = *entry_index.get();
|
||||||
let stack_depth = cache.depth(entry_index);
|
let stack_depth = cache.depth(entry_index);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue