Eager variables in Pure -> Thunk

[hrutvik]

Alluded to in #40, ThunkLang passes are unusual: pure_to_thunk first Forces all variables (which are thunks), then thunk_let_force attempts to detect eager variables (those that are seqed) and un-Force them. In other words:

    seq (var x) $ ... var x ...
--> let fresh = force (var x) in ... force (var x) ...        -- pure_to_thunk
--> let fresh = force (var x) in ... var fresh ...            -- thunk_let_force

It makes more sense to do this in one step (during pure_to_thunk) by tracking the eager variables currently in scope. This also avoids repeatedly seqed variables: we will know that x is eager when processing the second seq in seq (var x) $ ... seq (var x) ..., and will not issue a second Force (though we would still issue the let-binding).

We can verify this new pure_to_thunk by recombining existing relations. But we should consider combining the initial pure_to_thunk relation and thunk_let_forceProof$e_rel instead. This would reduce proof bloat, and conceptually these belong together because pure_to_thunk handles non-strictness. We can also compile the repeated seqs above without the second let-binding. Also, if we introduce Haskell's optionally-strict bindings (i.e. "bang patterns") we can more easily produce good code, as the combined relation already tracks lazy/eager bindings.