@@ -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                // 
@@ -977,22 +1011,33 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
9771011                        let  eph = ep. extend_with_paths ( ph) ; 
9781012                        heads. insert ( head_index,  eph,  head. usages ) ; 
9791013                    } 
980-                 } 
9811014
982-                 let  Some ( head_index)  = heads. opt_highest_cycle_head_index ( )  else  { 
983-                     return  false ; 
984-                 } ; 
1015+                     // The provisional cache entry does depend on the provisional result 
1016+                     // of the popped cycle head. We need to mutate the result of our 
1017+                     // provisional cache entry in case we did not reach a fixpoint. 
1018+                     * result = match  rebase_reason { 
1019+                         RebaseReason :: NoCycleUsages  => return  false , 
1020+                         RebaseReason :: Ambiguity  => D :: propagate_ambiguity ( cx,  input,  * result) , 
1021+                         RebaseReason :: Overflow  => D :: on_fixpoint_overflow ( cx,  input) , 
1022+                         RebaseReason :: ReachedFixpoint ( None )  => * result, 
1023+                         RebaseReason :: ReachedFixpoint ( Some ( path_kind) )  => { 
1024+                             if  popped_head. usages . is_single ( path_kind)  { 
1025+                                 * result
1026+                             }  else  { 
1027+                                 return  false ; 
1028+                             } 
1029+                         } 
1030+                     } ; 
1031+                 } 
9851032
9861033                // We now care about the path from the next highest cycle head to the 
9871034                // provisional cache entry. 
9881035                * path_from_head = path_from_head. extend ( Self :: cycle_path_kind ( 
9891036                    & self . stack , 
9901037                    stack_entry. step_kind_from_parent , 
991-                     head_index , 
1038+                     new_highest_head_index , 
9921039                ) ) ; 
993-                 // Mutate the result of the provisional cache entry in case we did 
994-                 // not reach a fixpoint. 
995-                 * result = mutate_result ( input,  * result) ; 
1040+ 
9961041                true 
9971042            } ) ; 
9981043            !entries. is_empty ( ) 
@@ -1209,33 +1254,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12091254    /// Whether we've reached a fixpoint when evaluating a cycle head. 
12101255     fn  reached_fixpoint ( 
12111256        & mut  self , 
1212-         cx :  X , 
12131257        stack_entry :  & StackEntry < X > , 
12141258        usages :  HeadUsages , 
12151259        result :  X :: Result , 
1216-     )  -> bool  { 
1260+     )  -> Result < Option < PathKind > ,   ( ) >  { 
12171261        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
1262+         if  let  Some ( provisional_result)  = provisional_result { 
1263+             if  provisional_result == result {  Ok ( None )  }  else  {  Err ( ( ) )  } 
1264+         }  else  if  let  Some ( path_kind)  = D :: is_initial_provisional_result ( result) 
1265+             . filter ( |& path_kind| usages. is_single ( path_kind) ) 
1266+         { 
1267+             Ok ( Some ( path_kind) ) 
12221268        }  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-             } 
1269+             Err ( ( ) ) 
12391270        } 
12401271    } 
12411272
@@ -1280,8 +1311,19 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12801311            // is equal to the provisional result of the previous iteration, or because 
12811312            // this was only the head of either coinductive or inductive cycles, and the 
12821313            // 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) ; 
1314+             if  let  Ok ( fixpoint)  = self . reached_fixpoint ( & stack_entry,  usages,  result)  { 
1315+                 self . rebase_provisional_cache_entries ( 
1316+                     cx, 
1317+                     & stack_entry, 
1318+                     RebaseReason :: ReachedFixpoint ( fixpoint) , 
1319+                 ) ; 
1320+                 return  EvaluationResult :: finalize ( stack_entry,  encountered_overflow,  result) ; 
1321+             }  else  if  usages. is_empty ( )  { 
1322+                 self . rebase_provisional_cache_entries ( 
1323+                     cx, 
1324+                     & stack_entry, 
1325+                     RebaseReason :: NoCycleUsages , 
1326+                 ) ; 
12851327                return  EvaluationResult :: finalize ( stack_entry,  encountered_overflow,  result) ; 
12861328            } 
12871329
@@ -1298,9 +1340,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
12981340            // we also taint all provisional cache entries which depend on the 
12991341            // current goal. 
13001342            if  D :: is_ambiguous_result ( result)  { 
1301-                 self . rebase_provisional_cache_entries ( & stack_entry,  |input,  _| { 
1302-                     D :: propagate_ambiguity ( cx,  input,  result) 
1303-                 } ) ; 
1343+                 self . rebase_provisional_cache_entries ( cx,  & stack_entry,  RebaseReason :: Ambiguity ) ; 
13041344                return  EvaluationResult :: finalize ( stack_entry,  encountered_overflow,  result) ; 
13051345            } ; 
13061346
@@ -1310,9 +1350,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
13101350            if  i >= D :: FIXPOINT_STEP_LIMIT  { 
13111351                debug ! ( "canonical cycle overflow" ) ; 
13121352                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-                 } ) ; 
1353+                 self . rebase_provisional_cache_entries ( cx,  & stack_entry,  RebaseReason :: Overflow ) ; 
13161354                return  EvaluationResult :: finalize ( stack_entry,  encountered_overflow,  result) ; 
13171355            } 
13181356
0 commit comments