Injective mapping from Cryptol types into saw-core

[brianhuffman]

Currently the Cryptol to saw-core translation conflates some types: Tuple types are represented as nested right-associative pairs, so e.g. (a, b, c) and (a, (b, c)) are both translated as the same type a * b * c. Also, Cryptol record types are simply converted to tuple types of the same size, so record field names are completely lost.

This causes some problems: For example, translated records are hard to make sense of because of the missing field names (#878). Also, it's currently not possible to reliably recover a cryptol type given a saw-core term (#718).

We need a new encoding of tuple and record types into saw-core that is injective, so that we don't lose information translating from Cryptol to saw-core. Also, to improve the user experience with saw-core, we should make tuples and records look, feel, and behave the same way they do in Cryptol (as much as possible).

[brianhuffman]

PR #1612 is a step in this direction.

[sauclovian-g]

See #659 and #2119.