@@ -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 //
@@ -941,6 +975,22 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
941975 heads. insert ( head_index, PathsToNested :: EMPTY , HeadUsages :: default ( ) ) ;
942976 }
943977 } else {
978+ // We may need to mutate the result of our cycle head in case we did not reach
979+ // a fixpoint.
980+ * result = match rebase_reason {
981+ RebaseReason :: NoCycleUsages => return false ,
982+ RebaseReason :: Ambiguity => D :: propagate_ambiguity ( cx, input, * result) ,
983+ RebaseReason :: Overflow => D :: on_fixpoint_overflow ( cx, input) ,
984+ RebaseReason :: ReachedFixpoint ( None ) => * result,
985+ RebaseReason :: ReachedFixpoint ( Some ( path_kind) ) => {
986+ if popped_head. usages . is_single ( path_kind) {
987+ * result
988+ } else {
989+ return false ;
990+ }
991+ }
992+ } ;
993+
944994 // The entry `e` actually depends on the value of `p`. We need
945995 // to make sure that the value of `p` wouldn't change even if we
946996 // were to reevaluate it as a nested goal of `e` instead. For this
@@ -979,20 +1029,14 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
9791029 }
9801030 }
9811031
982- let Some ( head_index) = heads. opt_highest_cycle_head_index ( ) else {
983- return false ;
984- } ;
985-
9861032 // We now care about the path from the next highest cycle head to the
9871033 // provisional cache entry.
9881034 * path_from_head = path_from_head. extend ( Self :: cycle_path_kind (
9891035 & self . stack ,
9901036 stack_entry. step_kind_from_parent ,
991- head_index ,
1037+ new_highest_head_index ,
9921038 ) ) ;
993- // Mutate the result of the provisional cache entry in case we did
994- // not reach a fixpoint.
995- * result = mutate_result ( input, * result) ;
1039+
9961040 true
9971041 } ) ;
9981042 !entries. is_empty ( )
@@ -1209,33 +1253,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12091253 /// Whether we've reached a fixpoint when evaluating a cycle head.
12101254 fn reached_fixpoint (
12111255 & mut self ,
1212- cx : X ,
12131256 stack_entry : & StackEntry < X > ,
12141257 usages : HeadUsages ,
12151258 result : X :: Result ,
1216- ) -> bool {
1259+ ) -> Result < Option < PathKind > , ( ) > {
12171260 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
1261+ if let Some ( provisional_result) = provisional_result {
1262+ if provisional_result == result { Ok ( None ) } else { Err ( ( ) ) }
1263+ } else if let Some ( path_kind) = D :: is_initial_provisional_result ( result)
1264+ . filter ( |& path_kind| usages. is_single ( path_kind) )
1265+ {
1266+ Ok ( Some ( path_kind) )
12221267 } 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- }
1268+ Err ( ( ) )
12391269 }
12401270 }
12411271
@@ -1280,8 +1310,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12801310 // is equal to the provisional result of the previous iteration, or because
12811311 // this was only the head of either coinductive or inductive cycles, and the
12821312 // 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) ;
1313+ if let Ok ( fixpoint) = self . reached_fixpoint ( & stack_entry, usages, result) {
1314+ self . rebase_provisional_cache_entries (
1315+ cx,
1316+ & stack_entry,
1317+ RebaseReason :: ReachedFixpoint ( fixpoint) ,
1318+ ) ;
1319+ return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1320+ } else if usages. is_empty ( ) {
1321+ self . rebase_provisional_cache_entries (
1322+ cx,
1323+ & stack_entry,
1324+ RebaseReason :: NoCycleUsages ,
1325+ ) ;
12851326 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
12861327 }
12871328
@@ -1298,9 +1339,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12981339 // we also taint all provisional cache entries which depend on the
12991340 // current goal.
13001341 if D :: is_ambiguous_result ( result) {
1301- self . rebase_provisional_cache_entries ( & stack_entry, |input, _| {
1302- D :: propagate_ambiguity ( cx, input, result)
1303- } ) ;
1342+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Ambiguity ) ;
13041343 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
13051344 } ;
13061345
@@ -1310,9 +1349,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
13101349 if i >= D :: FIXPOINT_STEP_LIMIT {
13111350 debug ! ( "canonical cycle overflow" ) ;
13121351 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- } ) ;
1352+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Overflow ) ;
13161353 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
13171354 }
13181355
0 commit comments