Reimplement translator

[myreen]

That CakeML translator is the oldest part of the CakeML project and has grown organically with the project.

There are a number of features we would like added or improved:

• support for congruence rules: better support for translating recursion through higher-order functions #9
• user specified names for side conditions and user specifies when they are allowed/expected Checking for translator pre/side conditions. #546
• better translation of natural number subtraction Translate natural number subtraction to unconditional code when possible #427
• store deltas rather than entire state on theory export Use ThmSetData correctly in translator #1088 Translator state should be stored as per-theory deltas (at least for load/save) #717
• speed up very slow induction proofs
• better names for local variables translator to produce better variable names #12

This issue is about reimplementing the translator and gradually moving to the new implementation.

It is tempting to just delete the current translator and start from scratch, but I suspect that's likely to be too disruptive. Instead, I propose implementing new translate-like functions that at first co-exist with the current implementation until all of the current translations have migrated to the new translate functions.

Care needs to be taken in the design from that start in order to ensure support for congruence rules (#9) is built in.

[myreen]

My current plan for this issue does not involve reimplementing ml_progLib and how it builds CakeML environments and CakeML programs. This issue is about reimplementing ml_translatorLib.

[tanyongkiam]

While implementing #1114 it turned out to be really nice to selectively be able to turn off how aggressive the translator is about simplifying preconditions. The reimplementation of the translator should ideally be made externally-configurable for experts.

[tanyongkiam]

Another useful change (mentioned by @myreen): the new translator API should become explicit about when a precondition is expected to be generated.