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

Copy requirements map to robot context when loading a new ProcessedTerm #827

Merged
merged 12 commits into from Nov 5, 2022

Conversation

byorgey
Copy link
Member

@byorgey byorgey commented Nov 5, 2022

Closes #540.

When we typecheck and capability check a new term, resulting in a ProcessedTerm, we already know the Requirements for all the defs it contains. This PR simply takes all those definition requirements and adds them to robotContext . defReqs just before installing the new ProcessedTerm in the CESK machine, so that if we ever encounter the name of any of the definitions inside an argument to build or reprogram---which we capability check at runtime---we will be able to properly match up names with their requirements.

This is a hack for several reasons:

  • We really shouldn't be capability-checking arguments to build and reprogram at runtime in the first place---ideally we should be able to check everything statically. But fixing that will require implementing Handle capabilities properly as part of the type system #231 .
  • We have to do this in three places in the code: when loading a new term into the base when the player hits Enter at the REPL; when executing run; and when running the solution from a scenario in the integration tests. Ideally, there would be only one place, but I don't have a good idea at the moment how to refactor things properly.
  • Technically, the names being defined shouldn't be in scope until after their corresponding def runs, so it's incorrect to dump them all into the defReqs prior to executing any of the defs.
    • However, doing it properly, with each name coming into scope with its requirements right after the def runs, is very tricky/annoying to implement for more reasons than I care to write about here (believe me, I tried, and it made my brain hurt). For starters, we don't really have access to the robot state when stepping the CESK machine.
    • The only scenario where this would be a problem is if (1) there is already a name x defined, and then we (2) run a .sw file containing, first, a build command whose argument references x, and second, a redefinition of x. In that case the build would incorrectly decide that the x in the argument to build has the requirements of the second x (the one that will be redefined later) even though the first x is the one that should still be in scope. However, this seems like a very unlikely scenario (who would write a .sw file that depends on some specific name already being defined before it is run, but then redefines that same name later?) and I'd much rather have that obscure problem than the current very relevant and annoying one.

However, it's a simple hack that solves the issue and will be easy to get rid of later if and when we do something better. I'm a big believer in doing things the right way, but in this instance I definitely think we should just do the simple thing that mostly works and then continue to make it better in the future.

@byorgey
Copy link
Member Author

byorgey commented Nov 5, 2022

Hmm, the lodestone test is failing, not sure why yet.

EDIT: haha, OK, figured it out. First, it was so nice having --autoplay to help track this down, thanks @kostmo! It turns out that the solution to that test was actually depending on #540 to work. 😆 The base did not have any lambdas, but the robot it was building required one. With #540 that did not get checked, and then as we learned in #785, the use of lambdas is not checked at runtime. So, I added some lambdas to the base's inventory.

@byorgey byorgey marked this pull request as ready for review November 5, 2022 14:26
@byorgey byorgey requested a review from xsebek November 5, 2022 16:23
Copy link
Member

@xsebek xsebek left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Kudos @byorgey! 👍

I would add that it will also be easier to optimize in the Web API future, so simple solutions now make sense. 😉

@byorgey byorgey added the merge me Trigger the merge process of the Pull request. label Nov 5, 2022
@mergify mergify bot merged commit 9d5df80 into main Nov 5, 2022
@mergify mergify bot deleted the fix/issue-540b branch November 5, 2022 17:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge me Trigger the merge process of the Pull request.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Definition capabilities are not available later in the same term
2 participants