"Pushing down" let bindings

[dhess]

Our evaluator should not eliminate lets until they're "pushed down" to their use sites. This would permit more flexible interactive evaluation strategies in eval mode (see discussion in https://github.com/hackworthltd/vonnegut/discussions/638). It might also potentially simplify the most complicated bit of the current evaluator — see https://github.com/hackworthltd/vonnegut/pull/768#discussion_r678488543.

In order to preserve the "small local changes" spirit of our reduction rules in the current eval mode, we should probably implement this as @brprice suggested (and I documented in https://github.com/hackworthltd/vonnegut/discussions/638), such that lets float down towards their occurrences. @georgefst also suggested that we could add an affordance to allow students to click-drag a let to each of its use sites before eliminating it, which seems like a good idea, though it should probably be part of a suite of similar interactions, rather than just a special case interaction for eliminating lets.

But let's start simple. I propose that we change the current let elimination rule so that a let can only be eliminated once it's adjacent to the use of the bound variable, and that we add a "push down" rule that moves a let one step closer to its use(s), splitting the let into multiple equivalent lets when more than one child contains a use . If the latter is too annoying in practice, we can try some alternate approaches, such as @georgefst's suggestion, or just a macro step that pushes a let all the way down to all of its bound variable's occurrences in one go.

(One special case that occurs to me as I write this: Imagine we have const x y = x and we evaluate const 3 2 giving let x = 3, y = 2 in x — we need to be able recognize and step-eliminate the let y = 2 in this case.)

See #28 for an example of why this feature would be useful.

[brprice]

Doing this for let and letrec should be fairly straightforward. However, we cannot do it for lettype in our current language -- that is blocked by not having support for let-bindings inside types. However, we could fairly easily add that in the same style as the current let type: it exists for evaluation but not in the language proper (see also #337)

[brprice]

Note that we should revisit #734 once we investigate doing this pushing down.

[dhess]

Will be closed by #736.

[brprice]

Closed by #736