Merge pull request #1406 from informalsystems/1401/empty-tuple-unit

Use the empty tuple for the unit

Author: bugarela

CHANGELOG.md

@@ -20,7 +20,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - The latest supported node version is now bounded at <= 20, which covers the
   latest LTS. (#1380)
 - Shadowing names are now supported, which means that the same name can be redefined 
-  in nested scopes (#1394)
+  in nested scopes. (#1394)
+- The canonical unit type is now the empty tuple, `()`, rather than the empty
+  record, `{}`. This should only affect invisible things to do with sum type
+  constructors. (#1401)
 
 ### Deprecated
 ### Removed

doc/lang.md

@@ -1300,14 +1300,14 @@ sets of records: (1) It often confuses beginners, (2) It can be expressed with
 
 ### Tuples
 
-In contrast to TLA+, Quint tuples have length of at least 2.
-If you need lists, use lists.
-
 ```scala
 // Tuple constructor: << e_1, ..., e_n >>
-// Warning: n >= 2
 (e_1, ..., e_n)
 Tup(e_1, ..., e_n)
+// The empty tuple is also the canonical unit type
+// <<>>
+()
+Tup()
 // t[1], t[2], t[3], t[4], ... , t[50]
 t._1
 t._2

quint/apalache-tests.md

@@ -224,34 +224,45 @@ An example execution:
 
 ### Test that we can compile to TLA+ of the expected form
 
-<!-- !test in can convert booleans.qnt to TLA+ -->
+<!-- !test in can convert ApalacheCompliation.qnt to TLA+ -->
 ```
-quint compile --target tlaplus  ../examples/language-features/booleans.qnt
+quint compile --target tlaplus ./testFixture/ApalacheCompilation.qnt
 ```
 
-<!-- !test out can convert booleans.qnt to TLA+ -->
+<!-- !test out can convert ApalacheCompliation.qnt to TLA+ -->
 ```
-------------------------------- MODULE booleans -------------------------------
+-------------------------- MODULE ApalacheCompilation --------------------------
 
-EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
+EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
 
-VARIABLE b
+VARIABLE x
 
-step ==
-  (b \/ TRUE)
-    /\ ~(b /\ FALSE)
-    /\ (b => b)
-    /\ (b <=> b)
-    /\ b = b
-    /\ b /= (~b)
-    /\ b' := (~b)
+A == Variant("A", "U_OF_UNIT")
 
-init == b' := TRUE
+B(__BParam_27) == Variant("B", __BParam_27)
+
+foo_bar(id__123_31) == id__123_31
+
+importedValue == 0
+
+ApalacheCompilation_ModuleToInstantiate_C == 0
+
+step == x' := (x + 1)
+
+inv == x >= 0
+
+ApalacheCompilation_ModuleToInstantiate_instantiatedValue ==
+  ApalacheCompilation_ModuleToInstantiate_C
+
+init ==
+  x'
+    := (importedValue
+      + ApalacheCompilation_ModuleToInstantiate_instantiatedValue)
 
 ================================================================================
 ```
 
-### Test that we can compile a module with imports and instances to TLA+
+### Test that we can compile a module to TLA+ that instantiates but has no declarations
 
 
 <!-- !test in can convert clockSync3.qnt to TLA+ -->
@@ -266,7 +277,7 @@ which leaves nothing, thanks to the way clockSync3 is instanced.
 ```
 ------------------------------ MODULE clockSync3 ------------------------------
 
-EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
+EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
 
 ================================================================================
 ```

quint/io-cli-tests.md

@@ -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

quint/src/apalache.ts

@@ -39,7 +39,7 @@ import type { Buffer } from 'buffer'
 import type { PackageDefinition as ProtoPackageDefinition } from '@grpc/proto-loader'
 
 const APALACHE_SERVER_URI = 'localhost:8822'
-const APALACHE_VERSION_TAG = '0.44.7'
+const APALACHE_VERSION_TAG = '0.44.9'
 // TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124
 // const APALACHE_TGZ = 'apalache.tgz'
 

quint/src/generated/Quint.g4

@@ -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