From 944de9f8ac09434ce32170089b697d53bfa127ba Mon Sep 17 00:00:00 2001 From: Kukovec Date: Mon, 22 Mar 2021 15:28:37 +0100 Subject: [PATCH 1/6] json ADR --- docs/src/adr/005adr-json.md | 121 ++++++++++++++++++++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 docs/src/adr/005adr-json.md diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md new file mode 100644 index 0000000000..9707c75e1e --- /dev/null +++ b/docs/src/adr/005adr-json.md @@ -0,0 +1,121 @@ +# ADR-005: JSON Serialization Format + +| author | revision | +| ------------ | --------:| +| Jure Kukovec | 1 | + +This ADR documents our decision on serializing the Apalache internal representation (IR) as JSON. +The purpose of introducing such a serialization is to expose the internal representation in a standardized format, which can be used for persistent storage, or for analysis by third-party tools in the future. + +## 1. Serializable classes + +The following classes are serializable: +1. TLA+ expressions `TlaEx` and subclasses thereof: + 1. Named expressions `NameEx` + 1. Literal values `ValEx` for the following literals: + 1. Integers `TlaInt` + 1. Strings `TlaStr` + 1. Booleans `TlaBool` + 1. Decimals `TlaDecimal` + 1. Operator expressions `OperEx` + 1. LET-IN expressions `LetInEx` +1. TLA+ declarations `TlaDecl` and subclasses thereof: + 1. Variable declarations `TlaVarDecl` + 1. Constant declarations `TlaConstDecl` + 1. Operator declarations `TlaOperDecl` + 1. Assumption declarations `TlaAssumeDecl` + 1. Theorem declarations `TlaTheoremDecl` +1. TLA+ modules `TlaModule` + +## 2. Disambiguation field + +Every serialization will contain a disambiguation field, named `kind`. This field holds the name of the class being serialized. For example, the serialization of a `NameEx` will have the shape +``` +{ + kind: "NameEx" + ... +} +``` + +## 3. Serializing typed entities + +Serializations of typed entities will have an additional field named `type`, containing the type of the expression (see [ADR-002][], [ADR-004][] for a description of our type system and the syntax for types-as-string-annotations respectively). For example, the integer literal `1` is represented by a `ValEx`, which has type `Int` and is serialized as follows: +``` +{ + kind: "NameEx" + type: "Int" + ... +} +``` + +## 4. Serialization rules + +The goal of the serialization is for the JSON structure to mimic the internal representation as closely as possible, for ease of deserialization. +Concretely, whenever a class declares a field `fld: T`, its serialization also contains a field named `fld`, containing the serialization of the field value. +For example, if `TlaConstDecl` declares a `name: String` field, its JSON serialization will have a `name` field as well, containing the name string. + +If a class field has the type `Traversable[T]`, for some `T`, the corresponding JSON entry is a list containing serializations of the individual arguments. For example, `OperEx` is variadic and declares `args: TlaEx*`, so its serialization has an `args` field containing a (possibly empty) list. + +As a running example, take the expression `1 + 1`, represented with the correct type annotations as +``` +OperEx( + oper = TlaArithOper.plus, + args = Seq( + ValEx( TlaInt( 1 ) )( typeTag = Typed( IntT1() ) ), + ValEx( TlaInt( 1 ) )( typeTag = Typed( IntT1() ) ) + ) + )( typeTag = Typed( IntT1() ) ) +``` + +Since both sub-expressions, the literals `1`, are identical, their serializations are equal as well: +``` +{ + kind: "ValEx", + type: "Int", + value: { + kind: "TlaInt", + value: 1 + } +} +``` + +Note that in the above example, the outer `value` field contains a JSON serialization of `TlaInt(1)`, and not just the JSON literal `1`. This is because of deserialization: +Apalache encodes its TLA+ integers as `BigInt`, which means that it permits values, for which `.isValidInt` does not hold. If we chose to encode values directly as JSON numbers, we would need a) a sensible encoding of `BigInt` values, which are not valid integers and b) a way to distinguish both variants of `BigInt`, as well as decimals, when deserializing (since JSON is not typed). +Alternatively, we could encode all values as strings, which would be similarly indistinguishable when deserializing. Importantly, the `type` field is not guaranteed to contain a hint, as it could be `Untyped`. +For the above reasons, we choose to instead serialize `TlaValue` as a JSON object, which is more verbose, but trivial to deserialize. It has the following shape +``` +{ + kind: _ + value: _ +} +``` + +The `value` field depends on the kind of `TlaValue`: +1. For `TlaStr`: a JSON string +1. For `TlaBool`: a JSON Boolean +1. For `TlaInt(bigIntValue)`: + 1. If `bigIntValue.isValidInt`: a JSON number + 2. Otherwise: `{ bigInt: bigIntValue.toString() }` +1. For `TlaDecimal(decValue)`: a JSON string `decValue.toString` + +Take `jsonOf1` to be the serialization of `ValEx( TlaInt( 1 ) )( typeTag = Typed( IntT1() ) )` shown above. The serialization of `1 + 1` is then equal to +``` +{ + kind: "OperEx", + type: "Int", + oper: "(+)", + args: [jsonOf1, jsonOf1] +} +``` +In general, for any given `oper: TlaOper` of `OperEx`, the value of the `oper` field in the serialization equals `oper.name`. + +## 5. Implementation + +The implementation of the serialization can be found in the class +`at.forsyte.apalache.io.json.TlaToJson` of the module `tla-import`, see [TlaToJson][]. + +[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html + +[ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html + +[TlaToJson]: https://github.com/informalsystems/apalache/blob/unstable/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala From 4a3f6991cb4a06ae55ffe8c33a2895f7378b1036 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Sun, 11 Apr 2021 02:00:27 +0200 Subject: [PATCH 2/6] JSON source field + misc --- docs/src/adr/005adr-json.md | 119 ++++++-- .../apalache/io/json/JsonRepresentation.scala | 1 + .../apalache/io/json/JsonVersion.scala | 12 + .../forsyte/apalache/io/json/TlaToJson.scala | 282 ++++++++++-------- .../apalache/io/json/impl/TlaToUJson.scala | 5 +- .../apalache/io/json/impl/UJsonRep.scala | 5 + .../apalache/io/json/TestTlaToUJson.scala | 2 +- .../passes/EtcTypeCheckerPassImpl.scala | 3 +- 8 files changed, 283 insertions(+), 146 deletions(-) create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonVersion.scala diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md index 9707c75e1e..1ee8e514ba 100644 --- a/docs/src/adr/005adr-json.md +++ b/docs/src/adr/005adr-json.md @@ -32,23 +32,93 @@ The following classes are serializable: Every serialization will contain a disambiguation field, named `kind`. This field holds the name of the class being serialized. For example, the serialization of a `NameEx` will have the shape ``` { - kind: "NameEx" + "kind": "NameEx" ... } ``` -## 3. Serializing typed entities +## 3. Serializing tagged entities -Serializations of typed entities will have an additional field named `type`, containing the type of the expression (see [ADR-002][], [ADR-004][] for a description of our type system and the syntax for types-as-string-annotations respectively). For example, the integer literal `1` is represented by a `ValEx`, which has type `Int` and is serialized as follows: +Serializations of entities annotated with a `TypeTag` will have an additional field named `type`, containing the type of the expression (see [ADR-002][], [ADR-004][] for a description of our type system and the syntax for types-as-string-annotations respectively), if the tag is `Typed`, or `Untyped` otherwise. For example, the integer literal `1` is represented by a `ValEx`, which has type `Int` and is serialized as follows: ``` { - kind: "NameEx" - type: "Int" + "kind": "ValEx", + "type": "Int" ... } ``` +in the typed encoding, or +``` +{ + "kind": "ValEx", + "type": "Untyped" + ... +} +``` +in the untyped encoding. -## 4. Serialization rules +## 4. Source information +Entities in the internal representation are usually annotated with source information, of the form `{filename}:{startLine}:{startColumn}-{endLine}:{endColumn}`, relating them to a file range in the provided specification (from which they may have been transformed as part of preprocessing). +JSON encodings may, but are not required to, contain a `source` providing this information, of the following shape: +``` +{ + "source": { + "filename" : , + "from" : { + "line" : , + "column" : + }, + "to" : { + "line" : , + "column" : + } + } +} +``` +or +``` +{ + "source": "UNKNOWN" +} +``` +if no source information is available (e.g. for expressions generated purely by Apalache). +Serializations generated by Apalache are always guaranteed to contain a `source` field entry. + +Example: +``` +{ + "kind" : "NameEx", + "type" : "Int", + "name" : "myName", + "source": { + "filename" : "MyModule.tla", + "from" : { + "line" : 3, + "column" : 5 + }, + "to" : { + "line" : 3, + "column" : 10 + } + } +} +``` + +## 5. Version information +JSON serializations of `TlaModule`s contain a filed named `version`, holding a string representation of the current JSON encoding version, shaped `{major}.{minor}`. +This document defines JSON Version 1.0. If and when a different JSON version is defined, this document will be updated accordingly. +Apalache may refuse to import, or trigger warnings for, JSON objects with obsolete versions of the encoding in the future. +Example: +``` +{ + "kind": "TlaModule", + "name": "MyModule", + "version": "1.0" + ... +} +``` + +## 6. General serialization rules The goal of the serialization is for the JSON structure to mimic the internal representation as closely as possible, for ease of deserialization. Concretely, whenever a class declares a field `fld: T`, its serialization also contains a field named `fld`, containing the serialization of the field value. @@ -70,23 +140,20 @@ OperEx( Since both sub-expressions, the literals `1`, are identical, their serializations are equal as well: ``` { - kind: "ValEx", - type: "Int", - value: { - kind: "TlaInt", - value: 1 + "kind": "ValEx", + "type": "Int", + "value": { + "kind": "TlaInt", + "value": 1 } } ``` -Note that in the above example, the outer `value` field contains a JSON serialization of `TlaInt(1)`, and not just the JSON literal `1`. This is because of deserialization: -Apalache encodes its TLA+ integers as `BigInt`, which means that it permits values, for which `.isValidInt` does not hold. If we chose to encode values directly as JSON numbers, we would need a) a sensible encoding of `BigInt` values, which are not valid integers and b) a way to distinguish both variants of `BigInt`, as well as decimals, when deserializing (since JSON is not typed). -Alternatively, we could encode all values as strings, which would be similarly indistinguishable when deserializing. Importantly, the `type` field is not guaranteed to contain a hint, as it could be `Untyped`. -For the above reasons, we choose to instead serialize `TlaValue` as a JSON object, which is more verbose, but trivial to deserialize. It has the following shape +Observe that we choose to serialize `TlaValue` as a JSON object, which is more verbose, but trivial to deserialize. It has the following shape ``` { - kind: _ - value: _ + "kind": _ , + "value": _ } ``` @@ -95,21 +162,27 @@ The `value` field depends on the kind of `TlaValue`: 1. For `TlaBool`: a JSON Boolean 1. For `TlaInt(bigIntValue)`: 1. If `bigIntValue.isValidInt`: a JSON number - 2. Otherwise: `{ bigInt: bigIntValue.toString() }` + 2. Otherwise: `{ "bigInt: bigIntValue.toString() }` 1. For `TlaDecimal(decValue)`: a JSON string `decValue.toString` +The reason for the non-uniform treatment of integers, is that Apalache encodes its TLA+ integers as `BigInt`, which means that it permits values, for which `.isValidInt` does not hold. + +While it might seem more natural to encode the entire `TlaValue` as a JSON primitive, without the added object layer, we would have a much tougher time deserializing. +We would need a) a sensible encoding of `BigInt` values, which are not valid integers, and b) a way to distinguish both variants of `BigInt`, as well as decimals, when deserializing (since JSON is not typed). +We could encode all values as strings, but they would be similarly indistinguishable when deserializing. Importantly, the `type` field of the `ValEx` expression is not guaranteed to contain a hint, as it could be `Untyped` + Take `jsonOf1` to be the serialization of `ValEx( TlaInt( 1 ) )( typeTag = Typed( IntT1() ) )` shown above. The serialization of `1 + 1` is then equal to ``` { - kind: "OperEx", - type: "Int", - oper: "(+)", - args: [jsonOf1, jsonOf1] + "kind": "OperEx", + "type": "Int", + "oper": "(+)", + "args": [jsonOf1, jsonOf1] } ``` In general, for any given `oper: TlaOper` of `OperEx`, the value of the `oper` field in the serialization equals `oper.name`. -## 5. Implementation +## 7. Implementation The implementation of the serialization can be found in the class `at.forsyte.apalache.io.json.TlaToJson` of the module `tla-import`, see [TlaToJson][]. diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala index 0e3811f6ea..b7f5bd48d3 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala @@ -6,4 +6,5 @@ package at.forsyte.apalache.io.json */ trait JsonRepresentation { def toString: String + def getFieldOpt(fieldName: String): Option[this.type] } diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonVersion.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonVersion.scala new file mode 100644 index 0000000000..e9c4cfbf65 --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonVersion.scala @@ -0,0 +1,12 @@ +package at.forsyte.apalache.io.json + +/** + * JSON serialization versions need not be tied to Apalache versions + * (Apalache versions, obtained from at.forsyte.apalache.tla.tooling.Version + * cannot be read here anyway, due to tooling -> import dependencies) + */ +object JsonVersion { + val major = 1 + val minor = 0 + def current: String = s"$major.$minor" +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala index 7741e16fe3..12e38eb8ea 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala @@ -3,6 +3,7 @@ package at.forsyte.apalache.io.json import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaDecimal, TlaInt, TlaStr} import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.io.TypeTagPrinter +import at.forsyte.apalache.tla.lir.storage.SourceLocator /** * A semi-abstraction of a json encoder. @@ -53,10 +54,11 @@ import at.forsyte.apalache.tla.lir.io.TypeTagPrinter * @param factory A json factory for the `T` variant of JsonRepresentation * @tparam T Any class extending JsonRepresentation */ -class TlaToJson[T <: JsonRepresentation](factory: JsonFactory[T])(implicit typTagPrinter: TypeTagPrinter) +class TlaToJson[T <: JsonRepresentation]( + factory: JsonFactory[T], locatorOpt: Option[SourceLocator] = None +)(implicit typeTagPrinter: TypeTagPrinter) extends JsonEncoder[T] { - val kindFieldName: String = "kind" - val typeFieldName: String = "type" + import TlaToJson._ implicit def liftString: String => T = factory.fromStr @@ -64,126 +66,157 @@ class TlaToJson[T <: JsonRepresentation](factory: JsonFactory[T])(implicit typTa implicit def liftBool: Boolean => T = factory.fromBool - override def apply(ex: TlaEx): T = ex match { - case NameEx(name) => - factory.mkObj( - typeFieldName -> typTagPrinter(ex.typeTag), - kindFieldName -> "NameEx", - "name" -> name - ) - - case ValEx(value) => - val inner = value match { - case TlaStr(strValue) => - factory.mkObj( - kindFieldName -> "TlaStr", - "value" -> strValue - ) - case TlaDecimal(decValue) => - factory.mkObj( - kindFieldName -> "TlaDecimal", - "value" -> decValue.toString() // let the parser care when reading - ) - case TlaInt(bigIntValue) => - val intVal: T = - if (bigIntValue.isValidInt) liftInt(bigIntValue.toInt) - else factory.mkObj("bigInt" -> bigIntValue.toString()) - factory.mkObj( - kindFieldName -> "TlaInt", - "value" -> intVal - ) - case TlaBool(boolValue) => - factory.mkObj( - kindFieldName -> "TlaBool", - "value" -> boolValue - ) - case _ => - //unsupported (TlaReal, TlaPredefSet) - factory.mkObj() + /** + * If a SourceLocator is given, prepare a `sourceFieldName` field, holding a JSON + * with file & position info, in addition to the given fields. + */ + private def withOptionalLoc(identifiable: Identifiable)(fields: (String, T)*): T = { + val locFieldOpt: Option[T] = locatorOpt map { locator => + locator.sourceOf(identifiable.ID) map { sourceLoc => + factory.mkObj( + "filename" -> sourceLoc.filename, + "from" -> factory.mkObj( + "line" -> sourceLoc.region.start.line, + "column" -> sourceLoc.region.start.column + ), + "to" -> factory.mkObj( + "line" -> sourceLoc.region.end.line, + "column" -> sourceLoc.region.end.column + ) + ) + } getOrElse { + "UNKNOWN" // Locator is given, but doesn't know the source } - factory.mkObj( - typeFieldName -> typTagPrinter(ex.typeTag), - kindFieldName -> "ValEx", - "value" -> inner - ) - - case OperEx(oper, args @ _*) => - val argJsons = args map apply - factory.mkObj( - typeFieldName -> typTagPrinter(ex.typeTag), - kindFieldName -> "OperEx", - "oper" -> oper.name, - "args" -> factory.fromTraversable(argJsons) - ) - case LetInEx(body, decls @ _*) => - val bodyJson = apply(body) - val declJsons = decls map apply - factory.mkObj( - typeFieldName -> typTagPrinter(ex.typeTag), - kindFieldName -> "LetInEx", - "body" -> bodyJson, - "decls" -> factory.fromTraversable(declJsons) - ) - - case NullEx => - factory.mkObj(kindFieldName -> "NullEx") + } + factory.mkObj((locFieldOpt map { sourceFieldName -> _ }) ++: fields: _*) } - override def apply(decl: TlaDecl): T = decl match { - case TlaTheoremDecl(name, body) => - val bodyJson = apply(body) - factory.mkObj( - typeFieldName -> typTagPrinter(decl.typeTag), - kindFieldName -> "TlaTheoremDecl", - "name" -> name, - "body" -> bodyJson - ) - - case TlaVarDecl(name) => - factory.mkObj( - typeFieldName -> typTagPrinter(decl.typeTag), - kindFieldName -> "TlaVarDecl", - "name" -> name - ) - - case TlaConstDecl(name) => - factory.mkObj( - typeFieldName -> typTagPrinter(decl.typeTag), - kindFieldName -> "TlaConstDecl", - "name" -> name - ) - - case decl @ TlaOperDecl(name, formalParams, body) => - val bodyJson = apply(body) - val paramsJsons = formalParams map { - case SimpleFormalParam(paramName) => - factory.mkObj( - kindFieldName -> "SimpleFormalParam", - "name" -> paramName - ) - case OperFormalParam(paramName, arity) => - factory.mkObj( - kindFieldName -> "OperFormalParam", - "name" -> paramName, - "arity" -> arity - ) - } - factory.mkObj( - typeFieldName -> typTagPrinter(decl.typeTag), - kindFieldName -> "TlaOperDecl", - "name" -> name, - "formalParams" -> factory.fromTraversable(paramsJsons), - "isRecursive" -> decl.isRecursive, - "body" -> bodyJson - ) - - case TlaAssumeDecl(body) => - val bodyJson = apply(body) - factory.mkObj( - typeFieldName -> typTagPrinter(decl.typeTag), - kindFieldName -> "TlaAssumeDecl", - "body" -> bodyJson - ) + override def apply(ex: TlaEx): T = { + def withLoc(fields: (String, T)*): T = withOptionalLoc(ex)(fields: _*) + ex match { + case NameEx(name) => + withLoc( + typeFieldName -> typeTagPrinter(ex.typeTag), + kindFieldName -> "NameEx", + "name" -> name + ) + + case ValEx(value) => + val inner = value match { + case TlaStr(strValue) => + factory.mkObj( + kindFieldName -> "TlaStr", + "value" -> strValue + ) + case TlaDecimal(decValue) => + factory.mkObj( + kindFieldName -> "TlaDecimal", + "value" -> decValue.toString() // let the parser care when reading + ) + case TlaInt(bigIntValue) => + val intVal: T = + if (bigIntValue.isValidInt) liftInt(bigIntValue.toInt) + else factory.mkObj("bigInt" -> bigIntValue.toString()) + factory.mkObj( + kindFieldName -> "TlaInt", + "value" -> intVal + ) + case TlaBool(boolValue) => + factory.mkObj( + kindFieldName -> "TlaBool", + "value" -> boolValue + ) + case _ => + //unsupported (TlaReal, TlaPredefSet) + factory.mkObj() + } + withLoc( + typeFieldName -> typeTagPrinter(ex.typeTag), + kindFieldName -> "ValEx", + "value" -> inner + ) + + case OperEx(oper, args @ _*) => + val argJsons = args map apply + withLoc( + typeFieldName -> typeTagPrinter(ex.typeTag), + kindFieldName -> "OperEx", + "oper" -> oper.name, + "args" -> factory.fromTraversable(argJsons) + ) + case LetInEx(body, decls @ _*) => + val bodyJson = apply(body) + val declJsons = decls map apply + withLoc( + typeFieldName -> typeTagPrinter(ex.typeTag), + kindFieldName -> "LetInEx", + "body" -> bodyJson, + "decls" -> factory.fromTraversable(declJsons) + ) + + case NullEx => + factory.mkObj(kindFieldName -> "NullEx") + } + } + + override def apply(decl: TlaDecl): T = { + def withLoc(fields: (String, T)*): T = withOptionalLoc(decl)(fields: _*) + decl match { + case TlaTheoremDecl(name, body) => + val bodyJson = apply(body) + withLoc( + typeFieldName -> typeTagPrinter(decl.typeTag), + kindFieldName -> "TlaTheoremDecl", + "name" -> name, + "body" -> bodyJson + ) + + case TlaVarDecl(name) => + withLoc( + typeFieldName -> typeTagPrinter(decl.typeTag), + kindFieldName -> "TlaVarDecl", + "name" -> name + ) + + case TlaConstDecl(name) => + withLoc( + typeFieldName -> typeTagPrinter(decl.typeTag), + kindFieldName -> "TlaConstDecl", + "name" -> name + ) + + case decl @ TlaOperDecl(name, formalParams, body) => + val bodyJson = apply(body) + val paramsJsons = formalParams map { + case SimpleFormalParam(paramName) => + factory.mkObj( + kindFieldName -> "SimpleFormalParam", + "name" -> paramName + ) + case OperFormalParam(paramName, arity) => + factory.mkObj( + kindFieldName -> "OperFormalParam", + "name" -> paramName, + "arity" -> arity + ) + } + withLoc( + typeFieldName -> typeTagPrinter(decl.typeTag), + kindFieldName -> "TlaOperDecl", + "name" -> name, + "formalParams" -> factory.fromTraversable(paramsJsons), + "isRecursive" -> decl.isRecursive, + "body" -> bodyJson + ) + + case TlaAssumeDecl(body) => + val bodyJson = apply(body) + withLoc( + typeFieldName -> typeTagPrinter(decl.typeTag), + kindFieldName -> "TlaAssumeDecl", + "body" -> bodyJson + ) + } } override def apply(module: TlaModule): T = { @@ -191,8 +224,17 @@ class TlaToJson[T <: JsonRepresentation](factory: JsonFactory[T])(implicit typTa apply(d) } factory.mkObj( + versionFieldName -> JsonVersion.current, kindFieldName -> "TlaModule", + "name" -> module.name, "declarations" -> factory.fromTraversable(declJsons) ) } } + +object TlaToJson { + val kindFieldName: String = "kind" + val typeFieldName: String = "type" + val sourceFieldName: String = "source" + val versionFieldName: String = "version" +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala index 7a297c6755..d4db947c08 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala @@ -2,8 +2,11 @@ package at.forsyte.apalache.io.json.impl import at.forsyte.apalache.io.json.TlaToJson import at.forsyte.apalache.tla.lir.io.TypeTagPrinter +import at.forsyte.apalache.tla.lir.storage.SourceLocator /** * A json encoder, using the UJson representation */ -class TlaToUJson(implicit typTagPrinter: TypeTagPrinter) extends TlaToJson[UJsonRep](UJsonFactory)(typTagPrinter) +class TlaToUJson(locatorOpt: Option[SourceLocator] = None)( + implicit typeTagPrinter: TypeTagPrinter +) extends TlaToJson[UJsonRep](UJsonFactory, locatorOpt)(typeTagPrinter) diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala index 649b89853e..148f99058c 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala @@ -7,4 +7,9 @@ import at.forsyte.apalache.io.json.JsonRepresentation */ sealed case class UJsonRep(protected[json] val value: ujson.Value) extends JsonRepresentation { override def toString: String = ujson.write(value, indent = 2, escapeUnicode = false) + + override def getFieldOpt(fieldName: String): Option[this.type] = { + if (!value.obj.contains(fieldName)) None + else Some(UJsonRep(value(fieldName)).asInstanceOf[UJsonRep.this.type]) + } } diff --git a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala index 3e67b1c247..08eb8ac5bd 100644 --- a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala +++ b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala @@ -18,7 +18,7 @@ class TestTlaToUJson extends FunSuite with BeforeAndAfterEach with TestingPredef } val enc = new TlaToUJson - val kindField = enc.kindFieldName + val kindField = TlaToJson.kindFieldName def getEncVal(ex: TlaEx): ujson.Value = enc(ex).value def getEncVal(decl: TlaDecl): ujson.Value = enc(decl).value diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala index 036f69f1f4..00b2aee816 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala @@ -81,7 +81,8 @@ class EtcTypeCheckerPassImpl @Inject() (val options: PassOptions, val sourceStor val outFile = new File(outdir.toFile, s"out-$prefix-$name.json") val writer = new PrintWriter(new FileWriter(outFile, false)) try { - val jsonText = new TlaToUJson().apply(module).toString + val sourceLocator: SourceLocator = SourceLocator(sourceStore.makeSourceMap, changeListener) + val jsonText = new TlaToUJson(Some(sourceLocator)).apply(module).toString writer.write(jsonText) logger.debug(" > JSON output: " + outFile) } finally { From db7ed1493e96680c75960d5019b3f6c9460ea6df Mon Sep 17 00:00:00 2001 From: Kukovec Date: Sun, 11 Apr 2021 15:18:14 +0200 Subject: [PATCH 3/6] Update docs/src/adr/005adr-json.md Co-authored-by: Igor Konnov --- docs/src/adr/005adr-json.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md index 1ee8e514ba..09afcdce2a 100644 --- a/docs/src/adr/005adr-json.md +++ b/docs/src/adr/005adr-json.md @@ -162,7 +162,7 @@ The `value` field depends on the kind of `TlaValue`: 1. For `TlaBool`: a JSON Boolean 1. For `TlaInt(bigIntValue)`: 1. If `bigIntValue.isValidInt`: a JSON number - 2. Otherwise: `{ "bigInt: bigIntValue.toString() }` + 2. Otherwise: `{ "bigInt": bigIntValue.toString() }` 1. For `TlaDecimal(decValue)`: a JSON string `decValue.toString` The reason for the non-uniform treatment of integers, is that Apalache encodes its TLA+ integers as `BigInt`, which means that it permits values, for which `.isValidInt` does not hold. From 8673ede3d85f46488fe6e5aab99cd41a343099b9 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Sun, 11 Apr 2021 15:41:48 +0200 Subject: [PATCH 4/6] Comments --- docs/src/adr/005adr-json.md | 18 +++++++++++++----- .../forsyte/apalache/io/json/JsonEncoder.scala | 1 + .../forsyte/apalache/io/json/TlaToJson.scala | 14 ++++++++++---- .../passes/EtcTypeCheckerPassImpl.scala | 2 +- 4 files changed, 25 insertions(+), 10 deletions(-) diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md index 09afcdce2a..b0b1ffd930 100644 --- a/docs/src/adr/005adr-json.md +++ b/docs/src/adr/005adr-json.md @@ -104,17 +104,25 @@ Example: } ``` -## 5. Version information -JSON serializations of `TlaModule`s contain a filed named `version`, holding a string representation of the current JSON encoding version, shaped `{major}.{minor}`. +## 5. Root wrapper +JSON serializations of one or more `TlaModule`s are wrapped in a root object with two required fields: + -`version`, the value of which is a string representation of the current JSON encoding version, shaped `{major}.{minor}`, and + -`modules`, the value of which is an array containing the JSON encodings of zero or more `TlaModule`s +It may optionally contain a field `"name" : "ApalacheIR"`. This document defines JSON Version 1.0. If and when a different JSON version is defined, this document will be updated accordingly. Apalache may refuse to import, or trigger warnings for, JSON objects with obsolete versions of the encoding in the future. Example: ``` { - "kind": "TlaModule", - "name": "MyModule", + "name": "ApalacheIR", "version": "1.0" - ... + "modules" = [ + { + "kind": "TlaModule", + "name": "MyModule", + ... + }, + ...] } ``` diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala index f6a8ffdab6..3a38a9a1e8 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala @@ -10,4 +10,5 @@ trait JsonEncoder[T <: JsonRepresentation] { def apply(ex: TlaEx): T def apply(decl: TlaDecl): T def apply(module: TlaModule): T + def makeRoot(modules: Traversable[TlaModule]): T } diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala index 12e38eb8ea..c378070d86 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala @@ -220,16 +220,22 @@ class TlaToJson[T <: JsonRepresentation]( } override def apply(module: TlaModule): T = { - val declJsons = module.declarations map { d => - apply(d) - } + val declJsons = module.declarations map apply factory.mkObj( - versionFieldName -> JsonVersion.current, kindFieldName -> "TlaModule", "name" -> module.name, "declarations" -> factory.fromTraversable(declJsons) ) } + + override def makeRoot(modules: Traversable[TlaModule]): T = { + val moduleJsons = modules map apply + factory.mkObj( + "name" -> "ApalacheIR", + versionFieldName -> JsonVersion.current, + "modules" -> factory.fromTraversable(moduleJsons) + ) + } } object TlaToJson { diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala index 00b2aee816..f36fe16377 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala @@ -82,7 +82,7 @@ class EtcTypeCheckerPassImpl @Inject() (val options: PassOptions, val sourceStor val writer = new PrintWriter(new FileWriter(outFile, false)) try { val sourceLocator: SourceLocator = SourceLocator(sourceStore.makeSourceMap, changeListener) - val jsonText = new TlaToUJson(Some(sourceLocator)).apply(module).toString + val jsonText = new TlaToUJson(Some(sourceLocator)).makeRoot(Seq(module)).toString writer.write(jsonText) logger.debug(" > JSON output: " + outFile) } finally { From 3500ed47e3e22b6d7cae33cee044897c7e54c47e Mon Sep 17 00:00:00 2001 From: Kukovec Date: Mon, 12 Apr 2021 15:31:27 +0200 Subject: [PATCH 5/6] Reader components --- .../apalache/io/json/JsonDecoder.scala | 15 ++ .../io/json/JsonDeserializationError.scala | 4 + .../forsyte/apalache/io/json/JsonToTla.scala | 211 ++++++++++++++++++ .../apalache/io/json/ScalaFactory.scala | 13 ++ .../forsyte/apalache/io/json/TlaToJson.scala | 3 - .../apalache/io/json/impl/UJsonRep.scala | 13 +- .../io/json/impl/UJsonScalaFactory.scala | 26 +++ .../apalache/io/json/impl/UJsonToTla.scala | 11 + .../apalache/io/json/TestUJsonToTla.scala | 66 ++++++ .../apalache/tla/lir/io/TypeTagReader.scala | 15 ++ 10 files changed, 370 insertions(+), 7 deletions(-) create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDecoder.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDeserializationError.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/json/ScalaFactory.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonScalaFactory.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonToTla.scala create mode 100644 tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TypeTagReader.scala diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDecoder.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDecoder.scala new file mode 100644 index 0000000000..ea89e7e92a --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDecoder.scala @@ -0,0 +1,15 @@ +package at.forsyte.apalache.io.json + +import at.forsyte.apalache.tla.lir.{TlaDecl, TlaEx, TlaModule} + +/** + * A JsonDecoder defines a conversion from a json (as represented by T) to a TLA+ expression/declaration/module + * + * @tparam T Any class extending JsonRepresentation + */ +trait JsonDecoder[T <: JsonRepresentation] { + def asTlaModule(moduleJson: T): TlaModule + def asTlaDecl(declJson: T): TlaDecl + def asTlaEx(exJson: T): TlaEx + def fromRoot(rootJson: T): Traversable[TlaModule] +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDeserializationError.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDeserializationError.scala new file mode 100644 index 0000000000..16bdbd5b9a --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDeserializationError.scala @@ -0,0 +1,4 @@ +package at.forsyte.apalache.io.json + +/** Thrown, when importing from JSON fails, due to malformed input */ +class JsonDeserializationError(msg: String) extends Exception(msg) 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 new file mode 100644 index 0000000000..0c3a0c4b33 --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala @@ -0,0 +1,211 @@ +package at.forsyte.apalache.io.json + +import at.forsyte.apalache.tla.imp.src.{SourceLocation, SourceStore} +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.lir.src.{SourceLocation, SourcePosition, SourceRegion} +import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaDecimal, TlaInt, TlaStr} +import convenience.tla +import UntypedPredefs._ +import at.forsyte.apalache.tla.lir.io.TypeTagReader + +/** + * A semi-abstraction of a json decoder. + * It is independent of the concrete JsonRepresentation, resp. ScalaFactory implementation. + * Inverse to TlaToJson, i.e. as{X}( TlaToJson( a : X) ) == a, where X = TlaEx/TlaDecl/TlaModule + */ + +class JsonToTla[T <: JsonRepresentation]( + scalaFactory: ScalaFactory[T], sourceStoreOpt: Option[SourceStore] = None +)(implicit typeTagReader: TypeTagReader) + extends JsonDecoder[T] { + + private def missingField(fieldName: String): JsonDeserializationError = + new JsonDeserializationError(s"JSON has no field named [$fieldName].") + + private def getOrThrow(json: T, fieldName: String): T = + json.getFieldOpt(fieldName).getOrElse { throw missingField(fieldName) } + + private def asFParam(json: T): FormalParam = { + val nameField = getOrThrow(json, "name") + val name = scalaFactory.asStr(nameField) + + val kindField = getOrThrow(json, TlaToJson.kindFieldName) + val kind = scalaFactory.asStr(kindField) + + kind match { + case "SimpleFormalParam" => + SimpleFormalParam(name) + case "OperFormalParam" => + val arityField = getOrThrow(json, "arity") + val arity = scalaFactory.asInt(arityField) + OperFormalParam(name, arity) + case _ => throw new JsonDeserializationError(s"$kind is not a valid FormalParam kind") + } + } + + private def asTlaVal(json: T): TlaValue = { + val kindField = getOrThrow(json, TlaToJson.kindFieldName) + val kind = scalaFactory.asStr(kindField) + + kind match { + case "TlaStr" => + val valField = getOrThrow(json, "value") + val valStr = scalaFactory.asStr(valField) + TlaStr(valStr) + case "TlaDecimal" => + val valField = getOrThrow(json, "value") + val valStr = scalaFactory.asStr(valField) + val dec = BigDecimal(valStr) + TlaDecimal(dec) + case "TlaInt" => + val valField = getOrThrow(json, "value") + val bi = valField.getFieldOpt("bigInt") map { biField => + BigInt(scalaFactory.asStr(biField)) + } getOrElse { + BigInt(scalaFactory.asInt(valField)) + } + TlaInt(bi) + case "TlaBool" => + val valField = getOrThrow(json, "value") + val valBool = scalaFactory.asBool(valField) + TlaBool(valBool) + case _ => throw new JsonDeserializationError(s"$kind is not a valid TlaValue kind") + } + } + + def getSourceLocationOpt(json: T): Option[SourceLocation] = for { + sourceObj <- json.getFieldOpt(TlaToJson.sourceFieldName) + fileName <- sourceObj.getFieldOpt("filename") map scalaFactory.asStr + fromObj <- sourceObj.getFieldOpt("from") + toObj <- sourceObj.getFieldOpt("to") + fromLine <- fromObj.getFieldOpt("line") map scalaFactory.asInt + fromCol <- fromObj.getFieldOpt("column") map scalaFactory.asInt + toLine <- toObj.getFieldOpt("line") map scalaFactory.asInt + toCol <- toObj.getFieldOpt("column") map scalaFactory.asInt + } yield SourceLocation( + fileName, + SourceRegion( + SourcePosition(fromLine, fromCol), + SourcePosition(toLine, toCol) + ) + ) + + def setLoc(identifiable: Identifiable, locationOpt: Option[SourceLocation]): Unit = + sourceStoreOpt foreach { store => + locationOpt foreach { loc => + store.add(identifiable.ID, loc) + } + } + + override def asTlaModule(moduleJson: T): TlaModule = { + val kindField = getOrThrow(moduleJson, TlaToJson.kindFieldName) + val kind = scalaFactory.asStr(kindField) + if (kind != "TlaModule") + throw new JsonDeserializationError(s"JSON kind is $kind, expected TlaModule") + + val nameField = getOrThrow(moduleJson, "name") + val name = scalaFactory.asStr(nameField) + val declField = getOrThrow(moduleJson, "declarations") + val declObjSeq = scalaFactory.asSeq(declField) + val decls = declObjSeq map asTlaDecl + + new TlaModule(name, decls) + } + + override def asTlaDecl(declJson: T): TlaDecl = { + val typeField = getOrThrow(declJson, TlaToJson.typeFieldName) + val tag = scalaFactory.asStr(typeField) + val typeTag = typeTagReader(tag) + val kindField = getOrThrow(declJson, TlaToJson.kindFieldName) + val kind = scalaFactory.asStr(kindField) + val decl = kind match { + case "TlaTheoremDecl" => + val nameField = getOrThrow(declJson, "name") + val name = scalaFactory.asStr(nameField) + val bodyField = getOrThrow(declJson, "body") + val body = asTlaEx(bodyField) + TlaTheoremDecl(name, body)(typeTag) + case "TlaVarDecl" => + val nameField = getOrThrow(declJson, "name") + val name = scalaFactory.asStr(nameField) + TlaVarDecl(name)(typeTag) + case "TlaConstDecl" => + val nameField = getOrThrow(declJson, "name") + val name = scalaFactory.asStr(nameField) + TlaConstDecl(name)(typeTag) + case "TlaOperDecl" => + val nameField = getOrThrow(declJson, "name") + val name = scalaFactory.asStr(nameField) + val recField = getOrThrow(declJson, "isRecursive") + val isRecursive = scalaFactory.asBool(recField) + val bodyField = getOrThrow(declJson, "body") + val body = asTlaEx(bodyField) + val paramsField = getOrThrow(declJson, "formalParams") + val paramsObjList = scalaFactory.asSeq(paramsField).toList + val fParams = paramsObjList map asFParam + val opDecl = TlaOperDecl(name, fParams, body)(typeTag) + opDecl.isRecursive = isRecursive + opDecl + + case "TlaAssumeDecl" => + val bodyField = getOrThrow(declJson, "body") + val body = asTlaEx(bodyField) + TlaAssumeDecl(body)(typeTag) + case _ => throw new JsonDeserializationError(s"$kind is not a valid TlaDecl kind") + } + setLoc(decl, getSourceLocationOpt(declJson)) + decl + } + + override def asTlaEx(exJson: T): TlaEx = { + val kindField = getOrThrow(exJson, TlaToJson.kindFieldName) + val kind = scalaFactory.asStr(kindField) + if (kind == "NullEx") NullEx // TODO: We really shouldn't support NullEx long-term + val typeField = getOrThrow(exJson, TlaToJson.typeFieldName) + val tag = scalaFactory.asStr(typeField) + val typeTag = typeTagReader(tag) + val ex = kind match { + case "NameEx" => + val nameField = getOrThrow(exJson, "name") + val name = scalaFactory.asStr(nameField) + NameEx(name)(typeTag) + case "ValEx" => + val valueField = getOrThrow(exJson, "value") + val value = asTlaVal(valueField) + ValEx(value)(typeTag) + case "OperEx" => + val operField = getOrThrow(exJson, "oper") + val operString = scalaFactory.asStr(operField) + val argsField = getOrThrow(exJson, "args") + val argsObjSeq = scalaFactory.asSeq(argsField) + // TODO: Implement a oper.name -> oper mapping and avoid Builder hackery + val args = argsObjSeq map asTlaEx map { BuilderTlaExWrapper } + tla.byName(operString, args: _*).withTag(typeTag) + case "LetInEx" => + val bodyField = getOrThrow(exJson, "body") + val body = asTlaEx(bodyField) + val declsField = getOrThrow(exJson, "decls") + val declsObjSeq = scalaFactory.asSeq(declsField) + val decls = declsObjSeq map asTlaDecl + assert(decls forall { _.isInstanceOf[TlaOperDecl] }) + val operDecls = decls map { _.asInstanceOf[TlaOperDecl] } + LetInEx(body, operDecls: _*)(typeTag) + case _ => throw new JsonDeserializationError(s"$kind is not a valid TlaEx kind") + } + setLoc(ex, getSourceLocationOpt(exJson)) + ex + } + + override def fromRoot(rootJson: T): Traversable[TlaModule] = { + val versionField = getOrThrow(rootJson, TlaToJson.versionFieldName) + val version = scalaFactory.asStr(versionField) + val current = JsonVersion.current + if (version != current) + throw new JsonDeserializationError(s"JSON version is $version, expected $current.") + + val modulesField = getOrThrow(rootJson, "modules") + val modulesObjSeq = scalaFactory.asSeq(modulesField) + + modulesObjSeq map asTlaModule + } +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/ScalaFactory.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/ScalaFactory.scala new file mode 100644 index 0000000000..3157cda824 --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/ScalaFactory.scala @@ -0,0 +1,13 @@ +package at.forsyte.apalache.io.json + +/** + * Generates Scala primitives/collections from JSON primitives/arrays. + * Inverse to JsonFactory, i.e. as{X}( JsonFactory.from{x}(v: X) ) == v, for X = Int/Str/Bool/Traversable + * @tparam T Any class extending JsonRepresentation + */ +trait ScalaFactory[T <: JsonRepresentation] { + def asInt(json: T): Int + def asStr(json: T): String + def asBool(json: T): Boolean + def asSeq(json: T): Seq[T] +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala index c378070d86..8ce8191e42 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala @@ -50,9 +50,6 @@ import at.forsyte.apalache.tla.lir.storage.SourceLocator * } * ] * } - * - * @param factory A json factory for the `T` variant of JsonRepresentation - * @tparam T Any class extending JsonRepresentation */ class TlaToJson[T <: JsonRepresentation]( factory: JsonFactory[T], locatorOpt: Option[SourceLocator] = None diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala index 148f99058c..909504a143 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala @@ -8,8 +8,13 @@ import at.forsyte.apalache.io.json.JsonRepresentation sealed case class UJsonRep(protected[json] val value: ujson.Value) extends JsonRepresentation { override def toString: String = ujson.write(value, indent = 2, escapeUnicode = false) - override def getFieldOpt(fieldName: String): Option[this.type] = { - if (!value.obj.contains(fieldName)) None - else Some(UJsonRep(value(fieldName)).asInstanceOf[UJsonRep.this.type]) - } + /** + * If `this` represents a JSON object defining a field + * `fieldName : val`, the method returns a Some(_), containing the representation of `val`, + * otherwise (if `this` is not an object or if it does not define a `fieldName` field) returns None. + */ + override def getFieldOpt(fieldName: String): Option[this.type] = for { + objAsMap <- value.objOpt + fieldVal <- objAsMap.get(fieldName) + } yield UJsonRep(fieldVal).asInstanceOf[UJsonRep.this.type] } diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonScalaFactory.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonScalaFactory.scala new file mode 100644 index 0000000000..f97a0fbb9b --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonScalaFactory.scala @@ -0,0 +1,26 @@ +package at.forsyte.apalache.io.json.impl + +import at.forsyte.apalache.io.json.{JsonDeserializationError, ScalaFactory} + +/** + * ScalaFactory for the UJsonRep variant of JsonRepresentation + */ +object UJsonScalaFactory extends ScalaFactory[UJsonRep] { + override def asInt(json: UJsonRep): Int = + json.value.numOpt map { _.toInt } getOrElse { + throw new JsonDeserializationError("Not an integer.") + } + + override def asStr(json: UJsonRep): String = json.value.strOpt getOrElse { + throw new JsonDeserializationError("Not a string.") + } + + override def asBool(json: UJsonRep): Boolean = json.value.boolOpt getOrElse { + throw new JsonDeserializationError("Not a Boolean.") + } + + override def asSeq(json: UJsonRep): Seq[UJsonRep] = + json.value.arrOpt map { _ map UJsonRep } getOrElse { + throw new JsonDeserializationError("Not an array.") + } +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonToTla.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonToTla.scala new file mode 100644 index 0000000000..835e2ac358 --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonToTla.scala @@ -0,0 +1,11 @@ +package at.forsyte.apalache.io.json.impl + +import at.forsyte.apalache.io.json.JsonToTla +import at.forsyte.apalache.tla.imp.src.SourceStore +import at.forsyte.apalache.tla.lir.io.TypeTagReader + +/** + * A json decoder, using the UJson representation + */ +class UJsonToTla(sourceStoreOpt: Option[SourceStore] = None)(implicit typeTagReader: TypeTagReader) + extends JsonToTla[UJsonRep](UJsonScalaFactory, sourceStoreOpt)(typeTagReader) diff --git a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala new file mode 100644 index 0000000000..236f0d8902 --- /dev/null +++ b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala @@ -0,0 +1,66 @@ +package at.forsyte.apalache.io.json + +import at.forsyte.apalache.io.json.impl.{TlaToUJson, UJsonToTla} +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.lir.convenience.tla +import org.junit.runner.RunWith +import org.scalatest.{BeforeAndAfterEach, FunSuite} +import org.scalatest.junit.JUnitRunner +import at.forsyte.apalache.tla.lir.UntypedPredefs._ +import at.forsyte.apalache.tla.lir.io.{TypeTagPrinter, UntypedReader} + +@RunWith(classOf[JUnitRunner]) +class TestUJsonToTla extends FunSuite with BeforeAndAfterEach with TestingPredefs { + implicit val reader = UntypedReader + implicit val printer = new TypeTagPrinter { + override def apply(tag: TypeTag): String = "" + } + + val dec = new UJsonToTla(sourceStoreOpt = None) + val enc = new TlaToUJson(locatorOpt = None) + + test("dec(enc(x)) =?= x") { + val exs: Seq[TlaEx] = Seq( + tla.and(tla.name("x"), tla.bool(true)), + tla.ite(tla.name("p"), tla.name("A"), tla.name("B")), + tla.letIn( + tla.appOp(tla.name("A"), tla.int(1)), + tla + .declOp( + "A", + tla.plus(tla.name("p"), tla.int(1)), + SimpleFormalParam("p") + ) + .withTag(Untyped()) + .asInstanceOf[TlaOperDecl] + ) + ) + + exs foreach { ex => + assert(dec.asTlaEx(enc(ex)) == ex) + } + + val decls: Seq[TlaDecl] = Seq( + tla.declOp("X", tla.eql(tla.name("a"), tla.int(1)), SimpleFormalParam("a")), + TlaAssumeDecl(tla.eql(tla.int(1), tla.int(0))), + TlaConstDecl("c"), + TlaVarDecl("v") + ) + + decls foreach { decl => + assert(dec.asTlaDecl(enc(decl)) == decl) + } + + val modules: Seq[TlaModule] = Seq( + new TlaModule("Empty", Seq.empty), + new TlaModule("Module", decls) + ) + + modules foreach { m => + assert(dec.asTlaModule(enc(m)) == m) + } + + assert(dec.fromRoot(enc.makeRoot(modules)) == modules) + } + +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TypeTagReader.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TypeTagReader.scala new file mode 100644 index 0000000000..8e6d8eff3e --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TypeTagReader.scala @@ -0,0 +1,15 @@ +package at.forsyte.apalache.tla.lir.io + +import at.forsyte.apalache.tla.lir.{TypeTag, Untyped} + +/** + * Recovers TypeTags from their string representations. + * Inverse of TypeTagPrinter. + */ +trait TypeTagReader { + def apply(tagStr: String): TypeTag +} + +object UntypedReader extends TypeTagReader { + override def apply(tagStr: String): TypeTag = Untyped() +} From 785f9c5937eefa087145de80ebfba109b4d41aa1 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Mon, 19 Apr 2021 15:32:28 +0200 Subject: [PATCH 6/6] Post-rebase fixes --- docs/src/adr/005adr-json.md | 6 +++--- .../at/forsyte/apalache/io/json/JsonToTla.scala | 15 ++++++--------- .../forsyte/apalache/io/json/TestUJsonToTla.scala | 4 ++-- 3 files changed, 11 insertions(+), 14 deletions(-) diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md index b0b1ffd930..0de1643756 100644 --- a/docs/src/adr/005adr-json.md +++ b/docs/src/adr/005adr-json.md @@ -160,8 +160,8 @@ Since both sub-expressions, the literals `1`, are identical, their serialization Observe that we choose to serialize `TlaValue` as a JSON object, which is more verbose, but trivial to deserialize. It has the following shape ``` { - "kind": _ , - "value": _ + "kind": , + "value": } ``` @@ -184,7 +184,7 @@ Take `jsonOf1` to be the serialization of `ValEx( TlaInt( 1 ) )( typeTag = Typed { "kind": "OperEx", "type": "Int", - "oper": "(+)", + "oper": "PLUS", "args": [jsonOf1, jsonOf1] } ``` 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 index 0c3a0c4b33..08ceccab04 100644 --- 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 @@ -25,21 +25,18 @@ class JsonToTla[T <: JsonRepresentation]( private def getOrThrow(json: T, fieldName: String): T = json.getFieldOpt(fieldName).getOrElse { throw missingField(fieldName) } - private def asFParam(json: T): FormalParam = { - val nameField = getOrThrow(json, "name") - val name = scalaFactory.asStr(nameField) - + private def asFParam(json: T): OperParam = { val kindField = getOrThrow(json, TlaToJson.kindFieldName) val kind = scalaFactory.asStr(kindField) kind match { - case "SimpleFormalParam" => - SimpleFormalParam(name) - case "OperFormalParam" => + case "OperParam" => + val nameField = getOrThrow(json, "name") + val name = scalaFactory.asStr(nameField) val arityField = getOrThrow(json, "arity") val arity = scalaFactory.asInt(arityField) - OperFormalParam(name, arity) - case _ => throw new JsonDeserializationError(s"$kind is not a valid FormalParam kind") + OperParam(name, arity) + case _ => throw new JsonDeserializationError(s"$kind is not a valid OperParam kind") } } diff --git a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala index 236f0d8902..df0efc4f91 100644 --- a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala +++ b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala @@ -29,7 +29,7 @@ class TestUJsonToTla extends FunSuite with BeforeAndAfterEach with TestingPredef .declOp( "A", tla.plus(tla.name("p"), tla.int(1)), - SimpleFormalParam("p") + OperParam("p") ) .withTag(Untyped()) .asInstanceOf[TlaOperDecl] @@ -41,7 +41,7 @@ class TestUJsonToTla extends FunSuite with BeforeAndAfterEach with TestingPredef } val decls: Seq[TlaDecl] = Seq( - tla.declOp("X", tla.eql(tla.name("a"), tla.int(1)), SimpleFormalParam("a")), + tla.declOp("X", tla.eql(tla.name("a"), tla.int(1)), OperParam("a")), TlaAssumeDecl(tla.eql(tla.int(1), tla.int(0))), TlaConstDecl("c"), TlaVarDecl("v")