informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
608 stars 30 forks source link

Parse the empty tuple type #1421

Closed bugarela closed 2 months ago

bugarela commented 2 months ago

Hello :octocat:

PS: large diff because of generated files. Files with unloaded diffs don't need reviewing, they were generated from Quint.g4.

Closes https://github.com/informalsystems/quint/issues/1420. In https://github.com/informalsystems/quint/pull/1406, we added parsing for the empty tuple value, but not for the type. This PR adds parsing for the empty tuple type.

A note on the grammar change: I couldn't just update the existing tuple type rule to parse 0+ types because of cases like (int), which we want to be parsed as int and not as a tuple of 1 type. So basically we can parse tuples of size 0 or 2+, but not 1.

bugarela commented 2 months ago

just one comment: should the testFixtures maybe be formatted before being pushed to the repo? The diff is rather useless because it's just one large line, if they were formatted nicely the diff would be much more targeted and understandable

Good idea! I was actually thinking last week about using a proper snapshot library, since I saw how practical they are after implementing those tests in rust you reviewed for the other project. With the insta tool I used for rust, it's easy to review the diffs both locally (i.e. accept or reject a diff via interactive CLI) and in GitHub. I think that would be ideal here. My current process is: I usually understand what the diff is about from the test errors that were happen before I re-generate the fixtures, which are better formatted. If it is not clear, I generate the fixtures either way, than manually format them and look at the formatted diff.

We used to have them formatted, but that resulted in really big diffs, while now it is always only one line per file. I think it is a price worth paying, and we should bring them back.

Opened https://github.com/informalsystems/quint/issues/1422 to track