@@ -18,8 +18,8 @@ use crate::solve::inspect::{self, ProofTreeBuilder};
18
18
use crate :: solve:: search_graph:: SearchGraph ;
19
19
use crate :: solve:: {
20
20
CanonicalInput , CanonicalResponse , Certainty , FIXPOINT_STEP_LIMIT , Goal , GoalEvaluationKind ,
21
- GoalSource , NestedNormalizationGoals , NoSolution , PredefinedOpaquesData , QueryResult ,
22
- SolverMode ,
21
+ GoalSource , HasChanged , NestedNormalizationGoals , NoSolution , PredefinedOpaquesData ,
22
+ QueryResult , SolverMode ,
23
23
} ;
24
24
25
25
pub ( super ) mod canonical;
@@ -126,11 +126,31 @@ pub enum GenerateProofTree {
126
126
}
127
127
128
128
pub trait SolverDelegateEvalExt : SolverDelegate {
129
+ /// Evaluates a goal from **outside** of the trait solver.
130
+ ///
131
+ /// Using this while inside of the solver is wrong as it uses a new
132
+ /// search graph which would break cycle detection.
129
133
fn evaluate_root_goal (
130
134
& self ,
131
135
goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
132
136
generate_proof_tree : GenerateProofTree ,
133
- ) -> ( Result < ( bool , Certainty ) , NoSolution > , Option < inspect:: GoalEvaluation < Self :: Interner > > ) ;
137
+ ) -> (
138
+ Result < ( HasChanged , Certainty ) , NoSolution > ,
139
+ Option < inspect:: GoalEvaluation < Self :: Interner > > ,
140
+ ) ;
141
+
142
+ /// Check whether evaluating `goal` with a depth of `root_depth` may
143
+ /// succeed. This only returns `false` if the goal is guaranteed to
144
+ /// not hold. In case evaluation overflows and fails with ambiguity this
145
+ /// returns `true`.
146
+ ///
147
+ /// This is only intended to be used as a performance optimization
148
+ /// in coherence checking.
149
+ fn root_goal_may_hold_with_depth (
150
+ & self ,
151
+ root_depth : usize ,
152
+ goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
153
+ ) -> bool ;
134
154
135
155
// FIXME: This is only exposed because we need to use it in `analyse.rs`
136
156
// which is not yet uplifted. Once that's done, we should remove this.
@@ -139,7 +159,7 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
139
159
goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
140
160
generate_proof_tree : GenerateProofTree ,
141
161
) -> (
142
- Result < ( NestedNormalizationGoals < Self :: Interner > , bool , Certainty ) , NoSolution > ,
162
+ Result < ( NestedNormalizationGoals < Self :: Interner > , HasChanged , Certainty ) , NoSolution > ,
143
163
Option < inspect:: GoalEvaluation < Self :: Interner > > ,
144
164
) ;
145
165
}
@@ -149,31 +169,41 @@ where
149
169
D : SolverDelegate < Interner = I > ,
150
170
I : Interner ,
151
171
{
152
- /// Evaluates a goal from **outside** of the trait solver.
153
- ///
154
- /// Using this while inside of the solver is wrong as it uses a new
155
- /// search graph which would break cycle detection.
156
172
#[ instrument( level = "debug" , skip( self ) ) ]
157
173
fn evaluate_root_goal (
158
174
& self ,
159
175
goal : Goal < I , I :: Predicate > ,
160
176
generate_proof_tree : GenerateProofTree ,
161
- ) -> ( Result < ( bool , Certainty ) , NoSolution > , Option < inspect:: GoalEvaluation < I > > ) {
162
- EvalCtxt :: enter_root ( self , generate_proof_tree, |ecx| {
177
+ ) -> ( Result < ( HasChanged , Certainty ) , NoSolution > , Option < inspect:: GoalEvaluation < I > > ) {
178
+ EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , generate_proof_tree, |ecx| {
163
179
ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
164
180
} )
165
181
}
166
182
183
+ fn root_goal_may_hold_with_depth (
184
+ & self ,
185
+ root_depth : usize ,
186
+ goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
187
+ ) -> bool {
188
+ self . probe ( || {
189
+ EvalCtxt :: enter_root ( self , root_depth, GenerateProofTree :: No , |ecx| {
190
+ ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
191
+ } )
192
+ . 0
193
+ } )
194
+ . is_ok ( )
195
+ }
196
+
167
197
#[ instrument( level = "debug" , skip( self ) ) ]
168
198
fn evaluate_root_goal_raw (
169
199
& self ,
170
200
goal : Goal < I , I :: Predicate > ,
171
201
generate_proof_tree : GenerateProofTree ,
172
202
) -> (
173
- Result < ( NestedNormalizationGoals < I > , bool , Certainty ) , NoSolution > ,
203
+ Result < ( NestedNormalizationGoals < I > , HasChanged , Certainty ) , NoSolution > ,
174
204
Option < inspect:: GoalEvaluation < I > > ,
175
205
) {
176
- EvalCtxt :: enter_root ( self , generate_proof_tree, |ecx| {
206
+ EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , generate_proof_tree, |ecx| {
177
207
ecx. evaluate_goal_raw ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
178
208
} )
179
209
}
@@ -197,10 +227,11 @@ where
197
227
/// over using this manually (such as [`SolverDelegateEvalExt::evaluate_root_goal`]).
198
228
pub ( super ) fn enter_root < R > (
199
229
delegate : & D ,
230
+ root_depth : usize ,
200
231
generate_proof_tree : GenerateProofTree ,
201
232
f : impl FnOnce ( & mut EvalCtxt < ' _ , D > ) -> R ,
202
233
) -> ( R , Option < inspect:: GoalEvaluation < I > > ) {
203
- let mut search_graph = SearchGraph :: new ( delegate. solver_mode ( ) ) ;
234
+ let mut search_graph = SearchGraph :: new ( delegate. solver_mode ( ) , root_depth ) ;
204
235
205
236
let mut ecx = EvalCtxt {
206
237
delegate,
@@ -339,7 +370,7 @@ where
339
370
goal_evaluation_kind : GoalEvaluationKind ,
340
371
source : GoalSource ,
341
372
goal : Goal < I , I :: Predicate > ,
342
- ) -> Result < ( bool , Certainty ) , NoSolution > {
373
+ ) -> Result < ( HasChanged , Certainty ) , NoSolution > {
343
374
let ( normalization_nested_goals, has_changed, certainty) =
344
375
self . evaluate_goal_raw ( goal_evaluation_kind, source, goal) ?;
345
376
assert ! ( normalization_nested_goals. is_empty( ) ) ;
@@ -360,7 +391,7 @@ where
360
391
goal_evaluation_kind : GoalEvaluationKind ,
361
392
_source : GoalSource ,
362
393
goal : Goal < I , I :: Predicate > ,
363
- ) -> Result < ( NestedNormalizationGoals < I > , bool , Certainty ) , NoSolution > {
394
+ ) -> Result < ( NestedNormalizationGoals < I > , HasChanged , Certainty ) , NoSolution > {
364
395
let ( orig_values, canonical_goal) = self . canonicalize_goal ( goal) ;
365
396
let mut goal_evaluation =
366
397
self . inspect . new_goal_evaluation ( goal, & orig_values, goal_evaluation_kind) ;
@@ -378,8 +409,13 @@ where
378
409
Ok ( response) => response,
379
410
} ;
380
411
381
- let has_changed = !response. value . var_values . is_identity_modulo_regions ( )
382
- || !response. value . external_constraints . opaque_types . is_empty ( ) ;
412
+ let has_changed = if !response. value . var_values . is_identity_modulo_regions ( )
413
+ || !response. value . external_constraints . opaque_types . is_empty ( )
414
+ {
415
+ HasChanged :: Yes
416
+ } else {
417
+ HasChanged :: No
418
+ } ;
383
419
384
420
let ( normalization_nested_goals, certainty) =
385
421
self . instantiate_and_apply_query_response ( goal. param_env , orig_values, response) ;
@@ -552,7 +588,7 @@ where
552
588
for ( source, goal) in goals. goals {
553
589
let ( has_changed, certainty) =
554
590
self . evaluate_goal ( GoalEvaluationKind :: Nested , source, goal) ?;
555
- if has_changed {
591
+ if has_changed == HasChanged :: Yes {
556
592
unchanged_certainty = None ;
557
593
}
558
594
0 commit comments