From a885e2c69c817191fc9229a7ea094ffacd113c47 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 29 Apr 2021 11:29:31 +0200 Subject: [PATCH] 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() }