Skip to content

Commit cc7f184

Browse files
nikomatsakisnikomatsakis
committed
move solve_goal into recursive context
1 parent 18994ec commit cc7f184

File tree

1 file changed

+128
-117
lines changed

1 file changed

+128
-117
lines changed

‎chalk-recursive/src/recursive.rs

Lines changed: 128 additions & 117 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,98 @@ where
8080
}
8181
}
8282

83+
/// Attempt to solve a goal that has been fully broken down into leaf form
84+
/// and canonicalized. This is where the action really happens, and is the
85+
/// place where we would perform caching in rustc (and may eventually do in Chalk).
86+
#[instrument(
87+
level = "info",
88+
skip(
89+
self,
90+
minimums,
91+
initial_value,
92+
solve_iteration,
93+
reached_fixed_point,
94+
error_value
95+
)
96+
)]
97+
fn solve_goal(
98+
&mut self,
99+
goal: &K,
100+
minimums: &mut Minimums,
101+
initial_value: impl Fn(&K) -> (bool, V),
102+
solve_iteration: impl FnMut(&mut Self, &K, &mut Minimums) -> V,
103+
reached_fixed_point: impl Fn(&V, &V) -> bool,
104+
error_value: impl Fn() -> V,
105+
) -> V {
106+
// First check the cache.
107+
if let Some(cache) = &self.cache {
108+
if let Some(value) = cache.get(&goal) {
109+
debug!("solve_reduced_goal: cache hit, value={:?}", value);
110+
return value.clone();
111+
}
112+
}
113+
114+
// Next, check if the goal is in the search tree already.
115+
if let Some(dfn) = self.search_graph.lookup(&goal) {
116+
// Check if this table is still on the stack.
117+
if let Some(depth) = self.search_graph[dfn].stack_depth {
118+
self.stack[depth].flag_cycle();
119+
// Mixed cycles are not allowed. For more information about this
120+
// see the corresponding section in the coinduction chapter:
121+
// https://rust-lang.github.io/chalk/book/recursive/coinduction.html#mixed-co-inductive-and-inductive-cycles
122+
if self.stack.mixed_inductive_coinductive_cycle_from(depth) {
123+
return error_value();
124+
}
125+
}
126+
127+
minimums.update_from(self.search_graph[dfn].links);
128+
129+
// Return the solution from the table.
130+
let previous_solution = self.search_graph[dfn].solution.clone();
131+
info!(
132+
"solve_goal: cycle detected, previous solution {:?}",
133+
previous_solution,
134+
);
135+
previous_solution
136+
} else {
137+
// Otherwise, push the goal onto the stack and create a table.
138+
// The initial result for this table depends on whether the goal is coinductive.
139+
let (coinductive_goal, initial_solution) = initial_value(goal);
140+
let depth = self.stack.push(coinductive_goal);
141+
let dfn = self.search_graph.insert(&goal, depth, initial_solution);
142+
143+
let subgoal_minimums =
144+
self.solve_new_subgoal(&goal, depth, dfn, solve_iteration, reached_fixed_point);
145+
146+
self.search_graph[dfn].links = subgoal_minimums;
147+
self.search_graph[dfn].stack_depth = None;
148+
self.stack.pop(depth);
149+
minimums.update_from(subgoal_minimums);
150+
151+
// Read final result from table.
152+
let result = self.search_graph[dfn].solution.clone();
153+
154+
// If processing this subgoal did not involve anything
155+
// outside of its subtree, then we can promote it to the
156+
// cache now. This is a sort of hack to alleviate the
157+
// worst of the repeated work that we do during tabling.
158+
if subgoal_minimums.positive >= dfn {
159+
if let Some(cache) = &mut self.cache {
160+
self.search_graph.move_to_cache(dfn, cache);
161+
debug!("solve_reduced_goal: SCC head encountered, moving to cache");
162+
} else {
163+
debug!(
164+
"solve_reduced_goal: SCC head encountered, rolling back as caching disabled"
165+
);
166+
self.search_graph.rollback_to(dfn);
167+
}
168+
}
169+
170+
info!("solve_goal: solution = {:?}", result);
171+
result
172+
}
173+
}
174+
83175
#[instrument(level = "debug", skip(self, solve_iteration, reached_fixed_point))]
84176
fn solve_new_subgoal(
85177
&mut self,
@@ -159,122 +251,6 @@ impl<'me, I: Interner> Solver<'me, I> {
159251
let minimums = &mut Minimums::new();
160252
self.solve_goal(canonical_goal.clone(), minimums)
161253
}
162-
163-
/// Attempt to solve a goal that has been fully broken down into leaf form
164-
/// and canonicalized. This is where the action really happens, and is the
165-
/// place where we would perform caching in rustc (and may eventually do in Chalk).
166-
#[instrument(level = "info", skip(self, minimums))]
167-
fn solve_goal(
168-
&mut self,
169-
goal: UCanonicalGoal<I>,
170-
minimums: &mut Minimums,
171-
) -> Fallible<Solution<I>> {
172-
// First check the cache.
173-
if let Some(cache) = &self.context.cache {
174-
if let Some(value) = cache.get(&goal) {
175-
debug!("solve_reduced_goal: cache hit, value={:?}", value);
176-
return value.clone();
177-
}
178-
}
179-
180-
// Next, check if the goal is in the search tree already.
181-
if let Some(dfn) = self.context.search_graph.lookup(&goal) {
182-
// Check if this table is still on the stack.
183-
if let Some(depth) = self.context.search_graph[dfn].stack_depth {
184-
self.context.stack[depth].flag_cycle();
185-
// Mixed cycles are not allowed. For more information about this
186-
// see the corresponding section in the coinduction chapter:
187-
// https://rust-lang.github.io/chalk/book/recursive/coinduction.html#mixed-co-inductive-and-inductive-cycles
188-
if self
189-
.context
190-
.stack
191-
.mixed_inductive_coinductive_cycle_from(depth)
192-
{
193-
return Err(NoSolution);
194-
}
195-
}
196-
197-
minimums.update_from(self.context.search_graph[dfn].links);
198-
199-
// Return the solution from the table.
200-
let previous_solution = self.context.search_graph[dfn].solution.clone();
201-
info!(
202-
"solve_goal: cycle detected, previous solution {:?}",
203-
previous_solution,
204-
);
205-
previous_solution
206-
} else {
207-
// Otherwise, push the goal onto the stack and create a table.
208-
// The initial result for this table depends on whether the goal is coinductive.
209-
let coinductive_goal = goal.is_coinductive(self.program);
210-
let depth = self.context.stack.push(coinductive_goal);
211-
let initial_solution = if coinductive_goal {
212-
Ok(Solution::Unique(Canonical {
213-
value: ConstrainedSubst {
214-
subst: goal.trivial_substitution(self.interner()),
215-
constraints: Constraints::empty(self.interner()),
216-
},
217-
binders: goal.canonical.binders.clone(),
218-
}))
219-
} else {
220-
Err(NoSolution)
221-
};
222-
let dfn = self
223-
.context
224-
.search_graph
225-
.insert(&goal, depth, initial_solution);
226-
227-
let program = self.program;
228-
let subgoal_minimums = self.context.solve_new_subgoal(
229-
&goal,
230-
depth,
231-
dfn,
232-
|context, goal, minimums| {
233-
Solver::new(context, program).solve_iteration(goal, minimums)
234-
},
235-
|old_answer, current_answer| {
236-
// Some of our subgoals depended on us. We need to re-run
237-
// with the current answer.
238-
old_answer == current_answer || {
239-
// Subtle: if our current answer is ambiguous, we can just stop, and
240-
// in fact we *must* -- otherwise, we sometimes fail to reach a
241-
// fixed point. See `multiple_ambiguous_cycles` for more.
242-
match &current_answer {
243-
Ok(s) => s.is_ambig(),
244-
Err(_) => false,
245-
}
246-
}
247-
},
248-
);
249-
250-
self.context.search_graph[dfn].links = subgoal_minimums;
251-
self.context.search_graph[dfn].stack_depth = None;
252-
self.context.stack.pop(depth);
253-
minimums.update_from(subgoal_minimums);
254-
255-
// Read final result from table.
256-
let result = self.context.search_graph[dfn].solution.clone();
257-
258-
// If processing this subgoal did not involve anything
259-
// outside of its subtree, then we can promote it to the
260-
// cache now. This is a sort of hack to alleviate the
261-
// worst of the repeated work that we do during tabling.
262-
if subgoal_minimums.positive >= dfn {
263-
if let Some(cache) = &mut self.context.cache {
264-
self.context.search_graph.move_to_cache(dfn, cache);
265-
debug!("solve_reduced_goal: SCC head encountered, moving to cache");
266-
} else {
267-
debug!(
268-
"solve_reduced_goal: SCC head encountered, rolling back as caching disabled"
269-
);
270-
self.context.search_graph.rollback_to(dfn);
271-
}
272-
}
273-
274-
info!("solve_goal: solution = {:?}", result);
275-
result
276-
}
277-
}
278254
}
279255

