Skip to content

Commit 82df0c3

Browse files
committed
move fixpoint step into subfunction
1 parent be71fd4 commit 82df0c3

File tree

1 file changed

+76
-53
lines changed

1 file changed

+76
-53
lines changed

compiler/rustc_trait_selection/src/solve/search_graph.rs

+76-53
Original file line numberDiff line numberDiff line change
@@ -391,60 +391,10 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
391391
// `with_anon_task` closure.
392392
let ((final_entry, result), dep_node) =
393393
tcx.dep_graph.with_anon_task(tcx, dep_kinds::TraitSelect, || {
394-
// When we encounter a coinductive cycle, we have to fetch the
395-
// result of that cycle while we are still computing it. Because
396-
// of this we continuously recompute the cycle until the result
397-
// of the previous iteration is equal to the final result, at which
398-
// point we are done.
399394
for _ in 0..FIXPOINT_STEP_LIMIT {
400-
let result = prove_goal(self, inspect);
401-
let stack_entry = self.pop_stack();
402-
debug_assert_eq!(stack_entry.input, input);
403-
404-
// If the current goal is not the root of a cycle, we are done.
405-
if stack_entry.has_been_used.is_empty() {
406-
return (stack_entry, result);
407-
}
408-
409-
// If it is a cycle head, we have to keep trying to prove it until
410-
// we reach a fixpoint. We need to do so for all cycle heads,
411-
// not only for the root.
412-
//
413-
// See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
414-
// for an example.
415-
416-
// Start by clearing all provisional cache entries which depend on this
417-
// the current goal.
418-
Self::clear_dependent_provisional_results(
419-
&mut self.provisional_cache,
420-
self.stack.next_index(),
421-
);
422-
423-
// Check whether we reached a fixpoint, either because the final result
424-
// is equal to the provisional result of the previous iteration, or because
425-
// this was only the root of either coinductive or inductive cycles, and the
426-
// final result is equal to the initial response for that case.
427-
let reached_fixpoint = if let Some(r) = stack_entry.provisional_result {
428-
r == result
429-
} else if stack_entry.has_been_used == HasBeenUsed::COINDUCTIVE_CYCLE {
430-
Self::response_no_constraints(tcx, input, Certainty::Yes) == result
431-
} else if stack_entry.has_been_used == HasBeenUsed::INDUCTIVE_CYCLE {
432-
Self::response_no_constraints(tcx, input, Certainty::overflow(false))
433-
== result
434-
} else {
435-
false
436-
};
437-
438-
// If we did not reach a fixpoint, update the provisional result and reevaluate.
439-
if reached_fixpoint {
440-
return (stack_entry, result);
441-
} else {
442-
let depth = self.stack.push(StackEntry {
443-
has_been_used: HasBeenUsed::empty(),
444-
provisional_result: Some(result),
445-
..stack_entry
446-
});
447-
debug_assert_eq!(self.provisional_cache[&input].stack_depth, Some(depth));
395+
match self.fixpoint_step_in_task(tcx, input, inspect, &mut prove_goal) {
396+
StepResult::Done(final_entry, result) => return (final_entry, result),
397+
StepResult::HasChanged => {}
448398
}
449399
}
450400

@@ -496,6 +446,79 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
496446

497447
result
498448
}
449+
}
450+
451+
enum StepResult<'tcx> {
452+
Done(StackEntry<'tcx>, QueryResult<'tcx>),
453+
HasChanged,
454+
}
455+
456+
impl<'tcx> SearchGraph<'tcx> {
457+
/// When we encounter a coinductive cycle, we have to fetch the
458+
/// result of that cycle while we are still computing it. Because
459+
/// of this we continuously recompute the cycle until the result
460+
/// of the previous iteration is equal to the final result, at which
461+
/// point we are done.
462+
fn fixpoint_step_in_task<F>(
463+
&mut self,
464+
tcx: TyCtxt<'tcx>,
465+
input: CanonicalInput<'tcx>,
466+
inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
467+
prove_goal: &mut F,
468+
) -> StepResult<'tcx>
469+
where
470+
F: FnMut(&mut Self, &mut ProofTreeBuilder<TyCtxt<'tcx>>) -> QueryResult<'tcx>,
471+
{
472+
let result = prove_goal(self, inspect);
473+
let stack_entry = self.pop_stack();
474+
debug_assert_eq!(stack_entry.input, input);
475+
476+
// If the current goal is not the root of a cycle, we are done.
477+
if stack_entry.has_been_used.is_empty() {
478+
return StepResult::Done(stack_entry, result);
479+
}
480+
481+
// If it is a cycle head, we have to keep trying to prove it until
482+
// we reach a fixpoint. We need to do so for all cycle heads,
483+
// not only for the root.
484+
//
485+
// See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
486+
// for an example.
487+
488+
// Start by clearing all provisional cache entries which depend on this
489+
// the current goal.
490+
Self::clear_dependent_provisional_results(
491+
&mut self.provisional_cache,
492+
self.stack.next_index(),
493+
);
494+
495+
// Check whether we reached a fixpoint, either because the final result
496+
// is equal to the provisional result of the previous iteration, or because
497+
// this was only the root of either coinductive or inductive cycles, and the
498+
// final result is equal to the initial response for that case.
499+
let reached_fixpoint = if let Some(r) = stack_entry.provisional_result {
500+
r == result
501+
} else if stack_entry.has_been_used == HasBeenUsed::COINDUCTIVE_CYCLE {
502+
Self::response_no_constraints(tcx, input, Certainty::Yes) == result
503+
} else if stack_entry.has_been_used == HasBeenUsed::INDUCTIVE_CYCLE {
504+
Self::response_no_constraints(tcx, input, Certainty::overflow(false)) == result
505+
} else {
506+
false
507+
};
508+
509+
// If we did not reach a fixpoint, update the provisional result and reevaluate.
510+
if reached_fixpoint {
511+
StepResult::Done(stack_entry, result)
512+
} else {
513+
let depth = self.stack.push(StackEntry {
514+
has_been_used: HasBeenUsed::empty(),
515+
provisional_result: Some(result),
516+
..stack_entry
517+
});
518+
debug_assert_eq!(self.provisional_cache[&input].stack_depth, Some(depth));
519+
StepResult::HasChanged
520+
}
521+
}
499522

500523
fn response_no_constraints(
501524
tcx: TyCtxt<'tcx>,

0 commit comments

Comments
 (0)