@@ -86,14 +86,12 @@ pub trait Delegate: Sized {
8686 kind : PathKind ,
8787 input : <Self :: Cx as Cx >:: Input ,
8888 ) -> <Self :: Cx as Cx >:: Result ;
89- fn is_initial_provisional_result (
89+ fn is_initial_provisional_result ( result : <Self :: Cx as Cx >:: Result ) -> Option < PathKind > ;
90+ fn stack_overflow_result (
9091 cx : Self :: Cx ,
91- kind : PathKind ,
9292 input : <Self :: Cx as Cx >:: Input ,
93- result : <Self :: Cx as Cx >:: Result ,
94- ) -> bool ;
95- fn on_stack_overflow ( cx : Self :: Cx , input : <Self :: Cx as Cx >:: Input ) -> <Self :: Cx as Cx >:: Result ;
96- fn on_fixpoint_overflow (
93+ ) -> <Self :: Cx as Cx >:: Result ;
94+ fn fixpoint_overflow_result (
9795 cx : Self :: Cx ,
9896 input : <Self :: Cx as Cx >:: Input ,
9997 ) -> <Self :: Cx as Cx >:: Result ;
@@ -215,6 +213,27 @@ impl HeadUsages {
215213 let HeadUsages { inductive, unknown, coinductive, forced_ambiguity } = self ;
216214 inductive == 0 && unknown == 0 && coinductive == 0 && forced_ambiguity == 0
217215 }
216+
217+ fn is_single ( self , path_kind : PathKind ) -> bool {
218+ match path_kind {
219+ PathKind :: Inductive => matches ! (
220+ self ,
221+ HeadUsages { inductive: _, unknown: 0 , coinductive: 0 , forced_ambiguity: 0 } ,
222+ ) ,
223+ PathKind :: Unknown => matches ! (
224+ self ,
225+ HeadUsages { inductive: 0 , unknown: _, coinductive: 0 , forced_ambiguity: 0 } ,
226+ ) ,
227+ PathKind :: Coinductive => matches ! (
228+ self ,
229+ HeadUsages { inductive: 0 , unknown: 0 , coinductive: _, forced_ambiguity: 0 } ,
230+ ) ,
231+ PathKind :: ForcedAmbiguity => matches ! (
232+ self ,
233+ HeadUsages { inductive: 0 , unknown: 0 , coinductive: 0 , forced_ambiguity: _ } ,
234+ ) ,
235+ }
236+ }
218237}
219238
220239#[ derive( Debug , Default ) ]
@@ -869,7 +888,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
869888 }
870889
871890 debug ! ( "encountered stack overflow" ) ;
872- D :: on_stack_overflow ( cx, input)
891+ D :: stack_overflow_result ( cx, input)
873892 }
874893
875894 /// When reevaluating a goal with a changed provisional result, all provisional cache entry
@@ -888,7 +907,29 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
888907 !entries. is_empty ( )
889908 } ) ;
890909 }
910+ }
891911
912+ /// We need to rebase provisional cache entries when popping one of their cycle
913+ /// heads from the stack. This may not necessarily mean that we've actually
914+ /// reached a fixpoint for that cycle head, which impacts the way we rebase
915+ /// provisional cache entries.
916+ enum RebaseReason {
917+ NoCycleUsages ,
918+ Ambiguity ,
919+ Overflow ,
920+ /// We've actually reached a fixpoint.
921+ ///
922+ /// This either happens in the first evaluation step for the cycle head.
923+ /// In this case the used provisional result depends on the cycle `PathKind`.
924+ /// We store this path kind to check whether the the provisional cache entry
925+ /// we're rebasing relied on the same cycles.
926+ ///
927+ /// In later iterations cycles always return `stack_entry.provisional_result`
928+ /// so we no longer depend on the `PathKind`. We store `None` in that case.
929+ ReachedFixpoint ( Option < PathKind > ) ,
930+ }
931+
932+ impl < D : Delegate < Cx = X > , X : Cx > SearchGraph < D , X > {
892933 /// A necessary optimization to handle complex solver cycles. A provisional cache entry
893934 /// relies on a set of cycle heads and the path towards these heads. When popping a cycle
894935 /// head from the stack after we've finished computing it, we can't be sure that the
@@ -908,8 +949,9 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
908949 /// to me.
909950 fn rebase_provisional_cache_entries (
910951 & mut self ,
952+ cx : X ,
911953 stack_entry : & StackEntry < X > ,
912- mut mutate_result : impl FnMut ( X :: Input , X :: Result ) -> X :: Result ,
954+ rebase_reason : RebaseReason ,
913955 ) {
914956 let popped_head_index = self . stack . next_index ( ) ;
915957 #[ allow( rustc:: potential_query_instability) ]
@@ -927,6 +969,10 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
927969 return true ;
928970 } ;
929971
972+ let Some ( new_highest_head_index) = heads. opt_highest_cycle_head_index ( ) else {
973+ return false ;
974+ } ;
975+
930976 // We're rebasing an entry `e` over a head `p`. This head
931977 // has a number of own heads `h` it depends on.
932978 //
@@ -977,22 +1023,37 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
9771023 let eph = ep. extend_with_paths ( ph) ;
9781024 heads. insert ( head_index, eph, head. usages ) ;
9791025 }
980- }
9811026
982- let Some ( head_index) = heads. opt_highest_cycle_head_index ( ) else {
983- return false ;
984- } ;
1027+ // The provisional cache entry does depend on the provisional result
1028+ // of the popped cycle head. We need to mutate the result of our
1029+ // provisional cache entry in case we did not reach a fixpoint.
1030+ match rebase_reason {
1031+ // If the cycle head does not actually depend on itself, then
1032+ // the provisional result used by the provisional cache entry
1033+ // is not actually equal to the final provisional result. We
1034+ // need to discard the provisional cache entry in this case.
1035+ RebaseReason :: NoCycleUsages => return false ,
1036+ RebaseReason :: Ambiguity => {
1037+ * result = D :: propagate_ambiguity ( cx, input, * result) ;
1038+ }
1039+ RebaseReason :: Overflow => * result = D :: fixpoint_overflow_result ( cx, input) ,
1040+ RebaseReason :: ReachedFixpoint ( None ) => { }
1041+ RebaseReason :: ReachedFixpoint ( Some ( path_kind) ) => {
1042+ if !popped_head. usages . is_single ( path_kind) {
1043+ return false ;
1044+ }
1045+ }
1046+ } ;
1047+ }
9851048
9861049 // We now care about the path from the next highest cycle head to the
9871050 // provisional cache entry.
9881051 * path_from_head = path_from_head. extend ( Self :: cycle_path_kind (
9891052 & self . stack ,
9901053 stack_entry. step_kind_from_parent ,
991- head_index ,
1054+ new_highest_head_index ,
9921055 ) ) ;
993- // Mutate the result of the provisional cache entry in case we did
994- // not reach a fixpoint.
995- * result = mutate_result ( input, * result) ;
1056+
9961057 true
9971058 } ) ;
9981059 !entries. is_empty ( )
@@ -1209,33 +1270,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12091270 /// Whether we've reached a fixpoint when evaluating a cycle head.
12101271 fn reached_fixpoint (
12111272 & mut self ,
1212- cx : X ,
12131273 stack_entry : & StackEntry < X > ,
12141274 usages : HeadUsages ,
12151275 result : X :: Result ,
1216- ) -> bool {
1276+ ) -> Result < Option < PathKind > , ( ) > {
12171277 let provisional_result = stack_entry. provisional_result ;
1218- if usages. is_empty ( ) {
1219- true
1220- } else if let Some ( provisional_result) = provisional_result {
1221- provisional_result == result
1278+ if let Some ( provisional_result) = provisional_result {
1279+ if provisional_result == result { Ok ( None ) } else { Err ( ( ) ) }
1280+ } else if let Some ( path_kind) = D :: is_initial_provisional_result ( result)
1281+ . filter ( |& path_kind| usages. is_single ( path_kind) )
1282+ {
1283+ Ok ( Some ( path_kind) )
12221284 } else {
1223- let check = |k| D :: is_initial_provisional_result ( cx, k, stack_entry. input , result) ;
1224- match usages {
1225- HeadUsages { inductive : _, unknown : 0 , coinductive : 0 , forced_ambiguity : 0 } => {
1226- check ( PathKind :: Inductive )
1227- }
1228- HeadUsages { inductive : 0 , unknown : _, coinductive : 0 , forced_ambiguity : 0 } => {
1229- check ( PathKind :: Unknown )
1230- }
1231- HeadUsages { inductive : 0 , unknown : 0 , coinductive : _, forced_ambiguity : 0 } => {
1232- check ( PathKind :: Coinductive )
1233- }
1234- HeadUsages { inductive : 0 , unknown : 0 , coinductive : 0 , forced_ambiguity : _ } => {
1235- check ( PathKind :: ForcedAmbiguity )
1236- }
1237- _ => false ,
1238- }
1285+ Err ( ( ) )
12391286 }
12401287 }
12411288
@@ -1280,8 +1327,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12801327 // is equal to the provisional result of the previous iteration, or because
12811328 // this was only the head of either coinductive or inductive cycles, and the
12821329 // final result is equal to the initial response for that case.
1283- if self . reached_fixpoint ( cx, & stack_entry, usages, result) {
1284- self . rebase_provisional_cache_entries ( & stack_entry, |_, result| result) ;
1330+ if let Ok ( fixpoint) = self . reached_fixpoint ( & stack_entry, usages, result) {
1331+ self . rebase_provisional_cache_entries (
1332+ cx,
1333+ & stack_entry,
1334+ RebaseReason :: ReachedFixpoint ( fixpoint) ,
1335+ ) ;
1336+ return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1337+ } else if usages. is_empty ( ) {
1338+ self . rebase_provisional_cache_entries (
1339+ cx,
1340+ & stack_entry,
1341+ RebaseReason :: NoCycleUsages ,
1342+ ) ;
12851343 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
12861344 }
12871345
@@ -1298,9 +1356,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12981356 // we also taint all provisional cache entries which depend on the
12991357 // current goal.
13001358 if D :: is_ambiguous_result ( result) {
1301- self . rebase_provisional_cache_entries ( & stack_entry, |input, _| {
1302- D :: propagate_ambiguity ( cx, input, result)
1303- } ) ;
1359+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Ambiguity ) ;
13041360 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
13051361 } ;
13061362
@@ -1309,10 +1365,8 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
13091365 i += 1 ;
13101366 if i >= D :: FIXPOINT_STEP_LIMIT {
13111367 debug ! ( "canonical cycle overflow" ) ;
1312- let result = D :: on_fixpoint_overflow ( cx, input) ;
1313- self . rebase_provisional_cache_entries ( & stack_entry, |input, _| {
1314- D :: on_fixpoint_overflow ( cx, input)
1315- } ) ;
1368+ let result = D :: fixpoint_overflow_result ( cx, input) ;
1369+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Overflow ) ;
13161370 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
13171371 }
13181372
0 commit comments