Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Output multiple solutions #263

Merged
merged 6 commits into from Oct 29, 2019

Conversation

@olegshtch
Copy link
Contributor

olegshtch commented Oct 19, 2019

I've tried to use chalk as generic logic solver and found I can not get output if there more than one solution.

This PR adds --multiple flag to chalki. If it enabled chalki iterates over multiple solutions with confirmation from user instead of generating "ambiguous" solution. If goal was provided with arguments it iterates over all solutions.

It uses callback function to manage iteration over solution because I couldn't export ForestSolver iterator structure.

Copy link
Collaborator

nikomatsakis left a comment

I left a few minor nits, but this seems like a reasonable addition. It can definitely be useful to see all the answers. It'd be nice to have some sort of text somewhere, though -- maybe you can adapt the testing infra so that you write a test like

goal { 
    XXX
} yields* {
    "...",
    "...",
}

The idea being that if you write yield* we will invoke solve_multiple instead? (And get back the answers in the order given)

/// each time you invoke `solve`, as otherwise the cached data may be
/// invalid.
/// - `goal` the goal to solve
/// - `f` -- function to proceed solution. New solutions will be generated

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Oct 21, 2019

Collaborator

It's not obvious what the parameters to f represent, can you comment them here?

This comment has been minimized.

Copy link
@olegshtch

olegshtch Oct 24, 2019

Author Contributor

I've added comment about parameters and return value.


/// Takes one answer and returns it as unique solution
impl<'me> context::UniqueOps<SlgContext> for SlgContextOps<'me> {
fn make_unique_solution(

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Oct 21, 2019

Collaborator

I don't really understand this name. It doesn't seem like it's making a "unique" solution -- it seems like it's just extracting the canonical substitution from the answer? Maybe we should just call it constrained_subst_from_answer or something?

I think I would also just add it to ContextOps instead of creating a new trait.

This comment has been minimized.

Copy link
@olegshtch

olegshtch Oct 24, 2019

Author Contributor

I've moved and renamed this function.

@olegshtch olegshtch force-pushed the olegshtch:multiple-answers branch from da86670 to a03ae42 Oct 24, 2019
@olegshtch

This comment has been minimized.

Copy link
Contributor Author

olegshtch commented Oct 24, 2019

@nikomatsakis Maybe it better to have two different syntax for testing? The frst for all answers and the second for the first some answers like yields* and yields+ or yields_all and yields_first.

Copy link
Collaborator

nikomatsakis left a comment

Thanks =)

@nikomatsakis nikomatsakis merged commit 8314f2f into rust-lang:master Oct 29, 2019
1 check passed
1 check passed
Travis CI - Pull Request Build Passed
Details
@olegshtch olegshtch deleted the olegshtch:multiple-answers branch Oct 29, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.