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