@@ -71,7 +71,7 @@ struct StackEntry<I: Interner> {
71
71
/// C :- D
72
72
/// D :- C
73
73
/// ```
74
- cycle_participants : HashSet < CanonicalInput < I > > ,
74
+ nested_goals : HashSet < CanonicalInput < I > > ,
75
75
/// Starts out as `None` and gets set when rerunning this
76
76
/// goal in case we encounter a cycle.
77
77
provisional_result : Option < QueryResult < I > > ,
@@ -139,18 +139,11 @@ impl<I: Interner> SearchGraph<I> {
139
139
self . mode
140
140
}
141
141
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;
152
146
}
153
- elem
154
147
}
155
148
156
149
pub ( super ) fn is_empty ( & self ) -> bool {
@@ -222,8 +215,8 @@ impl<I: Interner> SearchGraph<I> {
222
215
let current_cycle_root = & mut stack[ current_root. as_usize ( ) ] ;
223
216
for entry in cycle_participants {
224
217
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 ) ) ;
227
220
}
228
221
}
229
222
@@ -342,7 +335,7 @@ impl<I: Interner> SearchGraph<I> {
342
335
non_root_cycle_participant : None ,
343
336
encountered_overflow : false ,
344
337
has_been_used : HasBeenUsed :: empty ( ) ,
345
- cycle_participants : Default :: default ( ) ,
338
+ nested_goals : Default :: default ( ) ,
346
339
provisional_result : None ,
347
340
} ;
348
341
assert_eq ! ( self . stack. push( entry) , depth) ;
@@ -364,14 +357,16 @@ impl<I: Interner> SearchGraph<I> {
364
357
}
365
358
366
359
debug ! ( "canonical cycle overflow" ) ;
367
- let current_entry = self . pop_stack ( ) ;
360
+ let current_entry = self . stack . pop ( ) . unwrap ( ) ;
368
361
debug_assert ! ( current_entry. has_been_used. is_empty( ) ) ;
369
362
let result = Self :: response_no_constraints ( cx, input, Certainty :: overflow ( false ) ) ;
370
363
( current_entry, result)
371
364
} ) ;
372
365
373
366
let proof_tree = inspect. finalize_canonical_goal_evaluation ( cx) ;
374
367
368
+ self . update_parent_goal ( final_entry. reached_depth , final_entry. encountered_overflow ) ;
369
+
375
370
// We're now done with this goal. In case this goal is involved in a larger cycle
376
371
// do not remove it from the provisional cache and update its provisional result.
377
372
// We only add the root of cycles to the global cache.
@@ -394,15 +389,15 @@ impl<I: Interner> SearchGraph<I> {
394
389
//
395
390
// We must not use the global cache entry of a root goal if a cycle
396
391
// 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
398
393
// more details.
399
394
self . global_cache ( cx) . insert (
400
395
cx,
401
396
input,
402
397
proof_tree,
403
398
reached_depth,
404
399
final_entry. encountered_overflow ,
405
- final_entry. cycle_participants ,
400
+ final_entry. nested_goals ,
406
401
dep_node,
407
402
result,
408
403
)
@@ -441,14 +436,9 @@ impl<I: Interner> SearchGraph<I> {
441
436
}
442
437
}
443
438
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.
447
440
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) ;
452
442
453
443
Some ( result)
454
444
}
@@ -477,7 +467,7 @@ impl<I: Interner> SearchGraph<I> {
477
467
F : FnMut ( & mut Self , & mut ProofTreeBuilder < D > ) -> QueryResult < I > ,
478
468
{
479
469
let result = prove_goal ( self , inspect) ;
480
- let stack_entry = self . pop_stack ( ) ;
470
+ let stack_entry = self . stack . pop ( ) . unwrap ( ) ;
481
471
debug_assert_eq ! ( stack_entry. input, input) ;
482
472
483
473
// If the current goal is not the root of a cycle, we are done.
@@ -554,27 +544,27 @@ impl<I: Interner> SearchGraph<I> {
554
544
non_root_cycle_participant,
555
545
encountered_overflow : _,
556
546
has_been_used,
557
- ref cycle_participants ,
547
+ ref nested_goals ,
558
548
provisional_result,
559
549
} = * entry;
560
550
let cache_entry = provisional_cache. get ( & entry. input ) . unwrap ( ) ;
561
551
assert_eq ! ( cache_entry. stack_depth, Some ( depth) ) ;
562
552
if let Some ( head) = non_root_cycle_participant {
563
553
assert ! ( head < depth) ;
564
- assert ! ( cycle_participants . is_empty( ) ) ;
554
+ assert ! ( nested_goals . is_empty( ) ) ;
565
555
assert_ne ! ( stack[ head] . has_been_used, HasBeenUsed :: empty( ) ) ;
566
556
567
557
let mut current_root = head;
568
558
while let Some ( parent) = stack[ current_root] . non_root_cycle_participant {
569
559
current_root = parent;
570
560
}
571
- assert ! ( stack[ current_root] . cycle_participants . contains( & input) ) ;
561
+ assert ! ( stack[ current_root] . nested_goals . contains( & input) ) ;
572
562
}
573
563
574
- if !cycle_participants . is_empty ( ) {
564
+ if !nested_goals . is_empty ( ) {
575
565
assert ! ( provisional_result. is_some( ) || !has_been_used. is_empty( ) ) ;
576
566
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 ) ;
578
568
}
579
569
}
580
570
}
0 commit comments