Faster interpreter

[tjhance]

This is a proof-of-concept for a faster interpreter. It needs a lot of work to reach feature parity with the current one, but it is orders of magnitude faster. As a test case I have been using the bin-sizes lemma from the mem allocator project, which loops over 100k values. We previously found this example to be infeasible, taking several minutes at the very least. With the faster interpreter in this PR, it completes in a couple of seconds.

This new interpreter works by "compiling" spec expressions into a simple stack-based instruction set with instructions for unary ops, binary ops, jumps, constructors, calls, memoized calls, and closure calls. We also operate on a new datatype, called Value, rather than working with Exp. Though not implemented yet, the plan is to convert Values back to Exps for the 'compute-followed-by-z3' mode. The logic for all the different unary ops and binary ops is mostly unchanged, just copied and adjusted for the new datatypes.

Some advantages of this system:

• execution doesn't have to work with identifiers at all, reducing the need for hash lookups
• fewer allocations because we aren't working with Exps or Typs
• execution is driven by a loop { } rather than recursion, thus reducing the stack overflow issues that require the current interpreter to launch a new thread
• this is basically how computers work so it seemed reasonable to me that it'd be pretty fast

[tjhance]

This has been sitting untouched for a long while now, so people might wondering where it's at ...

The short answer is that I ran into a problem with the assert-by-computer-then-z3 mode, since it requires turning the optimized 'Value' nodes back into 'Exp' nodes, which requires computing the types of each expression. To resolve this, I either need to make types into first-class values into the executor, or do some kind of monomorphization thing. Anyway, it's not trivial to resolve.

[parno]

Hmm, that does sound annoying. Thanks for the update!