@@ -71,7 +71,7 @@ struct StackEntry<I: Interner> {
7171 /// C :- D
7272 /// D :- C
7373 /// ```
74- cycle_participants : HashSet < CanonicalInput < I > > ,
74+ nested_goals : HashSet < CanonicalInput < I > > ,
7575 /// Starts out as `None` and gets set when rerunning this
7676 /// goal in case we encounter a cycle.
7777 provisional_result : Option < QueryResult < I > > ,
@@ -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 {
@@ -222,8 +215,8 @@ impl<I: Interner> SearchGraph<I> {
222215 let current_cycle_root = & mut stack[ current_root. as_usize ( ) ] ;
223216 for entry in cycle_participants {
224217 entry. non_root_cycle_participant = entry. non_root_cycle_participant . max ( Some ( head) ) ;
225- current_cycle_root. cycle_participants . insert ( entry. input ) ;
226- current_cycle_root. cycle_participants . extend ( mem:: take ( & mut entry. cycle_participants ) ) ;
218+ current_cycle_root. nested_goals . insert ( entry. input ) ;
219+ current_cycle_root. nested_goals . extend ( mem:: take ( & mut entry. nested_goals ) ) ;
227220 }
228221 }
229222
@@ -342,7 +335,7 @@ impl<I: Interner> SearchGraph<I> {
342335 non_root_cycle_participant : None ,
343336 encountered_overflow : false ,
344337 has_been_used : HasBeenUsed :: empty ( ) ,
345- cycle_participants : Default :: default ( ) ,
338+ nested_goals : Default :: default ( ) ,
346339 provisional_result : None ,
347340 } ;
348341 assert_eq ! ( self . stack. push( entry) , depth) ;
@@ -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.
@@ -394,15 +389,15 @@ impl<I: Interner> SearchGraph<I> {
394389 //
395390 // We must not use the global cache entry of a root goal if a cycle
396391 // participant is on the stack. This is necessary to prevent unstable
397- // results. See the comment of `StackEntry::cycle_participants ` for
392+ // results. See the comment of `StackEntry::nested_goals ` for
398393 // more details.
399394 self . global_cache ( cx) . insert (
400395 cx,
401396 input,
402397 proof_tree,
403398 reached_depth,
404399 final_entry. encountered_overflow ,
405- final_entry. cycle_participants ,
400+ final_entry. nested_goals ,
406401 dep_node,
407402 result,
408403 )
@@ -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.
@@ -554,27 +544,27 @@ impl<I: Interner> SearchGraph<I> {
554544 non_root_cycle_participant,
555545 encountered_overflow : _,
556546 has_been_used,
557- ref cycle_participants ,
547+ ref nested_goals ,
558548 provisional_result,
559549 } = * entry;
560550 let cache_entry = provisional_cache. get ( & entry. input ) . unwrap ( ) ;
561551 assert_eq ! ( cache_entry. stack_depth, Some ( depth) ) ;
562552 if let Some ( head) = non_root_cycle_participant {
563553 assert ! ( head < depth) ;
564- assert ! ( cycle_participants . is_empty( ) ) ;
554+ assert ! ( nested_goals . is_empty( ) ) ;
565555 assert_ne ! ( stack[ head] . has_been_used, HasBeenUsed :: empty( ) ) ;
566556
567557 let mut current_root = head;
568558 while let Some ( parent) = stack[ current_root] . non_root_cycle_participant {
569559 current_root = parent;
570560 }
571- assert ! ( stack[ current_root] . cycle_participants . contains( & input) ) ;
561+ assert ! ( stack[ current_root] . nested_goals . contains( & input) ) ;
572562 }
573563
574- if !cycle_participants . is_empty ( ) {
564+ if !nested_goals . is_empty ( ) {
575565 assert ! ( provisional_result. is_some( ) || !has_been_used. is_empty( ) ) ;
576566 for entry in stack. iter ( ) . take ( depth. as_usize ( ) ) {
577- assert_eq ! ( cycle_participants . get( & entry. input) , None ) ;
567+ assert_eq ! ( nested_goals . get( & entry. input) , None ) ;
578568 }
579569 }
580570 }
0 commit comments