From b6d8824788cbafee7e035ca4360cd2be61b5f9a1 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 08:09:29 -0300 Subject: [PATCH 1/8] Change unit type representation for compatibility with TLC --- .../src/main/scala/at/forsyte/apalache/io/quint/Quint.scala | 2 +- .../at/forsyte/apalache/io/quint/QuintTypeConverter.scala | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) 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 index 5c965f921f..c740eabae5 100644 --- 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 @@ -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: _*)) } 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 index c1b93f5fa7..188d654913 100644 --- 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 @@ -97,7 +97,10 @@ private class QuintTypeConverter extends LazyLogging { case QuintFunT(arg, res) => FunT1(convert(arg), convert(res)) case QuintOperT(args, res) => OperT1(args.map(convert), convert(res)) case QuintTupleT(Row.Nil() | Row.Cell(Seq(), _)) => - ConstT1("UNIT") // Use the Unit type for empty tuples, since they are the unit type in Quint + // 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. + RecRowT1(RowT1("tag" -> StrT1)) case QuintTupleT(row) => rowToTupleT1(row) case QuintRecordT(row) => RecRowT1(rowToRowT1(row)) case QuintSumT(row) => VariantT1(rowToRowT1(row)) From 6f61e23d688c09c8fbffb4f5162492b36217d925 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 08:09:58 -0300 Subject: [PATCH 2/8] Apply `{}` instead of `[]` to the default eliminator --- tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index c740eabae5..91ef87fbea 100644 --- 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 @@ -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) From 65686e1e069a8594a434bf4f4f758d3711d8dd1b Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 08:10:23 -0300 Subject: [PATCH 3/8] Remove case that resulted in incorrect printing of `map[<<1>>]` when `<<1>>` is a list --- .../scala/at/forsyte/apalache/io/lir/PrettyWriter.scala | 8 -------- 1 file changed, 8 deletions(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala index a6e82952a0..da28c3b9ad 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala +++ b/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( From 8056710fdfb3e642a8d6461a53b206002c57da18 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 08:18:33 -0300 Subject: [PATCH 4/8] Prevent LET..IN to be printed as an operator argument --- .../apalache/io/lir/PrettyWriter.scala | 30 ++++++++++++++++--- 1 file changed, 26 insertions(+), 4 deletions(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala index da28c3b9ad..1fe31381a6 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala @@ -465,14 +465,17 @@ 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 { - group(parseableName(name) <> parens(commaSeparated)) + group(ssep(decls, line) <> line <> parseableName(name) <> parens(commaSeparated)) } wrapWithParen(parentPrecedence, op.precedence, doc) @@ -486,16 +489,18 @@ 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 { - group(unqualifiedName <> parens(commaSeparated)) + group(ssep(decls, line) <> line <> unqualifiedName <> parens(commaSeparated)) } wrapWithParen(parentPrecedence, op.precedence, doc) @@ -519,6 +524,23 @@ 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(_, decls @ _*) => decls + case _ => Nil + } + val newArgs = exprs.collect { + 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. From cb5ee57c6260c5a01651fbc2560a33c132c1c423 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 09:00:44 -0300 Subject: [PATCH 5/8] Update existing tests --- .../scala/at/forsyte/apalache/io/lir/PrettyWriter.scala | 6 ++++++ .../scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala | 2 +- .../scala/at/forsyte/apalache/io/quint/TestQuintEx.scala | 4 ++-- .../scala/at/forsyte/apalache/io/quint/TestQuintTypes.scala | 2 +- 4 files changed, 10 insertions(+), 4 deletions(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala index 1fe31381a6..b929a69256 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala @@ -474,6 +474,8 @@ class PrettyWriter( val doc = if (args.isEmpty) { text(parseableName(name)) + } else if (decls.isEmpty) { + group(parseableName(name) <> parens(commaSeparated)) } else { group(ssep(decls, line) <> line <> parseableName(name) <> parens(commaSeparated)) } @@ -499,6 +501,8 @@ class PrettyWriter( val doc = if (args.isEmpty) { text(unqualifiedName) + } else if (decls.isEmpty) { + group(unqualifiedName <> parens(commaSeparated)) } else { group(ssep(decls, line) <> line <> unqualifiedName <> parens(commaSeparated)) } @@ -530,10 +534,12 @@ class PrettyWriter( */ def extractDecls(exprs: Seq[TlaEx]): (List[Doc], Seq[TlaEx]) = { val decls = exprs.collect { + case LetInEx(body, d @ TlaOperDecl("LAMBDA", _, _)) => Nil case LetInEx(_, decls @ _*) => decls case _ => Nil } val newArgs = exprs.collect { + case expr @ LetInEx(body, d @ TlaOperDecl("LAMBDA", _, _)) => expr case LetInEx(body, _) => body case expr => expr } diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala index d72e1c1d2e..6b3461f81f 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala @@ -989,7 +989,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[<>] | |""".stripMargin assert(expected == stringWriter.toString) 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 index ee84a40fb5..9245bca5e1 100644 --- 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 @@ -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) } 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 index ed52dce3f4..01a7263eea 100644 --- 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 @@ -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") { From bb746fcc9904d1fd7f810909eb56e50735d00b78 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 09:13:49 -0300 Subject: [PATCH 6/8] Add test for LET-IN extraction --- .../apalache/io/lir/TestPrettyWriter.scala | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala index 6b3461f81f..f1ad544cbc 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala +++ b/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")) From ce5e61eed8e55c4ae13e26d17e6579510c5f6af2 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 09:34:45 -0300 Subject: [PATCH 7/8] Fix formatting --- .../at/forsyte/apalache/io/lir/PrettyWriter.scala | 12 ++++++------ .../apalache/io/quint/QuintTypeConverter.scala | 6 +++--- .../forsyte/apalache/io/quint/TestQuintTypes.scala | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala index b929a69256..a75f96b6fc 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala @@ -534,14 +534,14 @@ class PrettyWriter( */ def extractDecls(exprs: Seq[TlaEx]): (List[Doc], Seq[TlaEx]) = { val decls = exprs.collect { - case LetInEx(body, d @ TlaOperDecl("LAMBDA", _, _)) => Nil - case LetInEx(_, decls @ _*) => decls - case _ => Nil + case LetInEx(_, TlaOperDecl("LAMBDA", _, _)) => Nil + case LetInEx(_, decls @ _*) => decls + case _ => Nil } val newArgs = exprs.collect { - case expr @ LetInEx(body, d @ TlaOperDecl("LAMBDA", _, _)) => expr - case LetInEx(body, _) => body - case expr => expr + 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) 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 index 188d654913..7048875725 100644 --- 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 @@ -96,10 +96,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)) + // 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(), _)) => - // 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. RecRowT1(RowT1("tag" -> StrT1)) case QuintTupleT(row) => rowToTupleT1(row) case QuintRecordT(row) => RecRowT1(rowToRowT1(row)) 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 index 01a7263eea..87bcf9b1b6 100644 --- 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.{ - ConstT1, FunT1, IntT1, RecRowT1, RowT1, SparseTupT1, StrT1, TlaType1, TupT1, VarT1, VariantT1, + FunT1, IntT1, RecRowT1, RowT1, SparseTupT1, StrT1, TlaType1, TupT1, VarT1, VariantT1, } /** From f28e16e674751a45d71c46eb73f0dc2288f8aeae Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 29 Nov 2024 09:36:59 -0300 Subject: [PATCH 8/8] Add CHANGELOG entry --- .unreleased/bug-fixes/quint-to-tla-transpilation.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/quint-to-tla-transpilation.md diff --git a/.unreleased/bug-fixes/quint-to-tla-transpilation.md b/.unreleased/bug-fixes/quint-to-tla-transpilation.md new file mode 100644 index 0000000000..217cbaabed --- /dev/null +++ b/.unreleased/bug-fixes/quint-to-tla-transpilation.md @@ -0,0 +1 @@ +Fixed a few problems on parsing Quint and pretty printing TLA, see #3041