From 7dd9243cc394819158d0d9111b9f33066e811247 Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 2 May 2024 14:46:51 -0300 Subject: [PATCH 1/7] Fix slice conversion by removing an incorrect increment --- tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala | 2 +- .../test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala | 2 +- 2 files changed, 2 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 8b7f202624..b2ed2032ed 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 @@ -558,7 +558,7 @@ class Quint(quintOutput: QuintOutput) { case "foldl" => ternaryApp(opName, (seq, init, op) => tla.foldSeq(op, init, seq)) case "nth" => binaryApp(opName, (seq, idx) => tla.app(seq, incrTla(idx))) case "replaceAt" => ternaryApp(opName, (seq, idx, x) => tla.except(seq, incrTla(idx), x)) - case "slice" => ternaryApp(opName, (seq, from, to) => tla.subseq(seq, incrTla(from), incrTla(to))) + case "slice" => ternaryApp(opName, (seq, from, to) => tla.subseq(seq, incrTla(from), to)) case "select" => MkTla.selectSeq(opName, typeConv.convert(types(id).typ)) case "range" => binaryApp(opName, 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 44874fb55c..d28251f477 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 @@ -506,7 +506,7 @@ class TestQuintEx extends AnyFunSuite { test("can convert builtin slice operator application") { assert(convert(Q.app("slice", Q.intList, Q._0, Q._1)( - QuintSeqT(QuintIntT()))) == "Sequences!SubSeq(<<1, 2, 3>>, 0 + 1, 1 + 1)") + QuintSeqT(QuintIntT()))) == "Sequences!SubSeq(<<1, 2, 3>>, 0 + 1, 1)") } test("can convert builtin select operator application") { From 49e018660001850b5ad994c171dd703fe77c0f63 Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 2 May 2024 14:57:31 -0300 Subject: [PATCH 2/7] Include annotations to the compiled TLA module --- .../apalache/shai/v1/CmdExecutorService.scala | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala b/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala index c89abd7235..2d0ee07b39 100644 --- a/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala +++ b/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala @@ -1,5 +1,6 @@ package at.forsyte.apalache.shai.v1 +import java.io.{PrintWriter, StringWriter} import scala.util.Try import com.typesafe.scalalogging.Logger import io.grpc.Status @@ -16,7 +17,8 @@ import at.forsyte.apalache.tla.bmcmt.config.CheckerModule import at.forsyte.apalache.tla.passes.imp.ParserModule import at.forsyte.apalache.tla.passes.typecheck.TypeCheckerModule import at.forsyte.apalache.tla.lir.TlaModule -import at.forsyte.apalache.io.lir.PrettyWriter +import at.forsyte.apalache.io.annotations.PrettyWriterWithAnnotations +import at.forsyte.apalache.io.annotations.store._ /** * Provides the [[CmdExecutorService]] @@ -99,7 +101,13 @@ class CmdExecutorService(logger: Logger) extends ZioCmdExecutor.ZCmdExecutor[ZEn } private def tlaModuleToJsonString(module: TlaModule): ujson.Value = { - ujson.Str(PrettyWriter.writeAsString(module)) + val annotationStore = createAnnotationStore() + + val buf = new StringWriter() + val prettyWriter = new PrettyWriterWithAnnotations(annotationStore, new PrintWriter(buf)) + prettyWriter.write(module, List()) + + ujson.Str(buf.toString()) } // Allows us to handle invalid protobuf messages on the ZIO level, before From 8c3bba90efc8e9718acaa0c4521abe5115318f30 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 3 May 2024 10:14:05 -0300 Subject: [PATCH 3/7] Extract LET .. IN expressions from folds --- .../apalache/shai/v1/CmdExecutorService.scala | 23 +++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala b/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala index 2d0ee07b39..8c46ef5ad1 100644 --- a/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala +++ b/shai/src/main/scala/at/forsyte/apalache/shai/v1/CmdExecutorService.scala @@ -105,9 +105,28 @@ class CmdExecutorService(logger: Logger) extends ZioCmdExecutor.ZCmdExecutor[ZEn val buf = new StringWriter() val prettyWriter = new PrettyWriterWithAnnotations(annotationStore, new PrintWriter(buf)) - prettyWriter.write(module, List()) + val modules_to_extend = List("Integers", "Sequences", "FiniteSets", "TLC", "Apalache", "Variants") + prettyWriter.write(module, modules_to_extend) + val moduleString = buf.toString() - ujson.Str(buf.toString()) + val modifiedModule = extractLetFromFolds(moduleString) + ujson.Str(modifiedModule) + } + + // Apalache inlines fold operator arguments as LET .. IN expressions, but this + // is not valid for SANY. In order to produce a valid TLA+ module from Quint + // files, we transform expressions like: + // ``` + // ApaFoldSet(LET __QUINT_LAMBDAn(a, b) == c IN __QUINT_LAMBDAn, init, set) + // ``` + // + // into: + // ``` + // LET __QUINT_LAMBDAn(a, b) == c IN ApaFoldSet(__QUINT_LAMBDAn, init, set) + // ``` + private def extractLetFromFolds(module: String): String = { + val regex = """(?s)(ApaFold[\w]*\()\s*(LET\s.*?\sIN\s+)(__QUINT_LAMBDA)""" + return module.replaceAll(regex, "$2 $1$3") } // Allows us to handle invalid protobuf messages on the ZIO level, before From 788add26bbd88b3f2ac84a6138d033e904132a7b Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 3 May 2024 10:14:27 -0300 Subject: [PATCH 4/7] Sanitize bindings on exists and forall --- .../main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 9e9256fdfa..99fa3794ff 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 @@ -209,7 +209,7 @@ class PrettyWriter( val sign = PrettyWriter.bindingOps(op) val doc = group( - group(text(sign) <> space <> text(x.toString) <> space <> + group(text(sign) <> space <> text(sanatizeID(x.toString)) <> space <> text(PrettyWriter.binaryOps(TlaSetOper.in)) <> softline <> exToDoc(op.precedence, set, nameResolver) <> text(":")) <> nest(line <> exToDoc(op.precedence, pred, nameResolver)) From 6ada0892ff3082a406a3b19c89693cf3ff195b83 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 3 May 2024 10:40:39 -0300 Subject: [PATCH 5/7] Add test for sanitization of exists bindings --- .../at/forsyte/apalache/io/lir/TestPrettyWriter.scala | 10 ++++++++++ 1 file changed, 10 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 359498c4cc..d72e1c1d2e 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 @@ -379,6 +379,16 @@ class TestPrettyWriter extends AnyFunSuite with BeforeAndAfterEach { assert(expected == stringWriter.toString) } + test("an exists with a binding with invalid characters") { + val writer = new PrettyWriter(printWriter, layout40) + val expr = exists(name("a::x"), name("a::y"), name("a::z")) + writer.write(expr) + printWriter.flush() + // a multi-line vertical box always breaks from the previous line, as otherwise it is incredibly hard to indent + val expected = "\\E a_x \\in a_y: a_z" + assert(expected == stringWriter.toString) + } + test("nested \\EE and \\AA") { val writer = new PrettyWriter(printWriter, layout10) val ex1 = From 44fb6abf26a7909c86e1056a34f905bc1802e681 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 3 May 2024 16:34:03 -0300 Subject: [PATCH 6/7] Add CHANGELOG entries --- .unreleased/bug-fixes/fold-let-extraction.md | 1 + .unreleased/bug-fixes/sanitize-bindings.md | 1 + .unreleased/bug-fixes/slice-to-replaceAt.md | 1 + .unreleased/features/compilation-type-annotations.md | 1 + 4 files changed, 4 insertions(+) create mode 100644 .unreleased/bug-fixes/fold-let-extraction.md create mode 100644 .unreleased/bug-fixes/sanitize-bindings.md create mode 100644 .unreleased/bug-fixes/slice-to-replaceAt.md create mode 100644 .unreleased/features/compilation-type-annotations.md diff --git a/.unreleased/bug-fixes/fold-let-extraction.md b/.unreleased/bug-fixes/fold-let-extraction.md new file mode 100644 index 0000000000..df4e509277 --- /dev/null +++ b/.unreleased/bug-fixes/fold-let-extraction.md @@ -0,0 +1 @@ +Fixed a problem where folds produced by the Shai command `TLA` had an invalid form and could not be parsed back (#2891) diff --git a/.unreleased/bug-fixes/sanitize-bindings.md b/.unreleased/bug-fixes/sanitize-bindings.md new file mode 100644 index 0000000000..86368fa4e9 --- /dev/null +++ b/.unreleased/bug-fixes/sanitize-bindings.md @@ -0,0 +1 @@ +Fixed a problem where bindings from exists and forall operators where not properly sanitized before printing (#2891) diff --git a/.unreleased/bug-fixes/slice-to-replaceAt.md b/.unreleased/bug-fixes/slice-to-replaceAt.md new file mode 100644 index 0000000000..4a7af87d1d --- /dev/null +++ b/.unreleased/bug-fixes/slice-to-replaceAt.md @@ -0,0 +1 @@ +Fixed a problem where translation from `slice` to `replaceAt` added an incorrect increment to the last argument (#2891) diff --git a/.unreleased/features/compilation-type-annotations.md b/.unreleased/features/compilation-type-annotations.md new file mode 100644 index 0000000000..1d52d4f576 --- /dev/null +++ b/.unreleased/features/compilation-type-annotations.md @@ -0,0 +1 @@ +TLA+ modules produced by the Shai command `TLA` now include type annotations (#2891) From a4dee031f42dd894a18fd7f0b4c939a2a271a9a3 Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 6 May 2024 08:15:40 -0300 Subject: [PATCH 7/7] Fix spelling (sanatize -> sanitize) --- .../at/forsyte/apalache/io/lir/PrettyWriter.scala | 14 +++++++------- 1 file changed, 7 insertions(+), 7 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 99fa3794ff..a6e82952a0 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 @@ -89,7 +89,7 @@ class PrettyWriter( prettyWriteDoc(declToDoc(decl) <> line <> line) } - def write(expr: TlaEx): Unit = prettyWriteDoc(exToDoc((0, 0), expr, sanatizeID)) + def write(expr: TlaEx): Unit = prettyWriteDoc(exToDoc((0, 0), expr, sanitizeID)) def writeComment(commentStr: String): Unit = { prettyWriteDoc(wrapWithComment(commentStr) <> line) @@ -103,14 +103,14 @@ class PrettyWriter( def writeFooter(): Unit = prettyWriteDoc(moduleTerminalDoc) private def moduleNameDoc(name: String): Doc = { - val middle = s" MODULE ${sanatizeID(name)} " + val middle = s" MODULE ${sanitizeID(name)} " val nDashes = math.max(5, (layout.textWidth - middle.length) / 2) // int div rounds down s"${List.fill(nDashes)("-").mkString}$middle${List.fill(nDashes)("-").mkString}" <> line } private def moduleExtendsDoc(moduleNames: List[String]): Doc = if (moduleNames.isEmpty) emptyDoc - else line <> text("EXTENDS") <> space <> hsep(moduleNames.map(n => text(sanatizeID(n))), comma) <> line + else line <> text("EXTENDS") <> space <> hsep(moduleNames.map(n => text(sanitizeID(n))), comma) <> line private def moduleTerminalDoc: Doc = s"${List.fill(layout.textWidth)("=").mkString}" <> line @@ -209,7 +209,7 @@ class PrettyWriter( val sign = PrettyWriter.bindingOps(op) val doc = group( - group(text(sign) <> space <> text(sanatizeID(x.toString)) <> space <> + group(text(sign) <> space <> text(sanitizeID(x.toString)) <> space <> text(PrettyWriter.binaryOps(TlaSetOper.in)) <> softline <> exToDoc(op.precedence, set, nameResolver) <> text(":")) <> nest(line <> exToDoc(op.precedence, pred, nameResolver)) @@ -538,7 +538,7 @@ class PrettyWriter( })) } - def declToDoc(decl: TlaDecl, nameResolver: String => String = sanatizeID): Doc = { + def declToDoc(decl: TlaDecl, nameResolver: String => String = sanitizeID): Doc = { val annotations = declAnnotator(layout)(decl) decl match { @@ -680,7 +680,7 @@ class PrettyWriter( private val validIdentifierPrefix = """_*[a-zA-Z]""".r // Sanitize an identifier to ensure it can be read by TLC - private def sanatizeID(s: String): String = { + private def sanitizeID(s: String): String = { val s0 = if (validIdentifierPrefix.findPrefixOf(s).isDefined) s else "id" + s invalidIdentifierParts.replaceAllIn(s0, "_") } @@ -688,7 +688,7 @@ class PrettyWriter( private def parseableName(name: String): String = { // An operator name may contain '!' if it comes from an instance. Replace '!' with "_i_". // Additionally, the name may contain '$', which is produced during preprocessing. Replace '$' with "_si_". - sanatizeID(name.replaceAll("!", "_i_").replaceAll("\\$", "_si_")) + sanitizeID(name.replaceAll("!", "_i_").replaceAll("\\$", "_si_")) } def close(): Unit = writer.close()