Rollup merge of #124444 - compiler-errors:eval, r=lcnr
Record certainty of `evaluate_added_goals_and_make_canonical_response` call in candidate Naming subject to bikeshedding, but I will need this when moving `select` to a proof tree visitor. r? lcnr
This commit is contained in:
commit
a7771385e5
@ -122,6 +122,12 @@ pub enum ProbeStep<'tcx> {
|
|||||||
/// used whenever there are multiple candidates to prove the
|
/// used whenever there are multiple candidates to prove the
|
||||||
/// current goalby .
|
/// current goalby .
|
||||||
NestedProbe(Probe<'tcx>),
|
NestedProbe(Probe<'tcx>),
|
||||||
|
/// A call to `EvalCtxt::evaluate_added_goals_make_canonical_response` with
|
||||||
|
/// `Certainty` was made. This is the certainty passed in, so it's not unified
|
||||||
|
/// with the certainty of the `try_evaluate_added_goals` that is done within;
|
||||||
|
/// if it's `Certainty::Yes`, then we can trust that the candidate is "finished"
|
||||||
|
/// and we didn't force ambiguity for some reason.
|
||||||
|
MakeCanonicalResponse { shallow_certainty: Certainty },
|
||||||
}
|
}
|
||||||
|
|
||||||
/// What kind of probe we're in. In case the probe represents a candidate, or
|
/// What kind of probe we're in. In case the probe represents a candidate, or
|
||||||
|
@ -132,6 +132,9 @@ pub(super) fn format_probe(&mut self, probe: &Probe<'_>) -> std::fmt::Result {
|
|||||||
}
|
}
|
||||||
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
|
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
|
||||||
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
|
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
|
||||||
|
ProbeStep::MakeCanonicalResponse { shallow_certainty } => {
|
||||||
|
writeln!(this.f, "EVALUATE GOALS AND MAKE RESPONSE: {shallow_certainty:?}")?
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
Ok(())
|
Ok(())
|
||||||
|
@ -98,6 +98,8 @@ pub(in crate::solve) fn evaluate_added_goals_and_make_canonical_response(
|
|||||||
previous call to `try_evaluate_added_goals!`"
|
previous call to `try_evaluate_added_goals!`"
|
||||||
);
|
);
|
||||||
|
|
||||||
|
self.inspect.make_canonical_response(certainty);
|
||||||
|
|
||||||
// When normalizing, we've replaced the expected term with an unconstrained
|
// When normalizing, we've replaced the expected term with an unconstrained
|
||||||
// inference variable. This means that we dropped information which could
|
// inference variable. This means that we dropped information which could
|
||||||
// have been important. We handle this by instead returning the nested goals
|
// have been important. We handle this by instead returning the nested goals
|
||||||
|
@ -45,6 +45,7 @@ pub struct InspectCandidate<'a, 'tcx> {
|
|||||||
nested_goals: Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
|
nested_goals: Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
|
||||||
final_state: inspect::CanonicalState<'tcx, ()>,
|
final_state: inspect::CanonicalState<'tcx, ()>,
|
||||||
result: QueryResult<'tcx>,
|
result: QueryResult<'tcx>,
|
||||||
|
candidate_certainty: Option<Certainty>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
|
impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
|
||||||
@ -56,6 +57,19 @@ pub fn result(&self) -> Result<Certainty, NoSolution> {
|
|||||||
self.result.map(|c| c.value.certainty)
|
self.result.map(|c| c.value.certainty)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Certainty passed into `evaluate_added_goals_and_make_canonical_response`.
|
||||||
|
///
|
||||||
|
/// If this certainty is `Some(Yes)`, then we must be confident that the candidate
|
||||||
|
/// must hold iff it's nested goals hold. This is not true if the certainty is
|
||||||
|
/// `Some(Maybe)`, which suggests we forced ambiguity instead, or if it is `None`,
|
||||||
|
/// which suggests we may have not assembled any candidates at all.
|
||||||
|
///
|
||||||
|
/// This is *not* the certainty of the candidate's nested evaluation, which can be
|
||||||
|
/// accessed with [`Self::result`] instead.
|
||||||
|
pub fn candidate_certainty(&self) -> Option<Certainty> {
|
||||||
|
self.candidate_certainty
|
||||||
|
}
|
||||||
|
|
||||||
/// Visit all nested goals of this candidate without rolling
|
/// Visit all nested goals of this candidate without rolling
|
||||||
/// back their inference constraints. This function modifies
|
/// back their inference constraints. This function modifies
|
||||||
/// the state of the `infcx`.
|
/// the state of the `infcx`.
|
||||||
@ -160,7 +174,9 @@ fn candidates_recur(
|
|||||||
nested_goals: &mut Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
|
nested_goals: &mut Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
|
||||||
probe: &inspect::Probe<'tcx>,
|
probe: &inspect::Probe<'tcx>,
|
||||||
) {
|
) {
|
||||||
|
let mut candidate_certainty = None;
|
||||||
let num_candidates = candidates.len();
|
let num_candidates = candidates.len();
|
||||||
|
|
||||||
for step in &probe.steps {
|
for step in &probe.steps {
|
||||||
match step {
|
match step {
|
||||||
&inspect::ProbeStep::AddGoal(_source, goal) => nested_goals.push(goal),
|
&inspect::ProbeStep::AddGoal(_source, goal) => nested_goals.push(goal),
|
||||||
@ -172,6 +188,9 @@ fn candidates_recur(
|
|||||||
self.candidates_recur(candidates, nested_goals, probe);
|
self.candidates_recur(candidates, nested_goals, probe);
|
||||||
nested_goals.truncate(num_goals);
|
nested_goals.truncate(num_goals);
|
||||||
}
|
}
|
||||||
|
inspect::ProbeStep::MakeCanonicalResponse { shallow_certainty } => {
|
||||||
|
assert_eq!(candidate_certainty.replace(*shallow_certainty), None);
|
||||||
|
}
|
||||||
inspect::ProbeStep::EvaluateGoals(_) => (),
|
inspect::ProbeStep::EvaluateGoals(_) => (),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -195,6 +214,7 @@ fn candidates_recur(
|
|||||||
nested_goals: nested_goals.clone(),
|
nested_goals: nested_goals.clone(),
|
||||||
final_state: probe.final_state,
|
final_state: probe.final_state,
|
||||||
result,
|
result,
|
||||||
|
candidate_certainty,
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -206,6 +226,7 @@ fn candidates_recur(
|
|||||||
nested_goals: nested_goals.clone(),
|
nested_goals: nested_goals.clone(),
|
||||||
final_state: probe.final_state,
|
final_state: probe.final_state,
|
||||||
result,
|
result,
|
||||||
|
candidate_certainty,
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -241,6 +241,7 @@ enum WipProbeStep<'tcx> {
|
|||||||
AddGoal(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
|
AddGoal(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
|
||||||
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
|
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
|
||||||
NestedProbe(WipProbe<'tcx>),
|
NestedProbe(WipProbe<'tcx>),
|
||||||
|
MakeCanonicalResponse { shallow_certainty: Certainty },
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipProbeStep<'tcx> {
|
impl<'tcx> WipProbeStep<'tcx> {
|
||||||
@ -249,6 +250,9 @@ fn finalize(self) -> inspect::ProbeStep<'tcx> {
|
|||||||
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
|
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
|
||||||
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
||||||
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
|
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
|
||||||
|
WipProbeStep::MakeCanonicalResponse { shallow_certainty } => {
|
||||||
|
inspect::ProbeStep::MakeCanonicalResponse { shallow_certainty }
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -530,6 +534,19 @@ pub fn add_goal(
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn make_canonical_response(&mut self, shallow_certainty: Certainty) {
|
||||||
|
match self.as_mut() {
|
||||||
|
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||||
|
state
|
||||||
|
.current_evaluation_scope()
|
||||||
|
.steps
|
||||||
|
.push(WipProbeStep::MakeCanonicalResponse { shallow_certainty });
|
||||||
|
}
|
||||||
|
None => {}
|
||||||
|
_ => {}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub fn finish_probe(mut self) -> ProofTreeBuilder<'tcx> {
|
pub fn finish_probe(mut self) -> ProofTreeBuilder<'tcx> {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
|
Loading…
Reference in New Issue
Block a user