Skip to content

Commit

Permalink
Merge pull request #2979 from apalache-mc/gabriela/update-upickle
Browse files Browse the repository at this point in the history
Update upickle to 4.0.0 and remove unecessary customizations
  • Loading branch information
bugarela authored Sep 4, 2024
2 parents 00d502a + cecb070 commit f8a8826
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 85 deletions.
4 changes: 2 additions & 2 deletions project/Dependencies.scala
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ object Dependencies {
val slf4j = "org.slf4j" % "slf4j-api" % "2.0.16"
val shapeless = "com.chuusai" %% "shapeless" % "2.3.12"
val tla2tools = "org.lamport" % "tla2tools" % "1.7.0-SNAPSHOT"
val ujson = "com.lihaoyi" %% "ujson" % "3.2.0"
val upickle = "com.lihaoyi" %% "upickle" % "3.2.0"
val ujson = "com.lihaoyi" %% "ujson" % "4.0.0"
val upickle = "com.lihaoyi" %% "upickle" % "4.0.0"
val z3 = "tools.aqua" % "z3-turnkey" % "4.13.0"
val zio = "dev.zio" %% "zio" % zioVersion
// Keep up to sync with version in plugins.sbt
Expand Down
88 changes: 6 additions & 82 deletions tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintIR.scala
Original file line number Diff line number Diff line change
Expand Up @@ -146,16 +146,7 @@ sealed private[quint] trait QuintEx extends WithID

private[quint] object QuintEx {

implicit val rw: RW[QuintEx] =
RW.merge(
QuintName.rw,
QuintBool.rw,
QuintInt.rw,
QuintStr.rw,
QuintApp.rw,
QuintLambda.rw,
QuintLet.rw,
)
implicit val rw: RW[QuintEx] = macroRW

/** A name of: a variable, constant, parameter, user-defined operator */
@key("name") case class QuintName(id: BigInt, name: String) extends QuintEx {}
Expand Down Expand Up @@ -227,34 +218,7 @@ private[quint] object QuintEx {
sealed private[quint] trait QuintDef extends WithID

private[quint] object QuintDef {
// The boilerplate here is a result of the infectious nature
// of ser/de customization in upickle currently.
// See https://github.com/com-lihaoyi/upickle/issues/394
//
// The customization is needed for QuintTypeDef.
private val toJson: QuintDef => ujson.Value = {
case d: QuintOpDef => QuintDeserializer.writeJs(d)
case d: QuintVar => QuintDeserializer.writeJs(d)
case d: QuintConst => QuintDeserializer.writeJs(d)
case d: QuintAssume => QuintDeserializer.writeJs(d)
case d: QuintTypeDef => QuintDeserializer.writeJs(d)
}
private val ofJson: ujson.Value => QuintDef = {
case ujson.Obj(o) if o.get("kind").isDefined =>
o.get("kind").map(_.str) match {
case Some("def") => QuintDeserializer.read[QuintOpDef](o)
case Some("const") => QuintDeserializer.read[QuintConst](o)
case Some("var") => QuintDeserializer.read[QuintVar](o)
case Some("assume") => QuintDeserializer.read[QuintAssume](o)
case Some("typedef") => QuintDeserializer.read[QuintTypeDef](o)
case Some(_) => throw new QuintIRParseError(s"Definition has invalid `kind` field: ${o}")
case None => throw new QuintIRParseError(s"Definition missing `kind` field: ${o}")
}
case invalidJson =>
throw new QuintIRParseError(s"Unexpected JSON representation of Quint type definition: ${invalidJson}")
}

implicit val rw: RW[QuintDef] = QuintDeserializer.readwriter[ujson.Value].bimap(toJson, ofJson)
implicit val rw: RW[QuintDef] = macroRW

trait WithTypeAnnotation {
val typeAnnotation: QuintType
Expand Down Expand Up @@ -337,30 +301,10 @@ private[quint] object QuintDef {
*
* Type aliases have `Some(type)` while abstract types have `None`
*/
typ: Option[QuintType])
@key("type") typ: Option[QuintType] = None)
extends QuintDef {}
object QuintTypeDef {
// We need custom ser/de here to cope with the optionality of the `type` field
// see https://github.com/com-lihaoyi/upickle/issues/75
private val toJson: QuintTypeDef => ujson.Value = {
case QuintTypeDef(id, name, None) =>
ujson.Obj("id" -> QuintDeserializer.writeJs(id), "name" -> QuintDeserializer.writeJs(name))
case QuintTypeDef(id, name, Some(t)) =>
ujson.Obj("id" -> QuintDeserializer.writeJs(id), "name" -> QuintDeserializer.writeJs(name),
"type" -> QuintDeserializer.writeJs(t))
}

private val ofJson: ujson.Value => QuintTypeDef = {
case ujson.Obj(entries) if entries.get("id").isDefined && entries.get("name").isDefined =>
val id = QuintDeserializer.read[BigInt](entries.get("id").get)
val name = QuintDeserializer.read[String](entries.get("name").get)
val tt = entries.get("type").map(t => QuintDeserializer.read[QuintType](t))
QuintTypeDef(id, name, tt)
case invalidJson =>
throw new QuintIRParseError(s"Unexpected JSON representation of Quint type definition: ${invalidJson}")
}

implicit val rw: RW[QuintTypeDef] = QuintDeserializer.readwriter[ujson.Value].bimap(toJson, ofJson)
implicit val rw: RW[QuintTypeDef] = macroRW
}
}

Expand All @@ -374,27 +318,7 @@ sealed private[quint] trait QuintType

private[quint] object QuintType {

implicit val rw: RW[QuintType] = RW.merge(
QuintBoolT.rw,
QuintIntT.rw,
QuintStrT.rw,
QuintConstT.rw,
QuintVarT.rw,
QuintSetT.rw,
QuintSeqT.rw,
QuintFunT.rw,
QuintOperT.rw,
QuintTupleT.rw,
QuintRecordT.rw,
QuintSumT.rw,
)

// NOTE: Contrary to quint values, for quint types, source IDs are optional.
// This is because many types are inferred, and not derived from the soruce.
//
// We therefor default id to -1 in the following, because upickle handles
// optional values stupidly and if we specify `id` as `Option[Int]` it will
// require the value of the ID field to be a (possibly empty) singleton array.
implicit val rw: RW[QuintType] = macroRW

@key("bool") case class QuintBoolT() extends QuintType {}
object QuintBoolT {
Expand Down Expand Up @@ -449,7 +373,7 @@ private[quint] object QuintType {
sealed trait Row

object Row {
implicit val rw: RW[Row] = RW.merge(Cell.rw, Var.rw, Nil.rw)
implicit val rw: RW[Row] = macroRW

@key("row") case class Cell(fields: Seq[RecordField], other: Row) extends Row
object Cell {
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package at.forsyte.apalache.io.quint

import at.forsyte.apalache.io.quint.QuintDef.QuintAssume
import at.forsyte.apalache.io.quint.QuintDef.{QuintAssume, QuintOpDef, QuintTypeDef}
import at.forsyte.apalache.io.quint.QuintEx.QuintBool
import org.junit.runner.RunWith
import org.scalatest.funsuite.AnyFunSuite
Expand Down Expand Up @@ -47,6 +47,20 @@ class TestQuintIR extends AnyFunSuite {
assert(unnamedAssume.isUnnamed)
}

test("Simple QuintDef works correctly") {
val quintDef = QuintOpDef(1, "myDef", "val", QuintBool(2, true))
assert(QuintDeserializer.write[QuintDef](
quintDef) == """{"kind":"def","id":1,"name":"myDef","qualifier":"val","expr":{"kind":"bool","id":2,"value":true}}""")
}

test("QuintTypeDef works correctly") {
val typeDef = QuintTypeDef(1, "myType", None)
val typeDefJson = """{"kind":"typedef","id":1,"name":"myType"}"""

assert(QuintDeserializer.write[QuintTypeDef](typeDef) == typeDefJson)
assert(QuintDeserializer.read[QuintTypeDef](typeDefJson) == typeDef)
}

// tictactoe.json is located in tla-io/src/test/resources/tictactoe.json
test("Can load tictactoe.json") {
val tictactoeQuintJson = scala.io.Source.fromResource("tictactoe.json").mkString
Expand Down

0 comments on commit f8a8826

Please sign in to comment.