@@ -22,8 +22,8 @@ use crate::delegate::SolverDelegate;
22
22
use crate :: solve:: inspect:: { self , ProofTreeBuilder } ;
23
23
use crate :: solve:: search_graph:: SearchGraph ;
24
24
use crate :: solve:: {
25
- CanonicalGoalCacheKey , CanonicalInput , Certainty , FIXPOINT_STEP_LIMIT , Goal ,
26
- GoalEvaluationKind , GoalSource , HasChanged , NestedNormalizationGoals , NoSolution , QueryInput ,
25
+ CanonicalInput , Certainty , FIXPOINT_STEP_LIMIT , Goal , GoalEvaluation , GoalEvaluationKind ,
26
+ GoalSource , GoalStalledOn , HasChanged , NestedNormalizationGoals , NoSolution , QueryInput ,
27
27
QueryResult ,
28
28
} ;
29
29
@@ -116,7 +116,7 @@ where
116
116
117
117
pub ( super ) search_graph : & ' a mut SearchGraph < D > ,
118
118
119
- nested_goals : Vec < ( GoalSource , Goal < I , I :: Predicate > , Option < CanonicalGoalCacheKey < I > > ) > ,
119
+ nested_goals : Vec < ( GoalSource , Goal < I , I :: Predicate > , Option < GoalStalledOn < I > > ) > ,
120
120
121
121
pub ( super ) origin_span : I :: Span ,
122
122
@@ -148,9 +148,9 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
148
148
goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
149
149
generate_proof_tree : GenerateProofTree ,
150
150
span : <Self :: Interner as Interner >:: Span ,
151
- cache_key : Option < CanonicalGoalCacheKey < Self :: Interner > > ,
151
+ stalled_on : Option < GoalStalledOn < Self :: Interner > > ,
152
152
) -> (
153
- Result < ( HasChanged , Certainty , CanonicalGoalCacheKey < Self :: Interner > ) , NoSolution > ,
153
+ Result < GoalEvaluation < Self :: Interner > , NoSolution > ,
154
154
Option < inspect:: GoalEvaluation < Self :: Interner > > ,
155
155
) ;
156
156
@@ -173,15 +173,10 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
173
173
& self ,
174
174
goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
175
175
generate_proof_tree : GenerateProofTree ,
176
- cache_key : Option < CanonicalGoalCacheKey < Self :: Interner > > ,
176
+ stalled_on : Option < GoalStalledOn < Self :: Interner > > ,
177
177
) -> (
178
178
Result <
179
- (
180
- NestedNormalizationGoals < Self :: Interner > ,
181
- HasChanged ,
182
- Certainty ,
183
- CanonicalGoalCacheKey < Self :: Interner > ,
184
- ) ,
179
+ ( NestedNormalizationGoals < Self :: Interner > , GoalEvaluation < Self :: Interner > ) ,
185
180
NoSolution ,
186
181
> ,
187
182
Option < inspect:: GoalEvaluation < Self :: Interner > > ,
@@ -199,13 +194,10 @@ where
199
194
goal : Goal < I , I :: Predicate > ,
200
195
generate_proof_tree : GenerateProofTree ,
201
196
span : I :: Span ,
202
- cache_key : Option < CanonicalGoalCacheKey < I > > ,
203
- ) -> (
204
- Result < ( HasChanged , Certainty , CanonicalGoalCacheKey < I > ) , NoSolution > ,
205
- Option < inspect:: GoalEvaluation < I > > ,
206
- ) {
197
+ stalled_on : Option < GoalStalledOn < I > > ,
198
+ ) -> ( Result < GoalEvaluation < I > , NoSolution > , Option < inspect:: GoalEvaluation < I > > ) {
207
199
EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , generate_proof_tree, span, |ecx| {
208
- ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal, cache_key )
200
+ ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal, stalled_on )
209
201
} )
210
202
}
211
203
@@ -228,12 +220,9 @@ where
228
220
& self ,
229
221
goal : Goal < I , I :: Predicate > ,
230
222
generate_proof_tree : GenerateProofTree ,
231
- cache_key : Option < CanonicalGoalCacheKey < I > > ,
223
+ stalled_on : Option < GoalStalledOn < I > > ,
232
224
) -> (
233
- Result <
234
- ( NestedNormalizationGoals < I > , HasChanged , Certainty , CanonicalGoalCacheKey < I > ) ,
235
- NoSolution ,
236
- > ,
225
+ Result < ( NestedNormalizationGoals < I > , GoalEvaluation < I > ) , NoSolution > ,
237
226
Option < inspect:: GoalEvaluation < I > > ,
238
227
) {
239
228
EvalCtxt :: enter_root (
@@ -242,7 +231,7 @@ where
242
231
generate_proof_tree,
243
232
I :: Span :: dummy ( ) ,
244
233
|ecx| {
245
- ecx. evaluate_goal_raw ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal, cache_key )
234
+ ecx. evaluate_goal_raw ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal, stalled_on )
246
235
} ,
247
236
)
248
237
}
@@ -468,12 +457,12 @@ where
468
457
goal_evaluation_kind : GoalEvaluationKind ,
469
458
source : GoalSource ,
470
459
goal : Goal < I , I :: Predicate > ,
471
- cache_key : Option < CanonicalGoalCacheKey < I > > ,
472
- ) -> Result < ( HasChanged , Certainty , CanonicalGoalCacheKey < I > ) , NoSolution > {
473
- let ( normalization_nested_goals, has_changed , certainty , cache_key ) =
474
- self . evaluate_goal_raw ( goal_evaluation_kind, source, goal, cache_key ) ?;
460
+ stalled_on : Option < GoalStalledOn < I > > ,
461
+ ) -> Result < GoalEvaluation < I > , NoSolution > {
462
+ let ( normalization_nested_goals, goal_evaluation ) =
463
+ self . evaluate_goal_raw ( goal_evaluation_kind, source, goal, stalled_on ) ?;
475
464
assert ! ( normalization_nested_goals. is_empty( ) ) ;
476
- Ok ( ( has_changed , certainty , cache_key ) )
465
+ Ok ( goal_evaluation )
477
466
}
478
467
479
468
/// Recursively evaluates `goal`, returning the nested goals in case
@@ -488,23 +477,25 @@ where
488
477
goal_evaluation_kind : GoalEvaluationKind ,
489
478
source : GoalSource ,
490
479
goal : Goal < I , I :: Predicate > ,
491
- cache_key : Option < CanonicalGoalCacheKey < I > > ,
492
- ) -> Result <
493
- ( NestedNormalizationGoals < I > , HasChanged , Certainty , CanonicalGoalCacheKey < I > ) ,
494
- NoSolution ,
495
- > {
496
- if let Some ( cache_key ) = cache_key {
497
- if !cache_key . stalled_vars . iter ( ) . any ( |value| self . delegate . is_changed_arg ( * value) )
480
+ stalled_on : Option < GoalStalledOn < I > > ,
481
+ ) -> Result < ( NestedNormalizationGoals < I > , GoalEvaluation < I > ) , NoSolution > {
482
+ // If we have run this goal before, and it was stalled, check that any of the goal's
483
+ // args have changed. Otherwise, we don't need to re-run the goal because it'll remain
484
+ // stalled, since it'll canonicalize the same way and evaluation is pure.
485
+ if let Some ( stalled_on ) = stalled_on {
486
+ if !stalled_on . stalled_vars . iter ( ) . any ( |value| self . delegate . is_changed_arg ( * value) )
498
487
&& !self
499
488
. delegate
500
489
. opaque_types_storage_num_entries ( )
501
- . needs_reevaluation ( cache_key . num_opaques )
490
+ . needs_reevaluation ( stalled_on . num_opaques )
502
491
{
503
492
return Ok ( (
504
493
NestedNormalizationGoals :: empty ( ) ,
505
- HasChanged :: No ,
506
- cache_key. certainty ,
507
- cache_key,
494
+ GoalEvaluation {
495
+ certainty : Certainty :: Maybe ( stalled_on. stalled_cause ) ,
496
+ has_changed : HasChanged :: No ,
497
+ stalled_on : Some ( stalled_on) ,
498
+ } ,
508
499
) ) ;
509
500
}
510
501
}
@@ -544,33 +535,35 @@ where
544
535
// Once we have decided on how to handle trait-system-refactor-initiative#75,
545
536
// we should re-add an assert here.
546
537
547
- // Remove the unconstrained RHS arg, which is expected to have changed.
548
- let mut stalled_vars = orig_values;
549
- if let Some ( normalizes_to) = goal. predicate . as_normalizes_to ( ) {
550
- let normalizes_to = normalizes_to. skip_binder ( ) ;
551
- let rhs_arg: I :: GenericArg = normalizes_to. term . into ( ) ;
552
- let idx = stalled_vars
553
- . iter ( )
554
- . rposition ( |arg| * arg == rhs_arg)
555
- . expect ( "expected unconstrained arg" ) ;
556
- stalled_vars. swap_remove ( idx) ;
557
- }
538
+ let stalled_on = match certainty {
539
+ Certainty :: Yes => None ,
540
+ Certainty :: Maybe ( stalled_cause) => {
541
+ // Remove the unconstrained RHS arg, which is expected to have changed.
542
+ let mut stalled_vars = orig_values;
543
+ if let Some ( normalizes_to) = goal. predicate . as_normalizes_to ( ) {
544
+ let normalizes_to = normalizes_to. skip_binder ( ) ;
545
+ let rhs_arg: I :: GenericArg = normalizes_to. term . into ( ) ;
546
+ let idx = stalled_vars
547
+ . iter ( )
548
+ . rposition ( |arg| * arg == rhs_arg)
549
+ . expect ( "expected unconstrained arg" ) ;
550
+ stalled_vars. swap_remove ( idx) ;
551
+ }
558
552
559
- Ok ( (
560
- normalization_nested_goals,
561
- has_changed,
562
- certainty,
563
- CanonicalGoalCacheKey {
564
- num_opaques : canonical_goal
565
- . canonical
566
- . value
567
- . predefined_opaques_in_body
568
- . opaque_types
569
- . len ( ) ,
570
- stalled_vars,
571
- certainty,
572
- } ,
573
- ) )
553
+ Some ( GoalStalledOn {
554
+ num_opaques : canonical_goal
555
+ . canonical
556
+ . value
557
+ . predefined_opaques_in_body
558
+ . opaque_types
559
+ . len ( ) ,
560
+ stalled_vars,
561
+ stalled_cause,
562
+ } )
563
+ }
564
+ } ;
565
+
566
+ Ok ( ( normalization_nested_goals, GoalEvaluation { certainty, has_changed, stalled_on } ) )
574
567
}
575
568
576
569
fn compute_goal ( & mut self , goal : Goal < I , I :: Predicate > ) -> QueryResult < I > {
@@ -670,7 +663,7 @@ where
670
663
let cx = self . cx ( ) ;
671
664
// If this loop did not result in any progress, what's our final certainty.
672
665
let mut unchanged_certainty = Some ( Certainty :: Yes ) ;
673
- for ( source, goal, cache_key ) in mem:: take ( & mut self . nested_goals ) {
666
+ for ( source, goal, stalled_on ) in mem:: take ( & mut self . nested_goals ) {
674
667
if let Some ( has_changed) = self . delegate . compute_goal_fast_path ( goal, self . origin_span )
675
668
{
676
669
if matches ! ( has_changed, HasChanged :: Yes ) {
@@ -698,13 +691,15 @@ where
698
691
let unconstrained_goal =
699
692
goal. with ( cx, ty:: NormalizesTo { alias : pred. alias , term : unconstrained_rhs } ) ;
700
693
701
- let ( NestedNormalizationGoals ( nested_goals) , _, certainty, cache_key) = self
702
- . evaluate_goal_raw (
703
- GoalEvaluationKind :: Nested ,
704
- source,
705
- unconstrained_goal,
706
- cache_key,
707
- ) ?;
694
+ let (
695
+ NestedNormalizationGoals ( nested_goals) ,
696
+ GoalEvaluation { certainty, stalled_on, has_changed : _ } ,
697
+ ) = self . evaluate_goal_raw (
698
+ GoalEvaluationKind :: Nested ,
699
+ source,
700
+ unconstrained_goal,
701
+ stalled_on,
702
+ ) ?;
708
703
// Add the nested goals from normalization to our own nested goals.
709
704
trace ! ( ?nested_goals) ;
710
705
self . nested_goals . extend ( nested_goals. into_iter ( ) . map ( |( s, g) | ( s, g, None ) ) ) ;
@@ -743,21 +738,21 @@ where
743
738
match certainty {
744
739
Certainty :: Yes => { }
745
740
Certainty :: Maybe ( _) => {
746
- self . nested_goals . push ( ( source, with_resolved_vars, Some ( cache_key ) ) ) ;
741
+ self . nested_goals . push ( ( source, with_resolved_vars, stalled_on ) ) ;
747
742
unchanged_certainty = unchanged_certainty. map ( |c| c. and ( certainty) ) ;
748
743
}
749
744
}
750
745
} else {
751
- let ( has_changed , certainty, cache_key ) =
752
- self . evaluate_goal ( GoalEvaluationKind :: Nested , source, goal, cache_key ) ?;
746
+ let GoalEvaluation { certainty, has_changed , stalled_on } =
747
+ self . evaluate_goal ( GoalEvaluationKind :: Nested , source, goal, stalled_on ) ?;
753
748
if has_changed == HasChanged :: Yes {
754
749
unchanged_certainty = None ;
755
750
}
756
751
757
752
match certainty {
758
753
Certainty :: Yes => { }
759
754
Certainty :: Maybe ( _) => {
760
- self . nested_goals . push ( ( source, goal, Some ( cache_key ) ) ) ;
755
+ self . nested_goals . push ( ( source, goal, stalled_on ) ) ;
761
756
unchanged_certainty = unchanged_certainty. map ( |c| c. and ( certainty) ) ;
762
757
}
763
758
}
0 commit comments