cakeml
cakeml copied to clipboard
Add code quality tests to regression
At present, the compiler proofs are regression tested. This means the compiler generated code will always stay correct. However, the compiler and its configuration are not currently tested for quality.
This issue is about adding a collection of simple tests that ensure optimisations trigger in situations they are supposed to be triggered. One could, e.g., take a few simple code snippets, compile them to dataLang, and check that certain small functions are inlined in the generated dataLang program. See examples/cost
for nice pretty printing of dataLang programs.
The same can be done for wordLang
, one could check wordLang optimisations using functions already present in examples/compilation/to_word
.