[RobinWebbers]

This is a big adjustment, where we completely rebuilt the symbolic evaluator.

Symbolic evaluator

At a high level, the evaluator is now much closer to the actual evaluator scheme of Haskell. Allocated thunks are managed through IORef. This way we can apply the evaluation on such a Thunk while applying a side-effect. Previously we would keep arguments as actual Haskell thunks. This got very hairy... In any case, this closes #9.

With us now being able to inspect our runtime better through a Thunk, we can now print the (reachable) allocations from any expression. This allows us to inspect the RTS at any point of evaluation!

Instead of keeping an adjusted form of Expr (as we did previously), we define a WHNF value that is symbolic. This one contains closures, primitives, data constructors and literals. The merging of these is straightforward and does not propagate into its arguments. We also chose to deal with types and coercions in the same way Haskell does: types can be elided and coercions are unit values.

A Thunk comes in three shapes:

• It is a WHNF value (it was already evaluated)
• It is a Thunk containing the environment and expression to evaluate
• It is a Ite, i.e. a branch of two Thunks. This last one is used when merging e.g. a DataCon WHNF.

We leave an Ite thunk as non-merged to accommodate for when we want to add in pruning #7: this way we can decide to drop a Thunk before we actually evaluate it.

We also improved branch operations. On a case-of, we now first accumulate all of the patterns that can only match the default case. This way, we can run the default right-hand side once using this accumulate value!

Fresh variable generation

We also did some initial work for the new API as proposed by #6. This one is not fully done however, so we keep it open. The main change is that we now have a Sym monad in which symbolic statements are run. For now, we only support fresh, which constructs a fresh value. As we haven't implemented checking primitives, the expected type for checking a proposition is Sym Bool.

We do close #3 as we created a fresh variable generation API. It works through the Gen monad. It is a little specific so I'll explain it here. Fresh variable generation should be lazy. For example, we should be able to generate a infinite list of fresh values in a list (without looping forever).

There are two ways to achieve this:

• The build should pass a fresh identifier to every nested call. This has the downside however of very quickly growing the identifier size.
• We generate the fresh identifier when a values is demanded. This is a little bit more involved, as for example sharing an expression can create different identifiers if we are not careful. Still, we took this approach and we solved it by following the approach of lazy IO.

Lazy IO gets a very bad name in Haskell (for good reason), but in this case it is very much justified! The side effect we provide is about the same as an oracle that assigns a random unique identifier (which a user cannot actually inspect). Hence, this side-effect is completely harmless.

We use the exact same mechanism as unsafeInterleaveIO, which is used to implement lazy IO. It works by returning a SymWorld token on which the next computation depends. The token is not forced, but lifting of the inner value is blocked by marking the function NOINLINE (thereby no sharing happens, so we ensure that we do not get two fresh variables for the same call).

In the end, the primitive call symbolic# is of type Primitive a => Gen a, where Gen :: SymWorld -> a -> Gen a. Notice how we don't need to return a SymWorld as we never need non-lazy values in Gen. The monadic bind makes sure that we get the lazy behaviour by calling unsafeDefer (unsafeInterleaveIO for SymWorld) on every bind.

The Gen monad can be lifted into the Sym monad (but not vice versa). Note that we use separate monads because indeed Sym should not have these lazy semantics.