@@ -139,18 +139,11 @@ impl<I: Interner> SearchGraph<I> {
139139 self . mode
140140 }
141141
142- /// Pops the highest goal from the stack, lazily updating the
143- /// the next goal in the stack.
144- ///
145- /// Directly popping from the stack instead of using this method
146- /// would cause us to not track overflow and recursion depth correctly.
147- fn pop_stack ( & mut self ) -> StackEntry < I > {
148- let elem = self . stack . pop ( ) . unwrap ( ) ;
149- if let Some ( last) = self . stack . raw . last_mut ( ) {
150- last. reached_depth = last. reached_depth . max ( elem. reached_depth ) ;
151- last. encountered_overflow |= elem. encountered_overflow ;
142+ fn update_parent_goal ( & mut self , reached_depth : StackDepth , encountered_overflow : bool ) {
143+ if let Some ( parent) = self . stack . raw . last_mut ( ) {
144+ parent. reached_depth = parent. reached_depth . max ( reached_depth) ;
145+ parent. encountered_overflow |= encountered_overflow;
152146 }
153- elem
154147 }
155148
156149 pub ( super ) fn is_empty ( & self ) -> bool {
@@ -364,14 +357,16 @@ impl<I: Interner> SearchGraph<I> {
364357 }
365358
366359 debug ! ( "canonical cycle overflow" ) ;
367- let current_entry = self . pop_stack ( ) ;
360+ let current_entry = self . stack . pop ( ) . unwrap ( ) ;
368361 debug_assert ! ( current_entry. has_been_used. is_empty( ) ) ;
369362 let result = Self :: response_no_constraints ( cx, input, Certainty :: overflow ( false ) ) ;
370363 ( current_entry, result)
371364 } ) ;
372365
373366 let proof_tree = inspect. finalize_canonical_goal_evaluation ( cx) ;
374367
368+ self . update_parent_goal ( final_entry. reached_depth , final_entry. encountered_overflow ) ;
369+
375370 // We're now done with this goal. In case this goal is involved in a larger cycle
376371 // do not remove it from the provisional cache and update its provisional result.
377372 // We only add the root of cycles to the global cache.
@@ -441,14 +436,9 @@ impl<I: Interner> SearchGraph<I> {
441436 }
442437 }
443438
444- // Update the reached depth of the current goal to make sure
445- // its state is the same regardless of whether we've used the
446- // global cache or not.
439+ // Adjust the parent goal as if we actually computed this goal.
447440 let reached_depth = self . stack . next_index ( ) . plus ( additional_depth) ;
448- if let Some ( last) = self . stack . raw . last_mut ( ) {
449- last. reached_depth = last. reached_depth . max ( reached_depth) ;
450- last. encountered_overflow |= encountered_overflow;
451- }
441+ self . update_parent_goal ( reached_depth, encountered_overflow) ;
452442
453443 Some ( result)
454444 }
@@ -477,7 +467,7 @@ impl<I: Interner> SearchGraph<I> {
477467 F : FnMut ( & mut Self , & mut ProofTreeBuilder < D > ) -> QueryResult < I > ,
478468 {
479469 let result = prove_goal ( self , inspect) ;
480- let stack_entry = self . pop_stack ( ) ;
470+ let stack_entry = self . stack . pop ( ) . unwrap ( ) ;
481471 debug_assert_eq ! ( stack_entry. input, input) ;
482472
483473 // If the current goal is not the root of a cycle, we are done.
0 commit comments