closes #136: pretty writer extends the standard modules

apalache-mc · Apr 29, 2021 · a885e2c · a885e2c
1 parent cdf90cf
commit a885e2c
Show file tree

Hide file tree

Showing 16 changed files with 55 additions and 50 deletions.
diff --git a/...signments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala b/...signments/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/...nments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala b/...nments/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
@@ -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
@@ -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/...mport/src/main/scala/at/forsyte/apalache/io/annotations/PrettyWriterWithAnnotations.scala b/...mport/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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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}
-
 /**
  * <p>An abstract writer of TLA+ expressions. For an example, see `PrettyWriter`.</p>
  *
@@ -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
@@ -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()
     }