Replaced calls to old JSON reader/writer (#782)

* replaced old JSON reader/writer * unreleased * \n fix * Update tla-import/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala Co-authored-by: Igor Konnov <[email protected]>
apalache-mc · May 2, 2021 · 5fcea5f · 5fcea5f
1 parent 137e4b5
commit 5fcea5f
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 16 deletions.
diff --git a/UNRELEASED.md b/UNRELEASED.md
@@ -29,6 +29,7 @@
 * 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
+* IO: replaced calls to deprecated JsonReader/JsonWriter. out-parser.json is now compliant with the new format, see #778
 
 ### Changes
 

diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala
@@ -193,7 +193,7 @@ class JsonToTla[T <: JsonRepresentation](
     ex
   }
 
-  override def fromRoot(rootJson: T): Traversable[TlaModule] = {
+  override def fromRoot(rootJson: T): Seq[TlaModule] = {
     val versionField = getOrThrow(rootJson, TlaToJson.versionFieldName)
     val version = scalaFactory.asStr(versionField)
     val current = JsonVersion.current

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
@@ -2,18 +2,21 @@ package at.forsyte.apalache.tla.imp.passes
 
 import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin}
 import at.forsyte.apalache.io.annotations.store._
+import at.forsyte.apalache.io.json.impl.{TlaToUJson, UJsonRep, UJsonToTla}
 import at.forsyte.apalache.tla.imp.src.SourceStore
+import at.forsyte.apalache.tla.lir.{CyclicDependencyError, TlaModule}
+import at.forsyte.apalache.tla.lir.io.{TlaWriterFactory, UntypedReader}
+import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
+import at.forsyte.apalache.tla.lir.transformations.standard.DeclarationSorter
+import at.forsyte.apalache.tla.lir.io.TlaType1PrinterPredefs.printer
 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.{CyclicDependencyError, TlaModule}
 import com.google.inject.Inject
 import com.google.inject.name.Named
 import com.typesafe.scalalogging.LazyLogging
 
-import java.io.File
+import java.io.{File, FileWriter, PrintWriter}
 import java.nio.file.Path
 
 /**
@@ -22,8 +25,9 @@ import java.nio.file.Path
  * @author Igor Konnov
  */
 class SanyParserPassImpl @Inject() (
-    val options: PassOptions, val sourceStore: SourceStore, val annotationStore: AnnotationStore,
-    val writerFactory: TlaWriterFactory, @Named("AfterParser") val nextPass: Pass with TlaModuleMixin
+    val options: PassOptions, val sourceStore: SourceStore, val changeListener: ChangeListener,
+    val annotationStore: AnnotationStore, val writerFactory: TlaWriterFactory,
+    @Named("AfterParser") val nextPass: Pass with TlaModuleMixin
 ) extends SanyParserPass with LazyLogging {
 
   private var rootModule: Option[TlaModule] = None
@@ -44,7 +48,13 @@ class SanyParserPassImpl @Inject() (
     val filename = options.getOrError("parser", "filename").asInstanceOf[String]
     if (filename.endsWith(".json")) {
       try {
-        rootModule = Some(JsonReader.readModule(new File(filename)))
+        val moduleJson = UJsonRep(ujson.read(new File(filename)))
+        // TODO: Implement a TagReader in issue #780
+        val modules = new UJsonToTla(Some(sourceStore))(UntypedReader).fromRoot(moduleJson)
+        rootModule = modules match {
+          case rMod +: Nil => Some(rMod)
+          case _           => None
+        }
       } catch {
         case e: Exception =>
           logger.error("  > " + e.getMessage)
@@ -75,18 +85,15 @@ class SanyParserPassImpl @Inject() (
         val outdir = options.getOrError("io", "outdir").asInstanceOf[Path]
         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")
-        )
+        writeJson(rootModule.get, new File(outdir.toFile, "out-parser.json"))
 
         // write parser output to specified destination, if requested
         val output = options.getOrElse("parser", "output", "")
         if (output.nonEmpty) {
           if (output.contains(".tla"))
             writerFactory.writeModuleToFile(rootModule.get, TlaWriter.STANDARD_MODULES, new File(output))
           else if (output.contains(".json"))
-            JsonWriter.write(rootModule.get, new File(output))
+            writeJson(rootModule.get, new File(output))
           else
             logger.error(
                 "  > Error writing output: please give either .tla or .json filename"
@@ -108,6 +115,17 @@ class SanyParserPassImpl @Inject() (
     }
   }
 
+  private def writeJson(module: TlaModule, file: File): Unit = {
+    val writer = new PrintWriter(new FileWriter(file, false))
+    try {
+      val sourceLocator: SourceLocator = SourceLocator(sourceStore.makeSourceMap, changeListener)
+      val jsonText = new TlaToUJson(Some(sourceLocator)).makeRoot(Seq(module)).toString
+      writer.write(jsonText)
+    } finally {
+      writer.close()
+    }
+  }
+
   /**
    * Get the next pass in the chain. What is the next pass is up
    * to the module configuration and the pass outcome.

diff --git a/...ypes/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala b/...ypes/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala
@@ -8,7 +8,7 @@ import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
 import at.forsyte.apalache.tla.lir.transformations.TransformationTracker
 import at.forsyte.apalache.tla.lir.{TlaModule, TypeTag, UID, Untyped}
 import at.forsyte.apalache.tla.typecheck.TypeCheckerTool
-import at.forsyte.apalache.tla.types.TlaType1PrinterPredefs.printer
+import at.forsyte.apalache.tla.lir.io.TlaType1PrinterPredefs.printer
 import com.google.inject.Inject
 import com.google.inject.name.Named
 import com.typesafe.scalalogging.LazyLogging

diff --git a/...alache/tla/types/TlaType1TagPrinter.scala → ...lache/tla/lir/io/TlaType1TagPrinter.scala b/...alache/tla/types/TlaType1TagPrinter.scala → ...lache/tla/lir/io/TlaType1TagPrinter.scala
@@ -1,7 +1,6 @@
-package at.forsyte.apalache.tla.types
+package at.forsyte.apalache.tla.lir.io
 
 import at.forsyte.apalache.tla.lir.{TlaType1, TypeTag, Typed, Untyped}
-import at.forsyte.apalache.tla.lir.io.TypeTagPrinter
 
 class TlaType1TagPrinter extends TypeTagPrinter {
   def apply(tag: TypeTag): String = {