Remove the LambdaBoxMut language, translating directly from LambdaBox to LambdaBoxLocal

[mattam82]

Only issue is that the LambdaBox -> LambaBoxMut compilation is currently partial, which is implemented by a TWrong constructor in LambdaBoxMut that is blindly translated to Prf_e in LambdaBoxMut_to_LambdaBoxLocal.
Proposed fix:

• Translate directly from LambdaBox to LambdaBoxLocal (adapting the LambdaBox_to_LambdaBoxMut compilation function).
• Make it a total function by restricting to terms that do not contain the unsupported constructors (LambdaBox has a flag system to express that).
• Remove the unnecessary proofs

[yforster]

after additional discussion today, this is the new plan:

• implement and verify support for thunk and force on LambdaBox (this is currently done when going from LambdaBox to LambdaBoxMut). This should be easy.
• implement and verify localising global environments into lets on LambdaBox (this is currently done when going from LambdaBoxMut to LambdaBoxLocal). This should be tedious, but we can follow the old proof closely.
• we adapt what's done in fuel_sem.v, a fueled environment-based bigstep evaluation relation for LambaBoxLocal, to LambdaBox
• implement and verify CPS translation from LambdaBox to LambdaANF (this is currently done when going from LambdaBoxLocal to LambdaANF). This should not be too hard.
• implement ANF translation from named variant of LambdaBox to LambdaANF (this is currently implemented but not verified). This should be easy.

Overall the code that will be deleted should be around 10k lines (everything in LambdaBoxMut and LambdaBoxLocal). The code that will have to be adapted currently is 7k lines (everything of the form LambdaBoxLocal_to_LambdaANF*.v)

As a benefit, we can forget about both LambdaBoxMut and LambdaBoxLocal and just use the flag system of LambdaBox.

[andrew-appel]

For "thunk" and "force", are these memoizing, with mutable references, or forgetful (so, recompute every time) ?

[yforster]

These are not memoizing at the moment, and they won't be memoizing after. We could think about making them memoizing in the future.

We also noticed something: Currently LambdaBoxMut_to_LambdaBoxLocal goes from a named (global) environment to a de Bruijn substitution-based semantics. If we refactor, we can go from a named global environment to a de Bruijn environment, which should make the proof simpler because it only has to deal with one change of representation, not two.

[yforster]

One more discussion, one more plan:

• implement and verify support for thunk and force on LambdaBox (this is currently done when going from LambdaBox to LambdaBoxMut). This should be easy.
• use the existing transformation of tRel to named tVars for LambdaBox.
• prove on the named variant of LambdaBox that global environments can be translated into local environments (replacing tConstant by tVar). This should be easy.
• prove that local environments can be inlined as lets. This is super easy.
• implement and verify ANF translation to LambdaANF. This is a significant task, Zoe's estimate is that it's order of magnitude of 6 months work.
• adapt proof of CPS translation to LambdaANF. This is not too bad, Zoe's estimate is 2 weeks.

In this new plan, we do not have to introduce a new semantics, we can work with the relations that already exist. We also don't need any intermediate syntax anymore, so no code duplication for boilerplate.