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`.