Merge pull request #3041 from apalache-mc/gabriela/quint-to-tla-impro…

…vements

Quint -> TLA+ transpilation fixes

.unreleased/bug-fixes/quint-to-tla-transpilation.md

@@ -0,0 +1 @@
+Fixed a few problems on parsing Quint and pretty printing TLA, see #3041

tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala

@@ -297,14 +297,6 @@ class PrettyWriter(
             text("{") <> nest(line <> binding <> ":" <> nest(line <> filter)) <> line <> text("}")
         ) ///
 
-      // a function of multiple arguments that are packed into a tuple: don't print the angular brackets <<...>>
-      case OperEx(op @ TlaFunOper.app, funEx, OperEx(TlaFunOper.tuple, args @ _*)) =>
-        val argDocs = args.map(exToDoc(op.precedence, _, nameResolver))
-        val commaSeparatedArgs = folddoc(argDocs.toList, _ <> text(",") <@> _)
-        group(
-            exToDoc(TlaFunOper.app.precedence, funEx, nameResolver) <> brackets(commaSeparatedArgs)
-        ) ///
-
       // a function of a single argument
       case OperEx(TlaFunOper.app, funEx, argEx) =>
         group(
@@ -473,14 +465,19 @@ class PrettyWriter(
         wrapWithParen(parentPrecedence, op.precedence, group(doc))
 
       case OperEx(op @ TlaOper.apply, NameEx(name), args @ _*) =>
+        val (decls, newArgs) = extractDecls(args)
+
         // apply an operator by its name, e.g., F(x)
-        val argDocs = args.map(exToDoc(op.precedence, _, nameResolver)).toList
+        val argDocs = newArgs.map(exToDoc(op.precedence, _, nameResolver)).toList
         val commaSeparated = ssep(argDocs, "," <> softline)
+
         val doc =
           if (args.isEmpty) {
             text(parseableName(name))
-          } else {
+          } else if (decls.isEmpty) {
             group(parseableName(name) <> parens(commaSeparated))
+          } else {
+            group(ssep(decls, line) <> line <> parseableName(name) <> parens(commaSeparated))
           }
 
         wrapWithParen(parentPrecedence, op.precedence, doc)
@@ -494,16 +491,20 @@ class PrettyWriter(
         wrapWithParen(parentPrecedence, op.precedence, doc)
 
       case OperEx(op, args @ _*) =>
-        val argDocs = args.map(exToDoc(op.precedence, _, nameResolver)).toList
+        val (decls, newArgs) = extractDecls(args)
+        val argDocs = newArgs.map(exToDoc(op.precedence, _, nameResolver)).toList
         val commaSeparated = ssep(argDocs, "," <> softline)
         // The standard operators may contain a '!' that refers to the standard module. Remove it.
         val lastIndexOfBang = op.name.lastIndexOf("!")
         val unqualifiedName = if (lastIndexOfBang < 0) op.name else (op.name.substring(lastIndexOfBang + 1))
+
         val doc =
           if (args.isEmpty) {
             text(unqualifiedName)
-          } else {
+          } else if (decls.isEmpty) {
             group(unqualifiedName <> parens(commaSeparated))
+          } else {
+            group(ssep(decls, line) <> line <> unqualifiedName <> parens(commaSeparated))
           }
 
         wrapWithParen(parentPrecedence, op.precedence, doc)
@@ -527,6 +528,25 @@ class PrettyWriter(
     }
   }
 
+  /**
+   * On TLA+ files, we can't have LET..IN expressions as arguments. This is a helper function to extract the
+   * declarations so they can be printed before the operator application that would use them as arguments.
+   */
+  def extractDecls(exprs: Seq[TlaEx]): (List[Doc], Seq[TlaEx]) = {
+    val decls = exprs.collect {
+      case LetInEx(_, TlaOperDecl("LAMBDA", _, _)) => Nil
+      case LetInEx(_, decls @ _*)                  => decls
+      case _                                       => Nil
+    }
+    val newArgs = exprs.collect {
+      case expr @ LetInEx(_, TlaOperDecl("LAMBDA", _, _)) => expr
+      case LetInEx(body, _)                               => body
+      case expr                                           => expr
+    }
+
+    (decls.flatten.map(d => group("LET" <> space <> declToDoc(d) <> line <> "IN")).toList, newArgs)
+  }
+
   /**
    * Pretty-writes the given decl, while replacing names with the values in the NameReplacementMap. Then, wrap the
    * result as a comment, since the substituted names might not be valid TLA.

tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

@@ -446,7 +446,7 @@ class Quint(quintOutput: QuintOutput) {
             case ValEx(TlaStr("_")) =>
               // We have a default case, which is always paired with an eliminator that
               // can be applied to the unit value (an empty record).
-              (cs, Some(tla.appOp(defaultElim, tla.rowRec(None))))
+              (cs, Some(tla.appOp(defaultElim, tla.emptySet(IntT1))))
             case _ =>
               // All cases have match expressions
               (allCases, None)
@@ -573,7 +573,7 @@ class Quint(quintOutput: QuintOutput) {
         case "Tup" =>
           if (quintArgs.isEmpty) {
             // Translate empty tuples to values of type UNIT
-            (_) => Reader((_) => tla.const("U", ConstT1(("UNIT"))))
+            (_) => Reader((_) => tla.rowRec(None, "tag" -> tla.str("UNIT")))
           } else {
             variadicApp(args => tla.tuple(args: _*))
           }

tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintTypeConverter.scala

@@ -96,8 +96,11 @@ 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))
+    // Use the Unit type for empty tuples, since they are the unit type in Quint
+    // The unit type is a record like [ "tag" |-> "UNIT" ] so it can be compared to other constructed types.
+    // This is relevant when we produce a TLA+ file to be used with TLC.
     case QuintTupleT(Row.Nil() | Row.Cell(Seq(), _)) =>
-      ConstT1("UNIT") // Use the Unit type for empty tuples, since they are the unit type in Quint
+      RecRowT1(RowT1("tag" -> StrT1))
     case QuintTupleT(row)  => rowToTupleT1(row)
     case QuintRecordT(row) => RecRowT1(rowToRowT1(row))
     case QuintSumT(row)    => VariantT1(rowToRowT1(row))

tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala

@@ -844,6 +844,24 @@ class TestPrettyWriter extends AnyFunSuite with BeforeAndAfterEach {
     assert(expected == stringWriter.toString)
   }
 
+  test("operator application with LET-IN as argument") {
+    val writer = new PrettyWriter(printWriter, layout40)
+    val decl1 =
+      TlaOperDecl("A", List(OperParam("param1"), OperParam("param2")), plus(name("param1"), name("param2")))
+    val letInEx = letIn(appDecl(decl1, int(1), int(2)), decl1)
+    // Foo(LET A(param1, param2) == param1 + param2 IN A(1, 2))
+    val expr = OperEx(TlaOper.apply, NameEx("Foo"), letInEx)
+
+    writer.write(expr)
+    printWriter.flush()
+    // LET declaration needs to be printed before the application
+    val expected =
+      """LET A(param1, param2) == param1 + param2
+        |IN
+        |Foo((A(1, 2)))""".stripMargin
+    assert(expected == stringWriter.toString)
+  }
+
   test("a LAMBDA as LET-IN") {
     val writer = new PrettyWriter(printWriter, layout40)
     val aDecl = TlaOperDecl("LAMBDA", List(OperParam("x")), NameEx("x"))
@@ -989,7 +1007,7 @@ class TestPrettyWriter extends AnyFunSuite with BeforeAndAfterEach {
     writer.write(fDecl)
     printWriter.flush()
     val expected =
-      """f[x \in S, y \in S] == f[y, x]
+      """f[x \in S, y \in S] == f[<<y, x>>]
         |
         |""".stripMargin
     assert(expected == stringWriter.toString)

tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala

@@ -625,7 +625,7 @@ class TestQuintEx extends AnyFunSuite {
   }
 
   test("can convert builtin empty Tup operator application to uninterpreted value") {
-    assert(convert(Q.app("Tup")(QuintTupleT.ofTypes())) == "\"U_OF_UNIT\"")
+    assert(convert(Q.app("Tup")(QuintTupleT.ofTypes())) == "[\"tag\" ↦ \"UNIT\"]")
   }
 
   /// SUM TYPES
@@ -651,7 +651,7 @@ class TestQuintEx extends AnyFunSuite {
     val expected =
       """|CASE (Variants!VariantTag(Variants!Variant("F1", 42)) = "F1") → LET __QUINT_LAMBDA0(x) ≜ 1 IN __QUINT_LAMBDA0(Variants!VariantGetUnsafe("F1", Variants!Variant("F1", 42)))
          |☐ (Variants!VariantTag(Variants!Variant("F1", 42)) = "F2") → LET __QUINT_LAMBDA1(y) ≜ 2 IN __QUINT_LAMBDA1(Variants!VariantGetUnsafe("F2", Variants!Variant("F1", 42)))
-         |☐ OTHER → LET __QUINT_LAMBDA2(_) ≜ 2 IN __QUINT_LAMBDA2([])""".stripMargin
+         |☐ OTHER → LET __QUINT_LAMBDA2(_) ≜ 2 IN __QUINT_LAMBDA2({})""".stripMargin
         .replace('\n', ' ')
     assert(convert(quintMatch) == expected)
   }

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.{
-  ConstT1, FunT1, IntT1, RecRowT1, RowT1, SparseTupT1, StrT1, TlaType1, TupT1, VarT1, VariantT1,
+  FunT1, IntT1, RecRowT1, RowT1, SparseTupT1, StrT1, TlaType1, TupT1, VarT1, VariantT1,
 }
 
 /**
@@ -35,7 +35,7 @@ class TestQuintTypes extends AnyFunSuite {
 
   test("empty Quint tuple types are converted to the UNIT uninterpreted type") {
     val tuple = QuintTupleT(Row.Nil())
-    assert(translate(tuple) == ConstT1("UNIT"))
+    assert(translate(tuple) == RecRowT1(RowT1("tag" -> StrT1)))
   }
 
   test("Polymorphic Quint tuples types are converted to sparse tuples") {