@@ -13,8 +13,7 @@ use rustc_type_ir::{self as ty, Interner};
1313use crate :: delegate:: SolverDelegate ;
1414use crate :: solve:: eval_ctxt:: canonical;
1515use crate :: solve:: {
16- CanonicalInput , Certainty , GenerateProofTree , Goal , GoalEvaluationKind , GoalSource ,
17- QueryResult , inspect,
16+ Certainty , GenerateProofTree , Goal , GoalEvaluationKind , GoalSource , QueryResult , inspect,
1817} ;
1918
2019/// The core data structure when building proof trees.
5453enum DebugSolver < I : Interner > {
5554 Root ,
5655 GoalEvaluation ( WipGoalEvaluation < I > ) ,
57- CanonicalGoalEvaluation ( WipCanonicalGoalEvaluation < I > ) ,
5856 CanonicalGoalEvaluationStep ( WipCanonicalGoalEvaluationStep < I > ) ,
5957}
6058
@@ -64,12 +62,6 @@ impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
6462 }
6563}
6664
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-
7365impl < I : Interner > From < WipCanonicalGoalEvaluationStep < I > > for DebugSolver < I > {
7466 fn from ( g : WipCanonicalGoalEvaluationStep < I > ) -> DebugSolver < I > {
7567 DebugSolver :: CanonicalGoalEvaluationStep ( g)
@@ -80,39 +72,23 @@ impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
8072struct WipGoalEvaluation < I : Interner > {
8173 pub uncanonicalized_goal : Goal < I , I :: Predicate > ,
8274 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 > > ,
8479}
8580
8681impl < I : Interner > WipGoalEvaluation < I > {
8782 fn finalize ( self ) -> inspect:: GoalEvaluation < I > {
8883 inspect:: GoalEvaluation {
8984 uncanonicalized_goal : self . uncanonicalized_goal ,
9085 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 ,
11086 kind : if self . encountered_overflow {
11187 assert ! ( self . final_revision. is_none( ) ) ;
112- inspect:: CanonicalGoalEvaluationKind :: Overflow
88+ inspect:: GoalEvaluationKind :: Overflow
11389 } else {
11490 let final_revision = self . final_revision . unwrap ( ) . finalize ( ) ;
115- inspect:: CanonicalGoalEvaluationKind :: Evaluation { final_revision }
91+ inspect:: GoalEvaluationKind :: Evaluation { final_revision }
11692 } ,
11793 result : self . result . unwrap ( ) ,
11894 }
@@ -256,55 +232,27 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
256232
257233 pub ( in crate :: solve) fn new_goal_evaluation (
258234 & mut self ,
259- goal : Goal < I , I :: Predicate > ,
235+ uncanonicalized_goal : Goal < I , I :: Predicate > ,
260236 orig_values : & [ I :: GenericArg ] ,
261237 kind : GoalEvaluationKind ,
262238 ) -> ProofTreeBuilder < D > {
263239 self . opt_nested ( || match kind {
264240 GoalEvaluationKind :: Root => Some ( WipGoalEvaluation {
265- uncanonicalized_goal : goal ,
241+ uncanonicalized_goal,
266242 orig_values : orig_values. to_vec ( ) ,
267- evaluation : None ,
243+ encountered_overflow : false ,
244+ final_revision : None ,
245+ result : None ,
268246 } ) ,
269247 GoalEvaluationKind :: Nested => None ,
270248 } )
271249 }
272250
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-
303251 pub ( crate ) fn canonical_goal_evaluation_overflow ( & mut self ) {
304252 if let Some ( this) = self . as_mut ( ) {
305253 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 ;
308256 }
309257 _ => unreachable ! ( ) ,
310258 } ;
@@ -343,10 +291,10 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
343291 if let Some ( this) = self . as_mut ( ) {
344292 match ( this, * goal_evaluation_step. state . unwrap ( ) ) {
345293 (
346- DebugSolver :: CanonicalGoalEvaluation ( canonical_goal_evaluations ) ,
294+ DebugSolver :: GoalEvaluation ( goal_evaluation ) ,
347295 DebugSolver :: CanonicalGoalEvaluationStep ( goal_evaluation_step) ,
348296 ) => {
349- canonical_goal_evaluations . final_revision = Some ( goal_evaluation_step) ;
297+ goal_evaluation . final_revision = Some ( goal_evaluation_step) ;
350298 }
351299 _ => unreachable ! ( ) ,
352300 }
@@ -489,8 +437,8 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
489437 pub ( crate ) fn query_result ( & mut self , result : QueryResult < I > ) {
490438 if let Some ( this) = self . as_mut ( ) {
491439 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 ) ;
494442 }
495443 DebugSolver :: CanonicalGoalEvaluationStep ( evaluation_step) => {
496444 assert_eq ! (
0 commit comments