move compute_goal
and evaluate_x
methods to inner module
This commit is contained in:
parent
9df35a5050
commit
b85bc19705
@ -2,8 +2,11 @@
|
|||||||
use rustc_infer::infer::at::ToTrace;
|
use rustc_infer::infer::at::ToTrace;
|
||||||
use rustc_infer::infer::canonical::CanonicalVarValues;
|
use rustc_infer::infer::canonical::CanonicalVarValues;
|
||||||
use rustc_infer::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
|
use rustc_infer::infer::type_variable::{TypeVariableOrigin, TypeVariableOriginKind};
|
||||||
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk, LateBoundRegionConversionTime};
|
use rustc_infer::infer::{
|
||||||
|
DefineOpaqueTypes, InferCtxt, InferOk, LateBoundRegionConversionTime, TyCtxtInferExt,
|
||||||
|
};
|
||||||
use rustc_infer::traits::query::NoSolution;
|
use rustc_infer::traits::query::NoSolution;
|
||||||
|
use rustc_infer::traits::solve::{CanonicalGoal, Certainty, MaybeCause, QueryResult};
|
||||||
use rustc_infer::traits::ObligationCause;
|
use rustc_infer::traits::ObligationCause;
|
||||||
use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
|
use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
|
||||||
use rustc_middle::ty::{
|
use rustc_middle::ty::{
|
||||||
@ -13,6 +16,7 @@
|
|||||||
use rustc_span::DUMMY_SP;
|
use rustc_span::DUMMY_SP;
|
||||||
use std::ops::ControlFlow;
|
use std::ops::ControlFlow;
|
||||||
|
|
||||||
|
use super::search_graph::{self, OverflowHandler};
|
||||||
use super::{search_graph::SearchGraph, Goal};
|
use super::{search_graph::SearchGraph, Goal};
|
||||||
|
|
||||||
pub struct EvalCtxt<'a, 'tcx> {
|
pub struct EvalCtxt<'a, 'tcx> {
|
||||||
@ -57,6 +61,270 @@ pub(super) fn is_empty(&self) -> bool {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub trait InferCtxtEvalExt<'tcx> {
|
||||||
|
/// Evaluates a goal from **outside** of the trait solver.
|
||||||
|
///
|
||||||
|
/// Using this while inside of the solver is wrong as it uses a new
|
||||||
|
/// search graph which would break cycle detection.
|
||||||
|
fn evaluate_root_goal(
|
||||||
|
&self,
|
||||||
|
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
|
) -> Result<(bool, Certainty), NoSolution>;
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
|
||||||
|
#[instrument(level = "debug", skip(self))]
|
||||||
|
fn evaluate_root_goal(
|
||||||
|
&self,
|
||||||
|
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
|
) -> Result<(bool, Certainty), NoSolution> {
|
||||||
|
let mut search_graph = search_graph::SearchGraph::new(self.tcx);
|
||||||
|
|
||||||
|
let mut ecx = EvalCtxt {
|
||||||
|
search_graph: &mut search_graph,
|
||||||
|
infcx: self,
|
||||||
|
// Only relevant when canonicalizing the response.
|
||||||
|
max_input_universe: ty::UniverseIndex::ROOT,
|
||||||
|
var_values: CanonicalVarValues::dummy(),
|
||||||
|
nested_goals: NestedGoals::new(),
|
||||||
|
};
|
||||||
|
let result = ecx.evaluate_goal(IsNormalizesToHack::No, goal);
|
||||||
|
|
||||||
|
assert!(
|
||||||
|
ecx.nested_goals.is_empty(),
|
||||||
|
"root `EvalCtxt` should not have any goals added to it"
|
||||||
|
);
|
||||||
|
|
||||||
|
assert!(search_graph.is_empty());
|
||||||
|
result
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||||
|
/// The entry point of the solver.
|
||||||
|
///
|
||||||
|
/// This function deals with (coinductive) cycles, overflow, and caching
|
||||||
|
/// and then calls [`EvalCtxt::compute_goal`] which contains the actual
|
||||||
|
/// logic of the solver.
|
||||||
|
///
|
||||||
|
/// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
|
||||||
|
/// if you're inside of the solver or [InferCtxtEvalExt::evaluate_root_goal] if you're
|
||||||
|
/// outside of it.
|
||||||
|
#[instrument(level = "debug", skip(tcx, search_graph), ret)]
|
||||||
|
fn evaluate_canonical_goal(
|
||||||
|
tcx: TyCtxt<'tcx>,
|
||||||
|
search_graph: &'a mut search_graph::SearchGraph<'tcx>,
|
||||||
|
canonical_goal: CanonicalGoal<'tcx>,
|
||||||
|
) -> QueryResult<'tcx> {
|
||||||
|
// Deal with overflow, caching, and coinduction.
|
||||||
|
//
|
||||||
|
// The actual solver logic happens in `ecx.compute_goal`.
|
||||||
|
search_graph.with_new_goal(tcx, canonical_goal, |search_graph| {
|
||||||
|
let (ref infcx, goal, var_values) =
|
||||||
|
tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
|
||||||
|
let mut ecx = EvalCtxt {
|
||||||
|
infcx,
|
||||||
|
var_values,
|
||||||
|
max_input_universe: canonical_goal.max_universe,
|
||||||
|
search_graph,
|
||||||
|
nested_goals: NestedGoals::new(),
|
||||||
|
};
|
||||||
|
ecx.compute_goal(goal)
|
||||||
|
})
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Recursively evaluates `goal`, returning whether any inference vars have
|
||||||
|
/// been constrained and the certainty of the result.
|
||||||
|
fn evaluate_goal(
|
||||||
|
&mut self,
|
||||||
|
is_normalizes_to_hack: IsNormalizesToHack,
|
||||||
|
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
|
) -> Result<(bool, Certainty), NoSolution> {
|
||||||
|
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
||||||
|
let canonical_response =
|
||||||
|
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
|
||||||
|
|
||||||
|
let has_changed = !canonical_response.value.var_values.is_identity();
|
||||||
|
let certainty = self.instantiate_and_apply_query_response(
|
||||||
|
goal.param_env,
|
||||||
|
orig_values,
|
||||||
|
canonical_response,
|
||||||
|
)?;
|
||||||
|
|
||||||
|
// Check that rerunning this query with its inference constraints applied
|
||||||
|
// doesn't result in new inference constraints and has the same result.
|
||||||
|
//
|
||||||
|
// If we have projection goals like `<T as Trait>::Assoc == u32` we recursively
|
||||||
|
// call `exists<U> <T as Trait>::Assoc == U` to enable better caching. This goal
|
||||||
|
// could constrain `U` to `u32` which would cause this check to result in a
|
||||||
|
// solver cycle.
|
||||||
|
if cfg!(debug_assertions)
|
||||||
|
&& has_changed
|
||||||
|
&& is_normalizes_to_hack == IsNormalizesToHack::No
|
||||||
|
&& !self.search_graph.in_cycle()
|
||||||
|
{
|
||||||
|
debug!("rerunning goal to check result is stable");
|
||||||
|
let (_orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
||||||
|
let canonical_response =
|
||||||
|
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
|
||||||
|
if !canonical_response.value.var_values.is_identity() {
|
||||||
|
bug!("unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}");
|
||||||
|
}
|
||||||
|
assert_eq!(certainty, canonical_response.value.certainty);
|
||||||
|
}
|
||||||
|
|
||||||
|
Ok((has_changed, certainty))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
|
||||||
|
let Goal { param_env, predicate } = goal;
|
||||||
|
let kind = predicate.kind();
|
||||||
|
if let Some(kind) = kind.no_bound_vars() {
|
||||||
|
match kind {
|
||||||
|
ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
|
||||||
|
self.compute_trait_goal(Goal { param_env, predicate })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
|
||||||
|
self.compute_projection_goal(Goal { param_env, predicate })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
|
||||||
|
self.compute_type_outlives_goal(Goal { param_env, predicate })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
|
||||||
|
self.compute_region_outlives_goal(Goal { param_env, predicate })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::Clause(ty::Clause::ConstArgHasType(ct, ty)) => {
|
||||||
|
self.compute_const_arg_has_type_goal(Goal { param_env, predicate: (ct, ty) })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::Subtype(predicate) => {
|
||||||
|
self.compute_subtype_goal(Goal { param_env, predicate })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::Coerce(predicate) => {
|
||||||
|
self.compute_coerce_goal(Goal { param_env, predicate })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::ClosureKind(def_id, substs, kind) => self
|
||||||
|
.compute_closure_kind_goal(Goal {
|
||||||
|
param_env,
|
||||||
|
predicate: (def_id, substs, kind),
|
||||||
|
}),
|
||||||
|
ty::PredicateKind::ObjectSafe(trait_def_id) => {
|
||||||
|
self.compute_object_safe_goal(trait_def_id)
|
||||||
|
}
|
||||||
|
ty::PredicateKind::WellFormed(arg) => {
|
||||||
|
self.compute_well_formed_goal(Goal { param_env, predicate: arg })
|
||||||
|
}
|
||||||
|
ty::PredicateKind::Ambiguous => {
|
||||||
|
self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
|
||||||
|
}
|
||||||
|
// FIXME: implement these predicates :)
|
||||||
|
ty::PredicateKind::ConstEvaluatable(_) | ty::PredicateKind::ConstEquate(_, _) => {
|
||||||
|
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
|
||||||
|
}
|
||||||
|
ty::PredicateKind::TypeWellFormedFromEnv(..) => {
|
||||||
|
bug!("TypeWellFormedFromEnv is only used for Chalk")
|
||||||
|
}
|
||||||
|
ty::PredicateKind::AliasEq(lhs, rhs) => {
|
||||||
|
self.compute_alias_eq_goal(Goal { param_env, predicate: (lhs, rhs) })
|
||||||
|
}
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
let kind = self.infcx.instantiate_binder_with_placeholders(kind);
|
||||||
|
let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
|
||||||
|
self.add_goal(goal);
|
||||||
|
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
|
||||||
|
// the certainty of all the goals.
|
||||||
|
#[instrument(level = "debug", skip(self))]
|
||||||
|
pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
|
||||||
|
let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new());
|
||||||
|
let mut new_goals = NestedGoals::new();
|
||||||
|
|
||||||
|
let response = self.repeat_while_none(
|
||||||
|
|_| Ok(Certainty::Maybe(MaybeCause::Overflow)),
|
||||||
|
|this| {
|
||||||
|
let mut has_changed = Err(Certainty::Yes);
|
||||||
|
|
||||||
|
if let Some(goal) = goals.normalizes_to_hack_goal.take() {
|
||||||
|
let (_, certainty) = match this.evaluate_goal(
|
||||||
|
IsNormalizesToHack::Yes,
|
||||||
|
goal.with(this.tcx(), ty::Binder::dummy(goal.predicate)),
|
||||||
|
) {
|
||||||
|
Ok(r) => r,
|
||||||
|
Err(NoSolution) => return Some(Err(NoSolution)),
|
||||||
|
};
|
||||||
|
|
||||||
|
if goal.predicate.projection_ty
|
||||||
|
!= this.resolve_vars_if_possible(goal.predicate.projection_ty)
|
||||||
|
{
|
||||||
|
has_changed = Ok(())
|
||||||
|
}
|
||||||
|
|
||||||
|
match certainty {
|
||||||
|
Certainty::Yes => {}
|
||||||
|
Certainty::Maybe(_) => {
|
||||||
|
let goal = this.resolve_vars_if_possible(goal);
|
||||||
|
|
||||||
|
// The rhs of this `normalizes-to` must always be an unconstrained infer var as it is
|
||||||
|
// the hack used by `normalizes-to` to ensure that every `normalizes-to` behaves the same
|
||||||
|
// regardless of the rhs.
|
||||||
|
//
|
||||||
|
// However it is important not to unconditionally replace the rhs with a new infer var
|
||||||
|
// as otherwise we may replace the original unconstrained infer var with a new infer var
|
||||||
|
// and never propagate any constraints on the new var back to the original var.
|
||||||
|
let term = this
|
||||||
|
.term_is_fully_unconstrained(goal)
|
||||||
|
.then_some(goal.predicate.term)
|
||||||
|
.unwrap_or_else(|| {
|
||||||
|
this.next_term_infer_of_kind(goal.predicate.term)
|
||||||
|
});
|
||||||
|
let projection_pred = ty::ProjectionPredicate {
|
||||||
|
term,
|
||||||
|
projection_ty: goal.predicate.projection_ty,
|
||||||
|
};
|
||||||
|
new_goals.normalizes_to_hack_goal =
|
||||||
|
Some(goal.with(this.tcx(), projection_pred));
|
||||||
|
|
||||||
|
has_changed = has_changed.map_err(|c| c.unify_and(certainty));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
for nested_goal in goals.goals.drain(..) {
|
||||||
|
let (changed, certainty) =
|
||||||
|
match this.evaluate_goal(IsNormalizesToHack::No, nested_goal) {
|
||||||
|
Ok(result) => result,
|
||||||
|
Err(NoSolution) => return Some(Err(NoSolution)),
|
||||||
|
};
|
||||||
|
|
||||||
|
if changed {
|
||||||
|
has_changed = Ok(());
|
||||||
|
}
|
||||||
|
|
||||||
|
match certainty {
|
||||||
|
Certainty::Yes => {}
|
||||||
|
Certainty::Maybe(_) => {
|
||||||
|
new_goals.goals.push(nested_goal);
|
||||||
|
has_changed = has_changed.map_err(|c| c.unify_and(certainty));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
core::mem::swap(&mut new_goals, &mut goals);
|
||||||
|
match has_changed {
|
||||||
|
Ok(()) => None,
|
||||||
|
Err(certainty) => Some(Ok(certainty)),
|
||||||
|
}
|
||||||
|
},
|
||||||
|
);
|
||||||
|
|
||||||
|
self.nested_goals = goals;
|
||||||
|
response
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
impl<'tcx> EvalCtxt<'_, 'tcx> {
|
impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||||
pub(super) fn probe<T>(&mut self, f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> T) -> T {
|
pub(super) fn probe<T>(&mut self, f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> T) -> T {
|
||||||
let mut ecx = EvalCtxt {
|
let mut ecx = EvalCtxt {
|
||||||
|
@ -15,23 +15,19 @@
|
|||||||
|
|
||||||
// FIXME: uses of `infcx.at` need to enable deferred projection equality once that's implemented.
|
// FIXME: uses of `infcx.at` need to enable deferred projection equality once that's implemented.
|
||||||
|
|
||||||
use std::mem;
|
|
||||||
|
|
||||||
use rustc_hir::def_id::DefId;
|
use rustc_hir::def_id::DefId;
|
||||||
use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
|
use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
|
||||||
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk, TyCtxtInferExt};
|
use rustc_infer::infer::{DefineOpaqueTypes, InferOk};
|
||||||
use rustc_infer::traits::query::NoSolution;
|
use rustc_infer::traits::query::NoSolution;
|
||||||
use rustc_middle::traits::solve::{
|
use rustc_middle::traits::solve::{
|
||||||
CanonicalGoal, CanonicalResponse, Certainty, ExternalConstraints, ExternalConstraintsData,
|
CanonicalGoal, CanonicalResponse, Certainty, ExternalConstraints, ExternalConstraintsData,
|
||||||
Goal, MaybeCause, QueryResult, Response,
|
Goal, QueryResult, Response,
|
||||||
};
|
};
|
||||||
use rustc_middle::ty::{self, Ty, TyCtxt};
|
use rustc_middle::ty::{self, Ty, TyCtxt};
|
||||||
use rustc_middle::ty::{
|
use rustc_middle::ty::{
|
||||||
CoercePredicate, RegionOutlivesPredicate, SubtypePredicate, TypeOutlivesPredicate,
|
CoercePredicate, RegionOutlivesPredicate, SubtypePredicate, TypeOutlivesPredicate,
|
||||||
};
|
};
|
||||||
use rustc_span::DUMMY_SP;
|
|
||||||
|
|
||||||
use crate::solve::search_graph::OverflowHandler;
|
|
||||||
use crate::traits::ObligationCause;
|
use crate::traits::ObligationCause;
|
||||||
|
|
||||||
mod assembly;
|
mod assembly;
|
||||||
@ -42,11 +38,9 @@
|
|||||||
mod search_graph;
|
mod search_graph;
|
||||||
mod trait_goals;
|
mod trait_goals;
|
||||||
|
|
||||||
pub use eval_ctxt::EvalCtxt;
|
pub use eval_ctxt::{EvalCtxt, InferCtxtEvalExt};
|
||||||
pub use fulfill::FulfillmentCtxt;
|
pub use fulfill::FulfillmentCtxt;
|
||||||
|
|
||||||
use self::eval_ctxt::{IsNormalizesToHack, NestedGoals};
|
|
||||||
|
|
||||||
trait CanonicalResponseExt {
|
trait CanonicalResponseExt {
|
||||||
fn has_no_inference_or_external_constraints(&self) -> bool;
|
fn has_no_inference_or_external_constraints(&self) -> bool;
|
||||||
}
|
}
|
||||||
@ -59,180 +53,7 @@ fn has_no_inference_or_external_constraints(&self) -> bool {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub trait InferCtxtEvalExt<'tcx> {
|
|
||||||
/// Evaluates a goal from **outside** of the trait solver.
|
|
||||||
///
|
|
||||||
/// Using this while inside of the solver is wrong as it uses a new
|
|
||||||
/// search graph which would break cycle detection.
|
|
||||||
fn evaluate_root_goal(
|
|
||||||
&self,
|
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
|
||||||
) -> Result<(bool, Certainty), NoSolution>;
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
|
|
||||||
#[instrument(level = "debug", skip(self))]
|
|
||||||
fn evaluate_root_goal(
|
|
||||||
&self,
|
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
|
||||||
) -> Result<(bool, Certainty), NoSolution> {
|
|
||||||
let mut search_graph = search_graph::SearchGraph::new(self.tcx);
|
|
||||||
|
|
||||||
let mut ecx = EvalCtxt {
|
|
||||||
search_graph: &mut search_graph,
|
|
||||||
infcx: self,
|
|
||||||
// Only relevant when canonicalizing the response.
|
|
||||||
max_input_universe: ty::UniverseIndex::ROOT,
|
|
||||||
var_values: CanonicalVarValues::dummy(),
|
|
||||||
nested_goals: NestedGoals::new(),
|
|
||||||
};
|
|
||||||
let result = ecx.evaluate_goal(IsNormalizesToHack::No, goal);
|
|
||||||
|
|
||||||
assert!(
|
|
||||||
ecx.nested_goals.is_empty(),
|
|
||||||
"root `EvalCtxt` should not have any goals added to it"
|
|
||||||
);
|
|
||||||
|
|
||||||
assert!(search_graph.is_empty());
|
|
||||||
result
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||||
/// The entry point of the solver.
|
|
||||||
///
|
|
||||||
/// This function deals with (coinductive) cycles, overflow, and caching
|
|
||||||
/// and then calls [`EvalCtxt::compute_goal`] which contains the actual
|
|
||||||
/// logic of the solver.
|
|
||||||
///
|
|
||||||
/// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
|
|
||||||
/// if you're inside of the solver or [InferCtxtEvalExt::evaluate_root_goal] if you're
|
|
||||||
/// outside of it.
|
|
||||||
#[instrument(level = "debug", skip(tcx, search_graph), ret)]
|
|
||||||
fn evaluate_canonical_goal(
|
|
||||||
tcx: TyCtxt<'tcx>,
|
|
||||||
search_graph: &'a mut search_graph::SearchGraph<'tcx>,
|
|
||||||
canonical_goal: CanonicalGoal<'tcx>,
|
|
||||||
) -> QueryResult<'tcx> {
|
|
||||||
// Deal with overflow, caching, and coinduction.
|
|
||||||
//
|
|
||||||
// The actual solver logic happens in `ecx.compute_goal`.
|
|
||||||
search_graph.with_new_goal(tcx, canonical_goal, |search_graph| {
|
|
||||||
let (ref infcx, goal, var_values) =
|
|
||||||
tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
|
|
||||||
let mut ecx = EvalCtxt {
|
|
||||||
infcx,
|
|
||||||
var_values,
|
|
||||||
max_input_universe: canonical_goal.max_universe,
|
|
||||||
search_graph,
|
|
||||||
nested_goals: NestedGoals::new(),
|
|
||||||
};
|
|
||||||
ecx.compute_goal(goal)
|
|
||||||
})
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Recursively evaluates `goal`, returning whether any inference vars have
|
|
||||||
/// been constrained and the certainty of the result.
|
|
||||||
fn evaluate_goal(
|
|
||||||
&mut self,
|
|
||||||
is_normalizes_to_hack: IsNormalizesToHack,
|
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
|
||||||
) -> Result<(bool, Certainty), NoSolution> {
|
|
||||||
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
|
||||||
let canonical_response =
|
|
||||||
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
|
|
||||||
|
|
||||||
let has_changed = !canonical_response.value.var_values.is_identity();
|
|
||||||
let certainty = self.instantiate_and_apply_query_response(
|
|
||||||
goal.param_env,
|
|
||||||
orig_values,
|
|
||||||
canonical_response,
|
|
||||||
)?;
|
|
||||||
|
|
||||||
// Check that rerunning this query with its inference constraints applied
|
|
||||||
// doesn't result in new inference constraints and has the same result.
|
|
||||||
//
|
|
||||||
// If we have projection goals like `<T as Trait>::Assoc == u32` we recursively
|
|
||||||
// call `exists<U> <T as Trait>::Assoc == U` to enable better caching. This goal
|
|
||||||
// could constrain `U` to `u32` which would cause this check to result in a
|
|
||||||
// solver cycle.
|
|
||||||
if cfg!(debug_assertions)
|
|
||||||
&& has_changed
|
|
||||||
&& is_normalizes_to_hack == IsNormalizesToHack::No
|
|
||||||
&& !self.search_graph.in_cycle()
|
|
||||||
{
|
|
||||||
debug!("rerunning goal to check result is stable");
|
|
||||||
let (_orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
|
||||||
let canonical_response =
|
|
||||||
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
|
|
||||||
if !canonical_response.value.var_values.is_identity() {
|
|
||||||
bug!("unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}");
|
|
||||||
}
|
|
||||||
assert_eq!(certainty, canonical_response.value.certainty);
|
|
||||||
}
|
|
||||||
|
|
||||||
Ok((has_changed, certainty))
|
|
||||||
}
|
|
||||||
|
|
||||||
fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
|
|
||||||
let Goal { param_env, predicate } = goal;
|
|
||||||
let kind = predicate.kind();
|
|
||||||
if let Some(kind) = kind.no_bound_vars() {
|
|
||||||
match kind {
|
|
||||||
ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
|
|
||||||
self.compute_trait_goal(Goal { param_env, predicate })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
|
|
||||||
self.compute_projection_goal(Goal { param_env, predicate })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
|
|
||||||
self.compute_type_outlives_goal(Goal { param_env, predicate })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
|
|
||||||
self.compute_region_outlives_goal(Goal { param_env, predicate })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::Clause(ty::Clause::ConstArgHasType(ct, ty)) => {
|
|
||||||
self.compute_const_arg_has_type_goal(Goal { param_env, predicate: (ct, ty) })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::Subtype(predicate) => {
|
|
||||||
self.compute_subtype_goal(Goal { param_env, predicate })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::Coerce(predicate) => {
|
|
||||||
self.compute_coerce_goal(Goal { param_env, predicate })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::ClosureKind(def_id, substs, kind) => self
|
|
||||||
.compute_closure_kind_goal(Goal {
|
|
||||||
param_env,
|
|
||||||
predicate: (def_id, substs, kind),
|
|
||||||
}),
|
|
||||||
ty::PredicateKind::ObjectSafe(trait_def_id) => {
|
|
||||||
self.compute_object_safe_goal(trait_def_id)
|
|
||||||
}
|
|
||||||
ty::PredicateKind::WellFormed(arg) => {
|
|
||||||
self.compute_well_formed_goal(Goal { param_env, predicate: arg })
|
|
||||||
}
|
|
||||||
ty::PredicateKind::Ambiguous => {
|
|
||||||
self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
|
|
||||||
}
|
|
||||||
// FIXME: implement these predicates :)
|
|
||||||
ty::PredicateKind::ConstEvaluatable(_) | ty::PredicateKind::ConstEquate(_, _) => {
|
|
||||||
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
|
|
||||||
}
|
|
||||||
ty::PredicateKind::TypeWellFormedFromEnv(..) => {
|
|
||||||
bug!("TypeWellFormedFromEnv is only used for Chalk")
|
|
||||||
}
|
|
||||||
ty::PredicateKind::AliasEq(lhs, rhs) => {
|
|
||||||
self.compute_alias_eq_goal(Goal { param_env, predicate: (lhs, rhs) })
|
|
||||||
}
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
let kind = self.infcx.instantiate_binder_with_placeholders(kind);
|
|
||||||
let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
|
|
||||||
self.add_goal(goal);
|
|
||||||
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[instrument(level = "debug", skip(self))]
|
#[instrument(level = "debug", skip(self))]
|
||||||
fn compute_type_outlives_goal(
|
fn compute_type_outlives_goal(
|
||||||
&mut self,
|
&mut self,
|
||||||
@ -424,95 +245,6 @@ fn add_goals(&mut self, goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate
|
|||||||
debug!("added_goals={:?}", &self.nested_goals.goals[current_len..]);
|
debug!("added_goals={:?}", &self.nested_goals.goals[current_len..]);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
|
|
||||||
// the certainty of all the goals.
|
|
||||||
#[instrument(level = "debug", skip(self))]
|
|
||||||
fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
|
|
||||||
let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new());
|
|
||||||
let mut new_goals = NestedGoals::new();
|
|
||||||
|
|
||||||
let response = self.repeat_while_none(
|
|
||||||
|_| Ok(Certainty::Maybe(MaybeCause::Overflow)),
|
|
||||||
|this| {
|
|
||||||
let mut has_changed = Err(Certainty::Yes);
|
|
||||||
|
|
||||||
if let Some(goal) = goals.normalizes_to_hack_goal.take() {
|
|
||||||
let (_, certainty) = match this.evaluate_goal(
|
|
||||||
IsNormalizesToHack::Yes,
|
|
||||||
goal.with(this.tcx(), ty::Binder::dummy(goal.predicate)),
|
|
||||||
) {
|
|
||||||
Ok(r) => r,
|
|
||||||
Err(NoSolution) => return Some(Err(NoSolution)),
|
|
||||||
};
|
|
||||||
|
|
||||||
if goal.predicate.projection_ty
|
|
||||||
!= this.resolve_vars_if_possible(goal.predicate.projection_ty)
|
|
||||||
{
|
|
||||||
has_changed = Ok(())
|
|
||||||
}
|
|
||||||
|
|
||||||
match certainty {
|
|
||||||
Certainty::Yes => {}
|
|
||||||
Certainty::Maybe(_) => {
|
|
||||||
let goal = this.resolve_vars_if_possible(goal);
|
|
||||||
|
|
||||||
// The rhs of this `normalizes-to` must always be an unconstrained infer var as it is
|
|
||||||
// the hack used by `normalizes-to` to ensure that every `normalizes-to` behaves the same
|
|
||||||
// regardless of the rhs.
|
|
||||||
//
|
|
||||||
// However it is important not to unconditionally replace the rhs with a new infer var
|
|
||||||
// as otherwise we may replace the original unconstrained infer var with a new infer var
|
|
||||||
// and never propagate any constraints on the new var back to the original var.
|
|
||||||
let term = this
|
|
||||||
.term_is_fully_unconstrained(goal)
|
|
||||||
.then_some(goal.predicate.term)
|
|
||||||
.unwrap_or_else(|| {
|
|
||||||
this.next_term_infer_of_kind(goal.predicate.term)
|
|
||||||
});
|
|
||||||
let projection_pred = ty::ProjectionPredicate {
|
|
||||||
term,
|
|
||||||
projection_ty: goal.predicate.projection_ty,
|
|
||||||
};
|
|
||||||
new_goals.normalizes_to_hack_goal =
|
|
||||||
Some(goal.with(this.tcx(), projection_pred));
|
|
||||||
|
|
||||||
has_changed = has_changed.map_err(|c| c.unify_and(certainty));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
for nested_goal in goals.goals.drain(..) {
|
|
||||||
let (changed, certainty) =
|
|
||||||
match this.evaluate_goal(IsNormalizesToHack::No, nested_goal) {
|
|
||||||
Ok(result) => result,
|
|
||||||
Err(NoSolution) => return Some(Err(NoSolution)),
|
|
||||||
};
|
|
||||||
|
|
||||||
if changed {
|
|
||||||
has_changed = Ok(());
|
|
||||||
}
|
|
||||||
|
|
||||||
match certainty {
|
|
||||||
Certainty::Yes => {}
|
|
||||||
Certainty::Maybe(_) => {
|
|
||||||
new_goals.goals.push(nested_goal);
|
|
||||||
has_changed = has_changed.map_err(|c| c.unify_and(certainty));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
mem::swap(&mut new_goals, &mut goals);
|
|
||||||
match has_changed {
|
|
||||||
Ok(()) => None,
|
|
||||||
Err(certainty) => Some(Ok(certainty)),
|
|
||||||
}
|
|
||||||
},
|
|
||||||
);
|
|
||||||
|
|
||||||
self.nested_goals = goals;
|
|
||||||
response
|
|
||||||
}
|
|
||||||
|
|
||||||
fn try_merge_responses(
|
fn try_merge_responses(
|
||||||
&mut self,
|
&mut self,
|
||||||
responses: impl Iterator<Item = QueryResult<'tcx>>,
|
responses: impl Iterator<Item = QueryResult<'tcx>>,
|
||||||
|
Loading…
Reference in New Issue
Block a user