@@ -379,60 +379,10 @@ impl<'tcx> SearchGraph<'tcx> {
379
379
// `with_anon_task` closure.
380
380
let ( ( final_entry, result) , dep_node) =
381
381
tcx. dep_graph . with_anon_task ( tcx, dep_kinds:: TraitSelect , || {
382
- // When we encounter a coinductive cycle, we have to fetch the
383
- // result of that cycle while we are still computing it. Because
384
- // of this we continuously recompute the cycle until the result
385
- // of the previous iteration is equal to the final result, at which
386
- // point we are done.
387
382
for _ in 0 ..FIXPOINT_STEP_LIMIT {
388
- let result = prove_goal ( self , inspect) ;
389
- let stack_entry = self . pop_stack ( ) ;
390
- debug_assert_eq ! ( stack_entry. input, input) ;
391
-
392
- // If the current goal is not the root of a cycle, we are done.
393
- if stack_entry. has_been_used . is_empty ( ) {
394
- return ( stack_entry, result) ;
395
- }
396
-
397
- // If it is a cycle head, we have to keep trying to prove it until
398
- // we reach a fixpoint. We need to do so for all cycle heads,
399
- // not only for the root.
400
- //
401
- // See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
402
- // for an example.
403
-
404
- // Start by clearing all provisional cache entries which depend on this
405
- // the current goal.
406
- Self :: clear_dependent_provisional_results (
407
- & mut self . provisional_cache ,
408
- self . stack . next_index ( ) ,
409
- ) ;
410
-
411
- // Check whether we reached a fixpoint, either because the final result
412
- // is equal to the provisional result of the previous iteration, or because
413
- // this was only the root of either coinductive or inductive cycles, and the
414
- // final result is equal to the initial response for that case.
415
- let reached_fixpoint = if let Some ( r) = stack_entry. provisional_result {
416
- r == result
417
- } else if stack_entry. has_been_used == HasBeenUsed :: COINDUCTIVE_CYCLE {
418
- Self :: response_no_constraints ( tcx, input, Certainty :: Yes ) == result
419
- } else if stack_entry. has_been_used == HasBeenUsed :: INDUCTIVE_CYCLE {
420
- Self :: response_no_constraints ( tcx, input, Certainty :: overflow ( false ) )
421
- == result
422
- } else {
423
- false
424
- } ;
425
-
426
- // If we did not reach a fixpoint, update the provisional result and reevaluate.
427
- if reached_fixpoint {
428
- return ( stack_entry, result) ;
429
- } else {
430
- let depth = self . stack . push ( StackEntry {
431
- has_been_used : HasBeenUsed :: empty ( ) ,
432
- provisional_result : Some ( result) ,
433
- ..stack_entry
434
- } ) ;
435
- debug_assert_eq ! ( self . provisional_cache[ & input] . stack_depth, Some ( depth) ) ;
383
+ match self . fixpoint_step_in_task ( tcx, input, inspect, & mut prove_goal) {
384
+ StepResult :: Done ( final_entry, result) => return ( final_entry, result) ,
385
+ StepResult :: HasChanged => { }
436
386
}
437
387
}
438
388
@@ -484,6 +434,79 @@ impl<'tcx> SearchGraph<'tcx> {
484
434
485
435
result
486
436
}
437
+ }
438
+
439
+ enum StepResult < ' tcx > {
440
+ Done ( StackEntry < ' tcx > , QueryResult < ' tcx > ) ,
441
+ HasChanged ,
442
+ }
443
+
444
+ impl < ' tcx > SearchGraph < ' tcx > {
445
+ /// When we encounter a coinductive cycle, we have to fetch the
446
+ /// result of that cycle while we are still computing it. Because
447
+ /// of this we continuously recompute the cycle until the result
448
+ /// of the previous iteration is equal to the final result, at which
449
+ /// point we are done.
450
+ fn fixpoint_step_in_task < F > (
451
+ & mut self ,
452
+ tcx : TyCtxt < ' tcx > ,
453
+ input : CanonicalInput < ' tcx > ,
454
+ inspect : & mut ProofTreeBuilder < ' tcx > ,
455
+ prove_goal : & mut F ,
456
+ ) -> StepResult < ' tcx >
457
+ where
458
+ F : FnMut ( & mut Self , & mut ProofTreeBuilder < ' tcx > ) -> QueryResult < ' tcx > ,
459
+ {
460
+ let result = prove_goal ( self , inspect) ;
461
+ let stack_entry = self . pop_stack ( ) ;
462
+ debug_assert_eq ! ( stack_entry. input, input) ;
463
+
464
+ // If the current goal is not the root of a cycle, we are done.
465
+ if stack_entry. has_been_used . is_empty ( ) {
466
+ return StepResult :: Done ( stack_entry, result) ;
467
+ }
468
+
469
+ // If it is a cycle head, we have to keep trying to prove it until
470
+ // we reach a fixpoint. We need to do so for all cycle heads,
471
+ // not only for the root.
472
+ //
473
+ // See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
474
+ // for an example.
475
+
476
+ // Start by clearing all provisional cache entries which depend on this
477
+ // the current goal.
478
+ Self :: clear_dependent_provisional_results (
479
+ & mut self . provisional_cache ,
480
+ self . stack . next_index ( ) ,
481
+ ) ;
482
+
483
+ // Check whether we reached a fixpoint, either because the final result
484
+ // is equal to the provisional result of the previous iteration, or because
485
+ // this was only the root of either coinductive or inductive cycles, and the
486
+ // final result is equal to the initial response for that case.
487
+ let reached_fixpoint = if let Some ( r) = stack_entry. provisional_result {
488
+ r == result
489
+ } else if stack_entry. has_been_used == HasBeenUsed :: COINDUCTIVE_CYCLE {
490
+ Self :: response_no_constraints ( tcx, input, Certainty :: Yes ) == result
491
+ } else if stack_entry. has_been_used == HasBeenUsed :: INDUCTIVE_CYCLE {
492
+ Self :: response_no_constraints ( tcx, input, Certainty :: overflow ( false ) ) == result
493
+ } else {
494
+ false
495
+ } ;
496
+
497
+ // If we did not reach a fixpoint, update the provisional result and reevaluate.
498
+ if reached_fixpoint {
499
+ StepResult :: Done ( stack_entry, result)
500
+ } else {
501
+ let depth = self . stack . push ( StackEntry {
502
+ has_been_used : HasBeenUsed :: empty ( ) ,
503
+ provisional_result : Some ( result) ,
504
+ ..stack_entry
505
+ } ) ;
506
+ debug_assert_eq ! ( self . provisional_cache[ & input] . stack_depth, Some ( depth) ) ;
507
+ StepResult :: HasChanged
508
+ }
509
+ }
487
510
488
511
fn response_no_constraints (
489
512
tcx : TyCtxt < ' tcx > ,
0 commit comments