cleanup + review

This commit is contained in:
lcnr 2024-03-18 17:00:37 +01:00
parent 7c5a99b6a8
commit 0b29b71a2f
7 changed files with 31 additions and 35 deletions

View File

@ -275,12 +275,6 @@ pub enum GoalSource {
ImplWhereBound,
}
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, HashStable)]
pub enum IsNormalizesToHack {
Yes,
No,
}
/// Possible ways the given goal can be proven.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum CandidateSource {

View File

@ -19,8 +19,8 @@
//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
use super::{
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, GoalSource, IsNormalizesToHack,
NoSolution, QueryInput, QueryResult,
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, GoalSource, NoSolution,
QueryInput, QueryResult,
};
use crate::{infer::canonical::CanonicalVarValues, ty};
use format::ProofTreeFormatter;
@ -50,7 +50,7 @@ pub type CanonicalState<'tcx, T> = Canonical<'tcx, State<'tcx, T>>;
#[derive(Eq, PartialEq)]
pub enum GoalEvaluationKind<'tcx> {
Root { orig_values: Vec<ty::GenericArg<'tcx>> },
Nested { is_normalizes_to_hack: IsNormalizesToHack },
Nested,
}
#[derive(Eq, PartialEq)]

View File

@ -55,10 +55,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
let goal_text = match eval.kind {
GoalEvaluationKind::Root { orig_values: _ } => "ROOT GOAL",
GoalEvaluationKind::Nested { is_normalizes_to_hack } => match is_normalizes_to_hack {
IsNormalizesToHack::No => "GOAL",
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
},
GoalEvaluationKind::Nested => "GOAL",
};
write!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))

View File

@ -30,6 +30,7 @@ use rustc_middle::traits::ObligationCause;
use rustc_middle::ty::{self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable};
use rustc_next_trait_solver::canonicalizer::{CanonicalizeMode, Canonicalizer};
use rustc_span::DUMMY_SP;
use std::assert_matches::assert_matches;
use std::iter;
use std::ops::Deref;
@ -104,7 +105,12 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
// by `try_evaluate_added_goals()`.
let (certainty, normalization_nested_goals) = if self.is_normalizes_to_goal {
let NestedGoals { normalizes_to_goals, goals } = std::mem::take(&mut self.nested_goals);
assert!(normalizes_to_goals.is_empty());
if cfg!(debug_assertions) {
assert!(normalizes_to_goals.is_empty());
if goals.is_empty() {
assert_matches!(goals_certainty, Certainty::Yes);
}
}
(certainty, NestedNormalizationGoals(goals))
} else {
let certainty = certainty.unify_with(goals_certainty);

View File

@ -13,8 +13,8 @@ use rustc_middle::infer::canonical::CanonicalVarInfos;
use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
use rustc_middle::traits::solve::inspect;
use rustc_middle::traits::solve::{
CanonicalInput, CanonicalResponse, Certainty, IsNormalizesToHack, PredefinedOpaques,
PredefinedOpaquesData, QueryResult,
CanonicalInput, CanonicalResponse, Certainty, PredefinedOpaques, PredefinedOpaquesData,
QueryResult,
};
use rustc_middle::traits::specialization_graph;
use rustc_middle::ty::{
@ -337,8 +337,15 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
Ok((has_changed, certainty))
}
/// FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
/// be necessary once we implement the new coinduction approach.
/// Recursively evaluates `goal`, returning the nested goals in case
/// the nested goal is a `NormalizesTo` goal.
///
/// As all other goal kinds do not return any nested goals and
/// `NormalizesTo` is only used by `AliasRelate`, all other callsites
/// should use [`EvalCtxt::evaluate_goal`] which discards that empty
/// storage.
// FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
// be necessary once we implement the new coinduction approach.
fn evaluate_goal_raw(
&mut self,
goal_evaluation_kind: GoalEvaluationKind,
@ -522,7 +529,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
);
let (NestedNormalizationGoals(nested_goals), _, certainty) = self.evaluate_goal_raw(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
GoalEvaluationKind::Nested,
GoalSource::Misc,
unconstrained_goal,
)?;
@ -557,11 +564,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}
for (source, goal) in goals.goals {
let (has_changed, certainty) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
source,
goal,
)?;
let (has_changed, certainty) =
self.evaluate_goal(GoalEvaluationKind::Nested, source, goal)?;
if has_changed {
unchanged_certainty = None;
}

View File

@ -7,7 +7,7 @@ use std::mem;
use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{
CanonicalInput, Certainty, Goal, GoalSource, IsNormalizesToHack, QueryInput, QueryResult,
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
};
use rustc_middle::ty::{self, TyCtxt};
use rustc_session::config::DumpSolverProofTree;
@ -97,9 +97,7 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
WipGoalEvaluationKind::Root { orig_values } => {
inspect::GoalEvaluationKind::Root { orig_values }
}
WipGoalEvaluationKind::Nested { is_normalizes_to_hack } => {
inspect::GoalEvaluationKind::Nested { is_normalizes_to_hack }
}
WipGoalEvaluationKind::Nested => inspect::GoalEvaluationKind::Nested,
},
evaluation: self.evaluation.unwrap().finalize(),
}
@ -109,7 +107,7 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
#[derive(Eq, PartialEq, Debug)]
pub(in crate::solve) enum WipGoalEvaluationKind<'tcx> {
Root { orig_values: Vec<ty::GenericArg<'tcx>> },
Nested { is_normalizes_to_hack: IsNormalizesToHack },
Nested,
}
#[derive(Eq, PartialEq)]
@ -305,9 +303,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
solve::GoalEvaluationKind::Root => {
WipGoalEvaluationKind::Root { orig_values: orig_values.to_vec() }
}
solve::GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
WipGoalEvaluationKind::Nested { is_normalizes_to_hack }
}
solve::GoalEvaluationKind::Nested => WipGoalEvaluationKind::Nested,
},
evaluation: None,
})

View File

@ -18,8 +18,7 @@ use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
use rustc_infer::traits::query::NoSolution;
use rustc_middle::infer::canonical::CanonicalVarInfos;
use rustc_middle::traits::solve::{
CanonicalResponse, Certainty, ExternalConstraintsData, Goal, GoalSource, IsNormalizesToHack,
QueryResult, Response,
CanonicalResponse, Certainty, ExternalConstraintsData, Goal, GoalSource, QueryResult, Response,
};
use rustc_middle::ty::{self, AliasRelationDirection, Ty, TyCtxt, UniverseIndex};
use rustc_middle::ty::{
@ -69,7 +68,7 @@ enum SolverMode {
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
enum GoalEvaluationKind {
Root,
Nested { is_normalizes_to_hack: IsNormalizesToHack },
Nested,
}
#[extension(trait CanonicalResponseExt)]