@@ -21,7 +21,7 @@ use std::marker::PhantomData;
21
21
use derive_where:: derive_where;
22
22
#[ cfg( feature = "nightly" ) ]
23
23
use rustc_macros:: { Decodable_NoContext , Encodable_NoContext , HashStable_NoContext } ;
24
- use tracing:: debug;
24
+ use tracing:: { debug, instrument } ;
25
25
26
26
use crate :: data_structures:: HashMap ;
27
27
@@ -56,7 +56,7 @@ pub trait Cx: Copy {
56
56
fn evaluation_is_concurrent ( & self ) -> bool ;
57
57
}
58
58
59
- pub trait Delegate {
59
+ pub trait Delegate : Sized {
60
60
type Cx : Cx ;
61
61
/// Whether to use the provisional cache. Set to `false` by a fuzzer when
62
62
/// validating the search graph.
@@ -94,8 +94,8 @@ pub trait Delegate {
94
94
) -> bool ;
95
95
fn on_stack_overflow (
96
96
cx : Self :: Cx ,
97
- inspect : & mut Self :: ProofTreeBuilder ,
98
97
input : <Self :: Cx as Cx >:: Input ,
98
+ inspect : & mut Self :: ProofTreeBuilder ,
99
99
) -> <Self :: Cx as Cx >:: Result ;
100
100
fn on_fixpoint_overflow (
101
101
cx : Self :: Cx ,
@@ -108,6 +108,13 @@ pub trait Delegate {
108
108
for_input : <Self :: Cx as Cx >:: Input ,
109
109
from_result : <Self :: Cx as Cx >:: Result ,
110
110
) -> <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 ;
111
118
}
112
119
113
120
/// 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> {
589
596
590
597
/// Probably the most involved method of the whole solver.
591
598
///
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) , ret) ]
602
+ pub fn evaluate_goal (
595
603
& mut self ,
596
604
cx : X ,
597
605
input : X :: Input ,
598
606
step_kind_from_parent : PathKind ,
599
607
inspect : & mut D :: ProofTreeBuilder ,
600
- evaluate_goal : impl Fn ( & mut Self , X , X :: Input , & mut D :: ProofTreeBuilder ) -> X :: Result + Copy ,
601
608
) -> X :: Result {
602
609
let Some ( available_depth) =
603
610
AvailableDepth :: allowed_depth_for_nested :: < D > ( self . root_depth , & self . stack )
@@ -666,7 +673,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
666
673
// must not be added to the global cache. Notably, this is the case for
667
674
// trait solver cycles participants.
668
675
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) ) ;
670
677
671
678
// We've finished computing the goal and have popped it from the stack,
672
679
// lazily update its parent goal.
@@ -736,7 +743,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
736
743
}
737
744
738
745
debug ! ( "encountered stack overflow" ) ;
739
- D :: on_stack_overflow ( cx, inspect , input )
746
+ D :: on_stack_overflow ( cx, input , inspect )
740
747
}
741
748
742
749
/// 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> {
1064
1071
cx : X ,
1065
1072
input : X :: Input ,
1066
1073
inspect : & mut D :: ProofTreeBuilder ,
1067
- evaluate_goal : impl Fn ( & mut Self , X , X :: Input , & mut D :: ProofTreeBuilder ) -> X :: Result + Copy ,
1068
1074
) -> EvaluationResult < X > {
1069
1075
// We reset `encountered_overflow` each time we rerun this goal
1070
1076
// 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> {
1073
1079
let mut encountered_overflow = false ;
1074
1080
let mut i = 0 ;
1075
1081
loop {
1076
- let result = evaluate_goal ( self , cx, input, inspect) ;
1082
+ let result = D :: compute_goal ( self , cx, input, inspect) ;
1077
1083
let stack_entry = self . stack . pop ( ) ;
1078
1084
encountered_overflow |= stack_entry. encountered_overflow ;
1079
1085
debug_assert_eq ! ( stack_entry. input, input) ;
0 commit comments