1
Fork 0

Fix impl for SolverDelegate

This commit is contained in:
Michael Goulet 2024-06-17 19:09:46 -04:00
parent 532149eb88
commit 7d2be888b6
11 changed files with 385 additions and 85 deletions

View file

@ -9,6 +9,8 @@ pub trait SolverDelegate: Sized {
type Interner: Interner;
fn interner(&self) -> Self::Interner;
type Span: Copy;
fn solver_mode(&self) -> SolverMode;
fn build_with_canonical<V>(
@ -57,6 +59,12 @@ pub trait SolverDelegate: Sized {
def_id: <Self::Interner as Interner>::DefId,
) -> <Self::Interner as Interner>::GenericArgs;
fn fresh_var_for_kind_with_span(
&self,
arg: <Self::Interner as Interner>::GenericArg,
span: Self::Span,
) -> <Self::Interner as Interner>::GenericArg;
fn instantiate_binder_with_infer<T: TypeFoldable<Self::Interner> + Copy>(
&self,
value: ty::Binder<Self::Interner, T>,

View file

@ -394,3 +394,35 @@ where
state,
)
}
// FIXME: needs to be pub to be accessed by downstream
// `rustc_trait_selection::solve::inspect::analyse`.
pub fn instantiate_canonical_state<Infcx, I, T: TypeFoldable<I>>(
infcx: &Infcx,
span: Infcx::Span,
param_env: I::ParamEnv,
orig_values: &mut Vec<I::GenericArg>,
state: inspect::CanonicalState<I, T>,
) -> T
where
Infcx: SolverDelegate<Interner = I>,
I: Interner,
{
// In case any fresh inference variables have been created between `state`
// and the previous instantiation, extend `orig_values` for it.
assert!(orig_values.len() <= state.value.var_values.len());
for &arg in &state.value.var_values.var_values[orig_values.len()..state.value.var_values.len()]
{
// FIXME: This is so ugly.
let unconstrained = infcx.fresh_var_for_kind_with_span(arg, span);
orig_values.push(unconstrained);
}
let instantiation =
EvalCtxt::compute_query_response_instantiation_values(infcx, orig_values, &state);
let inspect::State { var_values, data } = infcx.instantiate_canonical(state, instantiation);
EvalCtxt::unify_query_var_values(infcx, param_env, orig_values, var_values);
data
}

View file

@ -127,6 +127,17 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
generate_proof_tree: GenerateProofTree,
) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<Self::Interner>>);
// FIXME: This is only exposed because we need to use it in `analyse.rs`
// which is not yet uplifted. Once that's done, we should remove this.
fn evaluate_root_goal_raw(
&self,
goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
generate_proof_tree: GenerateProofTree,
) -> (
Result<(NestedNormalizationGoals<Self::Interner>, bool, Certainty), NoSolution>,
Option<inspect::GoalEvaluation<Self::Interner>>,
);
}
impl<Infcx, I> SolverDelegateEvalExt for Infcx
@ -148,6 +159,20 @@ where
ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
})
}
#[instrument(level = "debug", skip(self))]
fn evaluate_root_goal_raw(
&self,
goal: Goal<I, I::Predicate>,
generate_proof_tree: GenerateProofTree,
) -> (
Result<(NestedNormalizationGoals<I>, bool, Certainty), NoSolution>,
Option<inspect::GoalEvaluation<I>>,
) {
EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Misc, goal)
})
}
}
impl<'a, Infcx, I> EvalCtxt<'a, Infcx>

View file

@ -2,3 +2,5 @@ pub use rustc_type_ir::solve::inspect::*;
mod build;
pub(in crate::solve) use build::*;
pub use crate::solve::eval_ctxt::canonical::instantiate_canonical_state;

View file

@ -12,7 +12,7 @@ use crate::solve::{
};
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub struct Limit(usize);
pub struct SolverLimit(usize);
rustc_index::newtype_index! {
#[orderable]
@ -35,7 +35,7 @@ bitflags::bitflags! {
struct StackEntry<I: Interner> {
input: CanonicalInput<I>,
available_depth: Limit,
available_depth: SolverLimit,
/// The maximum depth reached by this stack entry, only up-to date
/// for the top of the stack and lazily updated for the rest.
@ -164,19 +164,19 @@ impl<I: Interner> SearchGraph<I> {
fn allowed_depth_for_nested(
tcx: I,
stack: &IndexVec<StackDepth, StackEntry<I>>,
) -> Option<Limit> {
) -> Option<SolverLimit> {
if let Some(last) = stack.raw.last() {
if last.available_depth.0 == 0 {
return None;
}
Some(if last.encountered_overflow {
Limit(last.available_depth.0 / 4)
SolverLimit(last.available_depth.0 / 4)
} else {
Limit(last.available_depth.0 - 1)
SolverLimit(last.available_depth.0 - 1)
})
} else {
Some(Limit(tcx.recursion_limit()))
Some(SolverLimit(tcx.recursion_limit()))
}
}
@ -414,12 +414,12 @@ impl<I: Interner> SearchGraph<I> {
&mut self,
tcx: I,
input: CanonicalInput<I>,
available_depth: Limit,
available_depth: SolverLimit,
inspect: &mut ProofTreeBuilder<Infcx>,
) -> Option<QueryResult<I>> {
let CacheData { result, proof_tree, additional_depth, encountered_overflow } = self
.global_cache(tcx)
// TODO: Awkward `Limit -> usize -> Limit`.
// FIXME: Awkward `Limit -> usize -> Limit`.
.get(tcx, input, self.stack.iter().map(|e| e.input), available_depth.0)?;
// If we're building a proof tree and the current cache entry does not