@@ -34,7 +34,7 @@ use super::{search_graph::SearchGraph, Goal};
34
34
use super :: { GoalSource , SolverMode } ;
35
35
pub use select:: InferCtxtSelectExt ;
36
36
37
- mod canonical;
37
+ pub ( super ) mod canonical;
38
38
mod probe;
39
39
mod select;
40
40
@@ -84,7 +84,7 @@ pub struct EvalCtxt<'a, 'tcx> {
84
84
85
85
pub ( super ) search_graph : & ' a mut SearchGraph < ' tcx > ,
86
86
87
- pub ( super ) nested_goals : NestedGoals < ' tcx > ,
87
+ nested_goals : NestedGoals < ' tcx > ,
88
88
89
89
// Has this `EvalCtxt` errored out with `NoSolution` in `try_evaluate_added_goals`?
90
90
//
@@ -161,7 +161,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
161
161
/// Creates a root evaluation context and search graph. This should only be
162
162
/// used from outside of any evaluation, and other methods should be preferred
163
163
/// over using this manually (such as [`InferCtxtEvalExt::evaluate_root_goal`]).
164
- fn enter_root < R > (
164
+ pub ( super ) fn enter_root < R > (
165
165
infcx : & InferCtxt < ' tcx > ,
166
166
generate_proof_tree : GenerateProofTree ,
167
167
f : impl FnOnce ( & mut EvalCtxt < ' _ , ' tcx > ) -> R ,
@@ -242,7 +242,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
242
242
search_graph,
243
243
nested_goals : NestedGoals :: new ( ) ,
244
244
tainted : Ok ( ( ) ) ,
245
- inspect : canonical_goal_evaluation. new_goal_evaluation_step ( input) ,
245
+ inspect : canonical_goal_evaluation. new_goal_evaluation_step ( var_values , input) ,
246
246
} ;
247
247
248
248
for & ( key, ty) in & input. predefined_opaques_in_body . opaque_types {
@@ -255,7 +255,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
255
255
}
256
256
257
257
let result = f ( & mut ecx, input. goal ) ;
258
-
258
+ ecx . inspect . probe_final_state ( ecx . infcx , ecx . max_input_universe ) ;
259
259
canonical_goal_evaluation. goal_evaluation_step ( ecx. inspect ) ;
260
260
261
261
// When creating a query response we clone the opaque type constraints
@@ -338,7 +338,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
338
338
/// storage.
339
339
// FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
340
340
// be necessary once we implement the new coinduction approach.
341
- fn evaluate_goal_raw (
341
+ pub ( super ) fn evaluate_goal_raw (
342
342
& mut self ,
343
343
goal_evaluation_kind : GoalEvaluationKind ,
344
344
_source : GoalSource ,
@@ -458,13 +458,23 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
458
458
}
459
459
}
460
460
461
+ #[ instrument( level = "debug" , skip( self ) ) ]
462
+ pub ( super ) fn add_normalizes_to_goal ( & mut self , goal : Goal < ' tcx , ty:: NormalizesTo < ' tcx > > ) {
463
+ self . inspect . add_normalizes_to_goal ( self . infcx , self . max_input_universe , goal) ;
464
+ self . nested_goals . normalizes_to_goals . push ( goal) ;
465
+ }
466
+
467
+ #[ instrument( level = "debug" , skip( self ) ) ]
468
+ pub ( super ) fn add_goal ( & mut self , source : GoalSource , goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ) {
469
+ self . inspect . add_goal ( self . infcx , self . max_input_universe , source, goal) ;
470
+ self . nested_goals . goals . push ( ( source, goal) ) ;
471
+ }
472
+
461
473
// Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
462
474
// the certainty of all the goals.
463
475
#[ instrument( level = "debug" , skip( self ) ) ]
464
476
pub ( super ) fn try_evaluate_added_goals ( & mut self ) -> Result < Certainty , NoSolution > {
465
- let inspect = self . inspect . new_evaluate_added_goals ( ) ;
466
- let inspect = core:: mem:: replace ( & mut self . inspect , inspect) ;
467
-
477
+ self . inspect . start_evaluate_added_goals ( ) ;
468
478
let mut response = Ok ( Certainty :: overflow ( false ) ) ;
469
479
for _ in 0 ..FIXPOINT_STEP_LIMIT {
470
480
// FIXME: This match is a bit ugly, it might be nice to change the inspect
@@ -482,15 +492,12 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
482
492
}
483
493
}
484
494
485
- self . inspect . eval_added_goals_result ( response) ;
495
+ self . inspect . evaluate_added_goals_result ( response) ;
486
496
487
497
if response. is_err ( ) {
488
498
self . tainted = Err ( NoSolution ) ;
489
499
}
490
500
491
- let goal_evaluations = std:: mem:: replace ( & mut self . inspect , inspect) ;
492
- self . inspect . added_goals_evaluation ( goal_evaluations) ;
493
-
494
501
response
495
502
}
496
503
@@ -499,10 +506,9 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
499
506
/// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
500
507
fn evaluate_added_goals_step ( & mut self ) -> Result < Option < Certainty > , NoSolution > {
501
508
let tcx = self . tcx ( ) ;
509
+ self . inspect . start_evaluate_added_goals_step ( ) ;
502
510
let mut goals = core:: mem:: take ( & mut self . nested_goals ) ;
503
511
504
- self . inspect . evaluate_added_goals_loop_start ( ) ;
505
-
506
512
// If this loop did not result in any progress, what's our final certainty.
507
513
let mut unchanged_certainty = Some ( Certainty :: Yes ) ;
508
514
for goal in goals. normalizes_to_goals {
@@ -586,17 +592,23 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
586
592
self . infcx . tcx
587
593
}
588
594
589
- pub ( super ) fn next_ty_infer ( & self ) -> Ty < ' tcx > {
590
- self . infcx . next_ty_var ( TypeVariableOrigin { param_def_id : None , span : DUMMY_SP } )
595
+ pub ( super ) fn next_ty_infer ( & mut self ) -> Ty < ' tcx > {
596
+ let ty = self . infcx . next_ty_var ( TypeVariableOrigin { param_def_id : None , span : DUMMY_SP } ) ;
597
+ self . inspect . add_var_value ( ty) ;
598
+ ty
591
599
}
592
600
593
- pub ( super ) fn next_const_infer ( & self , ty : Ty < ' tcx > ) -> ty:: Const < ' tcx > {
594
- self . infcx . next_const_var ( ty, ConstVariableOrigin { param_def_id : None , span : DUMMY_SP } )
601
+ pub ( super ) fn next_const_infer ( & mut self , ty : Ty < ' tcx > ) -> ty:: Const < ' tcx > {
602
+ let ct = self
603
+ . infcx
604
+ . next_const_var ( ty, ConstVariableOrigin { param_def_id : None , span : DUMMY_SP } ) ;
605
+ self . inspect . add_var_value ( ct) ;
606
+ ct
595
607
}
596
608
597
609
/// Returns a ty infer or a const infer depending on whether `kind` is a `Ty` or `Const`.
598
610
/// If `kind` is an integer inference variable this will still return a ty infer var.
599
- pub ( super ) fn next_term_infer_of_kind ( & self , kind : ty:: Term < ' tcx > ) -> ty:: Term < ' tcx > {
611
+ pub ( super ) fn next_term_infer_of_kind ( & mut self , kind : ty:: Term < ' tcx > ) -> ty:: Term < ' tcx > {
600
612
match kind. unpack ( ) {
601
613
ty:: TermKind :: Ty ( _) => self . next_ty_infer ( ) . into ( ) ,
602
614
ty:: TermKind :: Const ( ct) => self . next_const_infer ( ct. ty ( ) ) . into ( ) ,
0 commit comments