Pass canonical goals to program clauses code in SLG solver #624
Conversation
There was a problem hiding this comment.
I'm on mobile, so not going to be a perfect response here. But this looks...not that great. I mean, it looks correct, but we went from instantiating in one place to two places, plus that rewrapping of the domain goal in the canonical binders and environment.
I guess it would nice if we could clean that up somehow. If you don't want to do that in this PR, I would like a FIXME at least and then r=me.
|
Overall this seemed pretty nice to me. I still think that it's the right setup -- I guess my reasoning is basically that I think we ought to be caching the results of those calls, so passing in canonical things seems correct. |
|
☔ The latest upstream changes (presumably #609) made this pull request unmergeable. Please resolve the merge conflicts. Note that reviewers usually do not review pull requests until merge conflicts are resolved! Once you resolve the conflicts, you should change the labels applied by bors to indicate that your PR is ready for review. Post this as a comment to change the labels: |
Instead of instantiating goals first, as is the case currently
jackh726
force-pushed
the
slg-program-clauses
branch
from
3d6e16c to
d719618
Compare
|
Review comments have been addressed and this should be good to merge. |
jackh726
force-pushed
the
slg-program-clauses
branch
from
328bb41 to
0b391f8
Compare
|
@bors r+ |
|
📌 Commit 0b391f8 has been approved by |
|
☀️ Test successful - checks-actions |
It seemed like we were leaning towards this solution in the design meeting, and it turned out (assuming these changes are right) to be pretty straightforward.
Closes #568.
This should stop seeing issues related to failing to generalize program clauses pop up, but I'm only going to cc #614 since I'd like some tests maybe.