@@ -22,8 +22,9 @@ 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
- CanonicalInput , Certainty , FIXPOINT_STEP_LIMIT , Goal , GoalEvaluationKind , GoalSource ,
26
- HasChanged , NestedNormalizationGoals , NoSolution , QueryInput , QueryResult ,
25
+ CanonicalInput , Certainty , FIXPOINT_STEP_LIMIT , Goal , GoalEvaluation , GoalEvaluationKind ,
26
+ GoalSource , GoalStalledOn , HasChanged , NestedNormalizationGoals , NoSolution , QueryInput ,
27
+ QueryResult ,
27
28
} ;
28
29
29
30
pub ( super ) mod canonical;
@@ -115,7 +116,7 @@ where
115
116
116
117
pub ( super ) search_graph : & ' a mut SearchGraph < D > ,
117
118
118
- nested_goals : Vec < ( GoalSource , Goal < I , I :: Predicate > ) > ,
119
+ nested_goals : Vec < ( GoalSource , Goal < I , I :: Predicate > , Option < GoalStalledOn < I > > ) > ,
119
120
120
121
pub ( super ) origin_span : I :: Span ,
121
122
@@ -147,8 +148,9 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
147
148
goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
148
149
generate_proof_tree : GenerateProofTree ,
149
150
span : <Self :: Interner as Interner >:: Span ,
151
+ stalled_on : Option < GoalStalledOn < Self :: Interner > > ,
150
152
) -> (
151
- Result < ( HasChanged , Certainty ) , NoSolution > ,
153
+ Result < GoalEvaluation < Self :: Interner > , NoSolution > ,
152
154
Option < inspect:: GoalEvaluation < Self :: Interner > > ,
153
155
) ;
154
156
@@ -171,8 +173,12 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
171
173
& self ,
172
174
goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
173
175
generate_proof_tree : GenerateProofTree ,
176
+ stalled_on : Option < GoalStalledOn < Self :: Interner > > ,
174
177
) -> (
175
- Result < ( NestedNormalizationGoals < Self :: Interner > , HasChanged , Certainty ) , NoSolution > ,
178
+ Result <
179
+ ( NestedNormalizationGoals < Self :: Interner > , GoalEvaluation < Self :: Interner > ) ,
180
+ NoSolution ,
181
+ > ,
176
182
Option < inspect:: GoalEvaluation < Self :: Interner > > ,
177
183
) ;
178
184
}
@@ -188,9 +194,10 @@ where
188
194
goal : Goal < I , I :: Predicate > ,
189
195
generate_proof_tree : GenerateProofTree ,
190
196
span : I :: Span ,
191
- ) -> ( Result < ( HasChanged , Certainty ) , NoSolution > , Option < inspect:: GoalEvaluation < I > > ) {
197
+ stalled_on : Option < GoalStalledOn < I > > ,
198
+ ) -> ( Result < GoalEvaluation < I > , NoSolution > , Option < inspect:: GoalEvaluation < I > > ) {
192
199
EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , generate_proof_tree, span, |ecx| {
193
- ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
200
+ ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal, stalled_on )
194
201
} )
195
202
}
196
203
@@ -201,7 +208,7 @@ where
201
208
) -> bool {
202
209
self . probe ( || {
203
210
EvalCtxt :: enter_root ( self , root_depth, GenerateProofTree :: No , I :: Span :: dummy ( ) , |ecx| {
204
- ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
211
+ ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal, None )
205
212
} )
206
213
. 0
207
214
} )
@@ -213,16 +220,19 @@ where
213
220
& self ,
214
221
goal : Goal < I , I :: Predicate > ,
215
222
generate_proof_tree : GenerateProofTree ,
223
+ stalled_on : Option < GoalStalledOn < I > > ,
216
224
) -> (
217
- Result < ( NestedNormalizationGoals < I > , HasChanged , Certainty ) , NoSolution > ,
225
+ Result < ( NestedNormalizationGoals < I > , GoalEvaluation < I > ) , NoSolution > ,
218
226
Option < inspect:: GoalEvaluation < I > > ,
219
227
) {
220
228
EvalCtxt :: enter_root (
221
229
self ,
222
230
self . cx ( ) . recursion_limit ( ) ,
223
231
generate_proof_tree,
224
232
I :: Span :: dummy ( ) ,
225
- |ecx| ecx. evaluate_goal_raw ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal) ,
233
+ |ecx| {
234
+ ecx. evaluate_goal_raw ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal, stalled_on)
235
+ } ,
226
236
)
227
237
}
228
238
}
@@ -447,11 +457,12 @@ where
447
457
goal_evaluation_kind : GoalEvaluationKind ,
448
458
source : GoalSource ,
449
459
goal : Goal < I , I :: Predicate > ,
450
- ) -> Result < ( HasChanged , Certainty ) , NoSolution > {
451
- let ( normalization_nested_goals, has_changed, certainty) =
452
- self . evaluate_goal_raw ( goal_evaluation_kind, source, goal) ?;
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) ?;
453
464
assert ! ( normalization_nested_goals. is_empty( ) ) ;
454
- Ok ( ( has_changed , certainty ) )
465
+ Ok ( goal_evaluation )
455
466
}
456
467
457
468
/// Recursively evaluates `goal`, returning the nested goals in case
@@ -466,7 +477,29 @@ where
466
477
goal_evaluation_kind : GoalEvaluationKind ,
467
478
source : GoalSource ,
468
479
goal : Goal < I , I :: Predicate > ,
469
- ) -> Result < ( NestedNormalizationGoals < I > , HasChanged , Certainty ) , NoSolution > {
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) )
487
+ && !self
488
+ . delegate
489
+ . opaque_types_storage_num_entries ( )
490
+ . needs_reevaluation ( stalled_on. num_opaques )
491
+ {
492
+ return Ok ( (
493
+ NestedNormalizationGoals :: empty ( ) ,
494
+ GoalEvaluation {
495
+ certainty : Certainty :: Maybe ( stalled_on. stalled_cause ) ,
496
+ has_changed : HasChanged :: No ,
497
+ stalled_on : Some ( stalled_on) ,
498
+ } ,
499
+ ) ) ;
500
+ }
501
+ }
502
+
470
503
let ( orig_values, canonical_goal) = self . canonicalize_goal ( goal) ;
471
504
let mut goal_evaluation =
472
505
self . inspect . new_goal_evaluation ( goal, & orig_values, goal_evaluation_kind) ;
@@ -489,7 +522,7 @@ where
489
522
if !has_only_region_constraints ( response) { HasChanged :: Yes } else { HasChanged :: No } ;
490
523
491
524
let ( normalization_nested_goals, certainty) =
492
- self . instantiate_and_apply_query_response ( goal. param_env , orig_values, response) ;
525
+ self . instantiate_and_apply_query_response ( goal. param_env , & orig_values, response) ;
493
526
self . inspect . goal_evaluation ( goal_evaluation) ;
494
527
495
528
// FIXME: We previously had an assert here that checked that recomputing
@@ -502,7 +535,42 @@ where
502
535
// Once we have decided on how to handle trait-system-refactor-initiative#75,
503
536
// we should re-add an assert here.
504
537
505
- Ok ( ( normalization_nested_goals, has_changed, certainty) )
538
+ let stalled_on = match certainty {
539
+ Certainty :: Yes => None ,
540
+ Certainty :: Maybe ( stalled_cause) => match has_changed {
541
+ // FIXME: We could recompute a *new* set of stalled variables by walking
542
+ // through the orig values, resolving, and computing the root vars of anything
543
+ // that is not resolved. Only when *these* have changed is it meaningful
544
+ // to recompute this goal.
545
+ HasChanged :: Yes => None ,
546
+ HasChanged :: No => {
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
+ }
558
+
559
+ Some ( GoalStalledOn {
560
+ num_opaques : canonical_goal
561
+ . canonical
562
+ . value
563
+ . predefined_opaques_in_body
564
+ . opaque_types
565
+ . len ( ) ,
566
+ stalled_vars,
567
+ stalled_cause,
568
+ } )
569
+ }
570
+ } ,
571
+ } ;
572
+
573
+ Ok ( ( normalization_nested_goals, GoalEvaluation { certainty, has_changed, stalled_on } ) )
506
574
}
507
575
508
576
fn compute_goal ( & mut self , goal : Goal < I , I :: Predicate > ) -> QueryResult < I > {
@@ -602,7 +670,7 @@ where
602
670
let cx = self . cx ( ) ;
603
671
// If this loop did not result in any progress, what's our final certainty.
604
672
let mut unchanged_certainty = Some ( Certainty :: Yes ) ;
605
- for ( source, goal) in mem:: take ( & mut self . nested_goals ) {
673
+ for ( source, goal, stalled_on ) in mem:: take ( & mut self . nested_goals ) {
606
674
if let Some ( has_changed) = self . delegate . compute_goal_fast_path ( goal, self . origin_span )
607
675
{
608
676
if matches ! ( has_changed, HasChanged :: Yes ) {
@@ -630,11 +698,18 @@ where
630
698
let unconstrained_goal =
631
699
goal. with ( cx, ty:: NormalizesTo { alias : pred. alias , term : unconstrained_rhs } ) ;
632
700
633
- let ( NestedNormalizationGoals ( nested_goals) , _, certainty) =
634
- self . evaluate_goal_raw ( GoalEvaluationKind :: Nested , source, unconstrained_goal) ?;
701
+ let (
702
+ NestedNormalizationGoals ( nested_goals) ,
703
+ GoalEvaluation { certainty, stalled_on, has_changed : _ } ,
704
+ ) = self . evaluate_goal_raw (
705
+ GoalEvaluationKind :: Nested ,
706
+ source,
707
+ unconstrained_goal,
708
+ stalled_on,
709
+ ) ?;
635
710
// Add the nested goals from normalization to our own nested goals.
636
711
trace ! ( ?nested_goals) ;
637
- self . nested_goals . extend ( nested_goals) ;
712
+ self . nested_goals . extend ( nested_goals. into_iter ( ) . map ( | ( s , g ) | ( s , g , None ) ) ) ;
638
713
639
714
// Finally, equate the goal's RHS with the unconstrained var.
640
715
//
@@ -660,6 +735,8 @@ where
660
735
// looking at the "has changed" return from evaluate_goal,
661
736
// because we expect the `unconstrained_rhs` part of the predicate
662
737
// to have changed -- that means we actually normalized successfully!
738
+ // FIXME: Do we need to eagerly resolve here? Or should we check
739
+ // if the cache key has any changed vars?
663
740
let with_resolved_vars = self . resolve_vars_if_possible ( goal) ;
664
741
if pred. alias != goal. predicate . as_normalizes_to ( ) . unwrap ( ) . skip_binder ( ) . alias {
665
742
unchanged_certainty = None ;
@@ -668,21 +745,21 @@ where
668
745
match certainty {
669
746
Certainty :: Yes => { }
670
747
Certainty :: Maybe ( _) => {
671
- self . nested_goals . push ( ( source, with_resolved_vars) ) ;
748
+ self . nested_goals . push ( ( source, with_resolved_vars, stalled_on ) ) ;
672
749
unchanged_certainty = unchanged_certainty. map ( |c| c. and ( certainty) ) ;
673
750
}
674
751
}
675
752
} else {
676
- let ( has_changed, certainty ) =
677
- self . evaluate_goal ( GoalEvaluationKind :: Nested , source, goal) ?;
753
+ let GoalEvaluation { certainty , has_changed, stalled_on } =
754
+ self . evaluate_goal ( GoalEvaluationKind :: Nested , source, goal, stalled_on ) ?;
678
755
if has_changed == HasChanged :: Yes {
679
756
unchanged_certainty = None ;
680
757
}
681
758
682
759
match certainty {
683
760
Certainty :: Yes => { }
684
761
Certainty :: Maybe ( _) => {
685
- self . nested_goals . push ( ( source, goal) ) ;
762
+ self . nested_goals . push ( ( source, goal, stalled_on ) ) ;
686
763
unchanged_certainty = unchanged_certainty. map ( |c| c. and ( certainty) ) ;
687
764
}
688
765
}
@@ -706,7 +783,7 @@ where
706
783
goal. predicate =
707
784
goal. predicate . fold_with ( & mut ReplaceAliasWithInfer :: new ( self , source, goal. param_env ) ) ;
708
785
self . inspect . add_goal ( self . delegate , self . max_input_universe , source, goal) ;
709
- self . nested_goals . push ( ( source, goal) ) ;
786
+ self . nested_goals . push ( ( source, goal, None ) ) ;
710
787
}
711
788
712
789
#[ instrument( level = "trace" , skip( self , goals) ) ]
0 commit comments