Records in saw-script have lost their field names, making reading difficult

[msaaltink]

One is occasionally obliged to read the output of print_goal to try to figure out why a proof script is not working. When doing this, it is rather annoying that record field names have been replaced by strings of digits. I'm never sure what field something like R.2.2.2.2.1 refers to, and while I can usually figure it out, that takes time away from actually identifying the problem with my proof attempt. If field names could be preserved in saw-core, this would be much easier.

[brianhuffman]

There are a lot of different potential encodings for tuples and records in saw-core, and we've tried a few of them. Each design has different tradeoffs, but our latest thinking is that to make things easiest on users, we should strive for as much consistency between saw-core and cryptol as possible—even if that makes things a bit more complicated on the implementation side.

Some possible designs for tuple/record encoding in saw-core are listed in the comment thread for GaloisInc/saw-core#6. The encoding we implemented at the time (2015) used a nested, nil-terminated representation for tuples and records. Record selectors used a position-independent name-only representation that was a little bit magic, and had questionable semantics; so later (2018) we simplified the tuple representation again and got rid of records entirely (using tuples also to represent cryptol records).

I should point out that we ruled out just having a primitive n-tuple type constructor at every size, because that wouldn't let us write generic saw-core code for implementing class dictionaries for abitrary tuple sizes (similarly for records).

Anyway, it seems like it's time to reconsider our options for saw-core tuples and records once again.

[brianhuffman]

Before we embark on a full redesign of tuples and records, there are a couple of changes to pretty-printing that would help. When printing nested tuple projections, we should display something like x.5 instead of x.2.2.2.2.1. Also, for consistency with Cryptol we should switch saw-core to use 0-based tuple indices instead of 1-based.

[msaaltink]

Those would definitely be helpful changes. Maybe a bit tricky because I see things like "let ... @5 = R.2; x@6 = [email protected]; in ... [email protected] ... when hash consing is on, and this R.2 and [email protected] are not fields of the original record.

[sauclovian-g]

Also see #2119 and #659.