Skip to content

Wingman should notice variables already used, outside of the hole #1704

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

Closed
isovector opened this issue Apr 11, 2021 · 1 comment
Closed

Wingman should notice variables already used, outside of the hole #1704

isovector opened this issue Apr 11, 2021 · 1 comment
Labels

Comments

@isovector
Copy link
Collaborator

test :: (a -> b -> b) -> b -> [a] -> b
test _ b [] = b
test f_b b (a : l_a4) = f_b a $ test f_b b _

Wingman wants to fill this hole with a : l_a4, since it uses more variables from the hypothesis. But it doesn't pay attention to the expression context, where it could learn that a has already been used.

This is not hard to fix --- subtract used-in-context variables from syn_used_vals before scoring.

@isovector
Copy link
Collaborator Author

Thinking further about this, we can use the provenance of a term to calculate its "specificity." If the user has gone through all of this work to get a specific variable in scope, which happens to have the same type as one more widely available, then it's probable that we should use the more specific one. At least for non-top holes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants