@@ -86,14 +86,12 @@ pub trait Delegate: Sized {
86
86
kind : PathKind ,
87
87
input : <Self :: Cx as Cx >:: Input ,
88
88
) -> <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 (
90
91
cx : Self :: Cx ,
91
- kind : PathKind ,
92
92
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 (
97
95
cx : Self :: Cx ,
98
96
input : <Self :: Cx as Cx >:: Input ,
99
97
) -> <Self :: Cx as Cx >:: Result ;
@@ -215,6 +213,27 @@ impl HeadUsages {
215
213
let HeadUsages { inductive, unknown, coinductive, forced_ambiguity } = self ;
216
214
inductive == 0 && unknown == 0 && coinductive == 0 && forced_ambiguity == 0
217
215
}
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
+ }
218
237
}
219
238
220
239
#[ derive( Debug , Default ) ]
@@ -869,7 +888,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
869
888
}
870
889
871
890
debug ! ( "encountered stack overflow" ) ;
872
- D :: on_stack_overflow ( cx, input)
891
+ D :: stack_overflow_result ( cx, input)
873
892
}
874
893
875
894
/// 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> {
888
907
!entries. is_empty ( )
889
908
} ) ;
890
909
}
910
+ }
891
911
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 > {
892
933
/// A necessary optimization to handle complex solver cycles. A provisional cache entry
893
934
/// relies on a set of cycle heads and the path towards these heads. When popping a cycle
894
935
/// 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> {
908
949
/// to me.
909
950
fn rebase_provisional_cache_entries (
910
951
& mut self ,
952
+ cx : X ,
911
953
stack_entry : & StackEntry < X > ,
912
- mut mutate_result : impl FnMut ( X :: Input , X :: Result ) -> X :: Result ,
954
+ rebase_reason : RebaseReason ,
913
955
) {
914
956
let popped_head_index = self . stack . next_index ( ) ;
915
957
#[ allow( rustc:: potential_query_instability) ]
@@ -927,6 +969,10 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
927
969
return true ;
928
970
} ;
929
971
972
+ let Some ( new_highest_head_index) = heads. opt_highest_cycle_head_index ( ) else {
973
+ return false ;
974
+ } ;
975
+
930
976
// We're rebasing an entry `e` over a head `p`. This head
931
977
// has a number of own heads `h` it depends on.
932
978
//
@@ -977,22 +1023,37 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
977
1023
let eph = ep. extend_with_paths ( ph) ;
978
1024
heads. insert ( head_index, eph, head. usages ) ;
979
1025
}
980
- }
981
1026
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
+ }
985
1048
986
1049
// We now care about the path from the next highest cycle head to the
987
1050
// provisional cache entry.
988
1051
* path_from_head = path_from_head. extend ( Self :: cycle_path_kind (
989
1052
& self . stack ,
990
1053
stack_entry. step_kind_from_parent ,
991
- head_index ,
1054
+ new_highest_head_index ,
992
1055
) ) ;
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
+
996
1057
true
997
1058
} ) ;
998
1059
!entries. is_empty ( )
@@ -1209,33 +1270,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1209
1270
/// Whether we've reached a fixpoint when evaluating a cycle head.
1210
1271
fn reached_fixpoint (
1211
1272
& mut self ,
1212
- cx : X ,
1213
1273
stack_entry : & StackEntry < X > ,
1214
1274
usages : HeadUsages ,
1215
1275
result : X :: Result ,
1216
- ) -> bool {
1276
+ ) -> Result < Option < PathKind > , ( ) > {
1217
1277
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) )
1222
1284
} 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 ( ( ) )
1239
1286
}
1240
1287
}
1241
1288
@@ -1280,8 +1327,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1280
1327
// is equal to the provisional result of the previous iteration, or because
1281
1328
// this was only the head of either coinductive or inductive cycles, and the
1282
1329
// 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
+ ) ;
1285
1343
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1286
1344
}
1287
1345
@@ -1298,9 +1356,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1298
1356
// we also taint all provisional cache entries which depend on the
1299
1357
// current goal.
1300
1358
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 ) ;
1304
1360
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1305
1361
} ;
1306
1362
@@ -1309,10 +1365,8 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1309
1365
i += 1 ;
1310
1366
if i >= D :: FIXPOINT_STEP_LIMIT {
1311
1367
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 ) ;
1316
1370
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1317
1371
}
1318
1372
0 commit comments