@@ -215,6 +215,27 @@ impl HeadUsages {
215
215
let HeadUsages { inductive, unknown, coinductive, forced_ambiguity } = self ;
216
216
inductive == 0 && unknown == 0 && coinductive == 0 && forced_ambiguity == 0
217
217
}
218
+
219
+ fn is_single ( self , path_kind : PathKind ) -> bool {
220
+ match path_kind {
221
+ PathKind :: Inductive => matches ! (
222
+ self ,
223
+ HeadUsages { inductive: _, unknown: 0 , coinductive: 0 , forced_ambiguity: 0 } ,
224
+ ) ,
225
+ PathKind :: Unknown => matches ! (
226
+ self ,
227
+ HeadUsages { inductive: 0 , unknown: _, coinductive: 0 , forced_ambiguity: 0 } ,
228
+ ) ,
229
+ PathKind :: Coinductive => matches ! (
230
+ self ,
231
+ HeadUsages { inductive: 0 , unknown: 0 , coinductive: _, forced_ambiguity: 0 } ,
232
+ ) ,
233
+ PathKind :: ForcedAmbiguity => matches ! (
234
+ self ,
235
+ HeadUsages { inductive: 0 , unknown: 0 , coinductive: 0 , forced_ambiguity: _ } ,
236
+ ) ,
237
+ }
238
+ }
218
239
}
219
240
220
241
#[ derive( Debug , Default ) ]
@@ -888,7 +909,20 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
888
909
!entries. is_empty ( )
889
910
} ) ;
890
911
}
912
+ }
891
913
914
+ /// We need to rebase provisional cache entries when popping one of their cycle
915
+ /// heads from the stack. This may not necessarily mean that we've actually
916
+ /// reached a fixpoint for that cycle head, which impacts the way we rebase
917
+ /// provisional cache entries.
918
+ enum RebaseReason {
919
+ NoCycleUsages ,
920
+ Ambiguity ,
921
+ Overflow ,
922
+ ReachedFixpoint ( Option < PathKind > ) ,
923
+ }
924
+
925
+ impl < D : Delegate < Cx = X > , X : Cx > SearchGraph < D , X > {
892
926
/// A necessary optimization to handle complex solver cycles. A provisional cache entry
893
927
/// relies on a set of cycle heads and the path towards these heads. When popping a cycle
894
928
/// head from the stack after we've finished computing it, we can't be sure that the
@@ -908,8 +942,9 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
908
942
/// to me.
909
943
fn rebase_provisional_cache_entries (
910
944
& mut self ,
945
+ cx : X ,
911
946
stack_entry : & StackEntry < X > ,
912
- mut mutate_result : impl FnMut ( X :: Input , X :: Result ) -> X :: Result ,
947
+ rebase_reason : RebaseReason ,
913
948
) {
914
949
let popped_head_index = self . stack . next_index ( ) ;
915
950
#[ allow( rustc:: potential_query_instability) ]
@@ -927,6 +962,10 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
927
962
return true ;
928
963
} ;
929
964
965
+ let Some ( new_highest_head_index) = heads. opt_highest_cycle_head_index ( ) else {
966
+ return false ;
967
+ } ;
968
+
930
969
// We're rebasing an entry `e` over a head `p`. This head
931
970
// has a number of own heads `h` it depends on.
932
971
//
@@ -941,6 +980,22 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
941
980
heads. insert ( head_index, PathsToNested :: EMPTY , HeadUsages :: default ( ) ) ;
942
981
}
943
982
} else {
983
+ // We may need to mutate the result of our cycle head in case we did not reach
984
+ // a fixpoint.
985
+ * result = match rebase_reason {
986
+ RebaseReason :: NoCycleUsages => return false ,
987
+ RebaseReason :: Ambiguity => D :: propagate_ambiguity ( cx, input, * result) ,
988
+ RebaseReason :: Overflow => D :: on_fixpoint_overflow ( cx, input) ,
989
+ RebaseReason :: ReachedFixpoint ( None ) => * result,
990
+ RebaseReason :: ReachedFixpoint ( Some ( path_kind) ) => {
991
+ if popped_head. usages . is_single ( path_kind) {
992
+ * result
993
+ } else {
994
+ return false ;
995
+ }
996
+ }
997
+ } ;
998
+
944
999
// The entry `e` actually depends on the value of `p`. We need
945
1000
// to make sure that the value of `p` wouldn't change even if we
946
1001
// were to reevaluate it as a nested goal of `e` instead. For this
@@ -979,20 +1034,14 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
979
1034
}
980
1035
}
981
1036
982
- let Some ( head_index) = heads. opt_highest_cycle_head_index ( ) else {
983
- return false ;
984
- } ;
985
-
986
1037
// We now care about the path from the next highest cycle head to the
987
1038
// provisional cache entry.
988
1039
* path_from_head = path_from_head. extend ( Self :: cycle_path_kind (
989
1040
& self . stack ,
990
1041
stack_entry. step_kind_from_parent ,
991
- head_index ,
1042
+ new_highest_head_index ,
992
1043
) ) ;
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
+
996
1045
true
997
1046
} ) ;
998
1047
!entries. is_empty ( )
@@ -1213,28 +1262,31 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1213
1262
stack_entry : & StackEntry < X > ,
1214
1263
usages : HeadUsages ,
1215
1264
result : X :: Result ,
1216
- ) -> bool {
1265
+ ) -> Result < Option < PathKind > , ( ) > {
1217
1266
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
1267
+ if let Some ( provisional_result) = provisional_result {
1268
+ if provisional_result == result { Ok ( None ) } else { Err ( ( ) ) }
1222
1269
} else {
1223
- let check = |k| D :: is_initial_provisional_result ( cx, k, stack_entry. input , result) ;
1224
- match usages {
1270
+ let path_kind = match usages {
1225
1271
HeadUsages { inductive : _, unknown : 0 , coinductive : 0 , forced_ambiguity : 0 } => {
1226
- check ( PathKind :: Inductive )
1272
+ PathKind :: Inductive
1227
1273
}
1228
1274
HeadUsages { inductive : 0 , unknown : _, coinductive : 0 , forced_ambiguity : 0 } => {
1229
- check ( PathKind :: Unknown )
1275
+ PathKind :: Unknown
1230
1276
}
1231
1277
HeadUsages { inductive : 0 , unknown : 0 , coinductive : _, forced_ambiguity : 0 } => {
1232
- check ( PathKind :: Coinductive )
1278
+ PathKind :: Coinductive
1233
1279
}
1234
1280
HeadUsages { inductive : 0 , unknown : 0 , coinductive : 0 , forced_ambiguity : _ } => {
1235
- check ( PathKind :: ForcedAmbiguity )
1281
+ PathKind :: ForcedAmbiguity
1236
1282
}
1237
- _ => false ,
1283
+ _ => return Err ( ( ) ) ,
1284
+ } ;
1285
+
1286
+ if D :: is_initial_provisional_result ( cx, path_kind, stack_entry. input , result) {
1287
+ Ok ( Some ( path_kind) )
1288
+ } else {
1289
+ Err ( ( ) )
1238
1290
}
1239
1291
}
1240
1292
}
@@ -1280,8 +1332,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1280
1332
// is equal to the provisional result of the previous iteration, or because
1281
1333
// this was only the head of either coinductive or inductive cycles, and the
1282
1334
// 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) ;
1335
+ if let Ok ( fixpoint) = self . reached_fixpoint ( cx, & stack_entry, usages, result) {
1336
+ self . rebase_provisional_cache_entries (
1337
+ cx,
1338
+ & stack_entry,
1339
+ RebaseReason :: ReachedFixpoint ( fixpoint) ,
1340
+ ) ;
1341
+ return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1342
+ } else if usages. is_empty ( ) {
1343
+ self . rebase_provisional_cache_entries (
1344
+ cx,
1345
+ & stack_entry,
1346
+ RebaseReason :: NoCycleUsages ,
1347
+ ) ;
1285
1348
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1286
1349
}
1287
1350
@@ -1298,9 +1361,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1298
1361
// we also taint all provisional cache entries which depend on the
1299
1362
// current goal.
1300
1363
if D :: is_ambiguous_result ( result) {
1301
- self . rebase_provisional_cache_entries ( & stack_entry, |input, _| {
1302
- D :: propagate_ambiguity ( cx, input, result)
1303
- } ) ;
1364
+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Ambiguity ) ;
1304
1365
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1305
1366
} ;
1306
1367
@@ -1310,9 +1371,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1310
1371
if i >= D :: FIXPOINT_STEP_LIMIT {
1311
1372
debug ! ( "canonical cycle overflow" ) ;
1312
1373
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
- } ) ;
1374
+ self . rebase_provisional_cache_entries ( cx, & stack_entry, RebaseReason :: Overflow ) ;
1316
1375
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1317
1376
}
1318
1377
0 commit comments