CakeML
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.
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.
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.
Another useful change (mentioned by @myreen): the new translator API should become explicit about when a precondition is expected to be generated.