Make proof tree building generic
This commit is contained in:
parent
0f528a4c08
commit
6ee22e184f
@ -4759,6 +4759,7 @@ name = "rustc_trait_selection"
|
|||||||
version = "0.0.0"
|
version = "0.0.0"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"bitflags 2.5.0",
|
"bitflags 2.5.0",
|
||||||
|
"derivative",
|
||||||
"itertools 0.12.1",
|
"itertools 0.12.1",
|
||||||
"rustc_ast",
|
"rustc_ast",
|
||||||
"rustc_ast_ir",
|
"rustc_ast_ir",
|
||||||
@ -4778,6 +4779,7 @@ dependencies = [
|
|||||||
"rustc_span",
|
"rustc_span",
|
||||||
"rustc_target",
|
"rustc_target",
|
||||||
"rustc_transmute",
|
"rustc_transmute",
|
||||||
|
"rustc_type_ir",
|
||||||
"smallvec",
|
"smallvec",
|
||||||
"tracing",
|
"tracing",
|
||||||
]
|
]
|
||||||
|
@ -6,6 +6,7 @@ edition = "2021"
|
|||||||
[dependencies]
|
[dependencies]
|
||||||
# tidy-alphabetical-start
|
# tidy-alphabetical-start
|
||||||
bitflags = "2.4.1"
|
bitflags = "2.4.1"
|
||||||
|
derivative = "2.2.0"
|
||||||
itertools = "0.12"
|
itertools = "0.12"
|
||||||
rustc_ast = { path = "../rustc_ast" }
|
rustc_ast = { path = "../rustc_ast" }
|
||||||
rustc_ast_ir = { path = "../rustc_ast_ir" }
|
rustc_ast_ir = { path = "../rustc_ast_ir" }
|
||||||
@ -25,6 +26,7 @@ rustc_session = { path = "../rustc_session" }
|
|||||||
rustc_span = { path = "../rustc_span" }
|
rustc_span = { path = "../rustc_span" }
|
||||||
rustc_target = { path = "../rustc_target" }
|
rustc_target = { path = "../rustc_target" }
|
||||||
rustc_transmute = { path = "../rustc_transmute", features = ["rustc"] }
|
rustc_transmute = { path = "../rustc_transmute", features = ["rustc"] }
|
||||||
|
rustc_type_ir = { path = "../rustc_type_ir" }
|
||||||
smallvec = { version = "1.8.1", features = ["union", "may_dangle"] }
|
smallvec = { version = "1.8.1", features = ["union", "may_dangle"] }
|
||||||
tracing = "0.1"
|
tracing = "0.1"
|
||||||
# tidy-alphabetical-end
|
# tidy-alphabetical-end
|
||||||
|
@ -95,7 +95,7 @@ pub struct EvalCtxt<'a, 'tcx> {
|
|||||||
// evaluation code.
|
// evaluation code.
|
||||||
tainted: Result<(), NoSolution>,
|
tainted: Result<(), NoSolution>,
|
||||||
|
|
||||||
pub(super) inspect: ProofTreeBuilder<'tcx>,
|
pub(super) inspect: ProofTreeBuilder<TyCtxt<'tcx>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(derivative::Derivative)]
|
#[derive(derivative::Derivative)]
|
||||||
@ -225,7 +225,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
search_graph: &'a mut search_graph::SearchGraph<'tcx>,
|
search_graph: &'a mut search_graph::SearchGraph<'tcx>,
|
||||||
canonical_input: CanonicalInput<'tcx>,
|
canonical_input: CanonicalInput<'tcx>,
|
||||||
canonical_goal_evaluation: &mut ProofTreeBuilder<'tcx>,
|
canonical_goal_evaluation: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
||||||
f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>, Goal<'tcx, ty::Predicate<'tcx>>) -> R,
|
f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>, Goal<'tcx, ty::Predicate<'tcx>>) -> R,
|
||||||
) -> R {
|
) -> R {
|
||||||
let intercrate = match search_graph.solver_mode() {
|
let intercrate = match search_graph.solver_mode() {
|
||||||
@ -287,7 +287,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
search_graph: &'a mut search_graph::SearchGraph<'tcx>,
|
search_graph: &'a mut search_graph::SearchGraph<'tcx>,
|
||||||
canonical_input: CanonicalInput<'tcx>,
|
canonical_input: CanonicalInput<'tcx>,
|
||||||
goal_evaluation: &mut ProofTreeBuilder<'tcx>,
|
goal_evaluation: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
||||||
) -> QueryResult<'tcx> {
|
) -> QueryResult<'tcx> {
|
||||||
let mut canonical_goal_evaluation =
|
let mut canonical_goal_evaluation =
|
||||||
goal_evaluation.new_canonical_goal_evaluation(canonical_input);
|
goal_evaluation.new_canonical_goal_evaluation(canonical_input);
|
||||||
|
@ -9,11 +9,12 @@ use rustc_infer::infer::InferCtxt;
|
|||||||
use rustc_middle::bug;
|
use rustc_middle::bug;
|
||||||
use rustc_middle::infer::canonical::CanonicalVarValues;
|
use rustc_middle::infer::canonical::CanonicalVarValues;
|
||||||
use rustc_middle::traits::query::NoSolution;
|
use rustc_middle::traits::query::NoSolution;
|
||||||
use rustc_middle::traits::solve::{
|
use rustc_middle::ty::{self, TyCtxt};
|
||||||
|
use rustc_next_trait_solver::solve::{
|
||||||
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
|
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
|
||||||
};
|
};
|
||||||
use rustc_middle::ty::{self, TyCtxt};
|
|
||||||
use rustc_session::config::DumpSolverProofTree;
|
use rustc_session::config::DumpSolverProofTree;
|
||||||
|
use rustc_type_ir::Interner;
|
||||||
|
|
||||||
use crate::solve::eval_ctxt::canonical;
|
use crate::solve::eval_ctxt::canonical;
|
||||||
use crate::solve::{self, inspect, GenerateProofTree};
|
use crate::solve::{self, inspect, GenerateProofTree};
|
||||||
@ -38,49 +39,51 @@ use crate::solve::{self, inspect, GenerateProofTree};
|
|||||||
/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
|
/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
|
||||||
/// is called to recursively convert the whole structure to a
|
/// is called to recursively convert the whole structure to a
|
||||||
/// finished proof tree.
|
/// finished proof tree.
|
||||||
pub(in crate::solve) struct ProofTreeBuilder<'tcx> {
|
pub(in crate::solve) struct ProofTreeBuilder<I: Interner> {
|
||||||
state: Option<Box<DebugSolver<'tcx>>>,
|
state: Option<Box<DebugSolver<I>>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
/// The current state of the proof tree builder, at most places
|
/// The current state of the proof tree builder, at most places
|
||||||
/// in the code, only one or two variants are actually possible.
|
/// in the code, only one or two variants are actually possible.
|
||||||
///
|
///
|
||||||
/// We simply ICE in case that assumption is broken.
|
/// We simply ICE in case that assumption is broken.
|
||||||
#[derive(Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
enum DebugSolver<'tcx> {
|
#[derivative(Debug(bound = ""))]
|
||||||
|
enum DebugSolver<I: Interner> {
|
||||||
Root,
|
Root,
|
||||||
GoalEvaluation(WipGoalEvaluation<'tcx>),
|
GoalEvaluation(WipGoalEvaluation<I>),
|
||||||
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<'tcx>),
|
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<I>),
|
||||||
GoalEvaluationStep(WipGoalEvaluationStep<'tcx>),
|
GoalEvaluationStep(WipGoalEvaluationStep<I>),
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> From<WipGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
|
impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
|
||||||
fn from(g: WipGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
|
fn from(g: WipGoalEvaluation<I>) -> DebugSolver<I> {
|
||||||
DebugSolver::GoalEvaluation(g)
|
DebugSolver::GoalEvaluation(g)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> From<WipCanonicalGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
|
impl<I: Interner> From<WipCanonicalGoalEvaluation<I>> for DebugSolver<I> {
|
||||||
fn from(g: WipCanonicalGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
|
fn from(g: WipCanonicalGoalEvaluation<I>) -> DebugSolver<I> {
|
||||||
DebugSolver::CanonicalGoalEvaluation(g)
|
DebugSolver::CanonicalGoalEvaluation(g)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> From<WipGoalEvaluationStep<'tcx>> for DebugSolver<'tcx> {
|
impl<I: Interner> From<WipGoalEvaluationStep<I>> for DebugSolver<I> {
|
||||||
fn from(g: WipGoalEvaluationStep<'tcx>) -> DebugSolver<'tcx> {
|
fn from(g: WipGoalEvaluationStep<I>) -> DebugSolver<I> {
|
||||||
DebugSolver::GoalEvaluationStep(g)
|
DebugSolver::GoalEvaluationStep(g)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
struct WipGoalEvaluation<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
struct WipGoalEvaluation<I: Interner> {
|
||||||
pub kind: WipGoalEvaluationKind<'tcx>,
|
pub uncanonicalized_goal: Goal<I, I::Predicate>,
|
||||||
pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
|
pub kind: WipGoalEvaluationKind<I>,
|
||||||
|
pub evaluation: Option<WipCanonicalGoalEvaluation<I>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipGoalEvaluation<'tcx> {
|
impl<I: Interner> WipGoalEvaluation<I> {
|
||||||
fn finalize(self) -> inspect::GoalEvaluation<TyCtxt<'tcx>> {
|
fn finalize(self) -> inspect::GoalEvaluation<I> {
|
||||||
inspect::GoalEvaluation {
|
inspect::GoalEvaluation {
|
||||||
uncanonicalized_goal: self.uncanonicalized_goal,
|
uncanonicalized_goal: self.uncanonicalized_goal,
|
||||||
kind: match self.kind {
|
kind: match self.kind {
|
||||||
@ -94,21 +97,23 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
pub(in crate::solve) enum WipGoalEvaluationKind<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||||
Root { orig_values: Vec<ty::GenericArg<'tcx>> },
|
pub(in crate::solve) enum WipGoalEvaluationKind<I: Interner> {
|
||||||
|
Root { orig_values: Vec<I::GenericArg> },
|
||||||
Nested,
|
Nested,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq)]
|
#[derive(derivative::Derivative)]
|
||||||
pub(in crate::solve) enum WipCanonicalGoalEvaluationKind<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""))]
|
||||||
|
pub(in crate::solve) enum WipCanonicalGoalEvaluationKind<I: Interner> {
|
||||||
Overflow,
|
Overflow,
|
||||||
CycleInStack,
|
CycleInStack,
|
||||||
ProvisionalCacheHit,
|
ProvisionalCacheHit,
|
||||||
Interned { revisions: &'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>] },
|
Interned { revisions: I::GoalEvaluationSteps },
|
||||||
}
|
}
|
||||||
|
|
||||||
impl std::fmt::Debug for WipCanonicalGoalEvaluationKind<'_> {
|
impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Self::Overflow => write!(f, "Overflow"),
|
Self::Overflow => write!(f, "Overflow"),
|
||||||
@ -119,18 +124,19 @@ impl std::fmt::Debug for WipCanonicalGoalEvaluationKind<'_> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
struct WipCanonicalGoalEvaluation<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||||
goal: CanonicalInput<'tcx>,
|
struct WipCanonicalGoalEvaluation<I: Interner> {
|
||||||
kind: Option<WipCanonicalGoalEvaluationKind<'tcx>>,
|
goal: CanonicalInput<I>,
|
||||||
|
kind: Option<WipCanonicalGoalEvaluationKind<I>>,
|
||||||
/// Only used for uncached goals. After we finished evaluating
|
/// Only used for uncached goals. After we finished evaluating
|
||||||
/// the goal, this is interned and moved into `kind`.
|
/// the goal, this is interned and moved into `kind`.
|
||||||
revisions: Vec<WipGoalEvaluationStep<'tcx>>,
|
revisions: Vec<WipGoalEvaluationStep<I>>,
|
||||||
result: Option<QueryResult<'tcx>>,
|
result: Option<QueryResult<I>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
|
impl<I: Interner> WipCanonicalGoalEvaluation<I> {
|
||||||
fn finalize(self) -> inspect::CanonicalGoalEvaluation<TyCtxt<'tcx>> {
|
fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
|
||||||
assert!(self.revisions.is_empty());
|
assert!(self.revisions.is_empty());
|
||||||
let kind = match self.kind.unwrap() {
|
let kind = match self.kind.unwrap() {
|
||||||
WipCanonicalGoalEvaluationKind::Overflow => {
|
WipCanonicalGoalEvaluationKind::Overflow => {
|
||||||
@ -151,14 +157,15 @@ impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
struct WipAddedGoalsEvaluation<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||||
evaluations: Vec<Vec<WipGoalEvaluation<'tcx>>>,
|
struct WipAddedGoalsEvaluation<I: Interner> {
|
||||||
|
evaluations: Vec<Vec<WipGoalEvaluation<I>>>,
|
||||||
result: Option<Result<Certainty, NoSolution>>,
|
result: Option<Result<Certainty, NoSolution>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
|
impl<I: Interner> WipAddedGoalsEvaluation<I> {
|
||||||
fn finalize(self) -> inspect::AddedGoalsEvaluation<TyCtxt<'tcx>> {
|
fn finalize(self) -> inspect::AddedGoalsEvaluation<I> {
|
||||||
inspect::AddedGoalsEvaluation {
|
inspect::AddedGoalsEvaluation {
|
||||||
evaluations: self
|
evaluations: self
|
||||||
.evaluations
|
.evaluations
|
||||||
@ -172,22 +179,23 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
struct WipGoalEvaluationStep<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||||
|
struct WipGoalEvaluationStep<I: Interner> {
|
||||||
/// Unlike `EvalCtxt::var_values`, we append a new
|
/// Unlike `EvalCtxt::var_values`, we append a new
|
||||||
/// generic arg here whenever we create a new inference
|
/// generic arg here whenever we create a new inference
|
||||||
/// variable.
|
/// variable.
|
||||||
///
|
///
|
||||||
/// This is necessary as we otherwise don't unify these
|
/// This is necessary as we otherwise don't unify these
|
||||||
/// vars when instantiating multiple `CanonicalState`.
|
/// vars when instantiating multiple `CanonicalState`.
|
||||||
var_values: Vec<ty::GenericArg<'tcx>>,
|
var_values: Vec<I::GenericArg>,
|
||||||
instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
instantiated_goal: QueryInput<I, I::Predicate>,
|
||||||
probe_depth: usize,
|
probe_depth: usize,
|
||||||
evaluation: WipProbe<'tcx>,
|
evaluation: WipProbe<I>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
impl<I: Interner> WipGoalEvaluationStep<I> {
|
||||||
fn current_evaluation_scope(&mut self) -> &mut WipProbe<'tcx> {
|
fn current_evaluation_scope(&mut self) -> &mut WipProbe<I> {
|
||||||
let mut current = &mut self.evaluation;
|
let mut current = &mut self.evaluation;
|
||||||
for _ in 0..self.probe_depth {
|
for _ in 0..self.probe_depth {
|
||||||
match current.steps.last_mut() {
|
match current.steps.last_mut() {
|
||||||
@ -198,7 +206,7 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
|||||||
current
|
current
|
||||||
}
|
}
|
||||||
|
|
||||||
fn added_goals_evaluation(&mut self) -> &mut WipAddedGoalsEvaluation<'tcx> {
|
fn added_goals_evaluation(&mut self) -> &mut WipAddedGoalsEvaluation<I> {
|
||||||
let mut current = &mut self.evaluation;
|
let mut current = &mut self.evaluation;
|
||||||
loop {
|
loop {
|
||||||
match current.steps.last_mut() {
|
match current.steps.last_mut() {
|
||||||
@ -209,7 +217,7 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn finalize(self) -> inspect::GoalEvaluationStep<TyCtxt<'tcx>> {
|
fn finalize(self) -> inspect::GoalEvaluationStep<I> {
|
||||||
let evaluation = self.evaluation.finalize();
|
let evaluation = self.evaluation.finalize();
|
||||||
match evaluation.kind {
|
match evaluation.kind {
|
||||||
inspect::ProbeKind::Root { .. } => (),
|
inspect::ProbeKind::Root { .. } => (),
|
||||||
@ -219,16 +227,17 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
struct WipProbe<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||||
|
struct WipProbe<I: Interner> {
|
||||||
initial_num_var_values: usize,
|
initial_num_var_values: usize,
|
||||||
steps: Vec<WipProbeStep<'tcx>>,
|
steps: Vec<WipProbeStep<I>>,
|
||||||
kind: Option<inspect::ProbeKind<TyCtxt<'tcx>>>,
|
kind: Option<inspect::ProbeKind<I>>,
|
||||||
final_state: Option<inspect::CanonicalState<TyCtxt<'tcx>, ()>>,
|
final_state: Option<inspect::CanonicalState<I, ()>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipProbe<'tcx> {
|
impl<I: Interner> WipProbe<I> {
|
||||||
fn finalize(self) -> inspect::Probe<TyCtxt<'tcx>> {
|
fn finalize(self) -> inspect::Probe<I> {
|
||||||
inspect::Probe {
|
inspect::Probe {
|
||||||
steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
|
steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
|
||||||
kind: self.kind.unwrap(),
|
kind: self.kind.unwrap(),
|
||||||
@ -237,17 +246,18 @@ impl<'tcx> WipProbe<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Debug)]
|
#[derive(derivative::Derivative)]
|
||||||
enum WipProbeStep<'tcx> {
|
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||||
AddGoal(GoalSource, inspect::CanonicalState<TyCtxt<'tcx>, Goal<'tcx, ty::Predicate<'tcx>>>),
|
enum WipProbeStep<I: Interner> {
|
||||||
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
|
AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, I::Predicate>>),
|
||||||
NestedProbe(WipProbe<'tcx>),
|
EvaluateGoals(WipAddedGoalsEvaluation<I>),
|
||||||
|
NestedProbe(WipProbe<I>),
|
||||||
MakeCanonicalResponse { shallow_certainty: Certainty },
|
MakeCanonicalResponse { shallow_certainty: Certainty },
|
||||||
RecordImplArgs { impl_args: inspect::CanonicalState<TyCtxt<'tcx>, ty::GenericArgsRef<'tcx>> },
|
RecordImplArgs { impl_args: inspect::CanonicalState<I, I::GenericArgs> },
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> WipProbeStep<'tcx> {
|
impl<I: Interner> WipProbeStep<I> {
|
||||||
fn finalize(self) -> inspect::ProbeStep<TyCtxt<'tcx>> {
|
fn finalize(self) -> inspect::ProbeStep<I> {
|
||||||
match self {
|
match self {
|
||||||
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
|
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
|
||||||
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
||||||
@ -262,20 +272,21 @@ impl<'tcx> WipProbeStep<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> ProofTreeBuilder<'tcx> {
|
// FIXME: Genericize this impl.
|
||||||
fn new(state: impl Into<DebugSolver<'tcx>>) -> ProofTreeBuilder<'tcx> {
|
impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
|
fn new(state: impl Into<DebugSolver<TyCtxt<'tcx>>>) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
ProofTreeBuilder { state: Some(Box::new(state.into())) }
|
ProofTreeBuilder { state: Some(Box::new(state.into())) }
|
||||||
}
|
}
|
||||||
|
|
||||||
fn nested<T: Into<DebugSolver<'tcx>>>(&self, state: impl FnOnce() -> T) -> Self {
|
fn nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(&self, state: impl FnOnce() -> T) -> Self {
|
||||||
ProofTreeBuilder { state: self.state.as_ref().map(|_| Box::new(state().into())) }
|
ProofTreeBuilder { state: self.state.as_ref().map(|_| Box::new(state().into())) }
|
||||||
}
|
}
|
||||||
|
|
||||||
fn as_mut(&mut self) -> Option<&mut DebugSolver<'tcx>> {
|
fn as_mut(&mut self) -> Option<&mut DebugSolver<TyCtxt<'tcx>>> {
|
||||||
self.state.as_deref_mut()
|
self.state.as_deref_mut()
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<'tcx> {
|
pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
let mut nested = ProofTreeBuilder { state: self.state.take() };
|
let mut nested = ProofTreeBuilder { state: self.state.take() };
|
||||||
nested.enter_probe();
|
nested.enter_probe();
|
||||||
nested
|
nested
|
||||||
@ -293,7 +304,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
pub fn new_maybe_root(
|
pub fn new_maybe_root(
|
||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
generate_proof_tree: GenerateProofTree,
|
generate_proof_tree: GenerateProofTree,
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
match generate_proof_tree {
|
match generate_proof_tree {
|
||||||
GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
|
GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
|
||||||
GenerateProofTree::IfEnabled => {
|
GenerateProofTree::IfEnabled => {
|
||||||
@ -311,11 +322,11 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn new_root() -> ProofTreeBuilder<'tcx> {
|
pub fn new_root() -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
ProofTreeBuilder::new(DebugSolver::Root)
|
ProofTreeBuilder::new(DebugSolver::Root)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn new_noop() -> ProofTreeBuilder<'tcx> {
|
pub fn new_noop() -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
ProofTreeBuilder { state: None }
|
ProofTreeBuilder { state: None }
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -325,10 +336,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
|
|
||||||
pub(in crate::solve) fn new_goal_evaluation(
|
pub(in crate::solve) fn new_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
goal: Goal<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
|
||||||
orig_values: &[ty::GenericArg<'tcx>],
|
orig_values: &[ty::GenericArg<'tcx>],
|
||||||
kind: solve::GoalEvaluationKind,
|
kind: solve::GoalEvaluationKind,
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
self.nested(|| WipGoalEvaluation {
|
self.nested(|| WipGoalEvaluation {
|
||||||
uncanonicalized_goal: goal,
|
uncanonicalized_goal: goal,
|
||||||
kind: match kind {
|
kind: match kind {
|
||||||
@ -343,8 +354,8 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
|
|
||||||
pub fn new_canonical_goal_evaluation(
|
pub fn new_canonical_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
goal: CanonicalInput<'tcx>,
|
goal: CanonicalInput<TyCtxt<'tcx>>,
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
self.nested(|| WipCanonicalGoalEvaluation {
|
self.nested(|| WipCanonicalGoalEvaluation {
|
||||||
goal,
|
goal,
|
||||||
kind: None,
|
kind: None,
|
||||||
@ -371,7 +382,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn canonical_goal_evaluation(&mut self, canonical_goal_evaluation: ProofTreeBuilder<'tcx>) {
|
pub fn canonical_goal_evaluation(
|
||||||
|
&mut self,
|
||||||
|
canonical_goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>,
|
||||||
|
) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match (this, *canonical_goal_evaluation.state.unwrap()) {
|
match (this, *canonical_goal_evaluation.state.unwrap()) {
|
||||||
(
|
(
|
||||||
@ -386,7 +400,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<'tcx>) {
|
pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||||
@ -397,7 +411,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<'tcx>) {
|
pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match (this, *goal_evaluation.state.unwrap()) {
|
match (this, *goal_evaluation.state.unwrap()) {
|
||||||
(
|
(
|
||||||
@ -418,8 +432,8 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
pub fn new_goal_evaluation_step(
|
pub fn new_goal_evaluation_step(
|
||||||
&mut self,
|
&mut self,
|
||||||
var_values: CanonicalVarValues<'tcx>,
|
var_values: CanonicalVarValues<'tcx>,
|
||||||
instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
instantiated_goal: QueryInput<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
|
||||||
) -> ProofTreeBuilder<'tcx> {
|
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
self.nested(|| WipGoalEvaluationStep {
|
self.nested(|| WipGoalEvaluationStep {
|
||||||
var_values: var_values.var_values.to_vec(),
|
var_values: var_values.var_values.to_vec(),
|
||||||
instantiated_goal,
|
instantiated_goal,
|
||||||
@ -433,7 +447,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
|
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<TyCtxt<'tcx>>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match (this, *goal_evaluation_step.state.unwrap()) {
|
match (this, *goal_evaluation_step.state.unwrap()) {
|
||||||
(
|
(
|
||||||
@ -510,7 +524,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
&mut self,
|
&mut self,
|
||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &InferCtxt<'tcx>,
|
||||||
max_input_universe: ty::UniverseIndex,
|
max_input_universe: ty::UniverseIndex,
|
||||||
goal: Goal<'tcx, ty::NormalizesTo<'tcx>>,
|
goal: Goal<TyCtxt<'tcx>, ty::NormalizesTo<'tcx>>,
|
||||||
) {
|
) {
|
||||||
self.add_goal(
|
self.add_goal(
|
||||||
infcx,
|
infcx,
|
||||||
@ -525,7 +539,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &InferCtxt<'tcx>,
|
||||||
max_input_universe: ty::UniverseIndex,
|
max_input_universe: ty::UniverseIndex,
|
||||||
source: GoalSource,
|
source: GoalSource,
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
goal: Goal<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
|
||||||
) {
|
) {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
@ -579,7 +593,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn finish_probe(mut self) -> ProofTreeBuilder<'tcx> {
|
pub fn finish_probe(mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||||
@ -627,7 +641,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn query_result(&mut self, result: QueryResult<'tcx>) {
|
pub fn query_result(&mut self, result: QueryResult<TyCtxt<'tcx>>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||||
|
@ -253,8 +253,8 @@ impl<'tcx> SearchGraph<'tcx> {
|
|||||||
&mut self,
|
&mut self,
|
||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
input: CanonicalInput<'tcx>,
|
input: CanonicalInput<'tcx>,
|
||||||
inspect: &mut ProofTreeBuilder<'tcx>,
|
inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
||||||
mut prove_goal: impl FnMut(&mut Self, &mut ProofTreeBuilder<'tcx>) -> QueryResult<'tcx>,
|
mut prove_goal: impl FnMut(&mut Self, &mut ProofTreeBuilder<TyCtxt<'tcx>>) -> QueryResult<'tcx>,
|
||||||
) -> QueryResult<'tcx> {
|
) -> QueryResult<'tcx> {
|
||||||
// Check for overflow.
|
// Check for overflow.
|
||||||
let Some(available_depth) = Self::allowed_depth_for_nested(tcx, &self.stack) else {
|
let Some(available_depth) = Self::allowed_depth_for_nested(tcx, &self.stack) else {
|
||||||
|
Loading…
x
Reference in New Issue
Block a user