SolverDelegate

This commit is contained in:
Michael Goulet
2024-06-17 11:58:38 -04:00
parent e7d2d95e5a
commit baf94bddf0
24 changed files with 363 additions and 310 deletions

View File

@@ -23,6 +23,7 @@ use rustc_next_trait_solver::resolve::EagerResolver;
use rustc_span::{Span, DUMMY_SP};
use crate::solve::eval_ctxt::canonical;
use crate::solve::infcx::SolverDelegate;
use crate::solve::{EvalCtxt, GoalEvaluationKind, GoalSource};
use crate::solve::{GenerateProofTree, InferCtxtEvalExt};
use crate::traits::ObligationCtxt;
@@ -199,8 +200,9 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
let _ = term_hack.constrain(infcx, span, param_env);
}
let opt_impl_args =
opt_impl_args.map(|impl_args| impl_args.fold_with(&mut EagerResolver::new(infcx)));
let opt_impl_args = opt_impl_args.map(|impl_args| {
impl_args.fold_with(&mut EagerResolver::new(<&SolverDelegate<'tcx>>::from(infcx)))
});
let goals = instantiated_goals
.into_iter()
@@ -403,7 +405,8 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
infcx,
depth,
orig_values,
goal: uncanonicalized_goal.fold_with(&mut EagerResolver::new(infcx)),
goal: uncanonicalized_goal
.fold_with(&mut EagerResolver::new(<&SolverDelegate<'tcx>>::from(infcx))),
result,
evaluation_kind: evaluation.kind,
normalizes_to_term_hack,

View File

@@ -9,10 +9,11 @@ use std::mem;
use crate::solve::eval_ctxt::canonical;
use crate::solve::{self, inspect, GenerateProofTree};
use rustc_middle::bug;
use rustc_next_trait_solver::infcx::SolverDelegate;
use rustc_next_trait_solver::solve::{
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
};
use rustc_type_ir::{self as ty, InferCtxtLike, Interner};
use rustc_type_ir::{self as ty, Interner};
/// The core data structure when building proof trees.
///
@@ -34,9 +35,9 @@ use rustc_type_ir::{self as ty, InferCtxtLike, Interner};
/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
/// is called to recursively convert the whole structure to a
/// finished proof tree.
pub(in crate::solve) struct ProofTreeBuilder<Infcx, I = <Infcx as InferCtxtLike>::Interner>
pub(in crate::solve) struct ProofTreeBuilder<Infcx, I = <Infcx as SolverDelegate>::Interner>
where
Infcx: InferCtxtLike<Interner = I>,
Infcx: SolverDelegate<Interner = I>,
I: Interner,
{
_infcx: PhantomData<Infcx>,
@@ -232,7 +233,7 @@ impl<I: Interner> WipProbeStep<I> {
}
}
impl<Infcx: InferCtxtLike<Interner = I>, I: Interner> ProofTreeBuilder<Infcx> {
impl<Infcx: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<Infcx> {
fn new(state: impl Into<DebugSolver<I>>) -> ProofTreeBuilder<Infcx> {
ProofTreeBuilder { state: Some(Box::new(state.into())), _infcx: PhantomData }
}