@@ -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