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

Refactor CESK machine to track environments through new Suspended state #1928

Merged
merged 54 commits into from
Jun 19, 2024

Conversation

byorgey
Copy link
Member

@byorgey byorgey commented Jun 14, 2024

The big idea of this PR is to add a new type of CESK machine state, Suspended, which is a state the base robot automatically goes into after completing execution of a program entered at the REPL. It is as if the base robot is still within the local context of any definitions etc. entered previously, just printed out an "intermediate result", and is now waiting to find out what the next term to be executed will be. This allows us to treat def as syntax sugar for let and results in a much cleaner way to manage the context of definitions, which in turn allows us to remove a whole lot of special cases and fixes several annoying bugs. See #1087 for more explanation and discussion.

Things that are deleted (!) by this PR:

  • TDef (def is now just syntax sugar for let) (Add the scope of definition to its constructor #997)
  • VResult (we no longer need to return anything other than plain values)
  • FUnionEnv, FDiscardEnv, FLoadEnv (we no longer need machinery to collect up definitions while evaluating terms)
  • ProcessedTerm (just a plain TSyntax (i.e. Syntax' Polytype) is now enough)
  • Module (it only existed to package up some contexts with typechecked terms, but we don't need them anymore)
  • RobotContext and topContext (we don't need to store those things separately any more, they are just stored in the CESK machine where they belong)

Additions/changes:

  • The Requirement module is split into Requirements.Type and Requirements.Analysis to avoid circular module imports
  • New Suspended state for the CESK machine
  • def and tydef are now allowed anywhere (even nested inside other definitions etc.) since def x = y end; z is just syntax sugar for let x = y in z (see Nested definitions #349)
  • Code size decreased slightly for many programs using def, since def is now a synonym for let, and consecutive defs therefore do not require a bind.

Closes #1087. Fixes #681 (hence also #736, #1796). Fixes #1032. Closes #1047. Closes #997. Fixes #1900. Fixes #1466. Fixes #1424.

See also #636.

@byorgey
Copy link
Member Author

byorgey commented Jun 15, 2024

I know this is a massive refactoring---and no, there's not really any nice way to split it up into more incremental changes that I know of. This was the kind of refactoring where I started making changes and then finally got it to compile again a week later. I'm not necessarily expecting that anyone will be able to audit every line of code. What would be especially helpful is to just check out this branch and play the game for a bit, see if you can break it. I've fixed everything that I knew to check but there are bound to be some lurking bugs.

@byorgey byorgey requested a review from xsebek June 15, 2024 20:52
@byorgey byorgey mentioned this pull request Jun 16, 2024
22 tasks
@byorgey byorgey marked this pull request as draft June 16, 2024 04:05
@byorgey
Copy link
Member Author

byorgey commented Jun 16, 2024

Every time I think this is ready I find another bug... 😠

@byorgey byorgey marked this pull request as ready for review June 16, 2024 04:31
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.

Wonderful work @byorgey!
This makes possibly the most tricky part of Swarm easier to reason about. 👍

Yay for nested (type)definitions! 🥳

def.sw Outdated Show resolved Hide resolved
src/swarm-engine/Swarm/Game/CESK.hs Show resolved Hide resolved
src/swarm-engine/Swarm/Game/CESK.hs Show resolved Hide resolved
test.txt Outdated Show resolved Hide resolved
@byorgey
Copy link
Member Author

byorgey commented Jun 16, 2024

I think I have (finally!) squashed all the bugs I know about... I played through some of the early classic game (set up automated tree + bit farms, built a robot to automatically construct drill bits by fetching materials from depot robots, etc.) with no issues. Anyone else who would like to take a look at this before we merge it is most welcome! Thanks to @xsebek for the good feedback already.

@byorgey
Copy link
Member Author

byorgey commented Jun 19, 2024

OK, I'm going to merge this now I think... hold onto your hats... 🎩

@byorgey byorgey added the merge me Trigger the merge process of the Pull request. label Jun 19, 2024
@mergify mergify bot merged commit 23b5398 into main Jun 19, 2024
11 checks passed
@byorgey byorgey deleted the refactor/suspend branch June 19, 2024 20:00
mergify bot pushed a commit that referenced this pull request Jun 19, 2024
Closes #1948; see that issue for a much more in-depth discussion.

Depends on merging #1928 first.

A lot of this PR consists in deleting code that is either (1) ugly or (2) overly clever! 🥳 

The short version is that the `Store` used to incorporate some laziness + memoization: when a cell was first allocated, it was an unevaluated thunk; it then got evaluated the first time it was referenced.  However, this wasn't really needed to handle recursive definitions (which is the only thing we were using it for).  Getting rid of it means we can get rid of a lot of weird ugly code needed to wrap free variables in extra calls to `force` and so on.

The new and improved `Store` just stores `Value`s, period.  A special `VBlackhole` value was added, to be used while evaluating a recursive `let`.

Note that `VRef` is no longer really used, but I left it there for use in implementing #1660 .  Once we have mutable references we can use them + delay/force to implement lazy cells.
mergify bot pushed a commit that referenced this pull request Jul 1, 2024
Fixes #2007.  After #1928, we handle exceptions a little differently, so it no longer works to simply set the base's CESK machine to an `Up` (exception) state no matter what.  Instead we have to first check if the base is running, and if so set it to `Up` as before; if not, do nothing (except clear the REPL prompt).
mergify bot pushed a commit that referenced this pull request Jul 6, 2024
The bug which necessitated the workaround was fixed in #1928.
xsebek added a commit that referenced this pull request Aug 9, 2024
```diff
 def intersperse
   = \n. \f2. \f1.
-  if (n > 0) {f1; if (n > 1) {f2} {}; intersperse (n - 1) f2 f1} {} end
+  if (n > 0) {f1; if (n > 1) {f2} {}; intersperse (n - 1) f2 f1} {}
+ end
```

* caused by #1928 where def was made more similar to let
mergify bot pushed a commit that referenced this pull request Aug 9, 2024
```diff
 def intersperse
   = \n. \f2. \f1.
-  if (n > 0) {f1; if (n > 1) {f2} {}; intersperse (n - 1) f2 f1} {} end
+  if (n > 0) {f1; if (n > 1) {f2} {}; intersperse (n - 1) f2 f1} {}
+ end
```

You can test it with:
```sh
swarm format -i data/scenarios/Challenges/_arbitrage/solution.sw
```

* caused by #1928 where def was made more similar to let
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CHANGELOG Once merged, this PR should be highlighted in the changelog for the next release. merge me Trigger the merge process of the Pull request.
Projects
None yet
3 participants