1
+ use crate :: cache:: Cache ;
1
2
use crate :: search_graph:: DepthFirstNumber ;
2
3
use crate :: search_graph:: SearchGraph ;
3
4
use crate :: solve:: { SolveDatabase , SolveIteration } ;
4
5
use crate :: stack:: { Stack , StackDepth } ;
5
- use crate :: { cache:: Cache , PrioritizedSolution } ;
6
6
use crate :: { Minimums , UCanonicalGoal } ;
7
7
use chalk_ir:: { interner:: Interner , NoSolution } ;
8
8
use chalk_ir:: { Canonical , ConstrainedSubst , Goal , InEnvironment , UCanonical } ;
@@ -17,12 +17,12 @@ struct RecursiveContext<I: Interner> {
17
17
18
18
/// The "search graph" stores "in-progress results" that are still being
19
19
/// solved.
20
- search_graph : SearchGraph < UCanonicalGoal < I > , PrioritizedSolution < I > > ,
20
+ search_graph : SearchGraph < UCanonicalGoal < I > , Fallible < Solution < I > > > ,
21
21
22
22
/// The "cache" stores results for goals that we have completely solved.
23
23
/// Things are added to the cache when we have completely processed their
24
24
/// result.
25
- cache : Option < Cache < UCanonicalGoal < I > , PrioritizedSolution < I > > > ,
25
+ cache : Option < Cache < UCanonicalGoal < I > , Fallible < Solution < I > > > > ,
26
26
27
27
/// The maximum size for goals.
28
28
max_size : usize ,
@@ -46,7 +46,7 @@ impl<I: Interner> RecursiveSolver<I> {
46
46
pub fn new (
47
47
overflow_depth : usize ,
48
48
max_size : usize ,
49
- cache : Option < Cache < UCanonicalGoal < I > , PrioritizedSolution < I > > > ,
49
+ cache : Option < Cache < UCanonicalGoal < I > , Fallible < Solution < I > > > > ,
50
50
) -> Self {
51
51
Self {
52
52
ctx : Box :: new ( RecursiveContext :: new ( overflow_depth, max_size, cache) ) ,
@@ -84,7 +84,7 @@ impl<I: Interner> RecursiveContext<I> {
84
84
pub fn new (
85
85
overflow_depth : usize ,
86
86
max_size : usize ,
87
- cache : Option < Cache < UCanonicalGoal < I > , PrioritizedSolution < I > > > ,
87
+ cache : Option < Cache < UCanonicalGoal < I > , Fallible < Solution < I > > > > ,
88
88
) -> Self {
89
89
RecursiveContext {
90
90
stack : Stack :: new ( overflow_depth) ,
@@ -149,7 +149,7 @@ impl<'me, I: Interner> Solver<'me, I> {
149
149
// so this function will eventually be constant and the loop terminates.
150
150
loop {
151
151
let minimums = & mut Minimums :: new ( ) ;
152
- let current_answer = self . solve_iteration ( & canonical_goal, minimums) ;
152
+ let ( current_answer, current_prio ) = self . solve_iteration ( & canonical_goal, minimums) ;
153
153
154
154
debug ! (
155
155
"solve_new_subgoal: loop iteration result = {:?} with minimums {:?}" ,
@@ -160,22 +160,24 @@ impl<'me, I: Interner> Solver<'me, I> {
160
160
// None of our subgoals depended on us directly.
161
161
// We can return.
162
162
self . context . search_graph [ dfn] . solution = current_answer;
163
+ self . context . search_graph [ dfn] . solution_priority = current_prio;
163
164
return * minimums;
164
165
}
165
166
166
167
// Some of our subgoals depended on us. We need to re-run
167
168
// with the current answer.
168
- if self . context . search_graph [ dfn] . solution . solution == current_answer. solution {
169
+ if self . context . search_graph [ dfn] . solution == current_answer {
169
170
// Reached a fixed point.
170
171
return * minimums;
171
172
}
172
173
173
- let current_answer_is_ambig = match & current_answer. solution {
174
+ let current_answer_is_ambig = match & current_answer {
174
175
Ok ( s) => s. is_ambig ( ) ,
175
176
Err ( _) => false ,
176
177
} ;
177
178
178
179
self . context . search_graph [ dfn] . solution = current_answer;
180
+ self . context . search_graph [ dfn] . solution_priority = current_prio;
179
181
180
182
// Subtle: if our current answer is ambiguous, we can just stop, and
181
183
// in fact we *must* -- otherwise, we sometimes fail to reach a
@@ -204,7 +206,7 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
204
206
if let Some ( cache) = & self . context . cache {
205
207
if let Some ( value) = cache. get ( & goal) {
206
208
debug ! ( "solve_reduced_goal: cache hit, value={:?}" , value) ;
207
- return value. solution . clone ( ) ;
209
+ return value. clone ( ) ;
208
210
}
209
211
}
210
212
@@ -229,11 +231,12 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
229
231
230
232
// Return the solution from the table.
231
233
let previous_solution = self . context . search_graph [ dfn] . solution . clone ( ) ;
234
+ let previous_solution_priority = self . context . search_graph [ dfn] . solution_priority ;
232
235
info ! (
233
- "solve_goal: cycle detected, previous solution {:?}" ,
234
- previous_solution,
236
+ "solve_goal: cycle detected, previous solution {:?} with prio {:?} " ,
237
+ previous_solution, previous_solution_priority
235
238
) ;
236
- previous_solution. solution
239
+ previous_solution
237
240
} else {
238
241
// Otherwise, push the goal onto the stack and create a table.
239
242
// The initial result for this table depends on whether the goal is coinductive.
@@ -250,11 +253,10 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
250
253
} else {
251
254
Err ( NoSolution )
252
255
} ;
253
- let dfn = self . context . search_graph . insert (
254
- & goal,
255
- depth,
256
- PrioritizedSolution :: high ( initial_solution) ,
257
- ) ;
256
+ let dfn = self
257
+ . context
258
+ . search_graph
259
+ . insert ( & goal, depth, initial_solution) ;
258
260
let subgoal_minimums = self . solve_new_subgoal ( goal, depth, dfn) ;
259
261
self . context . search_graph [ dfn] . links = subgoal_minimums;
260
262
self . context . search_graph [ dfn] . stack_depth = None ;
@@ -263,6 +265,7 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
263
265
264
266
// Read final result from table.
265
267
let result = self . context . search_graph [ dfn] . solution . clone ( ) ;
268
+ let priority = self . context . search_graph [ dfn] . solution_priority ;
266
269
267
270
// If processing this subgoal did not involve anything
268
271
// outside of its subtree, then we can promote it to the
@@ -280,8 +283,8 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
280
283
}
281
284
}
282
285
283
- info ! ( "solve_goal: solution = {:#?} " , result) ;
284
- result. solution
286
+ info ! ( "solve_goal: solution = {:?} prio {:?} " , result, priority ) ;
287
+ result
285
288
}
286
289
}
287
290
0 commit comments