@@ -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,24 @@ 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
+ /// Only used for uncached goals. After we finished evaluating
77
+ /// the goal, this is interned and moved into `kind`.
78
+ pub final_revision : Option < WipCanonicalGoalEvaluationStep < I > > ,
79
+ pub result : Option < QueryResult < I > > ,
84
80
}
85
81
86
82
impl < I : Interner > WipGoalEvaluation < I > {
87
83
fn finalize ( self ) -> inspect:: GoalEvaluation < I > {
88
84
inspect:: GoalEvaluation {
89
85
uncanonicalized_goal : self . uncanonicalized_goal ,
90
86
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
87
kind : if self . encountered_overflow {
111
88
assert ! ( self . final_revision. is_none( ) ) ;
112
- inspect:: CanonicalGoalEvaluationKind :: Overflow
89
+ inspect:: GoalEvaluationKind :: Overflow
113
90
} else {
114
91
let final_revision = self . final_revision . unwrap ( ) . finalize ( ) ;
115
- inspect:: CanonicalGoalEvaluationKind :: Evaluation { final_revision }
92
+ inspect:: GoalEvaluationKind :: Evaluation { final_revision }
116
93
} ,
117
94
result : self . result . unwrap ( ) ,
118
95
}
@@ -256,55 +233,27 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
256
233
257
234
pub ( in crate :: solve) fn new_goal_evaluation (
258
235
& mut self ,
259
- goal : Goal < I , I :: Predicate > ,
236
+ uncanonicalized_goal : Goal < I , I :: Predicate > ,
260
237
orig_values : & [ I :: GenericArg ] ,
261
238
kind : GoalEvaluationKind ,
262
239
) -> ProofTreeBuilder < D > {
263
240
self . opt_nested ( || match kind {
264
241
GoalEvaluationKind :: Root => Some ( WipGoalEvaluation {
265
- uncanonicalized_goal : goal ,
242
+ uncanonicalized_goal,
266
243
orig_values : orig_values. to_vec ( ) ,
267
- evaluation : None ,
244
+ encountered_overflow : false ,
245
+ final_revision : None ,
246
+ result : None ,
268
247
} ) ,
269
248
GoalEvaluationKind :: Nested => None ,
270
249
} )
271
250
}
272
251
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
252
pub ( crate ) fn canonical_goal_evaluation_overflow ( & mut self ) {
304
253
if let Some ( this) = self . as_mut ( ) {
305
254
match this {
306
- DebugSolver :: CanonicalGoalEvaluation ( canonical_goal_evaluation ) => {
307
- canonical_goal_evaluation . encountered_overflow = true ;
255
+ DebugSolver :: GoalEvaluation ( goal_evaluation ) => {
256
+ goal_evaluation . encountered_overflow = true ;
308
257
}
309
258
_ => unreachable ! ( ) ,
310
259
} ;
@@ -343,10 +292,10 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
343
292
if let Some ( this) = self . as_mut ( ) {
344
293
match ( this, * goal_evaluation_step. state . unwrap ( ) ) {
345
294
(
346
- DebugSolver :: CanonicalGoalEvaluation ( canonical_goal_evaluations ) ,
295
+ DebugSolver :: GoalEvaluation ( goal_evaluation ) ,
347
296
DebugSolver :: CanonicalGoalEvaluationStep ( goal_evaluation_step) ,
348
297
) => {
349
- canonical_goal_evaluations . final_revision = Some ( goal_evaluation_step) ;
298
+ goal_evaluation . final_revision = Some ( goal_evaluation_step) ;
350
299
}
351
300
_ => unreachable ! ( ) ,
352
301
}
@@ -489,8 +438,8 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
489
438
pub ( crate ) fn query_result ( & mut self , result : QueryResult < I > ) {
490
439
if let Some ( this) = self . as_mut ( ) {
491
440
match this {
492
- DebugSolver :: CanonicalGoalEvaluation ( canonical_goal_evaluation ) => {
493
- assert_eq ! ( canonical_goal_evaluation . result. replace( result) , None ) ;
441
+ DebugSolver :: GoalEvaluation ( goal_evaluation ) => {
442
+ assert_eq ! ( goal_evaluation . result. replace( result) , None ) ;
494
443
}
495
444
DebugSolver :: CanonicalGoalEvaluationStep ( evaluation_step) => {
496
445
assert_eq ! (
0 commit comments