Consolidate the 'match assumption' type methods in GoalKind

This commit is contained in:
Michael Goulet 2023-04-22 04:51:35 +00:00
parent 0dbaae4165
commit 3a863e534b
3 changed files with 47 additions and 140 deletions

View File

@ -99,6 +99,17 @@ pub(super) trait GoalKind<'tcx>:
fn trait_def_id(self, tcx: TyCtxt<'tcx>) -> DefId;
// Try equating an assumption predicate against a goal's predicate. If it
// holds, then execute the `then` callback, which should do any additional
// work, then produce a response (typically by executing
// [`EvalCtxt::evaluate_added_goals_and_make_canonical_response`]).
fn probe_and_match_goal_against_assumption(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
then: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> QueryResult<'tcx>,
) -> QueryResult<'tcx>;
// Consider a clause, which consists of a "assumption" and some "requirements",
// to satisfy a goal. If the requirements hold, then attempt to satisfy our
// goal by equating it with the assumption.
@ -107,7 +118,12 @@ pub(super) trait GoalKind<'tcx>:
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) -> QueryResult<'tcx>;
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
ecx.add_goals(requirements);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
/// Consider a bound originating from the item bounds of an alias. For this we
/// require that the well-formed requirements of the self type of the goal
@ -117,7 +133,11 @@ pub(super) trait GoalKind<'tcx>:
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
) -> QueryResult<'tcx>;
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
ecx.validate_alias_bound_self_from_param_env(goal)
})
}
// Consider a clause specifically for a `dyn Trait` self type. This requires
// additionally checking all of the supertraits and object bounds to hold,
@ -126,7 +146,25 @@ pub(super) trait GoalKind<'tcx>:
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
) -> QueryResult<'tcx>;
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
let tcx = ecx.tcx();
let ty::Dynamic(bounds, _, _) = *goal.predicate.self_ty().kind() else {
bug!("expected object type in `consider_object_bound_candidate`");
};
ecx.add_goals(
structural_traits::predicates_for_object_candidate(
&ecx,
goal.param_env,
goal.predicate.trait_ref(tcx),
bounds,
)
.into_iter()
.map(|pred| goal.with(tcx, pred)),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
fn consider_impl_candidate(
ecx: &mut EvalCtxt<'_, 'tcx>,

View File

@ -56,11 +56,11 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
self.trait_def_id(tcx)
}
fn consider_implied_clause(
fn probe_and_match_goal_against_assumption(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'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()
@ -75,73 +75,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
)?;
ecx.eq(goal.param_env, goal.predicate.term, assumption_projection_pred.term)
.expect("expected goal term to be fully unconstrained");
ecx.add_goals(requirements);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
} else {
Err(NoSolution)
}
}
fn consider_alias_bound_candidate(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'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()
{
ecx.probe(|ecx| {
let assumption_projection_pred =
ecx.instantiate_binder_with_infer(poly_projection_pred);
ecx.eq(
goal.param_env,
goal.predicate.projection_ty,
assumption_projection_pred.projection_ty,
)?;
ecx.eq(goal.param_env, goal.predicate.term, assumption_projection_pred.term)?;
ecx.validate_alias_bound_self_from_param_env(goal)
})
} else {
Err(NoSolution)
}
}
fn consider_object_bound_candidate(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'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()
{
ecx.probe(|ecx| {
let tcx = ecx.tcx();
let assumption_projection_pred =
ecx.instantiate_binder_with_infer(poly_projection_pred);
ecx.eq(
goal.param_env,
goal.predicate.projection_ty,
assumption_projection_pred.projection_ty,
)?;
let ty::Dynamic(bounds, _, _) = *goal.predicate.self_ty().kind() else {
bug!("expected object type in `consider_object_bound_candidate`");
};
ecx.add_goals(
structural_traits::predicates_for_object_candidate(
&ecx,
goal.param_env,
goal.predicate.projection_ty.trait_ref(tcx),
bounds,
)
.into_iter()
.map(|pred| goal.with(tcx, pred)),
);
ecx.eq(goal.param_env, goal.predicate.term, assumption_projection_pred.term)
.expect("expected goal term to be fully unconstrained");
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
then(ecx)
})
} else {
Err(NoSolution)

View File

@ -78,11 +78,11 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
})
}
fn consider_implied_clause(
fn probe_and_match_goal_against_assumption(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'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()
@ -97,72 +97,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
goal.predicate.trait_ref,
assumption_trait_pred.trait_ref,
)?;
ecx.add_goals(requirements);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
} else {
Err(NoSolution)
}
}
fn consider_alias_bound_candidate(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
) -> QueryResult<'tcx> {
if let Some(poly_trait_pred) = assumption.to_opt_poly_trait_pred()
&& poly_trait_pred.def_id() == goal.predicate.def_id()
{
// FIXME: Constness and polarity
ecx.probe(|ecx| {
let assumption_trait_pred =
ecx.instantiate_binder_with_infer(poly_trait_pred);
ecx.eq(
goal.param_env,
goal.predicate.trait_ref,
assumption_trait_pred.trait_ref,
)?;
ecx.validate_alias_bound_self_from_param_env(goal)
})
} else {
Err(NoSolution)
}
}
fn consider_object_bound_candidate(
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'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
{
// FIXME: Constness and polarity
ecx.probe(|ecx| {
let assumption_trait_pred =
ecx.instantiate_binder_with_infer(poly_trait_pred);
ecx.eq(
goal.param_env,
goal.predicate.trait_ref,
assumption_trait_pred.trait_ref,
)?;
let tcx = ecx.tcx();
let ty::Dynamic(bounds, _, _) = *goal.predicate.self_ty().kind() else {
bug!("expected object type in `consider_object_bound_candidate`");
};
ecx.add_goals(
structural_traits::predicates_for_object_candidate(
&ecx,
goal.param_env,
goal.predicate.trait_ref,
bounds,
)
.into_iter()
.map(|pred| goal.with(tcx, pred)),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
then(ecx)
})
} else {
Err(NoSolution)