@@ -18,8 +18,8 @@ use crate::solve::inspect::{self, ProofTreeBuilder};
1818use crate :: solve:: search_graph:: SearchGraph ;
1919use crate :: solve:: {
2020 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 ,
2323} ;
2424
2525pub ( super ) mod canonical;
@@ -126,11 +126,31 @@ pub enum GenerateProofTree {
126126}
127127
128128pub 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.
129133 fn evaluate_root_goal (
130134 & self ,
131135 goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
132136 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 ;
134154
135155 // FIXME: This is only exposed because we need to use it in `analyse.rs`
136156 // which is not yet uplifted. Once that's done, we should remove this.
@@ -139,7 +159,7 @@ pub trait SolverDelegateEvalExt: SolverDelegate {
139159 goal : Goal < Self :: Interner , <Self :: Interner as Interner >:: Predicate > ,
140160 generate_proof_tree : GenerateProofTree ,
141161 ) -> (
142- Result < ( NestedNormalizationGoals < Self :: Interner > , bool , Certainty ) , NoSolution > ,
162+ Result < ( NestedNormalizationGoals < Self :: Interner > , HasChanged , Certainty ) , NoSolution > ,
143163 Option < inspect:: GoalEvaluation < Self :: Interner > > ,
144164 ) ;
145165}
@@ -149,31 +169,41 @@ where
149169 D : SolverDelegate < Interner = I > ,
150170 I : Interner ,
151171{
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.
156172 #[ instrument( level = "debug" , skip( self ) ) ]
157173 fn evaluate_root_goal (
158174 & self ,
159175 goal : Goal < I , I :: Predicate > ,
160176 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| {
163179 ecx. evaluate_goal ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
164180 } )
165181 }
166182
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+
167197 #[ instrument( level = "debug" , skip( self ) ) ]
168198 fn evaluate_root_goal_raw (
169199 & self ,
170200 goal : Goal < I , I :: Predicate > ,
171201 generate_proof_tree : GenerateProofTree ,
172202 ) -> (
173- Result < ( NestedNormalizationGoals < I > , bool , Certainty ) , NoSolution > ,
203+ Result < ( NestedNormalizationGoals < I > , HasChanged , Certainty ) , NoSolution > ,
174204 Option < inspect:: GoalEvaluation < I > > ,
175205 ) {
176- EvalCtxt :: enter_root ( self , generate_proof_tree, |ecx| {
206+ EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , generate_proof_tree, |ecx| {
177207 ecx. evaluate_goal_raw ( GoalEvaluationKind :: Root , GoalSource :: Misc , goal)
178208 } )
179209 }
@@ -197,10 +227,11 @@ where
197227 /// over using this manually (such as [`SolverDelegateEvalExt::evaluate_root_goal`]).
198228 pub ( super ) fn enter_root < R > (
199229 delegate : & D ,
230+ root_depth : usize ,
200231 generate_proof_tree : GenerateProofTree ,
201232 f : impl FnOnce ( & mut EvalCtxt < ' _ , D > ) -> R ,
202233 ) -> ( 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 ) ;
204235
205236 let mut ecx = EvalCtxt {
206237 delegate,
@@ -339,7 +370,7 @@ where
339370 goal_evaluation_kind : GoalEvaluationKind ,
340371 source : GoalSource ,
341372 goal : Goal < I , I :: Predicate > ,
342- ) -> Result < ( bool , Certainty ) , NoSolution > {
373+ ) -> Result < ( HasChanged , Certainty ) , NoSolution > {
343374 let ( normalization_nested_goals, has_changed, certainty) =
344375 self . evaluate_goal_raw ( goal_evaluation_kind, source, goal) ?;
345376 assert ! ( normalization_nested_goals. is_empty( ) ) ;
@@ -360,7 +391,7 @@ where
360391 goal_evaluation_kind : GoalEvaluationKind ,
361392 _source : GoalSource ,
362393 goal : Goal < I , I :: Predicate > ,
363- ) -> Result < ( NestedNormalizationGoals < I > , bool , Certainty ) , NoSolution > {
394+ ) -> Result < ( NestedNormalizationGoals < I > , HasChanged , Certainty ) , NoSolution > {
364395 let ( orig_values, canonical_goal) = self . canonicalize_goal ( goal) ;
365396 let mut goal_evaluation =
366397 self . inspect . new_goal_evaluation ( goal, & orig_values, goal_evaluation_kind) ;
@@ -378,8 +409,13 @@ where
378409 Ok ( response) => response,
379410 } ;
380411
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+ } ;
383419
384420 let ( normalization_nested_goals, certainty) =
385421 self . instantiate_and_apply_query_response ( goal. param_env , orig_values, response) ;
@@ -552,7 +588,7 @@ where
552588 for ( source, goal) in goals. goals {
553589 let ( has_changed, certainty) =
554590 self . evaluate_goal ( GoalEvaluationKind :: Nested , source, goal) ?;
555- if has_changed {
591+ if has_changed == HasChanged :: Yes {
556592 unchanged_certainty = None ;
557593 }
558594
0 commit comments