@@ -13,8 +13,7 @@ use rustc_type_ir::{self as ty, Interner};
13
13
use crate::delegate::SolverDelegate;
14
14
use crate::solve::eval_ctxt::canonical;
15
15
use crate::solve::{
16
- CanonicalInput, Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource,
17
- QueryResult, inspect,
16
+ Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource, QueryResult, inspect,
18
17
};
19
18
20
19
/// The core data structure when building proof trees.
54
53
enum DebugSolver<I: Interner> {
55
54
Root,
56
55
GoalEvaluation(WipGoalEvaluation<I>),
57
- CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<I>),
58
56
CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
59
57
}
60
58
@@ -64,12 +62,6 @@ impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
64
62
}
65
63
}
66
64
67
- impl<I: Interner> From<WipCanonicalGoalEvaluation<I>> for DebugSolver<I> {
68
- fn from(g: WipCanonicalGoalEvaluation<I>) -> DebugSolver<I> {
69
- DebugSolver::CanonicalGoalEvaluation(g)
70
- }
71
- }
72
-
73
65
impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
74
66
fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
75
67
DebugSolver::CanonicalGoalEvaluationStep(g)
@@ -80,39 +72,23 @@ impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
80
72
struct WipGoalEvaluation<I: Interner> {
81
73
pub uncanonicalized_goal: Goal<I, I::Predicate>,
82
74
pub orig_values: Vec<I::GenericArg>,
83
- pub evaluation: Option<WipCanonicalGoalEvaluation<I>>,
75
+ pub encountered_overflow: bool,
76
+ /// After we finished evaluating this is moved into `kind`.
77
+ pub final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
78
+ pub result: Option<QueryResult<I>>,
84
79
}
85
80
86
81
impl<I: Interner> WipGoalEvaluation<I> {
87
82
fn finalize(self) -> inspect::GoalEvaluation<I> {
88
83
inspect::GoalEvaluation {
89
84
uncanonicalized_goal: self.uncanonicalized_goal,
90
85
orig_values: self.orig_values,
91
- evaluation: self.evaluation.unwrap().finalize(),
92
- }
93
- }
94
- }
95
-
96
- #[derive_where(PartialEq, Eq, Debug; I: Interner)]
97
- struct WipCanonicalGoalEvaluation<I: Interner> {
98
- goal: CanonicalInput<I>,
99
- encountered_overflow: bool,
100
- /// Only used for uncached goals. After we finished evaluating
101
- /// the goal, this is interned and moved into `kind`.
102
- final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
103
- result: Option<QueryResult<I>>,
104
- }
105
-
106
- impl<I: Interner> WipCanonicalGoalEvaluation<I> {
107
- fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
108
- inspect::CanonicalGoalEvaluation {
109
- goal: self.goal,
110
86
kind: if self.encountered_overflow {
111
87
assert!(self.final_revision.is_none());
112
- inspect::CanonicalGoalEvaluationKind ::Overflow
88
+ inspect::GoalEvaluationKind ::Overflow
113
89
} else {
114
90
let final_revision = self.final_revision.unwrap().finalize();
115
- inspect::CanonicalGoalEvaluationKind ::Evaluation { final_revision }
91
+ inspect::GoalEvaluationKind ::Evaluation { final_revision }
116
92
},
117
93
result: self.result.unwrap(),
118
94
}
@@ -256,55 +232,27 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
256
232
257
233
pub(in crate::solve) fn new_goal_evaluation(
258
234
&mut self,
259
- goal : Goal<I, I::Predicate>,
235
+ uncanonicalized_goal : Goal<I, I::Predicate>,
260
236
orig_values: &[I::GenericArg],
261
237
kind: GoalEvaluationKind,
262
238
) -> ProofTreeBuilder<D> {
263
239
self.opt_nested(|| match kind {
264
240
GoalEvaluationKind::Root => Some(WipGoalEvaluation {
265
- uncanonicalized_goal: goal ,
241
+ uncanonicalized_goal,
266
242
orig_values: orig_values.to_vec(),
267
- evaluation: None,
243
+ encountered_overflow: false,
244
+ final_revision: None,
245
+ result: None,
268
246
}),
269
247
GoalEvaluationKind::Nested => None,
270
248
})
271
249
}
272
250
273
- pub(crate) fn new_canonical_goal_evaluation(
274
- &mut self,
275
- goal: CanonicalInput<I>,
276
- ) -> ProofTreeBuilder<D> {
277
- self.nested(|| WipCanonicalGoalEvaluation {
278
- goal,
279
- encountered_overflow: false,
280
- final_revision: None,
281
- result: None,
282
- })
283
- }
284
-
285
- pub(crate) fn canonical_goal_evaluation(
286
- &mut self,
287
- canonical_goal_evaluation: ProofTreeBuilder<D>,
288
- ) {
289
- if let Some(this) = self.as_mut() {
290
- match (this, *canonical_goal_evaluation.state.unwrap()) {
291
- (
292
- DebugSolver::GoalEvaluation(goal_evaluation),
293
- DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation),
294
- ) => {
295
- let prev = goal_evaluation.evaluation.replace(canonical_goal_evaluation);
296
- assert_eq!(prev, None);
297
- }
298
- _ => unreachable!(),
299
- }
300
- }
301
- }
302
-
303
251
pub(crate) fn canonical_goal_evaluation_overflow(&mut self) {
304
252
if let Some(this) = self.as_mut() {
305
253
match this {
306
- DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation ) => {
307
- canonical_goal_evaluation .encountered_overflow = true;
254
+ DebugSolver::GoalEvaluation(goal_evaluation ) => {
255
+ goal_evaluation .encountered_overflow = true;
308
256
}
309
257
_ => unreachable!(),
310
258
};
@@ -343,10 +291,10 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
343
291
if let Some(this) = self.as_mut() {
344
292
match (this, *goal_evaluation_step.state.unwrap()) {
345
293
(
346
- DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations ),
294
+ DebugSolver::GoalEvaluation(goal_evaluation ),
347
295
DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
348
296
) => {
349
- canonical_goal_evaluations .final_revision = Some(goal_evaluation_step);
297
+ goal_evaluation .final_revision = Some(goal_evaluation_step);
350
298
}
351
299
_ => unreachable!(),
352
300
}
@@ -489,8 +437,8 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
489
437
pub(crate) fn query_result(&mut self, result: QueryResult<I>) {
490
438
if let Some(this) = self.as_mut() {
491
439
match this {
492
- DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation ) => {
493
- assert_eq!(canonical_goal_evaluation .result.replace(result), None);
440
+ DebugSolver::GoalEvaluation(goal_evaluation ) => {
441
+ assert_eq!(goal_evaluation .result.replace(result), None);
494
442
}
495
443
DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
496
444
assert_eq!(
0 commit comments