@@ -26,6 +26,8 @@ use tracing::debug;
26
26
27
27
use crate :: data_structures:: HashMap ;
28
28
29
+ mod stack;
30
+ use stack:: { Stack , StackDepth , StackEntry } ;
29
31
mod global_cache;
30
32
use global_cache:: CacheData ;
31
33
pub use global_cache:: GlobalCache ;
@@ -225,9 +227,9 @@ impl AvailableDepth {
225
227
/// in case there is exponential blowup.
226
228
fn allowed_depth_for_nested < D : Delegate > (
227
229
root_depth : AvailableDepth ,
228
- stack : & IndexVec < StackDepth , StackEntry < D :: Cx > > ,
230
+ stack : & Stack < D :: Cx > ,
229
231
) -> Option < AvailableDepth > {
230
- if let Some ( last) = stack. raw . last ( ) {
232
+ if let Some ( last) = stack. last ( ) {
231
233
if last. available_depth . 0 == 0 {
232
234
return None ;
233
235
}
@@ -433,50 +435,6 @@ impl<X: Cx> NestedGoals<X> {
433
435
}
434
436
}
435
437
436
- rustc_index:: newtype_index! {
437
- #[ orderable]
438
- #[ gate_rustc_only]
439
- pub struct StackDepth { }
440
- }
441
-
442
- /// Stack entries of the evaluation stack. Its fields tend to be lazily
443
- /// when popping a child goal or completely immutable.
444
- #[ derive_where( Debug ; X : Cx ) ]
445
- struct StackEntry < X : Cx > {
446
- input : X :: Input ,
447
-
448
- /// Whether proving this goal is a coinductive step.
449
- ///
450
- /// This is used when encountering a trait solver cycle to
451
- /// decide whether the initial provisional result of the cycle.
452
- step_kind_from_parent : PathKind ,
453
-
454
- /// The available depth of a given goal, immutable.
455
- available_depth : AvailableDepth ,
456
-
457
- /// The maximum depth reached by this stack entry, only up-to date
458
- /// for the top of the stack and lazily updated for the rest.
459
- reached_depth : StackDepth ,
460
-
461
- /// All cycle heads this goal depends on. Lazily updated and only
462
- /// up-to date for the top of the stack.
463
- heads : CycleHeads ,
464
-
465
- /// Whether evaluating this goal encountered overflow. Lazily updated.
466
- encountered_overflow : bool ,
467
-
468
- /// Whether this goal has been used as the root of a cycle. This gets
469
- /// eagerly updated when encountering a cycle.
470
- has_been_used : Option < UsageKind > ,
471
-
472
- /// The nested goals of this goal, see the doc comment of the type.
473
- nested_goals : NestedGoals < X > ,
474
-
475
- /// Starts out as `None` and gets set when rerunning this
476
- /// goal in case we encounter a cycle.
477
- provisional_result : Option < X :: Result > ,
478
- }
479
-
480
438
/// A provisional result of an already computed goals which depends on other
481
439
/// goals still on the stack.
482
440
#[ derive_where( Debug ; X : Cx ) ]
@@ -498,7 +456,7 @@ pub struct SearchGraph<D: Delegate<Cx = X>, X: Cx = <D as Delegate>::Cx> {
498
456
/// The stack of goals currently being computed.
499
457
///
500
458
/// An element is *deeper* in the stack if its index is *lower*.
501
- stack : IndexVec < StackDepth , StackEntry < X > > ,
459
+ stack : Stack < X > ,
502
460
/// The provisional cache contains entries for already computed goals which
503
461
/// still depend on goals higher-up in the stack. We don't move them to the
504
462
/// global cache and track them locally instead. A provisional cache entry
@@ -537,7 +495,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
537
495
/// and using existing global cache entries to make sure they
538
496
/// have the same impact on the remaining evaluation.
539
497
fn update_parent_goal (
540
- stack : & mut IndexVec < StackDepth , StackEntry < X > > ,
498
+ stack : & mut Stack < X > ,
541
499
step_kind_from_parent : PathKind ,
542
500
reached_depth : StackDepth ,
543
501
heads : & CycleHeads ,
@@ -588,13 +546,11 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
588
546
/// the stack which completes the cycle. This given an inductive step AB which then cycles
589
547
/// coinductively with A, we need to treat this cycle as coinductive.
590
548
fn cycle_path_kind (
591
- stack : & IndexVec < StackDepth , StackEntry < X > > ,
549
+ stack : & Stack < X > ,
592
550
step_kind_to_head : PathKind ,
593
551
head : StackDepth ,
594
552
) -> PathKind {
595
- stack. raw [ head. index ( ) + 1 ..]
596
- . iter ( )
597
- . fold ( step_kind_to_head, |curr, entry| curr. extend ( entry. step_kind_from_parent ) )
553
+ stack. cycle_step_kinds ( head) . fold ( step_kind_to_head, |curr, step| curr. extend ( step) )
598
554
}
599
555
600
556
/// Probably the most involved method of the whole solver.
@@ -728,7 +684,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
728
684
input : X :: Input ,
729
685
inspect : & mut D :: ProofTreeBuilder ,
730
686
) -> X :: Result {
731
- if let Some ( last) = self . stack . raw . last_mut ( ) {
687
+ if let Some ( last) = self . stack . last_mut ( ) {
732
688
last. encountered_overflow = true ;
733
689
// If computing a goal `B` depends on another goal `A` and
734
690
// `A` has a nested goal which overflows, then computing `B`
@@ -859,7 +815,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
859
815
// apply provisional cache entries which encountered overflow once the
860
816
// current goal is already part of the same cycle. This check could be
861
817
// improved but seems to be good enough for now.
862
- let last = self . stack . raw . last ( ) . unwrap ( ) ;
818
+ let last = self . stack . last ( ) . unwrap ( ) ;
863
819
if last. heads . opt_lowest_cycle_head ( ) . is_none_or ( |lowest| lowest > head) {
864
820
continue ;
865
821
}
@@ -893,7 +849,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
893
849
/// evaluating this entry would not have ended up depending on either a goal
894
850
/// already on the stack or a provisional cache entry.
895
851
fn candidate_is_applicable (
896
- stack : & IndexVec < StackDepth , StackEntry < X > > ,
852
+ stack : & Stack < X > ,
897
853
step_kind_from_parent : PathKind ,
898
854
provisional_cache : & HashMap < X :: Input , Vec < ProvisionalCacheEntry < X > > > ,
899
855
nested_goals : & NestedGoals < X > ,
@@ -1028,7 +984,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1028
984
input : X :: Input ,
1029
985
step_kind_from_parent : PathKind ,
1030
986
) -> Option < X :: Result > {
1031
- let ( head, _stack_entry ) = self . stack . iter_enumerated ( ) . find ( | ( _ , e ) | e . input == input) ?;
987
+ let head = self . stack . find ( input) ?;
1032
988
// We have a nested goal which directly relies on a goal deeper in the stack.
1033
989
//
1034
990
// We start by tagging all cycle participants, as that's necessary for caching.
@@ -1095,7 +1051,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1095
1051
let mut i = 0 ;
1096
1052
loop {
1097
1053
let result = evaluate_goal ( self , inspect) ;
1098
- let stack_entry = self . stack . pop ( ) . unwrap ( ) ;
1054
+ let stack_entry = self . stack . pop ( ) ;
1099
1055
debug_assert_eq ! ( stack_entry. input, input) ;
1100
1056
1101
1057
// If the current goal is not the root of a cycle, we are done.
0 commit comments