@@ -21,7 +21,7 @@ use std::marker::PhantomData;
2121use derive_where:: derive_where;
2222#[ cfg( feature = "nightly" ) ]
2323use rustc_macros:: { Decodable_NoContext , Encodable_NoContext , HashStable_NoContext } ;
24- use tracing:: debug;
24+ use tracing:: { debug, instrument } ;
2525
2626use crate :: data_structures:: HashMap ;
2727
@@ -56,7 +56,7 @@ pub trait Cx: Copy {
5656 fn evaluation_is_concurrent ( & self ) -> bool ;
5757}
5858
59- pub trait Delegate {
59+ pub trait Delegate : Sized {
6060 type Cx : Cx ;
6161 /// Whether to use the provisional cache. Set to `false` by a fuzzer when
6262 /// validating the search graph.
@@ -94,8 +94,8 @@ pub trait Delegate {
9494 ) -> bool ;
9595 fn on_stack_overflow (
9696 cx : Self :: Cx ,
97- inspect : & mut Self :: ProofTreeBuilder ,
9897 input : <Self :: Cx as Cx >:: Input ,
98+ inspect : & mut Self :: ProofTreeBuilder ,
9999 ) -> <Self :: Cx as Cx >:: Result ;
100100 fn on_fixpoint_overflow (
101101 cx : Self :: Cx ,
@@ -108,6 +108,13 @@ pub trait Delegate {
108108 for_input : <Self :: Cx as Cx >:: Input ,
109109 from_result : <Self :: Cx as Cx >:: Result ,
110110 ) -> <Self :: Cx as Cx >:: Result ;
111+
112+ fn compute_goal (
113+ search_graph : & mut SearchGraph < Self > ,
114+ cx : Self :: Cx ,
115+ input : <Self :: Cx as Cx >:: Input ,
116+ inspect : & mut Self :: ProofTreeBuilder ,
117+ ) -> <Self :: Cx as Cx >:: Result ;
111118}
112119
113120/// In the initial iteration of a cycle, we do not yet have a provisional
@@ -589,15 +596,15 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
589596
590597 /// Probably the most involved method of the whole solver.
591598 ///
592- /// Given some goal which is proven via the `prove_goal` closure, this
593- /// handles caching, overflow, and coinductive cycles.
594- pub fn with_new_goal (
599+ /// While goals get computed via `D::compute_goal, this function handles
600+ /// caching, overflow, and cycles.
601+ #[ instrument( level = "debug" , skip( self , cx, inspect) ) ]
602+ pub fn evaluate_goal (
595603 & mut self ,
596604 cx : X ,
597605 input : X :: Input ,
598606 step_kind_from_parent : PathKind ,
599607 inspect : & mut D :: ProofTreeBuilder ,
600- evaluate_goal : impl Fn ( & mut Self , X , X :: Input , & mut D :: ProofTreeBuilder ) -> X :: Result + Copy ,
601608 ) -> X :: Result {
602609 let Some ( available_depth) =
603610 AvailableDepth :: allowed_depth_for_nested :: < D > ( self . root_depth , & self . stack )
@@ -666,7 +673,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
666673 // must not be added to the global cache. Notably, this is the case for
667674 // trait solver cycles participants.
668675 let ( evaluation_result, dep_node) =
669- cx. with_cached_task ( || self . evaluate_goal_in_task ( cx, input, inspect, evaluate_goal ) ) ;
676+ cx. with_cached_task ( || self . evaluate_goal_in_task ( cx, input, inspect) ) ;
670677
671678 // We've finished computing the goal and have popped it from the stack,
672679 // lazily update its parent goal.
@@ -736,7 +743,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
736743 }
737744
738745 debug ! ( "encountered stack overflow" ) ;
739- D :: on_stack_overflow ( cx, inspect , input )
746+ D :: on_stack_overflow ( cx, input , inspect )
740747 }
741748
742749 /// When reevaluating a goal with a changed provisional result, all provisional cache entry
@@ -1064,7 +1071,6 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
10641071 cx : X ,
10651072 input : X :: Input ,
10661073 inspect : & mut D :: ProofTreeBuilder ,
1067- evaluate_goal : impl Fn ( & mut Self , X , X :: Input , & mut D :: ProofTreeBuilder ) -> X :: Result + Copy ,
10681074 ) -> EvaluationResult < X > {
10691075 // We reset `encountered_overflow` each time we rerun this goal
10701076 // but need to make sure we currently propagate it to the global
@@ -1073,7 +1079,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
10731079 let mut encountered_overflow = false ;
10741080 let mut i = 0 ;
10751081 loop {
1076- let result = evaluate_goal ( self , cx, input, inspect) ;
1082+ let result = D :: compute_goal ( self , cx, input, inspect) ;
10771083 let stack_entry = self . stack . pop ( ) ;
10781084 encountered_overflow |= stack_entry. encountered_overflow ;
10791085 debug_assert_eq ! ( stack_entry. input, input) ;
0 commit comments