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

apalache-mc · May 19, 2020 · 9cada27 · 9cada27
1 parent 59b3ac0
commit 9cada27
Show file tree

Hide file tree

Showing 4 changed files with 171 additions and 14 deletions.
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/JsonReader.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/JsonReader.scala
@@ -14,9 +14,24 @@ import scala.collection.mutable.LinkedHashMap
 
 object JsonReader {
 
-  def read(from: ujson.Readable): TlaEx = {
-    val json = ujson.read(from)
-    parseJson(json)
+  def readModule(from: ujson.Readable): TlaModule = {
+    parseModule(ujson.read(from))
+  }
+
+  def readExpr(from: ujson.Readable): TlaEx = {
+    parseJson(ujson.read(from))
+  }
+
+  // expect ujson.Value to be an encoding of a module
+  def parseModule(v: ujson.Value): TlaModule = {
+    // it should be a JSON object
+    val m = v.objOpt match {
+      case Some(value) => value
+      case None => throw new Exception("incorrect TLA+ JSON: expecting a module object")
+    }
+    if(!m.contains("MODULE") || !m.contains("declarations"))
+      throw new Exception("incorrect TLA+ JSON: malformed module object")
+    new TlaModule(parseStr(m("MODULE")), parseDecls(m("declarations")))
   }
 
   val unaryOps = JsonWriter.unaryOps.map(_.swap)

diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestJson.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestJson.scala
@@ -1,19 +1,12 @@
 package at.forsyte.apalache.tla.lir.io
 
-import java.io.{PrintWriter, StringWriter}
-
 import at.forsyte.apalache.tla.lir.convenience.tla._
 import at.forsyte.apalache.tla.lir.oper._
 import at.forsyte.apalache.tla.lir._
 import org.junit.runner.RunWith
 import org.scalatest.junit.JUnitRunner
-import org.scalatest.{BeforeAndAfterEach, FunSuite}
+import org.scalatest.FunSuite
 import at.forsyte.apalache.tla.lir.values._
-import upickle._
-
-import scala.collection.immutable.HashMap
-import scala.collection.mutable
-import scala.collection.mutable.ArrayBuffer
 
 /**
  * <p>Geeneric set of tests for conversion between TLA and JSON.</p>
@@ -23,6 +16,10 @@ import scala.collection.mutable.ArrayBuffer
 @RunWith(classOf[JUnitRunner])
 abstract class TestJson extends FunSuite {
 
+  // This abstract function should be defined in child class
+  // It should check that mod and json match after conversion
+  def compareModule(mod: TlaModule, json: String, indent: Int = -1): Unit
+
   // This abstract function should be defined in child class
   // It should check that expr and json match after conversion
   def compare(expr: TlaEx, json: String, indent: Int = -1): Unit
@@ -31,6 +28,9 @@ abstract class TestJson extends FunSuite {
   def compareMultiLine(ex: TlaEx, expected: String): Unit =
     compare(ex, expected, 2)
 
+  def compareModuleMultiLine(mod: TlaModule, expected: String): Unit =
+    compareModule(mod, expected, 2)
+
   test("id") {
     // awesome
     compare(
@@ -506,4 +506,133 @@ abstract class TestJson extends FunSuite {
         |}""".stripMargin
     )
   }
+
+  test("empty module") {
+    // awesome
+    compareModule(
+      new TlaModule("TEST", List()),
+      """{"MODULE":"TEST","declarations":[]}"""
+    )
+  }
+
+  test("module trivial") {
+    // awesome
+    compareModule(
+      new TlaModule("trivial", List(
+        TlaOperDecl("A", List(), int(42))
+      )),
+      """{"MODULE":"trivial","declarations":[{"OPERATOR":"A","body":42,"params":[]}]}"""
+    )
+  }
+
+  test("module simpleOperator") {
+    // awesome
+    compareModuleMultiLine(
+      new TlaModule("simpleOperator", List(
+        TlaOperDecl("A", List(SimpleFormalParam("age")), gt(name("age"),int(42)))
+      )),
+      """{
+        |  "MODULE": "simpleOperator",
+        |  "declarations": [
+        |    {
+        |      "OPERATOR": "A",
+        |      "body": {
+        |        ">": [
+        |          "age",
+        |          42
+        |        ]
+        |      },
+        |      "params": [
+        |        {
+        |          "name": "age",
+        |          "arity": 0
+        |        }
+        |      ]
+        |    }
+        |  ]
+        |}""".stripMargin
+    )
+  }
+
+  test("module level2Operators") {
+    // awesome
+    val aDecl = TlaOperDecl("A",
+      List(SimpleFormalParam("i"), SimpleFormalParam("j"), OperFormalParam("f", 1)),
+      OperEx(TlaOper.apply, NameEx("f"),
+        OperEx(TlaSetOper.cup, NameEx("i"), NameEx("j"))))
+    val bDecl = TlaOperDecl("B", List(SimpleFormalParam("y")), NameEx("y"))
+    compareModuleMultiLine(
+      new TlaModule("level2Operators", List(
+        aDecl,
+        bDecl,
+        TlaOperDecl("C", List(SimpleFormalParam("z")),
+          appDecl( aDecl, int(0), NameEx("z"), appDecl(bDecl, int(1))))
+      )),
+      """{
+        |  "MODULE": "level2Operators",
+        |  "declarations": [
+        |    {
+        |      "OPERATOR": "A",
+        |      "body": {
+        |        "apply-op": "f",
+        |        "args": [
+        |          {
+        |            "union": [
+        |              "i",
+        |              "j"
+        |            ]
+        |          }
+        |        ]
+        |      },
+        |      "params": [
+        |        {
+        |          "name": "i",
+        |          "arity": 0
+        |        },
+        |        {
+        |          "name": "j",
+        |          "arity": 0
+        |        },
+        |        {
+        |          "name": "f",
+        |          "arity": 1
+        |        }
+        |      ]
+        |    },
+        |    {
+        |      "OPERATOR": "B",
+        |      "body": "y",
+        |      "params": [
+        |        {
+        |          "name": "y",
+        |          "arity": 0
+        |        }
+        |      ]
+        |    },
+        |    {
+        |      "OPERATOR": "C",
+        |      "body": {
+        |        "apply-op": "A",
+        |        "args": [
+        |          0,
+        |          "z",
+        |          {
+        |            "apply-op": "B",
+        |            "args": [
+        |              1
+        |            ]
+        |          }
+        |        ]
+        |      },
+        |      "params": [
+        |        {
+        |          "name": "z",
+        |          "arity": 0
+        |        }
+        |      ]
+        |    }
+        |  ]
+        |}""".stripMargin
+    )
+  }
 }
diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestJsonReader.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestJsonReader.scala
@@ -4,8 +4,13 @@ import at.forsyte.apalache.tla.lir._
 
 class TestJsonReader extends TestJson {
 
-  // check that after reading from json the result matches expected
+  def compareModule(expected: TlaModule, json: String, indent: Int = -1): Unit = {
+    val mod = JsonReader.readModule(json)
+    assert(mod.name == expected.name)
+    assert(mod.declarations == expected.declarations)
+  }
+
   def compare(expected: TlaEx, json: String, indent: Int = -1): Unit = {
-    assert(JsonReader.read(json) == expected)
+    assert(JsonReader.readExpr(json) == expected)
   }
 }
diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestJsonWriter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestJsonWriter.scala
@@ -5,7 +5,15 @@ import at.forsyte.apalache.tla.lir._
 
 class TestJsonWriter extends TestJson {
 
-  // check that after writing to json the result matches expected
+  def compareModule(mod: TlaModule, json: String, indent: Int = -1): Unit = {
+    val stringWriter = new StringWriter()
+    val printWriter = new PrintWriter(stringWriter)
+    val writer = new JsonWriter(printWriter, indent)
+    writer.write(mod)
+    printWriter.flush()
+    assert(stringWriter.toString == json)
+  }
+
   def compare(ex: TlaEx, expected: String, indent: Int = -1): Unit = {
     val stringWriter = new StringWriter()
     val printWriter = new PrintWriter(stringWriter)