From cdf90cfb22da29c3c7b7d2940ff56fd438f3d8e4 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 29 Apr 2021 11:07:36 +0200 Subject: [PATCH 1/4] closes #633: correct pretty printing of type annotations --- UNRELEASED.md | 1 + .../PrettyWriterWithAnnotations.scala | 63 ++++--- .../io/TestPrettyWriterWithAnnotations.scala | 91 +++++++++- .../tla/pp/TestTlcConfigImporter.scala | 5 +- .../apalache/tla/lir/io/PrettyWriter.scala | 83 +++++++--- .../apalache/tla/lir/io/TextLayout.scala | 9 + .../tla/lir/io/TlaDeclAnnotator.scala | 22 +++ .../tla/lir/io/TestPrettyWriter.scala | 156 +++++++++--------- 8 files changed, 303 insertions(+), 127 deletions(-) create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TextLayout.scala create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaDeclAnnotator.scala diff --git a/UNRELEASED.md b/UNRELEASED.md index 88773a7386..85af80ad21 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -26,6 +26,7 @@ * Parser: better parser for annotations, see #757 * Parser: fixed two bugs in the declaration sorter, see #645 and #758 * Printer: fixed the output for EXCEPT, see #746 +* Printer: fixed pretty printing of annotations, see #633 * The command `config --enable-stats=true` creates `$HOME/.tlaplus` if needed, see #762 ### Changes diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala index ec4d6f4f8b..82a35d9ba0 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala @@ -1,8 +1,8 @@ package at.forsyte.apalache.io.annotations import at.forsyte.apalache.io.annotations.store.AnnotationStore -import at.forsyte.apalache.tla.lir.TlaDecl -import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriter} +import at.forsyte.apalache.tla.lir.{TlaDecl, TlaEx, TlaModule} +import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TextLayout, TlaDeclAnnotator, TlaWriter} import java.io.PrintWriter @@ -11,23 +11,48 @@ import java.io.PrintWriter * * @author Igor Konnov */ -class PrettyWriterWithAnnotations(annotationStore: AnnotationStore, writer: PrintWriter, textWidth: Int = 80, - indent: Int = 2) - extends PrettyWriter(writer, textWidth, indent) with TlaWriter { - - // override the translation of a declaration - override def toDoc(decl: TlaDecl): Doc = { - val underlyingDoc = super.toDoc(decl) - annotationStore - .get(decl.ID) - .flatMap { annotations => - Some(annotations.foldRight(underlyingDoc) { (anno, doc) => - // A simple implementation that is using Annotation.toPrettyString. - // In the future, we should implement a full pretty printer both for annotations and types. - "(*" <> space <> anno.toPrettyString <> space <> "*)" <> - linebreak <> doc - }) +class PrettyWriterWithAnnotations(annotationStore: AnnotationStore, writer: PrintWriter, + layout: TextLayout = TextLayout()) + extends TlaWriter { + + private object annotator extends TlaDeclAnnotator { + override def apply(layout: TextLayout)(decl: TlaDecl): Option[List[String]] = { + annotationStore.get(decl.ID) match { + case None | Some(List()) => + None + + case Some(annotations) => + Some(annotations.map(_.toPrettyString)) } - .getOrElse(underlyingDoc) + } + } + + private val prettyWriter: PrettyWriter = new PrettyWriter(writer, layout, annotator) + + /** + * Write a module, including all declarations + * + * @param mod a module + */ + override def write(mod: TlaModule): Unit = { + prettyWriter.write(mod) + } + + /** + * Write a declaration, including all expressions + * + * @param decl a declaration + */ + override def write(decl: TlaDecl): Unit = { + prettyWriter.write(decl) + } + + /** + * Write a TLA+ expression. + * + * @param expr an expression + */ + override def write(expr: TlaEx): Unit = { + prettyWriter.write(expr) } } diff --git a/tla-import/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithAnnotations.scala b/tla-import/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithAnnotations.scala index 0eabd70e16..96acf4c435 100644 --- a/tla-import/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithAnnotations.scala +++ b/tla-import/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithAnnotations.scala @@ -5,6 +5,7 @@ import at.forsyte.apalache.io.annotations.store.createAnnotationStore import at.forsyte.apalache.tla.lir._ import UntypedPredefs._ import at.forsyte.apalache.tla.lir.convenience.tla +import at.forsyte.apalache.tla.lir.io.TextLayout import org.junit.runner.RunWith import org.scalatest.junit.JUnitRunner import org.scalatest.{BeforeAndAfterEach, FunSuite} @@ -15,6 +16,7 @@ import java.io.{PrintWriter, StringWriter} class TestPrettyWriterWithAnnotations extends FunSuite with BeforeAndAfterEach { private var stringWriter: StringWriter = _ private var printWriter: PrintWriter = _ + private val layout80 = TextLayout().copy(textWidth = 80) override protected def beforeEach(): Unit = { stringWriter = new StringWriter() @@ -26,12 +28,29 @@ class TestPrettyWriterWithAnnotations extends FunSuite with BeforeAndAfterEach { val store = createAnnotationStore() store += decl.ID -> List(Annotation("type", AnnotationStr("Int -> Bool"))) - val writer = new PrettyWriterWithAnnotations(store, printWriter, 80) + val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80) writer.write(decl) printWriter.flush() val expected = - """(* @type: Int -> Bool; *) - |VARIABLE myFun + """VARIABLE + | (* + | @type: Int -> Bool; + | *) + | myFun + | + |""".stripMargin + assert(expected == stringWriter.toString) + } + + test("variable declaration without annotation") { + val decl = TlaVarDecl("myFun") + val store = createAnnotationStore() + + val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80) + writer.write(decl) + printWriter.flush() + val expected = + """VARIABLE myFun | |""".stripMargin assert(expected == stringWriter.toString) @@ -42,13 +61,16 @@ class TestPrettyWriterWithAnnotations extends FunSuite with BeforeAndAfterEach { val store = createAnnotationStore() store += decl.ID -> List(Annotation("type", AnnotationStr("Int")), Annotation("sweet", AnnotationBool(true))) - val writer = new PrettyWriterWithAnnotations(store, printWriter, 80) + val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80) writer.write(decl) printWriter.flush() val expected = - """(* @type: Int; *) - |(* @sweet(true) *) - |CONSTANT N + """CONSTANT + | (* + | @type: Int; + | @sweet(true) + | *) + | N | |""".stripMargin assert(expected == stringWriter.toString) @@ -59,14 +81,65 @@ class TestPrettyWriterWithAnnotations extends FunSuite with BeforeAndAfterEach { val store = createAnnotationStore() store += decl.ID -> List(Annotation("type", AnnotationStr("(Int, Str) -> Bool"))) - val writer = new PrettyWriterWithAnnotations(store, printWriter, 80) + val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80) writer.write(decl) printWriter.flush() val expected = - """(* @type: (Int, Str) -> Bool; *) + """(* + | @type: (Int, Str) -> Bool; + |*) |MyOper(x, y) == TRUE | |""".stripMargin assert(expected == stringWriter.toString) } + + test("recursive operator declaration") { + val decl = TlaOperDecl("RecOper", List(OperParam("x"), OperParam("y")), tla.bool(true)) + decl.isRecursive = true + val store = createAnnotationStore() + store += decl.ID -> List(Annotation("type", AnnotationStr("(Int, Str) -> Bool"))) + + val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80) + writer.write(decl) + printWriter.flush() + val expected = + """RECURSIVE RecOper(_, _) + |(* + | @type: (Int, Str) -> Bool; + |*) + |RecOper(x, y) == TRUE + | + |""".stripMargin + assert(expected == stringWriter.toString) + } + + test("operator declaration without annotation") { + val decl = TlaOperDecl("MyOper", List(OperParam("x"), OperParam("y")), tla.bool(true)) + val store = createAnnotationStore() + + val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80) + writer.write(decl) + printWriter.flush() + val expected = + """MyOper(x, y) == TRUE + | + |""".stripMargin + assert(expected == stringWriter.toString) + } + + test("operator declaration with an empty list") { + val decl = TlaOperDecl("MyOper", List(OperParam("x"), OperParam("y")), tla.bool(true)) + val store = createAnnotationStore() + store += decl.ID -> List() + + val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80) + writer.write(decl) + printWriter.flush() + val expected = + """MyOper(x, y) == TRUE + | + |""".stripMargin + assert(expected == stringWriter.toString) + } } diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestTlcConfigImporter.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestTlcConfigImporter.scala index 63d9bcdd2a..a8ce32b95d 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestTlcConfigImporter.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestTlcConfigImporter.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.io.tlc.TlcConfigParserApalache import at.forsyte.apalache.tla.imp.SanyImporter import at.forsyte.apalache.tla.imp.src.SourceStore import at.forsyte.apalache.tla.lir.Untyped -import at.forsyte.apalache.tla.lir.io.PrettyWriter +import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TextLayout} import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.typecheck.{MultiTypeCheckerListener, TypeCheckerTool} import org.junit.runner.RunWith @@ -21,6 +21,7 @@ class TestTlcConfigImporter extends FunSuite with BeforeAndAfterEach { private var annotationStore: AnnotationStore = _ private var sanyImporter: SanyImporter = _ private var typeChecker: TypeCheckerTool = _ + private val layout80 = TextLayout().copy(textWidth = 80) override def beforeEach() { sourceStore = new SourceStore() @@ -44,7 +45,7 @@ class TestTlcConfigImporter extends FunSuite with BeforeAndAfterEach { val mod2 = new TlcConfigImporter(config, new IdleTracker())(typedModule) val stringWriter = new StringWriter() val printWriter = new PrintWriter(stringWriter) - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(mod2) printWriter.flush() assert(stringWriter.toString == expected) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala index c2b7ae93ce..b741e8f44c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala @@ -25,8 +25,10 @@ import scala.collection.immutable.HashMap * * @author Igor Konnov */ -class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) extends PrettyPrinter with TlaWriter { - override val defaultIndent: Int = indent +class PrettyWriter(writer: PrintWriter, layout: TextLayout = new TextLayout, + declAnnotator: TlaDeclAnnotator = new TlaDeclAnnotator) + extends PrettyPrinter with TlaWriter { + override val defaultIndent: Int = layout.indent val REC_FUN_UNDEFINED = "recFunNameUndefined" // when printing a recursive function, this variable contains its name @@ -34,7 +36,7 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex // the stack of lambda declarations private var lambdaStack: List[TlaOperDecl] = Nil - private def prettyWriteDoc(doc: Doc): Unit = writer.write(pretty(doc, textWidth).layout) + private def prettyWriteDoc(doc: Doc): Unit = writer.write(pretty(doc, layout.textWidth).layout) def write(mod: TlaModule): Unit = prettyWriteDoc(toDoc(mod)) @@ -43,7 +45,9 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex def write(expr: TlaEx): Unit = prettyWriteDoc(toDoc((0, 0), expr)) - def writeComment(commentStr: String): Unit = prettyWriteDoc(toComment(commentStr)) + def writeComment(commentStr: String): Unit = { + prettyWriteDoc(wrapWithComment(commentStr) <> line) + } def writeHeader(moduleName: String, extensionModuleNames: List[TlaModule] = List.empty): Unit = prettyWriteDoc( @@ -52,11 +56,9 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex def writeFooter(): Unit = prettyWriteDoc(moduleTerminalDoc) - private def toComment(commentStr: String): Doc = text(s"(* $commentStr *)") <> line - private def moduleNameDoc(name: String): Doc = { val middle = s" MODULE $name " - val nDashes = math.max(5, (textWidth - middle.length) / 2) // int div rounds down + 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 } @@ -65,7 +67,7 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex else line <> text(s"EXTENDS ${moduleNames.map(_.name).mkString(", ")}") <> line private def moduleTerminalDoc: Doc = - s"${List.fill(textWidth)("=").mkString}" <> line + s"${List.fill(layout.textWidth)("=").mkString}" <> line def toDoc(mod: TlaModule, extensionModuleNames: List[TlaModule] = List.empty): Doc = { moduleNameDoc(mod.name) <> @@ -122,13 +124,13 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex // a set enumeration, e.g., { 1, 2, 3 } val argDocs = args.map(toDoc(op.precedence, _)) val commaSeparated = folddoc(argDocs.toList, _ <> text(",") <@> _) - group(braces(group(softline <> nest(commaSeparated, indent)) <> softline)) + group(braces(group(softline <> nest(commaSeparated, layout.indent)) <> softline)) case OperEx(op @ TlaFunOper.tuple, args @ _*) => // a tuple, e.g., <<1, 2, 3>> val argDocs = args.map(toDoc(op.precedence, _)) val commaSeparated = ssep(argDocs.toList, text(",") <> softline) - group(text("<<") <> nest(linebreak <> commaSeparated, indent) <> linebreak <> ">>") + group(text("<<") <> nest(linebreak <> commaSeparated, layout.indent) <> linebreak <> ">>") case OperEx(op, args @ _*) if op == TlaBoolOper.and || op == TlaBoolOper.or => // we are not using indented /\ and \/, as they are hard to get automatically @@ -454,15 +456,31 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex } def toDoc(decl: TlaDecl): Doc = { + val annotations = declAnnotator(layout)(decl) + decl match { case TlaConstDecl(name) => - group("CONSTANT" <> space <> name) + if (annotations.isEmpty) { + group("CONSTANT" <> space <> name) + } else { + "CONSTANT" <> nest(line <> wrapWithComment(annotations.get) <> line <> name) + } case TlaVarDecl(name) => - group("VARIABLE" <> space <> name) + if (annotations.isEmpty) { + group("VARIABLE" <> space <> name) + } else { + "VARIABLE" <> nest(line <> wrapWithComment(annotations.get) <> line <> name) + } case TlaAssumeDecl(body) => - group("ASSUME" <> parens(toDoc((0, 0), body))) + val doc = group("ASSUME" <> parens(toDoc((0, 0), body))) + if (annotations.isEmpty) { + doc + } else { + // there is no use case for annotations of assume, but we nevertheless implement it + wrapWithComment(annotations.get) <> line <> doc + } // a declaration of a recursive function case TlaOperDecl(name, List(), OperEx(TlaFunOper.recFunDef, body, keysAndValues @ _*)) => @@ -481,24 +499,37 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex // [x \in S] val binding = brackets(binders) // f[x \in S] == e - val doc = group(name <> binding <> space <> "==" <> space <> toDoc((0, 0), body)) + val doc = name <> binding <> space <> "==" <> space <> toDoc((0, 0), body) recFunName = REC_FUN_UNDEFINED - doc + if (annotations.isEmpty) { + group(doc) + } else { + wrapWithComment(annotations.get) <> line <> group(doc) + } // an operator declaration (may be recursive) case tod @ TlaOperDecl(name, params, body) => val recPreambule = - if (!tod.isRecursive) - text("") - else - "RECURSIVE" <> space <> toDoc(OperParam(name, params.length)) <> line + if (!tod.isRecursive) { + None + } else { + Some("RECURSIVE" <> space <> toDoc(OperParam(name, params.length))) + } val paramsDoc = - if (params.isEmpty) + if (params.isEmpty) { text("") - else parens(ssep(params map toDoc, "," <> softline)) + } else { + parens(ssep(params map toDoc, "," <> softline)) + } - recPreambule <> group(name <> paramsDoc <> space <> "==" <> nest(line <> toDoc((0, 0), body))) + val declDoc = group(name <> paramsDoc <> space <> "==" <> nest(line <> toDoc((0, 0), body))) + if (annotations.isEmpty) { + recPreambule.map(_ <> line <> declDoc).getOrElse(declDoc) + } else { + val withComment = wrapWithComment(annotations.get) <> line <> declDoc + recPreambule.map(_ <> line <> withComment).getOrElse(withComment) + } } } @@ -522,6 +553,14 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex } } + private def wrapWithComment(comment: Doc): Doc = { + text("(*") <> softbreak <> comment <> softbreak <> text("*)") + } + + private def wrapWithComment(strings: List[String]): Doc = { + text("(*") <> nest(lsep(strings.map(text), ""), defaultIndent) <> line <> text("*)") + } + private def strNoQuotes(ex: TlaEx): String = { ex match { case ValEx(TlaStr(s)) => s diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TextLayout.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TextLayout.scala new file mode 100644 index 0000000000..b803b5dcd2 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TextLayout.scala @@ -0,0 +1,9 @@ +package at.forsyte.apalache.tla.lir.io + +/** + * Settings for text output. + * + * @param textWidth the length of a single line. + * @param indent the number of characters in a single level of indentation. + */ +case class TextLayout(val textWidth: Int = 80, val indent: Int = 2) {} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaDeclAnnotator.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaDeclAnnotator.scala new file mode 100644 index 0000000000..172ce157a3 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaDeclAnnotator.scala @@ -0,0 +1,22 @@ +package at.forsyte.apalache.tla.lir.io + +import at.forsyte.apalache.tla.lir.TlaDecl + +/** + * An interface for additional decorators of declarations that can be used in PrettyWriter. + * The default behavior is to do nothing. + * + * @author Igor Konnov + */ +class TlaDeclAnnotator { + + /** + * Given the text layout settings and a declaration, produce a string representation of an annotation, + * which respects the layout settings. + * + * @param layout layout settings + * @param decl declaration to annotate + * @return a string annotation + */ + def apply(layout: TextLayout)(decl: TlaDecl): Option[List[String]] = None +} diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala index c06e28bb33..14494a44b2 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala @@ -16,6 +16,12 @@ import at.forsyte.apalache.tla.lir.UntypedPredefs._ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { private var stringWriter = new StringWriter() private var printWriter = new PrintWriter(stringWriter) + private val layout80 = TextLayout().copy(textWidth = 80) + private val layout40 = TextLayout().copy(textWidth = 40) + private val layout30 = TextLayout().copy(textWidth = 30) + private val layout20 = TextLayout().copy(textWidth = 20) + private val layout15 = TextLayout().copy(textWidth = 15) + private val layout10 = TextLayout().copy(textWidth = 10) override protected def beforeEach(): Unit = { stringWriter = new StringWriter() @@ -23,140 +29,140 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("name") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(name("awesome")) printWriter.flush() assert("awesome" == stringWriter.toString) } test("apply A") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(OperEx(TlaOper.apply, name("A"))) printWriter.flush() assert("A" == stringWriter.toString) } test("apply A to 1") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(OperEx(TlaOper.apply, name("A"), int(1))) printWriter.flush() assert("A(1)" == stringWriter.toString) } test("apply A to 1 and 2") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(OperEx(TlaOper.apply, name("A"), int(1), int(2))) printWriter.flush() assert("A(1, 2)" == stringWriter.toString) } test("assignment: x' := 2") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(assignPrime(name("x"), int(2))) printWriter.flush() assert("x' := 2" == stringWriter.toString) } test("ENABLED and prime") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(enabled(prime(name("x")))) printWriter.flush() assert("ENABLED x'" == stringWriter.toString) } test("UNCHANGED") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(unchanged(name("x"))) printWriter.flush() assert("UNCHANGED x" == stringWriter.toString) } test("[A]_vars") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(stutt(name("A"), name("vars"))) printWriter.flush() assert("[A]_vars" == stringWriter.toString) } test("_vars") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(nostutt(name("A"), name("vars"))) printWriter.flush() assert("_vars" == stringWriter.toString) } test("A \\cdot B") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(comp(name("A"), name("B"))) printWriter.flush() assert("A \\cdot B" == stringWriter.toString) } test("WF_vars(A)") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(WF(name("vars"), name("A"))) printWriter.flush() assert("WF_vars(A)" == stringWriter.toString) } test("SF_vars(A)") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(SF(name("vars"), name("A"))) printWriter.flush() assert("SF_vars(A)" == stringWriter.toString) } test("[]A") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(box(name("A"))) printWriter.flush() assert("[]A" == stringWriter.toString) } test("<>A") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(diamond(name("A"))) printWriter.flush() assert("<>A" == stringWriter.toString) } test("A ~> B") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(leadsTo(name("A"), name("B"))) printWriter.flush() assert("A ~> B" == stringWriter.toString) } test("A -+-> B") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(guarantees(name("A"), name("B"))) printWriter.flush() assert("A -+-> B" == stringWriter.toString) } test("empty set") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(enumSet()) printWriter.flush() assert("{}" == stringWriter.toString) } test("singleton set") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(enumSet(int(42))) printWriter.flush() assert("{42}" == stringWriter.toString) } test("one-line set") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(enumSet(int(1), int(2), int(3))) printWriter.flush() assert("{ 1, 2, 3 }" == stringWriter.toString) } test("multi-line set") { - val writer = new PrettyWriter(printWriter, 20) + val writer = new PrettyWriter(printWriter, layout20) writer.write(enumSet(1.to(10).map(int): _*)) printWriter.flush() val expected = @@ -189,14 +195,14 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("one-line tuple") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(tuple(int(1), int(2), int(3))) printWriter.flush() assert("<<1, 2, 3>>" == stringWriter.toString) } test("multi-line tuple") { - val writer = new PrettyWriter(printWriter, 20) + val writer = new PrettyWriter(printWriter, layout20) writer.write(tuple(1.to(10).map(int): _*)) printWriter.flush() val expected = @@ -208,14 +214,14 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("one-line Cartesian product") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(times(name("X"), name("Y"), name("Z"))) printWriter.flush() assert("X \\X Y \\X Z" == stringWriter.toString) } test("multi-line Cartesian product") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) writer.write(times(name("verylongname1"), name("verylongname2"), name("verylongname3"))) printWriter.flush() val expected = @@ -226,7 +232,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("one-line conjunction") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = and(1.to(3) map (_ => name("verylongname")): _*) writer.write(expr) printWriter.flush() @@ -236,7 +242,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("multi-line conjunction") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = impl(bool(true), and(1.to(5) map (_ => name("verylongname")): _*)) writer.write(expr) printWriter.flush() @@ -252,7 +258,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("nested multiline conjunction/disjunction") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val orEx = or(1.to(3) map (_ => name("verylongname")): _*) val andEx = and(1.to(3) map (_ => orEx): _*) writer.write(andEx) @@ -265,7 +271,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("nested multiline conjunction under negation") { - val writer = new PrettyWriter(printWriter, 20) + val writer = new PrettyWriter(printWriter, layout20) val andEx = and(1.to(3) map (_ => name("verylongname")): _*) writer.write(not(andEx)) printWriter.flush() @@ -277,42 +283,42 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("~x") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(not(name("x"))) printWriter.flush() assert("~x" == stringWriter.toString) } test("~(1 = 2)") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(not(eql(int(1), int(2)))) printWriter.flush() assert("~(1 = 2)" == stringWriter.toString) } test("[S -> T]") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(funSet(name("S"), name("T"))) printWriter.flush() assert("[S -> T]" == stringWriter.toString) } test("L2 :: 1") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(label(int(1), "L2")) printWriter.flush() assert("L2 :: 1" == stringWriter.toString) } test("L2(a, b) :: 1") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) writer.write(label(int(1), "L2", "a", "b")) printWriter.flush() assert("L2(a, b) :: 1" == stringWriter.toString) } test("one-line exists") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = exists(name("x"), name("y"), name("z")) writer.write(expr) printWriter.flush() @@ -322,7 +328,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("multi-line exists") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = exists(name("verylongname1"), name("verylongname2"), name("verylongname3")) writer.write(expr) @@ -335,7 +341,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("nested quantifiers") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val ex1 = exists(name("verylongname1"), name("verylongname2"), name("verylongname3")) val ex2 = @@ -351,7 +357,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("nested \\EE and \\AA") { - val writer = new PrettyWriter(printWriter, 10) + val writer = new PrettyWriter(printWriter, layout10) val ex1 = EE(name("verylongname1"), name("verylongname2")) val ex2 = @@ -367,7 +373,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line record") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = enumFun( str("x1"), name("x2"), @@ -384,7 +390,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line record") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = enumFun( str("verylong1"), name("verylong2"), @@ -403,7 +409,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a narrow multi-line record") { - val writer = new PrettyWriter(printWriter, 20) + val writer = new PrettyWriter(printWriter, layout20) val expr = enumFun( str("verylong1"), name("verylong2"), @@ -425,7 +431,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("TLC @@") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = atatInterleaved(str("a"), int(1), str("b"), int(2), str("c"), int(3)) writer.write(expr) printWriter.flush() @@ -434,7 +440,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line set of records") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = recSet( str("x1"), name("x2"), @@ -451,7 +457,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line set of records") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = recSet( str("verylong1"), name("verylong2"), @@ -470,7 +476,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line function") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = funDef(plus(name("x"), name("y")), name("x"), name("S"), name("y"), name("T")) writer.write(expr) printWriter.flush() @@ -480,7 +486,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line function") { - val writer = new PrettyWriter(printWriter, 30) + val writer = new PrettyWriter(printWriter, layout30) val expr = funDef(plus(name("verylong1"), name("verylong2")), name("verylong1"), name("verylong3"), name("verylong2"), name("verylong4")) writer.write(expr) @@ -495,7 +501,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line map") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = map(plus(name("x"), name("y")), name("x"), name("S"), name("y"), name("T")) writer.write(expr) printWriter.flush() @@ -505,7 +511,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line map") { - val writer = new PrettyWriter(printWriter, 30) + val writer = new PrettyWriter(printWriter, layout30) val expr = map(plus(name("verylong1"), name("verylong2")), name("verylong1"), name("verylong3"), name("verylong2"), name("verylong4")) writer.write(expr) @@ -520,7 +526,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line filter") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = filter(name("x"), name("S"), name("P")) writer.write(expr) printWriter.flush() @@ -530,7 +536,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("precedence in filter") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = filter(name("x"), name("S"), lt(name("x"), int(5))) writer.write(expr) printWriter.flush() @@ -540,7 +546,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line filter") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = filter(name("verylongname1"), name("verylongname2"), name("verylongname3")) writer.write(expr) @@ -554,7 +560,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line function application") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = appFun(name("f"), name("e")) writer.write(expr) printWriter.flush() @@ -563,7 +569,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line function application") { - val writer = new PrettyWriter(printWriter, 20) + val writer = new PrettyWriter(printWriter, layout20) val expr = appFun(name("verylongname1"), name("verylongname2")) writer.write(expr) printWriter.flush() @@ -575,7 +581,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line IF-THEN-ELSE") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = ite(name("a"), name("b"), name("c")) writer.write(expr) printWriter.flush() @@ -584,7 +590,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line IF-THEN-ELSE") { - val writer = new PrettyWriter(printWriter, 20) + val writer = new PrettyWriter(printWriter, layout20) val expr = ite(name("verylongname1"), name("verylongname2"), name("verylongname3")) writer.write(expr) printWriter.flush() @@ -596,7 +602,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line EXCEPT") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) // recall that EXCEPT indices are always wrapped in a tuple val expr = except(name("f"), tuple(name("k")), name("v")) writer.write(expr) @@ -606,7 +612,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a two-argument EXCEPT") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) // recall that EXCEPT indices are always wrapped in a tuple val expr = except(name("f"), tuple(name("i"), name("k")), name("v")) writer.write(expr) @@ -616,7 +622,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line EXCEPT") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = except( name("verylongname1"), tuple(name("verylongname2")), @@ -634,7 +640,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a monster EXCEPT") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = except( name("verylongname1"), tuple(name("verylongname2")), @@ -655,7 +661,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("FiniteSets!Cardinality") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = card(name("S")) writer.write(expr) printWriter.flush() @@ -664,7 +670,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("<> \\o <>") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = concat(tuple(name("a")), tuple(name("b"))) writer.write(expr) printWriter.flush() @@ -673,7 +679,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("Sequences!Append(<>, b)") { - val writer = new PrettyWriter(printWriter, 80) + val writer = new PrettyWriter(printWriter, layout80) val expr = append(tuple(name("a")), name("b")) writer.write(expr) printWriter.flush() @@ -682,7 +688,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line CASE") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = caseSplit(name("guard1"), name("action1"), name("guard2"), name("action2")) writer.write(expr) printWriter.flush() @@ -693,7 +699,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a concise multi-line CASE") { - val writer = new PrettyWriter(printWriter, 15) + val writer = new PrettyWriter(printWriter, layout15) val expr = caseSplit(name("guard1"), name("action1"), name("guard2"), name("action2")) writer.write(expr) printWriter.flush() @@ -706,7 +712,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line CASE with OTHER") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val expr = caseOther(name("otherAction"), name("guard1"), name("action1"), name("guard2"), name("action2")) writer.write(expr) printWriter.flush() @@ -718,7 +724,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line LET-IN") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val aDecl = TlaOperDecl("A", List(), int(1)) val expr = letIn(appDecl(aDecl), aDecl) writer.write(expr) @@ -729,7 +735,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a multi-line LET-IN") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val decl = TlaOperDecl("AVeryLongName", List(OperParam("param1"), OperParam("param2")), plus(name("param1"), name("param2"))) val expr = letIn(appDecl(decl, int(1), int(2)), decl) @@ -744,7 +750,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("multiple definitions in LET-IN") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val decl1 = TlaOperDecl("AVeryLongName", List(OperParam("param1"), OperParam("param2")), plus(name("param1"), name("param2"))) val decl2 = @@ -765,7 +771,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a LAMBDA as LET-IN") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val aDecl = TlaOperDecl("LAMBDA", List(OperParam("x")), NameEx("x")) val expr = letIn(NameEx("LAMBDA"), aDecl) writer.write(expr) @@ -777,7 +783,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { test("nested lambdas") { // A(LAMBDA x: A(LAMBDA y: y, x), z) - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) // A(LAMBDA y: y + 1, x) val innerDecl = TlaOperDecl("LAMBDA", List(OperParam("y")), tla.name("y")) @@ -796,7 +802,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line operator declaration") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val body = OperEx(TlaArithOper.plus, ValEx(TlaInt(1)), NameEx("x")) @@ -815,7 +821,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a recursive operator declaration") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val body = OperEx(TlaArithOper.plus, ValEx(TlaInt(1)), OperEx(TlaOper.apply, NameEx("A"), NameEx("x"))) @@ -837,7 +843,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a recursive operator declaration in LET-IN") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val body = OperEx(TlaArithOper.plus, ValEx(TlaInt(1)), OperEx(TlaOper.apply, NameEx("A"), NameEx("x"))) @@ -861,7 +867,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line recursive function in LET-IN") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val recFun = OperEx(TlaFunOper.recFunDef, OperEx(TlaArithOper.plus, ValEx(TlaInt(1)), @@ -880,7 +886,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("a one-line recursive function declaration") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val recFun = OperEx(TlaFunOper.recFunDef, OperEx(TlaArithOper.plus, ValEx(TlaInt(1)), @@ -900,7 +906,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { } test("declaration of a recursive function of two arguments") { - val writer = new PrettyWriter(printWriter, 40) + val writer = new PrettyWriter(printWriter, layout40) val body = tla.appFun(tla.recFunRef(), tla.tuple(tla.name("y"), tla.name("x"))) val recFun = tla.recFunDef(body, tla.name("x"), tla.name("S"), tla.name("y"), tla.name("S")) From a885e2c69c817191fc9229a7ea094ffacd113c47 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 29 Apr 2021 11:29:31 +0200 Subject: [PATCH 2/4] closes #136: pretty writer extends the standard modules --- .../tla/assignments/passes/PrimingPassImpl.scala | 4 ++-- .../assignments/passes/TransitionPassImpl.scala | 5 +++-- .../tla/bmcmt/passes/AnalysisPassImpl.scala | 4 ++-- .../tla/bmcmt/passes/VCGenPassImpl.scala | 4 ++-- .../PrettyWriterWithAnnotations.scala | 4 ++-- .../tla/imp/passes/SanyParserPassImpl.scala | 16 +++++++--------- .../tla/pp/passes/ConfigurationPassImpl.scala | 8 +++----- .../tla/pp/passes/DesugarerPassImpl.scala | 4 ++-- .../apalache/tla/pp/passes/InlinePassImpl.scala | 4 ++-- .../apalache/tla/pp/passes/OptPassImpl.scala | 4 ++-- .../apalache/tla/pp/passes/PreproPassImpl.scala | 10 ++++------ .../apalache/tla/pp/passes/UnrollPassImpl.scala | 4 ++-- .../tla/lir/io/CounterexampleWriter.scala | 2 +- .../apalache/tla/lir/io/PrettyWriter.scala | 11 ++++++----- .../forsyte/apalache/tla/lir/io/TlaWriter.scala | 16 ++++++++++++---- .../apalache/tla/lir/io/TlaWriterFactory.scala | 5 +++-- 16 files changed, 55 insertions(+), 50 deletions(-) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala index 4c72f45803..585174ddc6 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala @@ -4,7 +4,7 @@ import java.io.File import java.nio.file.Path import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriterFactory} +import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.storage.BodyMapFactory import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TransformationTracker} import at.forsyte.apalache.tla.lir.transformations.standard._ @@ -84,7 +84,7 @@ class PrimingPassImpl @Inject() (options: PassOptions, tracker: TransformationTr val newModule = new TlaModule(tlaModule.get.name, newDeclarations) val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(newModule, new File(outdir.toFile, "out-priming.tla")) + writerFactory.writeModuleToFile(newModule, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-priming.tla")) setModule(newModule) true diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala index e9e8b3433a..a471f0cc49 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.assignments._ import at.forsyte.apalache.tla.imp.findBodyOf import at.forsyte.apalache.tla.imp.src.SourceStore import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.lir.io.TlaWriterFactory +import at.forsyte.apalache.tla.lir.io.{TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator} import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming @@ -78,7 +78,8 @@ class TransitionPassImpl @Inject() (options: PassOptions, sourceStore: SourceSto // print the resulting module val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(outModule, new File(outdir.toFile, "out-transition.tla")) + writerFactory.writeModuleToFile(outModule, TlaWriter.STANDARD_MODULES, + new File(outdir.toFile, "out-transition.tla")) setModule(outModule) true diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala index 11d7574a27..1afaac56e0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala @@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.passes import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.bmcmt.CheckerException import at.forsyte.apalache.tla.bmcmt.analyses._ -import at.forsyte.apalache.tla.lir.io.TlaWriterFactory +import at.forsyte.apalache.tla.lir.io.{TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.transformations.standard.ModuleByExTransformer import at.forsyte.apalache.tla.lir.{NullEx, TlaAssumeDecl, TlaEx, TlaOperDecl} @@ -77,7 +77,7 @@ class AnalysisPassImpl @Inject() (val options: PassOptions, hintsStoreImpl: Form nextPass.setModule(marked) val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(marked, new File(outdir.toFile, "out-analysis.tla")) + writerFactory.writeModuleToFile(marked, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-analysis.tla")) logger.info(" > Introduced expression grades") logger.info(" > Introduced %d formula hints".format(hintsStoreImpl.store.size)) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala index 586f75ca3c..18460ddc46 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala @@ -5,7 +5,7 @@ import java.nio.file.Path import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.bmcmt.{CheckerException, VCGenerator} import at.forsyte.apalache.tla.lir.NullEx -import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriterFactory} +import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.UntypedPredefs._ import com.google.inject.Inject @@ -51,7 +51,7 @@ class VCGenPassImpl @Inject() (options: PassOptions, tracker: TransformationTrac } val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(newModule, new File(outdir.toFile, "out-vcgen.tla")) + writerFactory.writeModuleToFile(newModule, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-vcgen.tla")) nextPass.setModule(newModule) true diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala index 82a35d9ba0..2fb4162c8a 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala @@ -34,8 +34,8 @@ class PrettyWriterWithAnnotations(annotationStore: AnnotationStore, writer: Prin * * @param mod a module */ - override def write(mod: TlaModule): Unit = { - prettyWriter.write(mod) + override def write(mod: TlaModule, extendedModuleNames: List[String]): Unit = { + prettyWriter.write(mod, extendedModuleNames) } /** diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala index 23dbd46ed6..5fa88f0605 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala @@ -1,14 +1,14 @@ package at.forsyte.apalache.tla.imp.passes import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} -import at.forsyte.apalache.tla.imp.{SanyImporter, SanyImporterException} import at.forsyte.apalache.io.annotations.store._ import at.forsyte.apalache.tla.imp.src.SourceStore -import at.forsyte.apalache.tla.lir.{CyclicDependencyError, TlaModule} -import at.forsyte.apalache.tla.lir.io.{JsonReader, JsonWriter, PrettyWriter, TlaWriterFactory} +import at.forsyte.apalache.tla.imp.{SanyImporter, SanyImporterException} +import at.forsyte.apalache.tla.lir.UntypedPredefs._ +import at.forsyte.apalache.tla.lir.io.{JsonReader, JsonWriter, TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator} import at.forsyte.apalache.tla.lir.transformations.standard.DeclarationSorter -import at.forsyte.apalache.tla.lir.UntypedPredefs._ +import at.forsyte.apalache.tla.lir.{CyclicDependencyError, TlaModule} import com.google.inject.Inject import com.google.inject.name.Named import com.typesafe.scalalogging.LazyLogging @@ -73,10 +73,8 @@ class SanyParserPassImpl @Inject() ( } // save the output val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile( - rootModule.get, - new File(outdir.toFile, "out-parser.tla") - ) + writerFactory.writeModuleToFile(rootModule.get, TlaWriter.STANDARD_MODULES, + new File(outdir.toFile, "out-parser.tla")) JsonWriter.write( rootModule.get, new File(outdir.toFile, "out-parser.json") @@ -86,7 +84,7 @@ class SanyParserPassImpl @Inject() ( val output = options.getOrElse("parser", "output", "") if (output.nonEmpty) { if (output.contains(".tla")) - writerFactory.writeModuleToFile(rootModule.get, new File(output)) + writerFactory.writeModuleToFile(rootModule.get, TlaWriter.STANDARD_MODULES, new File(output)) else if (output.contains(".json")) JsonWriter.write(rootModule.get, new File(output)) else diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala index f943d27a91..534150c258 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.io.tlc.TlcConfigParserApalache import at.forsyte.apalache.io.tlc.config._ import at.forsyte.apalache.tla.lir.UntypedPredefs._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriterFactory} +import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaBoolOper, TlaOper, TlaTempOper} import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker @@ -70,10 +70,8 @@ class ConfigurationPassImpl @Inject() ( // dump the configuration result val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile( - configuredModule, - new File(outdir.toFile, "out-config.tla") - ) + writerFactory.writeModuleToFile(configuredModule, TlaWriter.STANDARD_MODULES, + new File(outdir.toFile, "out-config.tla")) outputTlaModule = Some(configuredModule) true diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala index 8cb0fbb2fe..68559877b4 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.pp.passes import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.lir.TlaModule -import at.forsyte.apalache.tla.lir.io.TlaWriterFactory +import at.forsyte.apalache.tla.lir.io.{TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.transformations.standard._ import at.forsyte.apalache.tla.pp.{Desugarer, UniqueNameGenerator} @@ -46,7 +46,7 @@ class DesugarerPassImpl @Inject() ( // dump the result of preprocessing val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(output, new File(outdir.toFile, "out-desugarer.tla")) + writerFactory.writeModuleToFile(output, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-desugarer.tla")) outputTlaModule = Some(output) true diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala index 52e8646fe4..259889168d 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.pp.passes import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.lir.UntypedPredefs._ -import at.forsyte.apalache.tla.lir.io.TlaWriterFactory +import at.forsyte.apalache.tla.lir.io.{TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.storage.BodyMapFactory import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.transformations.standard._ @@ -94,7 +94,7 @@ class InlinePassImpl @Inject() (val options: PassOptions, gen: UniqueNameGenerat // dump the result of preprocessing val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(filtered, new File(outdir.toFile, "out-inline.tla")) + writerFactory.writeModuleToFile(filtered, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-inline.tla")) outputTlaModule = Some(filtered) true diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala index 3b76b44f5a..60b68e9a7b 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala @@ -4,7 +4,7 @@ import java.io.File import java.nio.file.Path import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.lir.TlaModule -import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriterFactory} +import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.transformations.standard._ import at.forsyte.apalache.tla.lir.UntypedPredefs._ @@ -57,7 +57,7 @@ class OptPassImpl @Inject() (val options: PassOptions, gen: UniqueNameGenerator, // dump the result of preprocessing val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(optimized, new File(outdir.toFile, "out-opt.tla")) + writerFactory.writeModuleToFile(optimized, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-opt.tla")) outputTlaModule = Some(optimized) true diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala index 029c580354..25d0ca2b52 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.pp.passes import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.imp.src.SourceStore -import at.forsyte.apalache.tla.lir.io.TlaWriterFactory +import at.forsyte.apalache.tla.lir.io.{TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator} import at.forsyte.apalache.tla.lir.transformations.standard._ import at.forsyte.apalache.tla.lir.transformations.{TlaModuleTransformation, TransformationTracker} @@ -64,10 +64,8 @@ class PreproPassImpl @Inject() ( logger.info(s" > $name") val transfomed = xformer(m) // dump the result of preprocessing after every transformation, in case the next one fails - writerFactory.writeModuleToFile( - transfomed, - new File(outdir.toFile, s"out-prepro-$name.tla") - ) + writerFactory.writeModuleToFile(transfomed, TlaWriter.STANDARD_MODULES, + new File(outdir.toFile, s"out-prepro-$name.tla")) transfomed } @@ -76,7 +74,7 @@ class PreproPassImpl @Inject() ( val afterModule = renaming.renameInModule(preprocessed) // dump the result of preprocessing - writerFactory.writeModuleToFile(afterModule, new File(outdir.toFile, "out-prepro.tla")) + writerFactory.writeModuleToFile(afterModule, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-prepro.tla")) outputTlaModule = Some(afterModule) if (options.getOrElse("general", "debug", false)) { diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/UnrollPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/UnrollPassImpl.scala index 3a333ee13c..d15ecf9668 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/UnrollPassImpl.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/UnrollPassImpl.scala @@ -4,7 +4,7 @@ import java.io.File import java.nio.file.Path import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} import at.forsyte.apalache.tla.lir.TlaModule -import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriterFactory} +import at.forsyte.apalache.tla.lir.io.{PrettyWriter, TlaWriter, TlaWriterFactory} import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming import at.forsyte.apalache.tla.pp.{UniqueNameGenerator, Unroller} @@ -61,7 +61,7 @@ class UnrollPassImpl @Inject() (val options: PassOptions, nameGenerator: UniqueN // dump the result of preprocessing val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] - writerFactory.writeModuleToFile(newModule, new File(outdir.toFile, "out-unroll.tla")) + writerFactory.writeModuleToFile(newModule, TlaWriter.STANDARD_MODULES, new File(outdir.toFile, "out-unroll.tla")) outputTlaModule = Some(newModule) true diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/CounterexampleWriter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/CounterexampleWriter.scala index 54a0c8c74a..474cbd9000 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/CounterexampleWriter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/CounterexampleWriter.scala @@ -79,7 +79,7 @@ class TlaCounterexampleWriter(writer: PrintWriter) extends CounterexampleWriter override def write(rootModule: TlaModule, notInvariant: NotInvariant, states: List[NextState]): Unit = { val pretty = new PrettyWriter(writer) - pretty.writeHeader("counterexample", List(rootModule)) + pretty.writeHeader("counterexample", List(rootModule.name)) states.zipWithIndex.foreach { case (state, 0) => diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala index b741e8f44c..fb52b11800 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala @@ -38,7 +38,8 @@ class PrettyWriter(writer: PrintWriter, layout: TextLayout = new TextLayout, private def prettyWriteDoc(doc: Doc): Unit = writer.write(pretty(doc, layout.textWidth).layout) - def write(mod: TlaModule): Unit = prettyWriteDoc(toDoc(mod)) + def write(mod: TlaModule, extendedModuleNames: List[String] = List.empty): Unit = + prettyWriteDoc(toDoc(mod, extendedModuleNames)) // Declarations have a trailing empty line def write(decl: TlaDecl): Unit = prettyWriteDoc(toDoc(decl) <> line <> line) @@ -49,7 +50,7 @@ class PrettyWriter(writer: PrintWriter, layout: TextLayout = new TextLayout, prettyWriteDoc(wrapWithComment(commentStr) <> line) } - def writeHeader(moduleName: String, extensionModuleNames: List[TlaModule] = List.empty): Unit = + def writeHeader(moduleName: String, extensionModuleNames: List[String] = List.empty): Unit = prettyWriteDoc( moduleNameDoc(moduleName) <> moduleExtendsDoc(extensionModuleNames) <> line ) @@ -62,14 +63,14 @@ class PrettyWriter(writer: PrintWriter, layout: TextLayout = new TextLayout, s"${List.fill(nDashes)("-").mkString}$middle${List.fill(nDashes)("-").mkString}" <> line } - private def moduleExtendsDoc(moduleNames: List[TlaModule]): Doc = + private def moduleExtendsDoc(moduleNames: List[String]): Doc = if (moduleNames.isEmpty) emptyDoc - else line <> text(s"EXTENDS ${moduleNames.map(_.name).mkString(", ")}") <> line + else line <> text("EXTENDS") <> space <> hsep(moduleNames.map(text), comma) <> line private def moduleTerminalDoc: Doc = s"${List.fill(layout.textWidth)("=").mkString}" <> line - def toDoc(mod: TlaModule, extensionModuleNames: List[TlaModule] = List.empty): Doc = { + def toDoc(mod: TlaModule, extensionModuleNames: List[String] = List.empty): Doc = { moduleNameDoc(mod.name) <> moduleExtendsDoc(extensionModuleNames) <> lsep((mod.declarations.toList map toDoc) :+ moduleTerminalDoc, line) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriter.scala index 74ff9ae96b..e5f4e3c4bd 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriter.scala @@ -2,8 +2,6 @@ package at.forsyte.apalache.tla.lir.io import at.forsyte.apalache.tla.lir.{TlaDecl, TlaEx, TlaModule} -import java.io.{File, FileWriter, PrintWriter} - /** *

