@@ -170,28 +170,38 @@ impl PathKind {
170
170
/// This is used to avoid rerunning a cycle if there's
171
171
/// just a single usage kind and the final result matches
172
172
/// its provisional result.
173
- #[ derive( Debug , Clone , Copy , PartialEq , Eq ) ]
174
- pub enum UsageKind {
175
- Single ( PathKind ) ,
176
- Mixed ,
173
+ #[ derive( Default , Debug , Clone , Copy , PartialEq , Eq ) ]
174
+ struct Usages {
175
+ inductive : u32 ,
176
+ unknown : u32 ,
177
+ coinductive : u32 ,
178
+ forced_ambiguity : u32 ,
177
179
}
178
- impl From < PathKind > for UsageKind {
179
- fn from ( path : PathKind ) -> UsageKind {
180
- UsageKind :: Single ( path)
180
+
181
+ impl Usages {
182
+ fn add_usage ( & mut self , path : PathKind ) {
183
+ match path {
184
+ PathKind :: Inductive => self . inductive += 1 ,
185
+ PathKind :: Unknown => self . unknown += 1 ,
186
+ PathKind :: Coinductive => self . coinductive += 1 ,
187
+ PathKind :: ForcedAmbiguity => self . forced_ambiguity += 1 ,
188
+ }
181
189
}
182
- }
183
- impl UsageKind {
184
- #[ must_use]
185
- fn merge ( self , other : impl Into < Self > ) -> Self {
186
- match ( self , other. into ( ) ) {
187
- ( UsageKind :: Mixed , _) | ( _, UsageKind :: Mixed ) => UsageKind :: Mixed ,
188
- ( UsageKind :: Single ( lhs) , UsageKind :: Single ( rhs) ) => {
189
- if lhs == rhs {
190
- UsageKind :: Single ( lhs)
191
- } else {
192
- UsageKind :: Mixed
193
- }
194
- }
190
+
191
+ fn add_usages ( & mut self , usages : Usages ) {
192
+ let Usages { inductive, unknown, coinductive, forced_ambiguity } = usages;
193
+ self . inductive += inductive;
194
+ self . unknown += unknown;
195
+ self . coinductive += coinductive;
196
+ self . forced_ambiguity += forced_ambiguity;
197
+ }
198
+
199
+ fn compressed ( self ) -> Usages {
200
+ Usages {
201
+ inductive : if self . inductive == 0 { 0 } else { 1 } ,
202
+ unknown : if self . unknown == 0 { 0 } else { 1 } ,
203
+ coinductive : if self . coinductive == 0 { 0 } else { 1 } ,
204
+ forced_ambiguity : if self . forced_ambiguity == 0 { 0 } else { 1 } ,
195
205
}
196
206
}
197
207
}
@@ -234,7 +244,7 @@ impl AvailableDepth {
234
244
#[ derive( Clone , Copy , Debug ) ]
235
245
struct CycleHead {
236
246
paths_to_head : PathsToNested ,
237
- usage_kind : UsageKind ,
247
+ usages : Usages ,
238
248
}
239
249
240
250
/// All cycle heads a given goal depends on, ordered by their stack depth.
@@ -272,16 +282,16 @@ impl CycleHeads {
272
282
& mut self ,
273
283
head_index : StackDepth ,
274
284
path_from_entry : impl Into < PathsToNested > + Copy ,
275
- usage_kind : UsageKind ,
285
+ usages : Usages ,
276
286
) {
277
287
match self . heads . entry ( head_index) {
278
288
btree_map:: Entry :: Vacant ( entry) => {
279
- entry. insert ( CycleHead { paths_to_head : path_from_entry. into ( ) , usage_kind } ) ;
289
+ entry. insert ( CycleHead { paths_to_head : path_from_entry. into ( ) , usages } ) ;
280
290
}
281
291
btree_map:: Entry :: Occupied ( entry) => {
282
292
let head = entry. into_mut ( ) ;
283
293
head. paths_to_head |= path_from_entry. into ( ) ;
284
- head. usage_kind = head . usage_kind . merge ( usage_kind ) ;
294
+ head. usages . add_usages ( usages ) ;
285
295
}
286
296
}
287
297
}
@@ -550,13 +560,10 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
550
560
Ordering :: Less => parent. heads . insert (
551
561
head_index,
552
562
head. paths_to_head . extend_with ( step_kind_from_parent) ,
553
- head. usage_kind ,
563
+ head. usages . compressed ( ) ,
554
564
) ,
555
565
Ordering :: Equal => {
556
- let usage_kind = parent
557
- . has_been_used
558
- . map_or ( head. usage_kind , |prev| prev. merge ( head. usage_kind ) ) ;
559
- parent. has_been_used = Some ( usage_kind) ;
566
+ parent. usages . get_or_insert_default ( ) . add_usages ( head. usages . compressed ( ) ) ;
560
567
}
561
568
Ordering :: Greater => unreachable ! ( ) ,
562
569
}
@@ -681,7 +688,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
681
688
required_depth : 0 ,
682
689
heads : Default :: default ( ) ,
683
690
encountered_overflow : false ,
684
- has_been_used : None ,
691
+ usages : None ,
685
692
nested_goals : Default :: default ( ) ,
686
693
} ) ;
687
694
@@ -849,7 +856,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
849
856
// the heads of `e` to make sure that rebasing `e` again also considers
850
857
// them.
851
858
let eph = ep. extend_with_paths ( ph) ;
852
- heads. insert ( head_index, eph, head. usage_kind ) ;
859
+ heads. insert ( head_index, eph, head. usages . compressed ( ) ) ;
853
860
}
854
861
855
862
let Some ( head) = heads. opt_highest_cycle_head ( ) else {
@@ -1054,10 +1061,9 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1054
1061
// in case we're in the first fixpoint iteration for this goal.
1055
1062
let path_kind = Self :: cycle_path_kind ( & self . stack , step_kind_from_parent, head_index) ;
1056
1063
debug ! ( ?path_kind, "encountered cycle with depth {head_index:?}" ) ;
1057
- let head = CycleHead {
1058
- paths_to_head : step_kind_from_parent. into ( ) ,
1059
- usage_kind : UsageKind :: Single ( path_kind) ,
1060
- } ;
1064
+ let mut usages = Usages :: default ( ) ;
1065
+ usages. add_usage ( path_kind) ;
1066
+ let head = CycleHead { paths_to_head : step_kind_from_parent. into ( ) , usages } ;
1061
1067
Self :: update_parent_goal (
1062
1068
& mut self . stack ,
1063
1069
step_kind_from_parent,
@@ -1081,15 +1087,28 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1081
1087
& mut self ,
1082
1088
cx : X ,
1083
1089
stack_entry : & StackEntry < X > ,
1084
- usage_kind : UsageKind ,
1090
+ usages : Usages ,
1085
1091
result : X :: Result ,
1086
1092
) -> bool {
1087
- if let Some ( prev) = stack_entry. provisional_result {
1088
- prev == result
1089
- } else if let UsageKind :: Single ( kind) = usage_kind {
1090
- D :: is_initial_provisional_result ( cx, kind, stack_entry. input , result)
1091
- } else {
1092
- false
1093
+ let provisional_result = stack_entry. provisional_result ;
1094
+ let check = |kind| D :: is_initial_provisional_result ( cx, kind, stack_entry. input , result) ;
1095
+ match usages {
1096
+ Usages { inductive : 0 , unknown : 0 , coinductive : 0 , forced_ambiguity : 0 } => true ,
1097
+ // FIXME: use `feature(if_let_guard)` once it is stable.
1098
+ _ if provisional_result. is_some ( ) => provisional_result. unwrap ( ) == result,
1099
+ Usages { inductive : _, unknown : 0 , coinductive : 0 , forced_ambiguity : 0 } => {
1100
+ check ( PathKind :: Inductive )
1101
+ }
1102
+ Usages { inductive : 0 , unknown : _, coinductive : 0 , forced_ambiguity : 0 } => {
1103
+ check ( PathKind :: Unknown )
1104
+ }
1105
+ Usages { inductive : 0 , unknown : 0 , coinductive : _, forced_ambiguity : 0 } => {
1106
+ check ( PathKind :: Coinductive )
1107
+ }
1108
+ Usages { inductive : 0 , unknown : 0 , coinductive : 0 , forced_ambiguity : _ } => {
1109
+ check ( PathKind :: ForcedAmbiguity )
1110
+ }
1111
+ _ => false ,
1093
1112
}
1094
1113
}
1095
1114
@@ -1119,7 +1138,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1119
1138
// If the current goal is not the root of a cycle, we are done.
1120
1139
//
1121
1140
// There are no provisional cache entries which depend on this goal.
1122
- let Some ( usage_kind ) = stack_entry. has_been_used else {
1141
+ let Some ( usages ) = stack_entry. usages else {
1123
1142
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1124
1143
} ;
1125
1144
@@ -1134,7 +1153,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1134
1153
// is equal to the provisional result of the previous iteration, or because
1135
1154
// this was only the root of either coinductive or inductive cycles, and the
1136
1155
// final result is equal to the initial response for that case.
1137
- if self . reached_fixpoint ( cx, & stack_entry, usage_kind , result) {
1156
+ if self . reached_fixpoint ( cx, & stack_entry, usages , result) {
1138
1157
self . rebase_provisional_cache_entries ( & stack_entry, |_, result| result) ;
1139
1158
return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
1140
1159
}
@@ -1191,7 +1210,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
1191
1210
// similar to the previous iterations when reevaluating, it's better
1192
1211
// for caching if the reevaluation also starts out with `false`.
1193
1212
encountered_overflow : false ,
1194
- has_been_used : None ,
1213
+ usages : None ,
1195
1214
} ) ;
1196
1215
}
1197
1216
}
0 commit comments