Merge pull request #1416 from informalsystems/gabriela/fix-user-facing-unit-type

Fix user facing unit type

Author: bugarela

CHANGELOG.md

@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fix a problem where sum types with no parameters were being printed with
+  either Quint's unit type `()` or Apalache's unit type `"U_OF_UNIT"` (#1416).
+
 ### Security
 
 ## v0.19.0 -- 2024-03-25

quint/src/graphics.ts

@@ -108,8 +108,8 @@ export function prettyQuintEx(ex: QuintEx): Doc {
 
           const valueExpr = ex.args[1]
           const value =
-            valueExpr.kind === 'app' && valueExpr.opcode === 'Rec' && valueExpr.args.length === 0
-              ? [] // A payload with the empty record is shown as a bare label
+            valueExpr.kind === 'app' && valueExpr.opcode === 'Tup' && valueExpr.args.length === 0
+              ? [] // A payload with the empty tuple is shown as a bare label
               : [text('('), prettyQuintEx(valueExpr), text(')')]
 
           return group([label, ...value])

quint/src/itf.ts

@@ -189,6 +189,12 @@ export function ofItf(itf: ItfTrace): QuintEx[] {
     if (typeof value === 'boolean') {
       return { id, kind: 'bool', value }
     } else if (typeof value === 'string') {
+      if (value === 'U_OF_UNIT') {
+        // Apalache converts empty tuples to its unit value, "U_OF_UNIT".
+        // We need to convert it back to Quint's unit value, the empty tuple.
+        return { id, kind: 'app', opcode: 'Tup', args: [] }
+      }
+
       return { id, kind: 'str', value }
     } else if (isBigint(value)) {
       // this is the standard way of encoding an integer in ITF.

quint/test/itf.test.ts

@@ -88,4 +88,28 @@ describe('toItf', () => {
       `round trip conversion of trace failed`
     )
   })
+
+  it('converts unit type from Apalache', () => {
+    const text = '{ a: () }'
+
+    const trace = [buildExpression(text)]
+    const vars = ['a']
+    const itfTrace = {
+      vars: vars,
+      states: [
+        {
+          '#meta': {
+            index: 0,
+          },
+          a: 'U_OF_UNIT',
+        },
+      ],
+    }
+
+    const roundTripTrace = ofItf(itfTrace)
+    assert(
+      zip(roundTripTrace, trace).every(([a, b]) => quintExAreEqual(a, b)),
+      `round trip conversion of trace failed`
+    )
+  })
 })