An abstract writer of TLA+ expressions. For an example, see `PrettyWriter`.

* @@ -14,9 +12,10 @@ trait TlaWriter { /** * Write a module, including all declarations * - * @param mod a module + * @param mod a module + * @param extendedModuleNames the names of the modules to be extended */ - def write(mod: TlaModule): Unit + def write(mod: TlaModule, extendedModuleNames: List[String]): Unit /** * Write a declaration, including all expressions @@ -32,3 +31,12 @@ trait TlaWriter { */ def write(expr: TlaEx): Unit } + +object TlaWriter { + + /** + * The names of all standard modules that are supported by Apalache IR. + */ + val STANDARD_MODULES = List("Integers", "Sequences", "FiniteSets", "TLC", "Apalache") + +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriterFactory.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriterFactory.scala index c1596dc197..f6ce2ece4e 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriterFactory.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TlaWriterFactory.scala @@ -10,6 +10,7 @@ import java.io.{File, FileWriter, PrintWriter} * @author Igor Konnov */ trait TlaWriterFactory { + def create(printWriter: PrintWriter): TlaWriter /** @@ -18,10 +19,10 @@ trait TlaWriterFactory { * @param module a TLA module * @param outputFile an output file that will be created or overwritten */ - def writeModuleToFile(module: TlaModule, outputFile: File): Unit = { + def writeModuleToFile(module: TlaModule, extendedModuleNames: List[String], outputFile: File): Unit = { val writer = new PrintWriter(new FileWriter(outputFile, false)) try { - create(writer).write(module) + create(writer).write(module, extendedModuleNames) } finally { writer.close() } From bd5e67bf76eef2577d6f7b6aa9caca4da5e7cf96 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 29 Apr 2021 11:30:36 +0200 Subject: [PATCH 3/4] entry in unreleased --- UNRELEASED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/UNRELEASED.md b/UNRELEASED.md index 85af80ad21..ab6da709ee 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -27,6 +27,7 @@ * Parser: fixed two bugs in the declaration sorter, see #645 and #758 * Printer: fixed the output for EXCEPT, see #746 * Printer: fixed pretty printing of annotations, see #633 +* Printer: extending the standard modules, see #137 * The command `config --enable-stats=true` creates `$HOME/.tlaplus` if needed, see #762 ### Changes From f92d78dd38ca45538b9af09052666c1f92737ef5 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 29 Apr 2021 11:47:51 +0200 Subject: [PATCH 4/4] fix whitespaces in the comments --- .../scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala index fb52b11800..37fcfefb81 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala @@ -555,7 +555,7 @@ class PrettyWriter(writer: PrintWriter, layout: TextLayout = new TextLayout, } private def wrapWithComment(comment: Doc): Doc = { - text("(*") <> softbreak <> comment <> softbreak <> text("*)") + text("(*") <> space <> comment <> space <> text("*)") } private def wrapWithComment(strings: List[String]): Doc = {