@@ -3,9 +3,11 @@ use rustc_middle::traits::solve::inspect::{self, CacheHit, CandidateKind};
3
3
use rustc_middle:: traits:: solve:: {
4
4
CanonicalInput , Certainty , Goal , IsNormalizesToHack , QueryInput , QueryResult ,
5
5
} ;
6
- use rustc_middle:: ty;
6
+ use rustc_middle:: ty:: { self , TyCtxt } ;
7
+ use rustc_session:: config:: DumpSolverProofTree ;
7
8
8
- pub mod dump;
9
+ use super :: eval_ctxt:: UseGlobalCache ;
10
+ use super :: GenerateProofTree ;
9
11
10
12
#[ derive( Eq , PartialEq , Debug , Hash , HashStable ) ]
11
13
pub struct WipGoalEvaluation < ' tcx > {
@@ -144,29 +146,89 @@ impl<'tcx> From<WipGoalCandidate<'tcx>> for DebugSolver<'tcx> {
144
146
}
145
147
146
148
pub struct ProofTreeBuilder < ' tcx > {
147
- state : Option < Box < DebugSolver < ' tcx > > > ,
149
+ state : Option < Box < BuilderData < ' tcx > > > ,
150
+ }
151
+
152
+ struct BuilderData < ' tcx > {
153
+ tree : DebugSolver < ' tcx > ,
154
+ use_global_cache : UseGlobalCache ,
148
155
}
149
156
150
157
impl < ' tcx > ProofTreeBuilder < ' tcx > {
151
- fn new ( state : impl Into < DebugSolver < ' tcx > > ) -> ProofTreeBuilder < ' tcx > {
152
- ProofTreeBuilder { state : Some ( Box :: new ( state. into ( ) ) ) }
158
+ fn new (
159
+ state : impl Into < DebugSolver < ' tcx > > ,
160
+ use_global_cache : UseGlobalCache ,
161
+ ) -> ProofTreeBuilder < ' tcx > {
162
+ ProofTreeBuilder {
163
+ state : Some ( Box :: new ( BuilderData { tree : state. into ( ) , use_global_cache } ) ) ,
164
+ }
165
+ }
166
+
167
+ fn nested ( & self , state : impl Into < DebugSolver < ' tcx > > ) -> Self {
168
+ match & self . state {
169
+ Some ( prev_state) => Self {
170
+ state : Some ( Box :: new ( BuilderData {
171
+ tree : state. into ( ) ,
172
+ use_global_cache : prev_state. use_global_cache ,
173
+ } ) ) ,
174
+ } ,
175
+ None => Self { state : None } ,
176
+ }
153
177
}
154
178
155
179
fn as_mut ( & mut self ) -> Option < & mut DebugSolver < ' tcx > > {
156
- self . state . as_mut ( ) . map ( |boxed| & mut * * boxed)
180
+ self . state . as_mut ( ) . map ( |boxed| & mut boxed. tree )
157
181
}
158
182
159
183
pub fn finalize ( self ) -> Option < inspect:: GoalEvaluation < ' tcx > > {
160
- match * ( self . state ?) {
184
+ match self . state ?. tree {
161
185
DebugSolver :: GoalEvaluation ( wip_goal_evaluation) => {
162
186
Some ( wip_goal_evaluation. finalize ( ) )
163
187
}
164
188
root => unreachable ! ( "unexpected proof tree builder root node: {:?}" , root) ,
165
189
}
166
190
}
167
191
168
- pub fn new_root ( ) -> ProofTreeBuilder < ' tcx > {
169
- ProofTreeBuilder :: new ( DebugSolver :: Root )
192
+ pub fn use_global_cache ( & self ) -> bool {
193
+ self . state
194
+ . as_ref ( )
195
+ . map ( |state| matches ! ( state. use_global_cache, UseGlobalCache :: Yes ) )
196
+ . unwrap_or ( true )
197
+ }
198
+
199
+ pub fn new_maybe_root (
200
+ tcx : TyCtxt < ' tcx > ,
201
+ generate_proof_tree : GenerateProofTree ,
202
+ ) -> ProofTreeBuilder < ' tcx > {
203
+ let generate_proof_tree = match (
204
+ tcx. sess . opts . unstable_opts . dump_solver_proof_tree ,
205
+ tcx. sess . opts . unstable_opts . dump_solver_proof_tree_use_cache ,
206
+ generate_proof_tree,
207
+ ) {
208
+ ( _, Some ( use_cache) , GenerateProofTree :: Yes ( _) ) => {
209
+ GenerateProofTree :: Yes ( UseGlobalCache :: from_bool ( use_cache) )
210
+ }
211
+
212
+ ( DumpSolverProofTree :: Always , use_cache, GenerateProofTree :: No ) => {
213
+ let use_cache = use_cache. unwrap_or ( true ) ;
214
+ GenerateProofTree :: Yes ( UseGlobalCache :: from_bool ( use_cache) )
215
+ }
216
+
217
+ ( _, None , GenerateProofTree :: Yes ( _) ) => generate_proof_tree,
218
+ ( DumpSolverProofTree :: Never , _, _) => generate_proof_tree,
219
+ ( DumpSolverProofTree :: OnError , _, _) => generate_proof_tree,
220
+ } ;
221
+
222
+ match generate_proof_tree {
223
+ GenerateProofTree :: No => ProofTreeBuilder :: new_noop ( ) ,
224
+ GenerateProofTree :: Yes ( global_cache_disabled) => {
225
+ ProofTreeBuilder :: new_root ( global_cache_disabled)
226
+ }
227
+ }
228
+ }
229
+
230
+ pub fn new_root ( use_global_cache : UseGlobalCache ) -> ProofTreeBuilder < ' tcx > {
231
+ ProofTreeBuilder :: new ( DebugSolver :: Root , use_global_cache)
170
232
}
171
233
172
234
pub fn new_noop ( ) -> ProofTreeBuilder < ' tcx > {
@@ -186,7 +248,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
186
248
return ProofTreeBuilder { state : None } ;
187
249
}
188
250
189
- ProofTreeBuilder :: new ( WipGoalEvaluation {
251
+ self . nested ( WipGoalEvaluation {
190
252
uncanonicalized_goal : goal,
191
253
canonicalized_goal : None ,
192
254
evaluation_steps : vec ! [ ] ,
@@ -232,7 +294,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
232
294
}
233
295
pub fn goal_evaluation ( & mut self , goal_evaluation : ProofTreeBuilder < ' tcx > ) {
234
296
if let Some ( this) = self . as_mut ( ) {
235
- match ( this, * goal_evaluation. state . unwrap ( ) ) {
297
+ match ( this, goal_evaluation. state . unwrap ( ) . tree ) {
236
298
(
237
299
DebugSolver :: AddedGoalsEvaluation ( WipAddedGoalsEvaluation {
238
300
evaluations, ..
@@ -253,7 +315,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
253
315
return ProofTreeBuilder { state : None } ;
254
316
}
255
317
256
- ProofTreeBuilder :: new ( WipGoalEvaluationStep {
318
+ self . nested ( WipGoalEvaluationStep {
257
319
instantiated_goal,
258
320
nested_goal_evaluations : vec ! [ ] ,
259
321
candidates : vec ! [ ] ,
@@ -262,7 +324,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
262
324
}
263
325
pub fn goal_evaluation_step ( & mut self , goal_eval_step : ProofTreeBuilder < ' tcx > ) {
264
326
if let Some ( this) = self . as_mut ( ) {
265
- match ( this, * goal_eval_step. state . unwrap ( ) ) {
327
+ match ( this, goal_eval_step. state . unwrap ( ) . tree ) {
266
328
( DebugSolver :: GoalEvaluation ( goal_eval) , DebugSolver :: GoalEvaluationStep ( step) ) => {
267
329
goal_eval. evaluation_steps . push ( step) ;
268
330
}
@@ -276,7 +338,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
276
338
return ProofTreeBuilder { state : None } ;
277
339
}
278
340
279
- ProofTreeBuilder :: new ( WipGoalCandidate {
341
+ self . nested ( WipGoalCandidate {
280
342
nested_goal_evaluations : vec ! [ ] ,
281
343
candidates : vec ! [ ] ,
282
344
kind : None ,
@@ -296,7 +358,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
296
358
297
359
pub fn goal_candidate ( & mut self , candidate : ProofTreeBuilder < ' tcx > ) {
298
360
if let Some ( this) = self . as_mut ( ) {
299
- match ( this, * candidate. state . unwrap ( ) ) {
361
+ match ( this, candidate. state . unwrap ( ) . tree ) {
300
362
(
301
363
DebugSolver :: GoalCandidate ( WipGoalCandidate { candidates, .. } )
302
364
| DebugSolver :: GoalEvaluationStep ( WipGoalEvaluationStep { candidates, .. } ) ,
@@ -312,7 +374,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
312
374
return ProofTreeBuilder { state : None } ;
313
375
}
314
376
315
- ProofTreeBuilder :: new ( WipAddedGoalsEvaluation { evaluations : vec ! [ ] , result : None } )
377
+ self . nested ( WipAddedGoalsEvaluation { evaluations : vec ! [ ] , result : None } )
316
378
}
317
379
318
380
pub fn evaluate_added_goals_loop_start ( & mut self ) {
@@ -339,7 +401,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
339
401
340
402
pub fn added_goals_evaluation ( & mut self , goals_evaluation : ProofTreeBuilder < ' tcx > ) {
341
403
if let Some ( this) = self . as_mut ( ) {
342
- match ( this, * goals_evaluation. state . unwrap ( ) ) {
404
+ match ( this, goals_evaluation. state . unwrap ( ) . tree ) {
343
405
(
344
406
DebugSolver :: GoalEvaluationStep ( WipGoalEvaluationStep {
345
407
nested_goal_evaluations,
0 commit comments