Open
Description
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.