Implement and use a new RecordMap type #786

robdockins · 2020-06-26T23:49:49Z

This type stores records as a finite map from field names to
values, while also remembering the original order of the fields
from when the record was generated (usually, from the program source).
For all "semantic" purposes, the fields are treated as appearing in
a canoical order (in sorted order of the field names). However, for
user display purposes, records are presented in the order in which
the fields were originally stated.

In the course of implementing this, I discovered that we were not
previously checking for repeated fields in the parser or typechecker,
which would result in some rather strange situations and could probably
be used to break the type safety. This is now fixed and repeated fields
will result in either a parse error or a panic (for records generated
internally).

Fixes #706

src/Cryptol/Parser/NoPat.hs

src/Cryptol/TypeCheck/TypeMap.hs

src/Cryptol/Utils/RecordMap.hs

src/Cryptol/Eval.hs

src/Cryptol/Utils/RecordMap.hs

src/Cryptol/ModuleSystem/Renamer.hs

src/Cryptol/Parser/ParserUtils.hs

src/Cryptol/TypeCheck/Sanity.hs

brianhuffman · 2020-06-30T01:32:19Z

Overall, this looks great. Most of the files you had to change look better than before, both more concise and more directly expressing the code's intent. Thanks @robdockins for doing this!

This type stores records as a finite map from field names to values, while also remembering the original order of the fields from when the record was generated (usually, from the program source). For all "semantic" purposes, the fields are treated as appearing in a canoical order (in sorted order of the field names). However, for user display purposes, records are presented in the order in which the fields were originally stated. In the course of implementing this, I discovered that we were not previously checking for repeated fields in the parser or typechecker, which would result in some rather strange situations and could probably be used to break the type safety. This is now fixed and repeated fields will result in either a parse error or a panic (for records generated internally). Fixes #706

address review comments.

Also update cryptol-verifier and saw-script to adapt to cryptol changes.

robdockins requested a review from brianhuffman June 26, 2020 23:49

robdockins commented Jun 27, 2020

View reviewed changes

src/Cryptol/Parser/NoPat.hs Show resolved Hide resolved

robdockins commented Jun 27, 2020

View reviewed changes

src/Cryptol/TypeCheck/TypeMap.hs Show resolved Hide resolved