@@ -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