@@ -212,9 +212,7 @@ where
212
212
goal : Goal < I , I :: Predicate > ,
213
213
span : I :: Span ,
214
214
) -> ( Result < NestedNormalizationGoals < I > , NoSolution > , inspect:: GoalEvaluation < I > ) {
215
- EvalCtxt :: enter_root ( self , self . cx ( ) . recursion_limit ( ) , span, |ecx| {
216
- ecx. evaluate_goal_for_proof_tree ( goal)
217
- } )
215
+ evaluate_root_goal_for_proof_tree ( self , goal, span)
218
216
}
219
217
}
220
218
@@ -324,11 +322,10 @@ where
324
322
cx : I ,
325
323
search_graph : & ' a mut SearchGraph < D > ,
326
324
canonical_input : CanonicalInput < I > ,
327
- canonical_goal_evaluation : & mut inspect:: GoalEvaluationBuilder < D > ,
325
+ proof_tree_builder : & mut inspect:: ProofTreeBuilder < D > ,
328
326
f : impl FnOnce ( & mut EvalCtxt < ' _ , D > , Goal < I , I :: Predicate > ) -> R ,
329
327
) -> R {
330
328
let ( ref delegate, input, var_values) = D :: build_with_canonical ( cx, & canonical_input) ;
331
-
332
329
for & ( key, ty) in & input. predefined_opaques_in_body . opaque_types {
333
330
let prev = delegate. register_hidden_type_in_storage ( key, ty, I :: Span :: dummy ( ) ) ;
334
331
// It may be possible that two entries in the opaque type storage end up
@@ -359,12 +356,12 @@ where
359
356
nested_goals : Default :: default ( ) ,
360
357
origin_span : I :: Span :: dummy ( ) ,
361
358
tainted : Ok ( ( ) ) ,
362
- inspect : canonical_goal_evaluation . new_goal_evaluation_step ( var_values) ,
359
+ inspect : proof_tree_builder . new_evaluation_step ( var_values) ,
363
360
} ;
364
361
365
362
let result = f ( & mut ecx, input. goal ) ;
366
363
ecx. inspect . probe_final_state ( ecx. delegate , ecx. max_input_universe ) ;
367
- canonical_goal_evaluation . goal_evaluation_step ( ecx. inspect ) ;
364
+ proof_tree_builder . finish_evaluation_step ( ecx. inspect ) ;
368
365
369
366
// When creating a query response we clone the opaque type constraints
370
367
// instead of taking them. This would cause an ICE here, since we have
@@ -434,12 +431,13 @@ where
434
431
let opaque_types = self . delegate . clone_opaque_types_lookup_table ( ) ;
435
432
let ( goal, opaque_types) = eager_resolve_vars ( self . delegate , ( goal, opaque_types) ) ;
436
433
437
- let ( orig_values, canonical_goal) = self . canonicalize_goal ( goal, opaque_types) ;
434
+ let ( orig_values, canonical_goal) =
435
+ Self :: canonicalize_goal ( self . delegate , goal, opaque_types) ;
438
436
let canonical_result = self . search_graph . evaluate_goal (
439
437
self . cx ( ) ,
440
438
canonical_goal,
441
439
self . step_kind_for_source ( source) ,
442
- & mut inspect:: GoalEvaluationBuilder :: new_noop ( ) ,
440
+ & mut inspect:: ProofTreeBuilder :: new_noop ( ) ,
443
441
) ;
444
442
let response = match canonical_result {
445
443
Err ( e) => return Err ( e) ,
@@ -449,8 +447,13 @@ where
449
447
let has_changed =
450
448
if !has_only_region_constraints ( response) { HasChanged :: Yes } else { HasChanged :: No } ;
451
449
452
- let ( normalization_nested_goals, certainty) =
453
- self . instantiate_and_apply_query_response ( goal. param_env , & orig_values, response) ;
450
+ let ( normalization_nested_goals, certainty) = Self :: instantiate_and_apply_query_response (
451
+ self . delegate ,
452
+ goal. param_env ,
453
+ & orig_values,
454
+ response,
455
+ self . origin_span ,
456
+ ) ;
454
457
455
458
// FIXME: We previously had an assert here that checked that recomputing
456
459
// a goal after applying its constraints did not change its response.
@@ -514,35 +517,6 @@ where
514
517
) )
515
518
}
516
519
517
- /// Evaluate a goal to build a proof tree. This is a copy of [EvalCtxt::evaluate_goal_raw].
518
- pub ( super ) fn evaluate_goal_for_proof_tree (
519
- & mut self ,
520
- goal : Goal < I , I :: Predicate > ,
521
- ) -> ( Result < NestedNormalizationGoals < I > , NoSolution > , inspect:: GoalEvaluation < I > ) {
522
- let opaque_types = self . delegate . clone_opaque_types_lookup_table ( ) ;
523
- let ( goal, opaque_types) = eager_resolve_vars ( self . delegate , ( goal, opaque_types) ) ;
524
-
525
- let ( orig_values, canonical_goal) = self . canonicalize_goal ( goal, opaque_types) ;
526
- let mut goal_evaluation = inspect:: GoalEvaluationBuilder :: new ( goal, & orig_values) ;
527
- let canonical_result = self . search_graph . evaluate_goal (
528
- self . cx ( ) ,
529
- canonical_goal,
530
- self . step_kind_for_source ( GoalSource :: Misc ) ,
531
- & mut goal_evaluation,
532
- ) ;
533
- goal_evaluation. query_result ( canonical_result) ;
534
- let proof_tree = goal_evaluation. finalize ( ) ;
535
- let response = match canonical_result {
536
- Err ( e) => return ( Err ( e) , proof_tree) ,
537
- Ok ( response) => response,
538
- } ;
539
-
540
- let ( normalization_nested_goals, _certainty) =
541
- self . instantiate_and_apply_query_response ( goal. param_env , & orig_values, response) ;
542
-
543
- ( Ok ( normalization_nested_goals) , proof_tree)
544
- }
545
-
546
520
pub ( super ) fn compute_goal ( & mut self , goal : Goal < I , I :: Predicate > ) -> QueryResult < I > {
547
521
let Goal { param_env, predicate } = goal;
548
522
let kind = predicate. kind ( ) ;
@@ -1293,3 +1267,62 @@ where
1293
1267
if predicate. allow_normalization ( ) { predicate. super_fold_with ( self ) } else { predicate }
1294
1268
}
1295
1269
}
1270
+
1271
+ /// Do not call this directly, use the `tcx` query instead.
1272
+ pub fn evaluate_root_goal_for_proof_tree_raw_provider <
1273
+ D : SolverDelegate < Interner = I > ,
1274
+ I : Interner ,
1275
+ > (
1276
+ cx : I ,
1277
+ canonical_goal : CanonicalInput < I > ,
1278
+ ) -> ( QueryResult < I > , I :: ProbeRef ) {
1279
+ let mut inspect = inspect:: ProofTreeBuilder :: new ( ) ;
1280
+ let canonical_result = SearchGraph :: < D > :: evaluate_root_goal_for_proof_tree (
1281
+ cx,
1282
+ cx. recursion_limit ( ) ,
1283
+ canonical_goal,
1284
+ & mut inspect,
1285
+ ) ;
1286
+ let final_revision = inspect. unwrap ( ) ;
1287
+ ( canonical_result, cx. mk_probe_ref ( final_revision) )
1288
+ }
1289
+
1290
+ /// Evaluate a goal to build a proof tree.
1291
+ ///
1292
+ /// This is a copy of [EvalCtxt::evaluate_goal_raw] which avoids relying on the
1293
+ /// [EvalCtxt] and uses a separate cache.
1294
+ pub ( super ) fn evaluate_root_goal_for_proof_tree < D : SolverDelegate < Interner = I > , I : Interner > (
1295
+ delegate : & D ,
1296
+ goal : Goal < I , I :: Predicate > ,
1297
+ origin_span : I :: Span ,
1298
+ ) -> ( Result < NestedNormalizationGoals < I > , NoSolution > , inspect:: GoalEvaluation < I > ) {
1299
+ let opaque_types = delegate. clone_opaque_types_lookup_table ( ) ;
1300
+ let ( goal, opaque_types) = eager_resolve_vars ( delegate, ( goal, opaque_types) ) ;
1301
+
1302
+ let ( orig_values, canonical_goal) = EvalCtxt :: canonicalize_goal ( delegate, goal, opaque_types) ;
1303
+
1304
+ let ( canonical_result, final_revision) =
1305
+ delegate. cx ( ) . evaluate_root_goal_for_proof_tree_raw ( canonical_goal) ;
1306
+
1307
+ let proof_tree = inspect:: GoalEvaluation {
1308
+ uncanonicalized_goal : goal,
1309
+ orig_values,
1310
+ final_revision,
1311
+ result : canonical_result,
1312
+ } ;
1313
+
1314
+ let response = match canonical_result {
1315
+ Err ( e) => return ( Err ( e) , proof_tree) ,
1316
+ Ok ( response) => response,
1317
+ } ;
1318
+
1319
+ let ( normalization_nested_goals, _certainty) = EvalCtxt :: instantiate_and_apply_query_response (
1320
+ delegate,
1321
+ goal. param_env ,
1322
+ & proof_tree. orig_values ,
1323
+ response,
1324
+ origin_span,
1325
+ ) ;
1326
+
1327
+ ( Ok ( normalization_nested_goals) , proof_tree)
1328
+ }
0 commit comments