@@ -15,119 +15,71 @@ pub enum DebugSolver<'tcx> {
1515 GoalCandidate ( GoalCandidate < ' tcx > ) ,
1616}
1717
18- pub trait InspectSolve < ' tcx > {
19- fn into_debug_solver ( self : Box < Self > ) -> Option < Box < DebugSolver < ' tcx > > > ;
18+ pub struct ProofTreeBuilder < ' tcx > ( Option < Box < DebugSolver < ' tcx > > > ) ;
2019
21- fn new_goal_evaluation (
22- & mut self ,
23- goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
24- ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > ;
25- fn canonicalized_goal ( & mut self , canonical_goal : CanonicalInput < ' tcx > ) ;
26- fn cache_hit ( & mut self , cache_hit : CacheHit ) ;
27- fn goal_evaluation ( & mut self , goal_evaluation : Box < dyn InspectSolve < ' tcx > + ' tcx > ) ;
28-
29- fn new_goal_evaluation_step (
30- & mut self ,
31- instantiated_goal : QueryInput < ' tcx , ty:: Predicate < ' tcx > > ,
32- ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > ;
33- fn goal_evaluation_step ( & mut self , goal_eval_step : Box < dyn InspectSolve < ' tcx > + ' tcx > ) ;
34-
35- fn new_goal_candidate ( & mut self ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > ;
36- fn candidate_name ( & mut self , f : & mut dyn FnMut ( ) -> String ) ;
37- fn goal_candidate ( & mut self , candidate : Box < dyn InspectSolve < ' tcx > + ' tcx > ) ;
38-
39- fn new_evaluate_added_goals ( & mut self ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > ;
40- fn evaluate_added_goals_loop_start ( & mut self ) ;
41- fn eval_added_goals_result ( & mut self , result : Result < Certainty , NoSolution > ) ;
42- fn added_goals_evaluation ( & mut self , goals_evaluation : Box < dyn InspectSolve < ' tcx > + ' tcx > ) ;
43-
44- fn query_result ( & mut self , result : QueryResult < ' tcx > ) ;
45- }
46-
47- /// No-op `InspectSolve` impl to use for normal trait solving when we do not want
48- /// to take a performance hit from recording information about how things are being
49- /// proven.
50- impl < ' tcx > InspectSolve < ' tcx > for ( ) {
51- fn into_debug_solver ( self : Box < Self > ) -> Option < Box < DebugSolver < ' tcx > > > {
52- None
53- }
54-
55- fn new_goal_evaluation (
56- & mut self ,
57- _goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
58- ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
59- Box :: new ( ( ) )
60- }
61- fn canonicalized_goal ( & mut self , _canonical_goal : CanonicalInput < ' tcx > ) { }
62- fn cache_hit ( & mut self , _cache_hit : CacheHit ) { }
63- fn goal_evaluation ( & mut self , _goal_evaluation : Box < dyn InspectSolve < ' tcx > + ' tcx > ) { }
64-
65- fn new_goal_evaluation_step (
66- & mut self ,
67- _instantiated_goal : QueryInput < ' tcx , ty:: Predicate < ' tcx > > ,
68- ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
69- Box :: new ( ( ) )
20+ impl < ' tcx > ProofTreeBuilder < ' tcx > {
21+ pub fn into_proof_tree ( self ) -> Option < DebugSolver < ' tcx > > {
22+ self . 0 . map ( |tree| * tree)
7023 }
71- fn goal_evaluation_step ( & mut self , _goal_eval_step : Box < dyn InspectSolve < ' tcx > + ' tcx > ) { }
7224
73- fn new_goal_candidate ( & mut self ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
74- Box :: new ( ( ) )
25+ pub fn new_root ( ) -> ProofTreeBuilder < ' tcx > {
26+ Self ( Some ( Box :: new ( DebugSolver :: Root ) ) )
7527 }
76- fn candidate_name ( & mut self , _f : & mut dyn FnMut ( ) -> String ) { }
77- fn goal_candidate ( & mut self , _candidate : Box < dyn InspectSolve < ' tcx > + ' tcx > ) { }
7828
79- fn new_evaluate_added_goals ( & mut self ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
80- Box :: new ( ( ) )
81- }
82- fn evaluate_added_goals_loop_start ( & mut self ) { }
83- fn eval_added_goals_result ( & mut self , _result : Result < Certainty , NoSolution > ) { }
84- fn added_goals_evaluation ( & mut self , _goals_evaluation : Box < dyn InspectSolve < ' tcx > + ' tcx > ) { }
85-
86- fn query_result ( & mut self , _result : QueryResult < ' tcx > ) { }
87- }
88-
89- impl < ' tcx > DebugSolver < ' tcx > {
90- pub fn new ( ) -> Self {
91- Self :: Root
92- }
93- }
94- impl < ' tcx > InspectSolve < ' tcx > for DebugSolver < ' tcx > {
95- fn into_debug_solver ( self : Box < Self > ) -> Option < Box < DebugSolver < ' tcx > > > {
96- Some ( self )
29+ pub fn new_noop ( ) -> ProofTreeBuilder < ' tcx > {
30+ Self ( None )
9731 }
9832
99- fn new_goal_evaluation (
33+ pub fn new_goal_evaluation (
10034 & mut self ,
10135 goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
102- ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
103- Box :: new ( DebugSolver :: GoalEvaluation ( GoalEvaluation {
36+ ) -> ProofTreeBuilder < ' tcx > {
37+ if self . 0 . is_none ( ) {
38+ return ProofTreeBuilder ( None ) ;
39+ }
40+
41+ Self ( Some ( Box :: new ( DebugSolver :: GoalEvaluation ( GoalEvaluation {
10442 uncanonicalized_goal : goal,
10543 canonicalized_goal : None ,
10644 evaluation_steps : vec ! [ ] ,
10745 cache_hit : None ,
10846 result : None ,
109- } ) )
47+ } ) ) ) )
11048 }
111- fn canonicalized_goal ( & mut self , canonical_goal : CanonicalInput < ' tcx > ) {
112- match self {
49+ pub fn canonicalized_goal ( & mut self , canonical_goal : CanonicalInput < ' tcx > ) {
50+ let this = match self . 0 . as_mut ( ) {
51+ None => return ,
52+ Some ( this) => & mut * * this,
53+ } ;
54+
55+ match this {
11356 DebugSolver :: GoalEvaluation ( goal_evaluation) => {
11457 assert ! ( goal_evaluation. canonicalized_goal. is_none( ) ) ;
11558 goal_evaluation. canonicalized_goal = Some ( canonical_goal)
11659 }
11760 _ => unreachable ! ( ) ,
11861 }
11962 }
120- fn cache_hit ( & mut self , cache_hit : CacheHit ) {
121- match self {
63+ pub fn cache_hit ( & mut self , cache_hit : CacheHit ) {
64+ let this = match self . 0 . as_mut ( ) {
65+ None => return ,
66+ Some ( this) => & mut * * this,
67+ } ;
68+
69+ match this {
12270 DebugSolver :: GoalEvaluation ( goal_evaluation) => {
12371 goal_evaluation. cache_hit = Some ( cache_hit)
12472 }
12573 _ => unreachable ! ( ) ,
12674 } ;
12775 }
128- fn goal_evaluation ( & mut self , goal_evaluation : Box < dyn InspectSolve < ' tcx > + ' tcx > ) {
129- let goal_evaluation = goal_evaluation. into_debug_solver ( ) . unwrap ( ) ;
130- match ( self , * goal_evaluation) {
76+ pub fn goal_evaluation ( & mut self , goal_evaluation : ProofTreeBuilder < ' tcx > ) {
77+ let this = match self . 0 . as_mut ( ) {
78+ None => return ,
79+ Some ( this) => & mut * * this,
80+ } ;
81+
82+ match ( this, * goal_evaluation. 0 . unwrap ( ) ) {
13183 (
13284 DebugSolver :: AddedGoalsEvaluation ( AddedGoalsEvaluation { evaluations, .. } ) ,
13385 DebugSolver :: GoalEvaluation ( goal_evaluation) ,
@@ -137,49 +89,61 @@ impl<'tcx> InspectSolve<'tcx> for DebugSolver<'tcx> {
13789 }
13890 }
13991
140- fn new_goal_evaluation_step (
92+ pub fn new_goal_evaluation_step (
14193 & mut self ,
14294 instantiated_goal : QueryInput < ' tcx , ty:: Predicate < ' tcx > > ,
143- ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
144- Box :: new ( DebugSolver :: GoalEvaluationStep ( GoalEvaluationStep {
95+ ) -> ProofTreeBuilder < ' tcx > {
96+ Self ( Some ( Box :: new ( DebugSolver :: GoalEvaluationStep ( GoalEvaluationStep {
14597 instantiated_goal,
14698 nested_goal_evaluations : vec ! [ ] ,
14799 candidates : vec ! [ ] ,
148100 result : None ,
149- } ) )
101+ } ) ) ) )
150102 }
151- fn goal_evaluation_step ( & mut self , goal_eval_step : Box < dyn InspectSolve < ' tcx > + ' tcx > ) {
152- let goal_eval_step = goal_eval_step. into_debug_solver ( ) . unwrap ( ) ;
153- match ( self , * goal_eval_step) {
103+ pub fn goal_evaluation_step ( & mut self , goal_eval_step : ProofTreeBuilder < ' tcx > ) {
104+ let this = match self . 0 . as_mut ( ) {
105+ None => return ,
106+ Some ( this) => & mut * * this,
107+ } ;
108+
109+ match ( this, * goal_eval_step. 0 . unwrap ( ) ) {
154110 ( DebugSolver :: GoalEvaluation ( goal_eval) , DebugSolver :: GoalEvaluationStep ( step) ) => {
155111 goal_eval. evaluation_steps . push ( step) ;
156112 }
157113 _ => unreachable ! ( ) ,
158114 }
159115 }
160116
161- fn new_goal_candidate ( & mut self ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
162- Box :: new ( DebugSolver :: GoalCandidate ( GoalCandidate {
117+ pub fn new_goal_candidate ( & mut self ) -> ProofTreeBuilder < ' tcx > {
118+ Self ( Some ( Box :: new ( DebugSolver :: GoalCandidate ( GoalCandidate {
163119 nested_goal_evaluations : vec ! [ ] ,
164120 candidates : vec ! [ ] ,
165121 name : None ,
166122 result : None ,
167- } ) )
123+ } ) ) ) )
168124 }
169- fn candidate_name ( & mut self , f : & mut dyn FnMut ( ) -> String ) {
170- let name = f ( ) ;
125+ pub fn candidate_name ( & mut self , f : & mut dyn FnMut ( ) -> String ) {
126+ let this = match self . 0 . as_mut ( ) {
127+ None => return ,
128+ Some ( this) => & mut * * this,
129+ } ;
171130
172- match self {
131+ match this {
173132 DebugSolver :: GoalCandidate ( goal_candidate) => {
133+ let name = f ( ) ;
174134 assert ! ( goal_candidate. name. is_none( ) ) ;
175135 goal_candidate. name = Some ( name) ;
176136 }
177137 _ => unreachable ! ( ) ,
178138 }
179139 }
180- fn goal_candidate ( & mut self , candidate : Box < dyn InspectSolve < ' tcx > + ' tcx > ) {
181- let candidate = candidate. into_debug_solver ( ) . unwrap ( ) ;
182- match ( self , * candidate) {
140+ pub fn goal_candidate ( & mut self , candidate : ProofTreeBuilder < ' tcx > ) {
141+ let this = match self . 0 . as_mut ( ) {
142+ None => return ,
143+ Some ( this) => & mut * * this,
144+ } ;
145+
146+ match ( this, * candidate. 0 . unwrap ( ) ) {
183147 (
184148 DebugSolver :: GoalCandidate ( GoalCandidate { candidates, .. } )
185149 | DebugSolver :: GoalEvaluationStep ( GoalEvaluationStep { candidates, .. } ) ,
@@ -189,32 +153,46 @@ impl<'tcx> InspectSolve<'tcx> for DebugSolver<'tcx> {
189153 }
190154 }
191155
192- fn new_evaluate_added_goals ( & mut self ) -> Box < dyn InspectSolve < ' tcx > + ' tcx > {
193- Box :: new ( DebugSolver :: AddedGoalsEvaluation ( AddedGoalsEvaluation {
156+ pub fn new_evaluate_added_goals ( & mut self ) -> ProofTreeBuilder < ' tcx > {
157+ Self ( Some ( Box :: new ( DebugSolver :: AddedGoalsEvaluation ( AddedGoalsEvaluation {
194158 evaluations : vec ! [ ] ,
195159 result : None ,
196- } ) )
160+ } ) ) ) )
197161 }
198- fn evaluate_added_goals_loop_start ( & mut self ) {
199- match self {
162+ pub fn evaluate_added_goals_loop_start ( & mut self ) {
163+ let this = match self . 0 . as_mut ( ) {
164+ None => return ,
165+ Some ( this) => & mut * * this,
166+ } ;
167+
168+ match this {
200169 DebugSolver :: AddedGoalsEvaluation ( this) => {
201170 this. evaluations . push ( vec ! [ ] ) ;
202171 }
203172 _ => unreachable ! ( ) ,
204173 }
205174 }
206- fn eval_added_goals_result ( & mut self , result : Result < Certainty , NoSolution > ) {
207- match self {
175+ pub fn eval_added_goals_result ( & mut self , result : Result < Certainty , NoSolution > ) {
176+ let this = match self . 0 . as_mut ( ) {
177+ None => return ,
178+ Some ( this) => & mut * * this,
179+ } ;
180+
181+ match this {
208182 DebugSolver :: AddedGoalsEvaluation ( this) => {
209183 assert ! ( this. result. is_none( ) ) ;
210184 this. result = Some ( result) ;
211185 }
212186 _ => unreachable ! ( ) ,
213187 }
214188 }
215- fn added_goals_evaluation ( & mut self , goals_evaluation : Box < dyn InspectSolve < ' tcx > + ' tcx > ) {
216- let goals_evaluation = goals_evaluation. into_debug_solver ( ) . unwrap ( ) ;
217- match ( self , * goals_evaluation) {
189+ pub fn added_goals_evaluation ( & mut self , goals_evaluation : ProofTreeBuilder < ' tcx > ) {
190+ let this = match self . 0 . as_mut ( ) {
191+ None => return ,
192+ Some ( this) => & mut * * this,
193+ } ;
194+
195+ match ( this, * goals_evaluation. 0 . unwrap ( ) ) {
218196 (
219197 DebugSolver :: GoalEvaluationStep ( GoalEvaluationStep {
220198 nested_goal_evaluations, ..
@@ -226,8 +204,13 @@ impl<'tcx> InspectSolve<'tcx> for DebugSolver<'tcx> {
226204 }
227205 }
228206
229- fn query_result ( & mut self , result : QueryResult < ' tcx > ) {
230- match self {
207+ pub fn query_result ( & mut self , result : QueryResult < ' tcx > ) {
208+ let this = match self . 0 . as_mut ( ) {
209+ None => return ,
210+ Some ( this) => & mut * * this,
211+ } ;
212+
213+ match this {
231214 DebugSolver :: GoalEvaluation ( goal_evaluation) => {
232215 assert ! ( goal_evaluation. result. is_none( ) ) ;
233216 goal_evaluation. result = Some ( result) ;
0 commit comments