1
Fork 0

Take proof trees by value in inspect goal

This commit is contained in:
Michael Goulet 2024-04-29 11:16:21 -04:00
parent a8a1d3a771
commit 13825dcc15
2 changed files with 15 additions and 18 deletions

View file

@ -60,14 +60,14 @@ pub struct GoalEvaluation<'tcx> {
pub evaluation: CanonicalGoalEvaluation<'tcx>, pub evaluation: CanonicalGoalEvaluation<'tcx>,
} }
#[derive(Eq, PartialEq)] #[derive(Eq, PartialEq, Debug)]
pub struct CanonicalGoalEvaluation<'tcx> { pub struct CanonicalGoalEvaluation<'tcx> {
pub goal: CanonicalInput<'tcx>, pub goal: CanonicalInput<'tcx>,
pub kind: CanonicalGoalEvaluationKind<'tcx>, pub kind: CanonicalGoalEvaluationKind<'tcx>,
pub result: QueryResult<'tcx>, pub result: QueryResult<'tcx>,
} }
#[derive(Eq, PartialEq)] #[derive(Eq, PartialEq, Debug)]
pub enum CanonicalGoalEvaluationKind<'tcx> { pub enum CanonicalGoalEvaluationKind<'tcx> {
Overflow, Overflow,
CycleInStack, CycleInStack,
@ -86,7 +86,7 @@ pub struct AddedGoalsEvaluation<'tcx> {
pub result: Result<Certainty, NoSolution>, pub result: Result<Certainty, NoSolution>,
} }
#[derive(Eq, PartialEq)] #[derive(Eq, PartialEq, Debug)]
pub struct GoalEvaluationStep<'tcx> { pub struct GoalEvaluationStep<'tcx> {
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>, pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,

View file

@ -34,9 +34,9 @@ pub struct InspectConfig {
pub struct InspectGoal<'a, 'tcx> { pub struct InspectGoal<'a, 'tcx> {
infcx: &'a InferCtxt<'tcx>, infcx: &'a InferCtxt<'tcx>,
depth: usize, depth: usize,
orig_values: &'a [ty::GenericArg<'tcx>], orig_values: Vec<ty::GenericArg<'tcx>>,
goal: Goal<'tcx, ty::Predicate<'tcx>>, goal: Goal<'tcx, ty::Predicate<'tcx>>,
evaluation: &'a inspect::GoalEvaluation<'tcx>, evaluation: inspect::CanonicalGoalEvaluation<'tcx>,
} }
pub struct InspectCandidate<'a, 'tcx> { pub struct InspectCandidate<'a, 'tcx> {
@ -139,7 +139,7 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
try_visit!(visitor.visit_goal(&InspectGoal::new( try_visit!(visitor.visit_goal(&InspectGoal::new(
infcx, infcx,
self.goal.depth + 1, self.goal.depth + 1,
&proof_tree.unwrap(), proof_tree.unwrap(),
))); )));
} }
} }
@ -164,7 +164,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
} }
pub fn result(&self) -> Result<Certainty, NoSolution> { pub fn result(&self) -> Result<Certainty, NoSolution> {
self.evaluation.evaluation.result.map(|c| c.value.certainty) self.evaluation.result.map(|c| c.value.certainty)
} }
fn candidates_recur( fn candidates_recur(
@ -221,7 +221,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
pub fn candidates(&'a self) -> Vec<InspectCandidate<'a, 'tcx>> { pub fn candidates(&'a self) -> Vec<InspectCandidate<'a, 'tcx>> {
let mut candidates = vec![]; let mut candidates = vec![];
let last_eval_step = match self.evaluation.evaluation.kind { let last_eval_step = match self.evaluation.kind {
inspect::CanonicalGoalEvaluationKind::Overflow inspect::CanonicalGoalEvaluationKind::Overflow
| inspect::CanonicalGoalEvaluationKind::CycleInStack | inspect::CanonicalGoalEvaluationKind::CycleInStack
| inspect::CanonicalGoalEvaluationKind::ProvisionalCacheHit => { | inspect::CanonicalGoalEvaluationKind::ProvisionalCacheHit => {
@ -254,18 +254,15 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
candidates.pop().filter(|_| candidates.is_empty()) candidates.pop().filter(|_| candidates.is_empty())
} }
fn new( fn new(infcx: &'a InferCtxt<'tcx>, depth: usize, root: inspect::GoalEvaluation<'tcx>) -> Self {
infcx: &'a InferCtxt<'tcx>, let inspect::GoalEvaluation { uncanonicalized_goal, kind, evaluation } = root;
depth: usize, match kind {
root: &'a inspect::GoalEvaluation<'tcx>, inspect::GoalEvaluationKind::Root { orig_values } => InspectGoal {
) -> Self {
match root.kind {
inspect::GoalEvaluationKind::Root { ref orig_values } => InspectGoal {
infcx, infcx,
depth, depth,
orig_values, orig_values,
goal: root.uncanonicalized_goal.fold_with(&mut EagerResolver::new(infcx)), goal: uncanonicalized_goal.fold_with(&mut EagerResolver::new(infcx)),
evaluation: root, evaluation,
}, },
inspect::GoalEvaluationKind::Nested { .. } => unreachable!(), inspect::GoalEvaluationKind::Nested { .. } => unreachable!(),
} }
@ -294,6 +291,6 @@ impl<'tcx> InferCtxt<'tcx> {
) -> V::Result { ) -> V::Result {
let (_, proof_tree) = self.evaluate_root_goal(goal, GenerateProofTree::Yes); let (_, proof_tree) = self.evaluate_root_goal(goal, GenerateProofTree::Yes);
let proof_tree = proof_tree.unwrap(); let proof_tree = proof_tree.unwrap();
visitor.visit_goal(&InspectGoal::new(self, 0, &proof_tree)) visitor.visit_goal(&InspectGoal::new(self, 0, proof_tree))
} }
} }