280256
impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
@@ -283,7 +259,42 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
283259
goal: UCanonicalGoal<I>,
284260
minimums: &mut Minimums,
285261
) -> Fallible<Solution<I>> {
286-
self.solve_goal(goal, minimums)
262+
let program = self.program;
263+
let interner = program.interner();
264+
self.context.solve_goal(
265+
&goal,
266+
minimums,
267+
|goal| {
268+
let coinductive_goal = goal.is_coinductive(program);
269+
let initial_solution = if coinductive_goal {
270+
Ok(Solution::Unique(Canonical {
271+
value: ConstrainedSubst {
272+
subst: goal.trivial_substitution(interner),
273+
constraints: Constraints::empty(interner),
274+
},
275+
binders: goal.canonical.binders.clone(),
276+
}))
277+
} else {
278+
Err(NoSolution)
279+
};
280+
(coinductive_goal, initial_solution)
281+
},
282+
|context, goal, minimums| Solver::new(context, program).solve_iteration(goal, minimums),
283+
|old_answer, current_answer| {
284+
// Some of our subgoals depended on us. We need to re-run
285+
// with the current answer.
286+
old_answer == current_answer || {
287+
// Subtle: if our current answer is ambiguous, we can just stop, and
288+
// in fact we *must* -- otherwise, we sometimes fail to reach a
289+
// fixed point. See `multiple_ambiguous_cycles` for more.
290+
match &current_answer {
291+
Ok(s) => s.is_ambig(),
292+
Err(_) => false,
293+
}
294+
}
295+
},
296+
|| Err(NoSolution),
297+
)
287298
}
288299

289300
fn interner(&self) -> &I {

0 commit comments

Comments
 (0)