@@ -170,28 +170,38 @@ impl PathKind {
170170/// This is used to avoid rerunning a cycle if there's
171171/// just a single usage kind and the final result matches
172172/// 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 ,
177179}
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+ }
181189 }
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 } ,
195205 }
196206 }
197207}
@@ -234,7 +244,7 @@ impl AvailableDepth {
234244#[ derive( Clone , Copy , Debug ) ]
235245struct CycleHead {
236246 paths_to_head : PathsToNested ,
237- usage_kind : UsageKind ,
247+ usages : Usages ,
238248}
239249
240250/// All cycle heads a given goal depends on, ordered by their stack depth.
@@ -272,16 +282,16 @@ impl CycleHeads {
272282 & mut self ,
273283 head_index : StackDepth ,
274284 path_from_entry : impl Into < PathsToNested > + Copy ,
275- usage_kind : UsageKind ,
285+ usages : Usages ,
276286 ) {
277287 match self . heads . entry ( head_index) {
278288 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 } ) ;
280290 }
281291 btree_map:: Entry :: Occupied ( entry) => {
282292 let head = entry. into_mut ( ) ;
283293 head. paths_to_head |= path_from_entry. into ( ) ;
284- head. usage_kind = head . usage_kind . merge ( usage_kind ) ;
294+ head. usages . add_usages ( usages ) ;
285295 }
286296 }
287297 }
@@ -550,13 +560,10 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
550560 Ordering :: Less => parent. heads . insert (
551561 head_index,
552562 head. paths_to_head . extend_with ( step_kind_from_parent) ,
553- head. usage_kind ,
563+ head. usages . compressed ( ) ,
554564 ) ,
555565 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 ( ) ) ;
560567 }
561568 Ordering :: Greater => unreachable ! ( ) ,
562569 }
@@ -681,7 +688,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
681688 required_depth : 0 ,
682689 heads : Default :: default ( ) ,
683690 encountered_overflow : false ,
684- has_been_used : None ,
691+ usages : None ,
685692 nested_goals : Default :: default ( ) ,
686693 } ) ;
687694
@@ -849,7 +856,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
849856 // the heads of `e` to make sure that rebasing `e` again also considers
850857 // them.
851858 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 ( ) ) ;
853860 }
854861
855862 let Some ( head) = heads. opt_highest_cycle_head ( ) else {
@@ -1054,10 +1061,9 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
10541061 // in case we're in the first fixpoint iteration for this goal.
10551062 let path_kind = Self :: cycle_path_kind ( & self . stack , step_kind_from_parent, head_index) ;
10561063 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 } ;
10611067 Self :: update_parent_goal (
10621068 & mut self . stack ,
10631069 step_kind_from_parent,
@@ -1081,15 +1087,28 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
10811087 & mut self ,
10821088 cx : X ,
10831089 stack_entry : & StackEntry < X > ,
1084- usage_kind : UsageKind ,
1090+ usages : Usages ,
10851091 result : X :: Result ,
10861092 ) -> 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 ,
10931112 }
10941113 }
10951114
@@ -1119,7 +1138,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
11191138 // If the current goal is not the root of a cycle, we are done.
11201139 //
11211140 // 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 {
11231142 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
11241143 } ;
11251144
@@ -1134,7 +1153,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
11341153 // is equal to the provisional result of the previous iteration, or because
11351154 // this was only the root of either coinductive or inductive cycles, and the
11361155 // 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) {
11381157 self . rebase_provisional_cache_entries ( & stack_entry, |_, result| result) ;
11391158 return EvaluationResult :: finalize ( stack_entry, encountered_overflow, result) ;
11401159 }
@@ -1191,7 +1210,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
11911210 // similar to the previous iterations when reevaluating, it's better
11921211 // for caching if the reevaluation also starts out with `false`.
11931212 encountered_overflow : false ,
1194- has_been_used : None ,
1213+ usages : None ,
11951214 } ) ;
11961215 }
11971216 }
0 commit comments