This is in preparation for rethinking how we evaluate let bindings.

Signed-off-by: Ben Price <[email protected]>

we do this because we are changing eval a lot shortly, and want to be able to see changes. is also easier to update when bounds are broken!

…ith next commit!

This can be seen as an explicit-substitution style operational
semantics.

This change in approach means that our evaluation rules are much more
local, and will enable some future simplifications. In particular we
will avoid using the `Accum` machinery, simplify the eval `Cxt` and not
have to have a separate eval mode for substitutions.

We temporarily disable EvalFull.unit_8. It does pass (note that the step
count is bumped), but takes a long time (almost 10 minutes on my
machine!). This will be massively improved shortly, by being more
aggressive in eliding pointless `let`s.

Signed-off-by: Ben Price <[email protected]>

pushMulti opt

Signed-off-by: Ben Price <[email protected]>

…mbiguous

bump limit on unit_prim_partial_map because...

it turns out that on this workload the aggressive elision optimisation
actually takes more step. However, the trees are somewhat smaller.
this is because the optimisation makes no difference on terms like
  let x1=_ in ... let xn=_ in xi
as `xi` is a leaf. This workload has many such subterms which get created when pushing lets down. Aggressive elision will remove some of the lets early, when they are (for example)
  let x1=_ in ... let xn=_ in C xi xj
but this takes an extra step

This phenomenon is also seen in unit_type_preservation_BETA_regression

Since we are eliding aggressively, we may as well not create the
pointless lets in the first place. (Note that we may still create
pointless lets when renaming binders.)

This again noticably speeds up unit_8 and unit_9.

Signed-off-by: Ben Price <[email protected]>

This fixes unit_redexes_lettype_capture, where we want to not consider a
burried binder renamable.

Signed-off-by: Ben Price <[email protected]>

Now we are pushing down lets, we do not need so much information about
bindings. In particular, we do not need to record the original binding
location, or the original binding's context, since we do not do
long-range substitution where care is needed to avoid capture.

Signed-off-by: Ben Price <[email protected]>

This fixes a rare issue that if one has two adjacent lets with the same
name, we would only record one of them in the `Cxt`, and thus
miscalculate whether a binder they immediately contain needs to be
renamed before we can push the lets under.

Signed-off-by: Ben Price <[email protected]>

This is because we "push down lets", rather than doing long-range substitutions.

Signed-off-by: Ben Price <[email protected]>