Skip to content

Commit

Permalink
Use () instead of {} for the unit
Browse files Browse the repository at this point in the history
We had been using the empty record `{}` for the unit, but this was
causing problems with conversion to TLA+. We now use the empty tuple,
`()`, which is easily and type-correctly represented in TLA+ as `<<>>`.
  • Loading branch information
Shon Feder committed Mar 14, 2024
1 parent 393ec51 commit 2c03d46
Show file tree
Hide file tree
Showing 15 changed files with 623 additions and 563 deletions.
2 changes: 1 addition & 1 deletion quint/io-cli-tests.md
Original file line number Diff line number Diff line change
Expand Up @@ -1130,7 +1130,7 @@ rm xTest.itf.json

<!-- !test out variants in itf -->
```
[{"#meta":{"index":0},"x":{"tag":"None","value":{}}},{"#meta":{"index":1},"x":{"tag":"Some","value":{"#bigint":"1"}}},{"#meta":{"index":2},"x":{"tag":"Some","value":{"#bigint":"2"}}}]
[{"#meta":{"index":0},"x":{"tag":"None","value":{"#tup":[]}}},{"#meta":{"index":1},"x":{"tag":"Some","value":{"#bigint":"1"}}},{"#meta":{"index":2},"x":{"tag":"Some","value":{"#bigint":"2"}}}]
```

### FAIL on parsing filenames with different casing
Expand Down
3 changes: 2 additions & 1 deletion quint/src/generated/Quint.g4
Original file line number Diff line number Diff line change
Expand Up @@ -176,8 +176,9 @@ expr: // apply a built-in operator via the dot notation
| 'all' '{' expr (',' expr)* ','? '}' # actionAll
| 'any' '{' expr (',' expr)* ','? '}' # actionAny
| ( qualId | INT | BOOL | STRING) # literalOrId
// a tuple constructor, the form tup(...) is just an operator call
// a tuple constructor, the form Tup(...) is just an operator call
| '(' expr ',' expr (',' expr)* ','? ')' # tuple
| '(' ')' # unit
// short-hand syntax for pairs, mainly designed for maps
| expr '->' expr # pair
| '{' recElem (',' recElem)* ','? '}' # record
Expand Down
2 changes: 1 addition & 1 deletion quint/src/generated/Quint.interp

Large diffs are not rendered by default.

14 changes: 14 additions & 0 deletions quint/src/generated/QuintListener.ts

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading

0 comments on commit 2c03d46

Please sign in to comment.