Integrating types 8: using new types in the checker core

[konnov]

This is the final piece of the puzzle. The translation rules to SMT are now using TlaType1 as input as well. Unfortunately, I don't know yet, whether we can get rid of the intermediate type CellT that is used in the rewriting process. So you will see that in some cases TlaType1 is translated to CellT and back. The reason is that CellT is slightly reacher than TlaType1. For instance, CellT has power sets and infinite sets, whereas TlaType1 has just sets.

I did not anticipate that several rewriting rules had to be changed. The reason is that we now infer types from top to the bottom, instead of bottom to the top. As a result, sets can now contain records that have different (though compatible) record types. In the old implementation, all records were immediately normalized to the most general type by padding them with extra fields. We cannot do it any longer, so translation of several operators on records became more nuanced.

As with previous PRs on this feature, we should check that no stupid bugs were introduced and open issues on the follow-up design improvements and refactoring. This has been too many changes for one feature. Once the review is done, we should merge this feature, cut a new release, clearly mark it as unstable and improve in the next month (or two ;-)).

Since the changes have been touching large portions of the codebase, I would prefer bumping the version by several increments, like 0.15.0, so the users would clearly see that it is not just one more release, but something much more different.

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entry added to UNRELEASED.md for any new functionality

[shonfeder]

I gave this a very cursory view, as discussed in meeting, the context of these PRs and the time pressured don't allow for proper reviews, so no guarantees on my signoff ;)