Merge pull request #2869 from informalsystems/gabriela/empty-tuple-as…

…-unit Convert Quint empty tuples into uninterpreted types/values
apalache-mc · Mar 21, 2024 · b7a583e · b7a583e
2 parents 8366559 + 6124007
commit b7a583e
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 5 deletions.
diff --git a/.unreleased/bug-fixes/converting-unit-types.md b/.unreleased/bug-fixes/converting-unit-types.md
@@ -0,0 +1 @@
+Convert Quint empty tuples as uninterpreted types/values (#2869)
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
@@ -570,7 +570,14 @@ class Quint(quintOutput: QuintOutput) {
               })
 
         // Tuples
-        case "Tup" => variadicApp(args => tla.tuple(args: _*))
+        case "Tup" =>
+          if (quintArgs.isEmpty) {
+            // Translate empty tuples to values of type UNIT
+            (_) => Reader((_) => tla.const("U", ConstT1(("UNIT"))))
+          } else {
+            variadicApp(args => tla.tuple(args: _*))
+          }
+
         // product projection is just function application on TLA
         case "item"   => binaryApp(opName, tla.app)
         case "tuples" => variadicApp(tla.times)

diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintTypeConverter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintTypeConverter.scala
@@ -89,8 +89,10 @@ private class QuintTypeConverter extends LazyLogging {
     case QuintSeqT(elem)       => SeqT1(convert(elem))
     case QuintFunT(arg, res)   => FunT1(convert(arg), convert(res))
     case QuintOperT(args, res) => OperT1(args.map(convert), convert(res))
-    case QuintTupleT(row)      => rowToTupleT1(row)
-    case QuintRecordT(row)     => RecRowT1(rowToRowT1(row))
-    case QuintSumT(row)        => VariantT1(rowToRowT1(row))
+    case QuintTupleT(Row.Nil() | Row.Cell(Seq(), _)) =>
+      ConstT1("UNIT") // Use the Unit type for empty tuples, since they are the unit type in Quint
+    case QuintTupleT(row)  => rowToTupleT1(row)
+    case QuintRecordT(row) => RecRowT1(rowToRowT1(row))
+    case QuintSumT(row)    => VariantT1(rowToRowT1(row))
   }
 }
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
@@ -609,6 +609,10 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(Q.app("tuples", Q.intSet, Q.intSet, Q.intSet)(typ)) == "{1, 2, 3} × {1, 2, 3} × {1, 2, 3}")
   }
 
+  test("can convert builtin empty Tup operator application to uninterpreted value") {
+    assert(convert(Q.app("Tup")(QuintTupleT.ofTypes())) == "\"U_OF_UNIT\"")
+  }
+
   /// SUM TYPES
 
   test("can convert builtin variant operator application") {

diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintTypes.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintTypes.scala
@@ -5,7 +5,7 @@ import org.scalatest.funsuite.AnyFunSuite
 import org.scalatestplus.junit.JUnitRunner
 import at.forsyte.apalache.io.quint.QuintType._
 import at.forsyte.apalache.tla.lir.{
-  FunT1, IntT1, RecRowT1, RowT1, SparseTupT1, StrT1, TlaType1, TupT1, VarT1, VariantT1,
+  ConstT1, FunT1, IntT1, RecRowT1, RowT1, SparseTupT1, StrT1, TlaType1, TupT1, VarT1, VariantT1,
 }
 
 /**
@@ -33,6 +33,11 @@ class TestQuintTypes extends AnyFunSuite {
     assert(translate(tuple) == TupT1(IntT1, StrT1))
   }
 
+  test("empty Quint tuple types are converted to the UNIT uninterpreted type") {
+    val tuple = QuintTupleT(Row.Nil())
+    assert(translate(tuple) == ConstT1("UNIT"))
+  }
+
   test("Polymorphic Quint tuples types are converted to sparse tuples") {
     val tuple =
       // i.e.: (int, string | r)