Reimplement translator

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: #9
- user specified names for side conditions and user specifies when they are allowed/expected #546
- better translation of natural number subtraction #427
- store deltas rather than entire state on theory export #1088 #717
- speed up very slow induction proofs
- better names for local variables #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.