1
Fork 0

Make assumption functions in new solver take clause

This commit is contained in:
Michael Goulet 2023-06-15 16:18:38 +00:00
parent 4996b56ba9
commit b4ba7c4f93
4 changed files with 98 additions and 26 deletions

View file

@ -105,7 +105,7 @@ pub(super) trait GoalKind<'tcx>:
fn probe_and_match_goal_against_assumption(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
assumption: ty::Binder<'tcx, ty::Clause<'tcx>>,
then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
) -> QueryResult<'tcx>;
@ -115,7 +115,7 @@ pub(super) trait GoalKind<'tcx>:
fn consider_implied_clause(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
assumption: ty::Binder<'tcx, ty::Clause<'tcx>>,
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
@ -131,7 +131,7 @@ pub(super) trait GoalKind<'tcx>:
fn consider_alias_bound_candidate(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
assumption: ty::Binder<'tcx, ty::Clause<'tcx>>,
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
ecx.validate_alias_bound_self_from_param_env(goal)
@ -144,7 +144,7 @@ pub(super) trait GoalKind<'tcx>:
fn consider_object_bound_candidate(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
assumption: ty::Binder<'tcx, ty::Clause<'tcx>>,
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
let tcx = ecx.tcx();
@ -467,11 +467,13 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
candidates: &mut Vec<Candidate<'tcx>>,
) {
for (i, assumption) in goal.param_env.caller_bounds().iter().enumerate() {
match G::consider_implied_clause(self, goal, assumption, []) {
Ok(result) => {
candidates.push(Candidate { source: CandidateSource::ParamEnv(i), result })
if let Some(clause) = assumption.as_clause() {
match G::consider_implied_clause(self, goal, clause, []) {
Ok(result) => {
candidates.push(Candidate { source: CandidateSource::ParamEnv(i), result })
}
Err(NoSolution) => (),
}
Err(NoSolution) => (),
}
}
}
@ -517,11 +519,13 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
for assumption in self.tcx().item_bounds(alias_ty.def_id).subst(self.tcx(), alias_ty.substs)
{
match G::consider_alias_bound_candidate(self, goal, assumption) {
Ok(result) => {
candidates.push(Candidate { source: CandidateSource::AliasBound, result })
if let Some(clause) = assumption.as_clause() {
match G::consider_alias_bound_candidate(self, goal, clause) {
Ok(result) => {
candidates.push(Candidate { source: CandidateSource::AliasBound, result })
}
Err(NoSolution) => (),
}
Err(NoSolution) => (),
}
}
}
@ -675,18 +679,20 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
// projection predicates that we reach by elaborating the principal trait ref,
// since that'll cause ambiguity.
//
// We can remove this when we have implemented intersections in responses.
// We can remove this when we have implemented lifetime intersections in responses.
if assumption.to_opt_poly_projection_pred().is_some()
&& !own_bounds.contains(&assumption)
{
continue;
}
match G::consider_object_bound_candidate(self, goal, assumption) {
Ok(result) => {
candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result })
if let Some(clause) = assumption.as_clause() {
match G::consider_object_bound_candidate(self, goal, clause) {
Ok(result) => {
candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result })
}
Err(NoSolution) => (),
}
Err(NoSolution) => (),
}
}
}

View file

@ -105,15 +105,15 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
fn probe_and_match_goal_against_assumption(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
assumption: ty::Binder<'tcx, ty::Clause<'tcx>>,
then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
) -> QueryResult<'tcx> {
if let Some(poly_projection_pred) = assumption.to_opt_poly_projection_pred()
&& poly_projection_pred.projection_def_id() == goal.predicate.def_id()
if let Some(projection_pred) = assumption.as_projection_clause()
&& projection_pred.projection_def_id() == goal.predicate.def_id()
{
ecx.probe(|ecx| {
let assumption_projection_pred =
ecx.instantiate_binder_with_infer(poly_projection_pred);
ecx.instantiate_binder_with_infer(projection_pred);
ecx.eq(
goal.param_env,
goal.predicate.projection_ty,

View file

@ -81,17 +81,17 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
fn probe_and_match_goal_against_assumption(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
assumption: ty::Binder<'tcx, ty::Clause<'tcx>>,
then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
) -> QueryResult<'tcx> {
if let Some(poly_trait_pred) = assumption.to_opt_poly_trait_pred()
&& poly_trait_pred.def_id() == goal.predicate.def_id()
&& poly_trait_pred.polarity() == goal.predicate.polarity
if let Some(trait_clause) = assumption.as_trait_clause()
&& trait_clause.def_id() == goal.predicate.def_id()
&& trait_clause.polarity() == goal.predicate.polarity
{
// FIXME: Constness
ecx.probe(|ecx| {
let assumption_trait_pred =
ecx.instantiate_binder_with_infer(poly_trait_pred);
ecx.instantiate_binder_with_infer(trait_clause);
ecx.eq(
goal.param_env,
goal.predicate.trait_ref,