@@ -15,119 +15,71 @@ pub enum DebugSolver<'tcx> {
15
15
GoalCandidate ( GoalCandidate < ' tcx > ) ,
16
16
}
17
17
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 > > > ) ;
20
19
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)
70
23
}
71
- fn goal_evaluation_step ( & mut self , _goal_eval_step : Box < dyn InspectSolve < ' tcx > + ' tcx > ) { }
72
24
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 ) ) )
75
27
}
76
- fn candidate_name ( & mut self , _f : & mut dyn FnMut ( ) -> String ) { }
77
- fn goal_candidate ( & mut self , _candidate : Box < dyn InspectSolve < ' tcx > + ' tcx > ) { }
78
28
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 )
97
31
}
98
32
99
- fn new_goal_evaluation (
33
+ pub fn new_goal_evaluation (
100
34
& mut self ,
101
35
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 {
104
42
uncanonicalized_goal : goal,
105
43
canonicalized_goal : None ,
106
44
evaluation_steps : vec ! [ ] ,
107
45
cache_hit : None ,
108
46
result : None ,
109
- } ) )
47
+ } ) ) ) )
110
48
}
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 {
113
56
DebugSolver :: GoalEvaluation ( goal_evaluation) => {
114
57
assert ! ( goal_evaluation. canonicalized_goal. is_none( ) ) ;
115
58
goal_evaluation. canonicalized_goal = Some ( canonical_goal)
116
59
}
117
60
_ => unreachable ! ( ) ,
118
61
}
119
62
}
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 {
122
70
DebugSolver :: GoalEvaluation ( goal_evaluation) => {
123
71
goal_evaluation. cache_hit = Some ( cache_hit)
124
72
}
125
73
_ => unreachable ! ( ) ,
126
74
} ;
127
75
}
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 ( ) ) {
131
83
(
132
84
DebugSolver :: AddedGoalsEvaluation ( AddedGoalsEvaluation { evaluations, .. } ) ,
133
85
DebugSolver :: GoalEvaluation ( goal_evaluation) ,
@@ -137,49 +89,61 @@ impl<'tcx> InspectSolve<'tcx> for DebugSolver<'tcx> {
137
89
}
138
90
}
139
91
140
- fn new_goal_evaluation_step (
92
+ pub fn new_goal_evaluation_step (
141
93
& mut self ,
142
94
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 {
145
97
instantiated_goal,
146
98
nested_goal_evaluations : vec ! [ ] ,
147
99
candidates : vec ! [ ] ,
148
100
result : None ,
149
- } ) )
101
+ } ) ) ) )
150
102
}
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 ( ) ) {
154
110
( DebugSolver :: GoalEvaluation ( goal_eval) , DebugSolver :: GoalEvaluationStep ( step) ) => {
155
111
goal_eval. evaluation_steps . push ( step) ;
156
112
}
157
113
_ => unreachable ! ( ) ,
158
114
}
159
115
}
160
116
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 {
163
119
nested_goal_evaluations : vec ! [ ] ,
164
120
candidates : vec ! [ ] ,
165
121
name : None ,
166
122
result : None ,
167
- } ) )
123
+ } ) ) ) )
168
124
}
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
+ } ;
171
130
172
- match self {
131
+ match this {
173
132
DebugSolver :: GoalCandidate ( goal_candidate) => {
133
+ let name = f ( ) ;
174
134
assert ! ( goal_candidate. name. is_none( ) ) ;
175
135
goal_candidate. name = Some ( name) ;
176
136
}
177
137
_ => unreachable ! ( ) ,
178
138
}
179
139
}
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 ( ) ) {
183
147
(
184
148
DebugSolver :: GoalCandidate ( GoalCandidate { candidates, .. } )
185
149
| DebugSolver :: GoalEvaluationStep ( GoalEvaluationStep { candidates, .. } ) ,
@@ -189,32 +153,46 @@ impl<'tcx> InspectSolve<'tcx> for DebugSolver<'tcx> {
189
153
}
190
154
}
191
155
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 {
194
158
evaluations : vec ! [ ] ,
195
159
result : None ,
196
- } ) )
160
+ } ) ) ) )
197
161
}
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 {
200
169
DebugSolver :: AddedGoalsEvaluation ( this) => {
201
170
this. evaluations . push ( vec ! [ ] ) ;
202
171
}
203
172
_ => unreachable ! ( ) ,
204
173
}
205
174
}
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 {
208
182
DebugSolver :: AddedGoalsEvaluation ( this) => {
209
183
assert ! ( this. result. is_none( ) ) ;
210
184
this. result = Some ( result) ;
211
185
}
212
186
_ => unreachable ! ( ) ,
213
187
}
214
188
}
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 ( ) ) {
218
196
(
219
197
DebugSolver :: GoalEvaluationStep ( GoalEvaluationStep {
220
198
nested_goal_evaluations, ..
@@ -226,8 +204,13 @@ impl<'tcx> InspectSolve<'tcx> for DebugSolver<'tcx> {
226
204
}
227
205
}
228
206
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 {
231
214
DebugSolver :: GoalEvaluation ( goal_evaluation) => {
232
215
assert ! ( goal_evaluation. result. is_none( ) ) ;
233
216
goal_evaluation. result = Some ( result) ;
0 commit comments