feat: optionally do not evaluate under binders (except lets)

[brprice]

This change means our EvalFull is "closed evaluation", rather than "open evaluation". The main reason to do this is so that evaluations of programs-in-construction (especially recursive ones) do not pointlessly blow up in size: if even and odd are defined recursively, then evaluating even would evaluate under the lambda and inside case branches, expanding odd and recursing; when it eventually times out one would have a big tree with many unrolled copies of even and odd, which is not very illuminating.

Note that we do not evaluate in the RHS of pattern match branches which bind variables, for the same reason as we do not evaluate under lambdas; for consistency we also do not evaluate in the RHS of branches which do not bind variables.

[brprice]

Status: Ready for review, but

• This will need some integration work with feat: push down lets #736 . In particular, we will not need to treat lets specially (currently we eval under them), but will want to push them through binders; and we will want to not eval under ∀ (currently we don't bother to do any "not eval under binders" at the type level, since the only computation is inlining lets, which we need to do under binders anyway (else they could block e.g. beta). Commit messages (and comments?) will also need updating
• Rebase away a few TODO/REVIEW comments

[dhess]

Once #736 is merged, I would like to get this merged, as well. This will become even more important once we implement #1119.

[brprice]

This has been rebased on top of the push-down-lets work, and is ready for a review.

Reviewer note: please give extra scrutiny to comments and code that may have not been updated for push-down-lets (this branch originated before #736)

[dhess]

@brprice Can you mark this as ready for review so that it shows up in the UI?

[georgefst]

For the record, I'm still not fully convinced that this is the right long-term solution to the UX issue of showing unproductive eval steps for unapplied functions etc. But since we're making this optional that doesn't matter.

[dhess]

For the record, I'm still not fully convinced that this is the right long-term solution to the UX issue of showing unproductive eval steps for unapplied functions etc. But since we're making this optional that doesn't matter.

Any better ideas?

[georgefst]

I'm sure we discussed this at length at some point but I can't find any notes. But I remember a suggestion that we stop with an "are you sure you want to continue?"-style message when the size of the eval tree reaches a certain multiple of the original. Anyway, I don't feel too strongly about it and think further explorations should at least wait for #1119.