differentiate root and nested goals
This commit is contained in:
parent
1b141b6d73
commit
0cb800ec34
6 changed files with 76 additions and 35 deletions
|
@ -14,10 +14,16 @@ pub enum CacheHit {
|
||||||
Global,
|
Global,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Eq, PartialEq)]
|
||||||
|
pub enum GoalEvaluationKind {
|
||||||
|
Root,
|
||||||
|
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq)]
|
#[derive(Eq, PartialEq)]
|
||||||
pub struct GoalEvaluation<'tcx> {
|
pub struct GoalEvaluation<'tcx> {
|
||||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
pub is_normalizes_to_hack: IsNormalizesToHack,
|
pub kind: GoalEvaluationKind,
|
||||||
pub evaluation: CanonicalGoalEvaluation<'tcx>,
|
pub evaluation: CanonicalGoalEvaluation<'tcx>,
|
||||||
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||||
}
|
}
|
||||||
|
@ -25,12 +31,12 @@ pub struct GoalEvaluation<'tcx> {
|
||||||
#[derive(Eq, PartialEq)]
|
#[derive(Eq, PartialEq)]
|
||||||
pub struct CanonicalGoalEvaluation<'tcx> {
|
pub struct CanonicalGoalEvaluation<'tcx> {
|
||||||
pub goal: CanonicalInput<'tcx>,
|
pub goal: CanonicalInput<'tcx>,
|
||||||
pub kind: GoalEvaluationKind<'tcx>,
|
pub kind: CanonicalGoalEvaluationKind<'tcx>,
|
||||||
pub result: QueryResult<'tcx>,
|
pub result: QueryResult<'tcx>,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq)]
|
#[derive(Eq, PartialEq)]
|
||||||
pub enum GoalEvaluationKind<'tcx> {
|
pub enum CanonicalGoalEvaluationKind<'tcx> {
|
||||||
Overflow,
|
Overflow,
|
||||||
CacheHit(CacheHit),
|
CacheHit(CacheHit),
|
||||||
Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
|
Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
|
||||||
|
|
|
@ -40,9 +40,12 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
|
pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
|
||||||
let goal_text = match eval.is_normalizes_to_hack {
|
let goal_text = match eval.kind {
|
||||||
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
|
GoalEvaluationKind::Root => "ROOT GOAL",
|
||||||
IsNormalizesToHack::No => "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)?;
|
writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
|
||||||
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
|
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)?;
|
writeln!(self.f, "GOAL: {:?}", eval.goal)?;
|
||||||
|
|
||||||
match &eval.kind {
|
match &eval.kind {
|
||||||
GoalEvaluationKind::Overflow => {
|
CanonicalGoalEvaluationKind::Overflow => {
|
||||||
writeln!(self.f, "OVERFLOW: {:?}", eval.result)
|
writeln!(self.f, "OVERFLOW: {:?}", eval.result)
|
||||||
}
|
}
|
||||||
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
|
CanonicalGoalEvaluationKind::CacheHit(CacheHit::Global) => {
|
||||||
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
|
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
|
||||||
}
|
}
|
||||||
GoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
|
CanonicalGoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
|
||||||
writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
|
writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
|
||||||
}
|
}
|
||||||
GoalEvaluationKind::Uncached { revisions } => {
|
CanonicalGoalEvaluationKind::Uncached { revisions } => {
|
||||||
for (n, step) in revisions.iter().enumerate() {
|
for (n, step) in revisions.iter().enumerate() {
|
||||||
writeln!(self.f, "REVISION {n}")?;
|
writeln!(self.f, "REVISION {n}")?;
|
||||||
self.nested(|this| this.format_evaluation_step(step))?;
|
self.nested(|this| this.format_evaluation_step(step))?;
|
||||||
|
|
|
@ -28,8 +28,8 @@ use std::ops::ControlFlow;
|
||||||
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
|
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
|
||||||
|
|
||||||
use super::inspect::ProofTreeBuilder;
|
use super::inspect::ProofTreeBuilder;
|
||||||
use super::search_graph;
|
|
||||||
use super::SolverMode;
|
use super::SolverMode;
|
||||||
|
use super::{search_graph, GoalEvaluationKind};
|
||||||
use super::{search_graph::SearchGraph, Goal};
|
use super::{search_graph::SearchGraph, Goal};
|
||||||
pub use select::InferCtxtSelectExt;
|
pub use select::InferCtxtSelectExt;
|
||||||
|
|
||||||
|
@ -164,7 +164,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
|
||||||
Option<inspect::GoalEvaluation<'tcx>>,
|
Option<inspect::GoalEvaluation<'tcx>>,
|
||||||
) {
|
) {
|
||||||
EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
|
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.
|
/// been constrained and the certainty of the result.
|
||||||
fn evaluate_goal(
|
fn evaluate_goal(
|
||||||
&mut self,
|
&mut self,
|
||||||
is_normalizes_to_hack: IsNormalizesToHack,
|
goal_evaluation_kind: GoalEvaluationKind,
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
|
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
|
||||||
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
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 encountered_overflow = self.search_graph.encountered_overflow();
|
||||||
let canonical_response = EvalCtxt::evaluate_canonical_goal(
|
let canonical_response = EvalCtxt::evaluate_canonical_goal(
|
||||||
self.tcx(),
|
self.tcx(),
|
||||||
|
@ -389,7 +389,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||||
// solver cycle.
|
// solver cycle.
|
||||||
if cfg!(debug_assertions)
|
if cfg!(debug_assertions)
|
||||||
&& has_changed
|
&& 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()
|
&& !self.search_graph.in_cycle()
|
||||||
{
|
{
|
||||||
// The nested evaluation has to happen with the original state
|
// The nested evaluation has to happen with the original state
|
||||||
|
@ -561,8 +564,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
|
|
||||||
let (_, certainty, instantiate_goals) =
|
let (_, certainty, instantiate_goals) = self.evaluate_goal(
|
||||||
self.evaluate_goal(IsNormalizesToHack::Yes, unconstrained_goal)?;
|
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
|
||||||
|
unconstrained_goal,
|
||||||
|
)?;
|
||||||
self.add_goals(instantiate_goals);
|
self.add_goals(instantiate_goals);
|
||||||
|
|
||||||
// Finally, equate the goal's RHS with the unconstrained var.
|
// 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(..) {
|
for goal in goals.goals.drain(..) {
|
||||||
let (has_changed, certainty, instantiate_goals) =
|
let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
|
||||||
self.evaluate_goal(IsNormalizesToHack::No, goal)?;
|
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
|
||||||
|
goal,
|
||||||
|
)?;
|
||||||
self.add_goals(instantiate_goals);
|
self.add_goals(instantiate_goals);
|
||||||
if has_changed {
|
if has_changed {
|
||||||
unchanged_certainty = None;
|
unchanged_certainty = None;
|
||||||
|
|
|
@ -7,13 +7,13 @@ use rustc_middle::ty::{self, TyCtxt};
|
||||||
use rustc_session::config::DumpSolverProofTree;
|
use rustc_session::config::DumpSolverProofTree;
|
||||||
|
|
||||||
use super::eval_ctxt::UseGlobalCache;
|
use super::eval_ctxt::UseGlobalCache;
|
||||||
use super::GenerateProofTree;
|
use super::{GenerateProofTree, GoalEvaluationKind};
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(Eq, PartialEq, Debug)]
|
||||||
pub struct WipGoalEvaluation<'tcx> {
|
pub struct WipGoalEvaluation<'tcx> {
|
||||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
|
pub kind: WipGoalEvaluationKind,
|
||||||
pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
|
pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
|
||||||
pub is_normalizes_to_hack: IsNormalizesToHack,
|
|
||||||
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -21,8 +21,13 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
|
||||||
pub fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
|
pub fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
|
||||||
inspect::GoalEvaluation {
|
inspect::GoalEvaluation {
|
||||||
uncanonicalized_goal: self.uncanonicalized_goal,
|
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(),
|
evaluation: self.evaluation.unwrap().finalize(),
|
||||||
is_normalizes_to_hack: self.is_normalizes_to_hack,
|
|
||||||
returned_goals: self.returned_goals,
|
returned_goals: self.returned_goals,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -30,6 +35,12 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(Eq, PartialEq, Debug)]
|
||||||
pub enum WipGoalEvaluationKind {
|
pub enum WipGoalEvaluationKind {
|
||||||
|
Root,
|
||||||
|
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Eq, PartialEq, Debug)]
|
||||||
|
pub enum WipCanonicalGoalEvaluationKind {
|
||||||
Overflow,
|
Overflow,
|
||||||
CacheHit(CacheHit),
|
CacheHit(CacheHit),
|
||||||
}
|
}
|
||||||
|
@ -37,7 +48,7 @@ pub enum WipGoalEvaluationKind {
|
||||||
#[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 kind: Option<WipGoalEvaluationKind>,
|
pub kind: Option<WipCanonicalGoalEvaluationKind>,
|
||||||
pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
|
pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
|
||||||
pub result: Option<QueryResult<'tcx>>,
|
pub result: Option<QueryResult<'tcx>>,
|
||||||
}
|
}
|
||||||
|
@ -45,11 +56,13 @@ pub struct WipCanonicalGoalEvaluation<'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.kind {
|
let kind = match self.kind {
|
||||||
Some(WipGoalEvaluationKind::Overflow) => inspect::GoalEvaluationKind::Overflow,
|
Some(WipCanonicalGoalEvaluationKind::Overflow) => {
|
||||||
Some(WipGoalEvaluationKind::CacheHit(hit)) => {
|
inspect::CanonicalGoalEvaluationKind::Overflow
|
||||||
inspect::GoalEvaluationKind::CacheHit(hit)
|
|
||||||
}
|
}
|
||||||
None => inspect::GoalEvaluationKind::Uncached {
|
Some(WipCanonicalGoalEvaluationKind::CacheHit(hit)) => {
|
||||||
|
inspect::CanonicalGoalEvaluationKind::CacheHit(hit)
|
||||||
|
}
|
||||||
|
None => inspect::CanonicalGoalEvaluationKind::Uncached {
|
||||||
revisions: self
|
revisions: self
|
||||||
.revisions
|
.revisions
|
||||||
.into_iter()
|
.into_iter()
|
||||||
|
@ -260,15 +273,20 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||||
self.state.is_none()
|
self.state.is_none()
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn new_goal_evaluation(
|
pub(super) fn new_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
is_normalizes_to_hack: IsNormalizesToHack,
|
kind: GoalEvaluationKind,
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<'tcx> {
|
||||||
self.nested(|| WipGoalEvaluation {
|
self.nested(|| WipGoalEvaluation {
|
||||||
uncanonicalized_goal: goal,
|
uncanonicalized_goal: goal,
|
||||||
|
kind: match kind {
|
||||||
|
GoalEvaluationKind::Root => WipGoalEvaluationKind::Root,
|
||||||
|
GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
|
||||||
|
WipGoalEvaluationKind::Nested { is_normalizes_to_hack }
|
||||||
|
}
|
||||||
|
},
|
||||||
evaluation: None,
|
evaluation: None,
|
||||||
is_normalizes_to_hack,
|
|
||||||
returned_goals: vec![],
|
returned_goals: vec![],
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
@ -297,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() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||||
|
|
|
@ -19,7 +19,8 @@ use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
|
||||||
use rustc_infer::traits::query::NoSolution;
|
use rustc_infer::traits::query::NoSolution;
|
||||||
use rustc_middle::infer::canonical::CanonicalVarInfos;
|
use rustc_middle::infer::canonical::CanonicalVarInfos;
|
||||||
use rustc_middle::traits::solve::{
|
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::{self, Ty, TyCtxt, UniverseIndex};
|
||||||
use rustc_middle::ty::{
|
use rustc_middle::ty::{
|
||||||
|
@ -59,6 +60,12 @@ enum SolverMode {
|
||||||
Coherence,
|
Coherence,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
|
||||||
|
enum GoalEvaluationKind {
|
||||||
|
Root,
|
||||||
|
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||||
|
}
|
||||||
|
|
||||||
trait CanonicalResponseExt {
|
trait CanonicalResponseExt {
|
||||||
fn has_no_inference_or_external_constraints(&self) -> bool;
|
fn has_no_inference_or_external_constraints(&self) -> bool;
|
||||||
|
|
||||||
|
|
|
@ -187,7 +187,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||||
last.encountered_overflow = true;
|
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);
|
return Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -203,7 +203,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
||||||
available_depth,
|
available_depth,
|
||||||
)
|
)
|
||||||
{
|
{
|
||||||
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
|
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CacheHit(
|
||||||
CacheHit::Global,
|
CacheHit::Global,
|
||||||
));
|
));
|
||||||
self.on_cache_hit(reached_depth, encountered_overflow);
|
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
|
// 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.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
|
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CacheHit(
|
||||||
CacheHit::Provisional,
|
CacheHit::Provisional,
|
||||||
));
|
));
|
||||||
|
|
||||||
|
|
Loading…
Add table
Reference in a new issue