Evaluate arbitrary lambdas in animation primitive #1169
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The major limitation of #1164 is that we can only use trivial functions as the second argument to
animate, without the evaluator getting stuck. That is, functions where only a substitution is needed for the function body to reach a normal form.Consider an expression
animate 5 (λt. circle (t × 2)). Note that both arguments are normal forms. The problem is that evaluating this requires evaluatingcircle (0 × 2),circle (0.1 × 2),circle (0.2 × 2)etc. in order to generate the frames of the animation. Whereas for all of our other primitives, once the arguments are in normal form, computing the normal form of the applied function is trivial. This all happens in the functionprimFunDef, which establishes the semantics of our primitive functions, and is not set up to be able evaluate further. Even at a higher level, it's not clear how we should handle this, given that the new expressions requiring evaluation are not guaranteed to be normalizing.This PR lifts the trivial-functions restriction in most circumstances, in a hacky unprincipled way. It breaks all sorts of abstractions, and doesn't guarantee that evaluation respects the configured termination bound. Of course, it should not be merged in anything resembling its current form, but it's useful for exploring more complex animations. A proper solution will require some sort of reworking of the evaluator, and I'm not yet sure what that should look like. Alternatively, and this is my personal preference, we could just embrace the projections-based approach discussed in #1173.