Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update upickle to 4.0.0 and remove unecessary customizations #2979

Merged
merged 2 commits into from
Sep 4, 2024
Merged

Update upickle to 4.0.0 and remove unecessary customizations #2979

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
90acff9
Update upickle to 4.0.0 and remove unecessary customizations
bugarela Sep 3, 2024
cecb070
Fix formatting
bugarela Sep 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions project/Dependencies.scala
View file
Open in desktop
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
View file
Open in desktop
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.
Comment on lines -392 to -397
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unrelated to the PR, this comment was just outdated (the thing it refers to no longer exists)

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
16 changes: 15 additions & 1 deletion tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintIR.scala
View file
Open in desktop
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
Loading