@@ -86,12 +86,7 @@ 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 (
90- cx : Self :: Cx ,
91- kind : PathKind ,
92- input : <Self :: Cx as Cx >:: Input ,
93- result : <Self :: Cx as Cx >:: Result ,
94- ) -> bool ;
89+ fn is_initial_provisional_result ( result : <Self :: Cx as Cx >:: Result ) -> Option < PathKind > ;
9590 fn on_stack_overflow ( cx : Self :: Cx , input : <Self :: Cx as Cx >:: Input ) -> <Self :: Cx as Cx >:: Result ;
9691 fn on_fixpoint_overflow (
9792 cx : Self :: Cx ,
@@ -215,6 +210,27 @@ impl HeadUsages {
215210 let HeadUsages { inductive, unknown, coinductive, forced_ambiguity } = self ;
216211 inductive == 0 && unknown == 0 && coinductive == 0 && forced_ambiguity == 0
217212 }
213+
214+ fn is_single ( self , path_kind : PathKind ) -> bool {
215+ match path_kind {
216+ PathKind :: Inductive => matches ! (
217+ self ,
218+ HeadUsages { inductive: _, unknown: 0 , coinductive: 0 , forced_ambiguity: 0 } ,
219+ ) ,
220+ PathKind :: Unknown => matches ! (
221+ self ,
222+ HeadUsages { inductive: 0 , unknown: _, coinductive: 0 , forced_ambiguity: 0 } ,
223+ ) ,
224+ PathKind :: Coinductive => matches ! (
225+ self ,
226+ HeadUsages { inductive: 0 , unknown: 0 , coinductive: _, forced_ambiguity: 0 } ,
227+ ) ,
228+ PathKind :: ForcedAmbiguity => matches ! (
229+ self ,
230+ HeadUsages { inductive: 0 , unknown: 0 , coinductive: 0 , forced_ambiguity: _ } ,
231+ ) ,
232+ }
233+ }
218234}
219235
220236#[ derive( Debug , Default ) ]
@@ -888,7 +904,20 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
888904 !entries. is_empty ( )
889905 } ) ;
890906 }
907+ }
908+
909+ /// We need to rebase provisional cache entries when popping one of their cycle
910+ /// heads from the stack. This may not necessarily mean that we've actually
911+ /// reached a fixpoint for that cycle head, which impacts the way we rebase
912+ /// provisional cache entries.
913+ enum RebaseReason {
914+ NoCycleUsages ,
915+ Ambiguity ,
916+ Overflow ,
917+ ReachedFixpoint ( Option < PathKind > ) ,
918+ }
891919
920+ impl < D : Delegate < Cx = X > , X : Cx > SearchGraph < D , X > {
892921 /// A necessary optimization to handle complex solver cycles. A provisional cache entry
893922 /// relies on a set of cycle heads and the path towards these heads. When popping a cycle
894923 /// head from the stack after we've finished computing it, we can't be sure that the
@@ -908,8 +937,9 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
908937 /// to me.
909938 fn rebase_provisional_cache_entries (
910939 & mut self ,
940+ cx : X ,
911941 stack_entry : & StackEntry < X > ,
912- mut mutate_result : impl FnMut ( X :: Input , X :: Result ) -> X :: Result ,
942+ rebase_reason : RebaseReason ,
913943 ) {
914944 let popped_head_index = self . stack . next_index ( ) ;
915945 #[ allow( rustc:: potential_query_instability) ]
@@ -927,6 +957,10 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
927957 return true ;
928958 } ;
929959
960+ let Some ( new_highest_head_index) = heads. opt_highest_cycle_head_index ( ) else {
961+ return false ;
962+ } ;
963+
930964 // We're rebasing an entry `e` over a head `p`. This head
931965 // has a number of own heads `h` it depends on.
932966 //
@@ -977,22 +1011,37 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
9771011 let eph = ep. extend_with_paths ( ph) ;
9781012 heads. insert ( head_index, eph, head. usages ) ;
9791013 }
980- }
9811014
982- let Some ( head_index) = heads. opt_highest_cycle_head_index ( ) else {
983- return false ;
984- } ;
1015+ // The provisional cache entry does depend on the provisional result
1016+ // of the popped cycle head. We need to mutate the result of our
1017+ // provisional cache entry in case we did not reach a fixpoint.
1018+ match rebase_reason {
1019+ // If the cycle head does not actually depend on itself, then
1020+ // the provisional result used by the provisional cache entry
1021+ // is not actually equal to the final provisional result. We
1022+ // need to discard the provisional cache entry in this case.
1023+ RebaseReason :: NoCycleUsages => return false ,
1024+ RebaseReason :: Ambiguity => {
1025+ * result = D :: propagate_ambiguity ( cx, input, * result) ;
1026+ }
1027+ RebaseReason :: Overflow => * result = D :: on_fixpoint_overflow ( cx, input) ,
1028+ RebaseReason :: ReachedFixpoint ( None ) => { }
1029+ RebaseReason :: ReachedFixpoint ( Some ( path_kind) ) => {
1030+ if !popped_head. usages . is_single ( path_kind) {
1031+ return false ;
1032+ }
1033+ }
1034+ } ;
1035+ }
9851036
9861037 // We now care about the path from the next highest cycle head to the
9871038 // provisional cache entry.
9881039 * path_from_head = path_from_head. extend ( Self :: cycle_path_kind (
9891040 & self . stack ,
9901041 stack_entry. step_kind_from_parent ,
991- head_index ,
1042+ new_highest_head_index ,
9921043 ) ) ;
993- // Mutate the result of the provisional cache entry in case we did
994- // not reach a fixpoint.
995- * result = mutate_result ( input, * result) ;
1044+
9961045 true
9971046 } ) ;
9981047 !entries. is_empty ( )
@@ -1209,33 +1258,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12091258 /// Whether we've reached a fixpoint when evaluating a cycle head.
12101259 fn reached_fixpoint (
12111260 & mut self ,
1212- cx : X ,
12131261 stack_entry : & StackEntry < X > ,
12141262 usages : HeadUsages ,
12151263 result : X :: Result ,
1216- ) -> bool {
1264+ ) -> Result < Option < PathKind > , ( ) > {
12171265 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
1266+ if let Some ( provisional_result) = provisional_result {
1267+ if provisional_result == result { Ok ( None ) } else { Err ( ( ) ) }
1268+ } else if let Some ( path_kind) = D :: is_initial_provisional_result ( result)
1269+ . filter ( |& path_kind| usages. is_single ( path_kind) )
1270+ {
1271+ Ok ( Some ( path_kind) )
12221272 } 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- }
1273+ Err ( ( ) )
12391274 }
12401275 }
12411276
@@ -1280,8 +1315,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12801315 // is equal to the provisional result of the previous iteration, or because
12811316 // this was only the head of either coinductive or inductive cycles, and the
12821317 // 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) ;
1318+ if let Ok ( fixpoint) = self . reached_fixpoint ( & stack_entry, usages, result) {
1319+ self . rebase_provisional_cache_entries (
1320+ cx,
1321+ & stack_entry,
1322+ RebaseReason :: ReachedFixpoint ( fixpoint) ,
1323+ ) ;
1324+ return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1325+ } else if usages. is_empty ( ) {
1326+ self . rebase_provisional_cache_entries (
1327+ cx,
1328+ & stack_entry,
1329+ RebaseReason :: NoCycleUsages ,
1330+ ) ;
12851331 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
12861332 }
12871333
@@ -1298,9 +1344,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12981344 // we also taint all provisional cache entries which depend on the
12991345 // current goal.
13001346 if D :: is_ambiguous_result ( result) {
1301- self . rebase_provisional_cache_entries ( & stack_entry, |input, _| {
1302- D :: propagate_ambiguity ( cx, input, result)
1303- } ) ;
1347+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Ambiguity ) ;
13041348 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
13051349 } ;
13061350
@@ -1310,9 +1354,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
13101354 if i >= D :: FIXPOINT_STEP_LIMIT {
13111355 debug ! ( "canonical cycle overflow" ) ;
13121356 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- } ) ;
1357+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Overflow ) ;
13161358 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
13171359 }
13181360
0 commit comments