Refactor the recursive solver a bit #487
Conversation
| /// Solves a given goal, producing the solution. This will do only | ||
| /// as much work towards `goal` as it has to (and that works is | ||
| /// cached for future attempts). | ||
| pub fn solve( |
There was a problem hiding this comment.
As sort of a drive-by change, I moved these two functions solve and solve_multiple out of Forest (and chalk-engine) and into chalk_solve::solve. For solve, it honestly just makes more sense, since this is the only place solution is needed. For solve_multiple, there's a little work done here, but really I think these are implementation details akin to aggregate.
| pub(crate) infer: InferenceTable<I>, | ||
| } | ||
|
|
||
| impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I> { |
There was a problem hiding this comment.
I started to wonder if maybe it's worth having this notion of an InferenceTable (as a trait) in chalk_ir. A lot of these functions are also used for slg. Notable differences include invert_then_canonicalize and actually using the free_vars from canonicalize
There was a problem hiding this comment.
I think the inference code itself should maybe move to chalk-ir, actually, but we should discuss, especially in light of your idea to "invert" the dependency layers.
|
|
||
| /// A (possible) solution for a proposed goal. | ||
| #[derive(Clone, Debug, PartialEq, Eq)] | ||
| pub enum Solution<I: Interner> { |
There was a problem hiding this comment.
This is mostly just copied from chalk_solve::solve. But I didn't really think of a good way to handle this. We can make SearchGraph generic over Solution, but Fulfill:solve needs to know about these. I wish it was easier to split out solve from Fulfill (similar to how we split out aggregate from chalk-engine, but the solve function needs to know a lot about the internals of Fulfill that we would have to expose publicly.
There was a problem hiding this comment.
I feel.. hmm.. a bit confused about this. I guess I think I would expect this type to potentially be in chalk-ir -- is it really specific to the recursive solver? Don't we use a similar type for SLG? (I guess as the output from aggregation?)
I think my take is that aggregation probably belongs in with the SLG solver in the end, although it is definitely a distinct "layer".
| @@ -57,100 +60,6 @@ impl<I: Interner> Solution<I> { | |||
| } | |||
| } | |||
|
|
|||
| /// There are multiple candidate solutions, which may or may not agree on | |||
There was a problem hiding this comment.
On the other hand (continued from where these are copied to), the fact that several of these functions are only used in the recursive solver makes me wonder if this is mostly okay anyways.
| } | ||
| #[cfg(feature = "recursive-solver")] | ||
| SolverImpl::Recursive(ctx) => ctx.solver(program).solve_root_goal(goal).ok(), | ||
| SolverImpl::Recursive(ctx) => { | ||
| ctx.solver(program) |
There was a problem hiding this comment.
But (continued from above still), this is a bit annoying.
There was a problem hiding this comment.
Yes.. that is indeed a bit annoying. Nevertheless if what you suggested happens (chalk engine + chalk_recursive depending on chalk solve), this one solver struct can go away correct?
This is about 95% of the work needed to put the recursive solver in a separate crate.
Everything in
chalk_solve::recursive::*can get moved.recursive.rsis mostly the equivalent of theslgsubmodule.