Ak/jsoninput (#146)

* JsonReader: started on #121, reading JSON input

* #121 TestJson: refactor JSON tests to use common testset for both reader and writer

* #121 JsonReader: extending coverage

* * join together functional ops into a common pattern
* make json name mappings public for usage in JsonReader
* make unique names for bounded set operators

* #121 JsonWriter merge binary and nary ops into the same case

* #121 JsonReader: extending coverage (added functional and predicate ops)

* #121 JsonWriter: always specify args for operator calls

* #121 JsonReader: add function and operator applications

* #121 JsonReader: add IF, CASE, stutter, fairness

* #121 JsonReader: add labels

* #121 JsonWriter: make params in operator decl non-optional

* #121 JsonReader: add LET-IN expressions; current unit tests pass

* #121 JsonReader: add reading of modules + some module tests

* #121 JsonReader: integrate JSON input into parse and check commands

* #121 JsonReader/Writer: add --output option to parse command

* #121 JsonReader/Writer: bump up version of ujson library

* merge 'unstable' into 'ak/jsoninput'

* #121 JsonReader: update TestCounterexampleWriter

* #121 ParseCmd: simplify handling of parse --output

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

@@ -105,6 +105,7 @@ object Tool extends App with LazyLogging {
     val executor = injector.getInstance(classOf[PassChainExecutor])
     executor.options.set("io.outdir", createOutputDir())
     executor.options.set("parser.filename", parse.file.getAbsolutePath)
+    executor.options.set("parser.output", parse.output)
 
     val result = executor.run()
     if (result.isDefined) {

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -12,7 +12,7 @@ import org.backuity.clist.{Command, _}
 class CheckCmd extends Command(name = "check",
   description = "Check a TLA+ specification") with General {
 
-  var file: File = arg[File](description = "a file containing a TLA+ specification")
+  var file: File = arg[File](description = "a file containing a TLA+ specification (.tla or .json)")
   var config: String = opt[String](
     name = "config", default = "",
     description = "configuration file in TLC format,\n" +

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ParseCmd.scala

@@ -12,5 +12,9 @@ import org.backuity.clist.{Command, _}
 class ParseCmd extends Command(name = "parse",
   description = "Parse a TLA+ specification and quit") with General {
 
-  var file: File = arg[File](description = "a file containing a TLA+ specification")
+  var file: File = arg[File](description = "a file containing a TLA+ specification (.tla or .json)")
+  var output: String = opt[String](
+    name = "output", default = "",
+    description = "filename where to output the parsed source (.tla or .json),\n" +
+    "default: None")
 }

tla-import/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala

@@ -7,7 +7,7 @@ import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin}
 import at.forsyte.apalache.tla.imp.SanyImporter
 import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.tla.lir.TlaModule
-import at.forsyte.apalache.tla.lir.io.{JsonWriter, PrettyWriter}
+import at.forsyte.apalache.tla.lir.io.{JsonReader, JsonWriter, PrettyWriter}
 import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
 import com.google.inject.Inject
 import com.google.inject.name.Named
@@ -40,23 +40,49 @@ class SanyParserPassImpl @Inject()(val options: PassOptions,
     */
   override def execute(): Boolean = {
     val filename = options.getOrError("parser", "filename").asInstanceOf[String]
-    val (rootName, modules) = new SanyImporter(sourceStore).loadFromFile(new File(filename))
-    rootModule = modules.get(rootName)
+    if (filename.endsWith(".json")) {
+      try {
+        rootModule = Some(JsonReader.readModule(new File(filename)))
+      }
+      catch {
+        case e: Exception =>
+          logger.error("  > " + e.getMessage)
+          rootModule = None
+      }
+    }
+    else {
+      val (rootName, modules) = new SanyImporter(sourceStore).loadFromFile(new File(filename))
+      rootModule = modules.get(rootName)
+    }
     if (rootModule.isEmpty) {
-      logger.error("Error parsing file " + filename)
+      logger.error("  > Error parsing file " + filename)
     } else {
       val outdir = options.getOrError("io", "outdir").asInstanceOf[Path]
       PrettyWriter.write(rootModule.get, new File(outdir.toFile, "out-parser.tla"))
       JsonWriter.write(rootModule.get, new File(outdir.toFile, "out-parser.json"))
 
-      if (options.getOrElse("general", "debug", false)) {
-        val sourceLocator = SourceLocator(sourceStore.makeSourceMap, new ChangeListener())
-        rootModule.get.operDeclarations foreach sourceLocator.checkConsistency
+      // write parser output to specified destination, if requested
+      val output = options.getOrElse("parser", "output", "")
+      if (output.nonEmpty) {
+        if (output.contains(".tla"))
+          PrettyWriter.write(rootModule.get, new File(output))
+        else if (output.contains(".json"))
+          JsonWriter.write(rootModule.get, new File(output))
+        else
+          logger.error("  > Error writing output: please give either .tla or .json filename")
+
+        if (options.getOrElse("general", "debug", false)) {
+          val sourceLocator = SourceLocator(sourceStore.makeSourceMap, new ChangeListener())
+          rootModule.get.operDeclarations foreach sourceLocator.checkConsistency
+        }
+        if (options.getOrElse("general", "debug", false)) {
+          val sourceLocator = SourceLocator(sourceStore.makeSourceMap, new ChangeListener())
+          rootModule.get.operDeclarations foreach sourceLocator.checkConsistency
+        }
       }
     }
     rootModule.isDefined
   }
-
   /**
     * Get the next pass in the chain. What is the next pass is up
     * to the module configuration and the pass outcome.

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala

@@ -50,7 +50,7 @@ class ConfigurationPassImpl @Inject()(val options: PassOptions,
     val filename =
       if(configFilename.isEmpty)
         options.getOrError("parser", "filename").asInstanceOf[String]
-        .replaceFirst("\\.tla$", "\\.cfg")
+        .replaceFirst("\\.(tla|json)$", "\\.cfg")
       else
         configFilename
     val basename = FilenameUtils.getName(filename)

tlair/pom.xml

@@ -55,7 +55,7 @@
         <dependency>
             <groupId>com.lihaoyi</groupId>
             <artifactId>ujson_2.12</artifactId>
-            <version>0.9.8</version>
+            <version>1.1.0</version>
         </dependency>
 
     </dependencies>