Skip to content

Commit

Permalink
#121 JsonReader: add IF, CASE, stutter, fairness
Browse files Browse the repository at this point in the history
  • Loading branch information
@andrey-kuprianov
andrey-kuprianov committed May 18, 2020
1 parent eb3f101 commit bd57c12
Showing 1 changed file with 65 additions and 35 deletions.
100 changes: 65 additions & 35 deletions tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/JsonReader.scala
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package at.forsyte.apalache.tla.lir.io

import at.forsyte.apalache.tla.lir._
import at.forsyte.apalache.tla.lir.oper.{TlaFunOper, TlaOper}
import at.forsyte.apalache.tla.lir.oper.{TlaControlOper, TlaFunOper, TlaOper}
import at.forsyte.apalache.tla.lir.values._

import scala.collection.immutable.HashMap
Expand All @@ -21,10 +21,13 @@ object JsonReader {

val unaryOps = JsonWriter.unaryOps.map(_.swap)
val naryOps = JsonWriter.naryOps.map(_.swap)
val naryPairOps = JsonWriter.naryPairOps.map(_.swap)
val functionalOps = JsonWriter.functionalOps.map(_.swap)
val boundedPredOps = JsonWriter.boundedPredOps.map(_.swap)
val unboundedPredOps = JsonWriter.unboundedPredOps.map(_.swap)
val otherOps = Set("str", "int", "set", "apply-fun", "apply-op")
val stutterOps = JsonWriter.stutterOps.map(_.swap)
val fairnessOps = JsonWriter.fairnessOps.map(_.swap)
val otherOps = Set("str", "int", "set", "apply-fun", "apply-op", "IF", "CASE")

val sets = HashMap(
"BOOLEAN" -> TlaBoolSet,
Expand All @@ -51,13 +54,16 @@ object JsonReader {
// expect ujson.Value to be an encoding of TLA+ expression
def parseExpr(m: LinkedHashMap[String, ujson.Value]): TlaEx = {
val unary = m.keySet & unaryOps.keySet
val nary = m.keySet & naryOps.keySet
val naryPair = m.keySet & naryPairOps.keySet
val functional = m.keySet & functionalOps.keySet
val boundedPred = m.keySet & boundedPredOps.keySet
val unboundedPred = m.keySet & unboundedPredOps.keySet
val nary = m.keySet & naryOps.keySet
val stutter = m.keySet & stutterOps.keySet
val fairness = m.keySet & fairnessOps.keySet
val other = m.keySet & otherOps
val ourKeys = unary.size + nary.size + functional.size +
+ boundedPred.size + unboundedPred.size + other.size
val ourKeys = unary.size + nary.size + naryPair.size + functional.size +
+ boundedPred.size + unboundedPred.size + stutter.size + fairness.size + other.size
if(ourKeys < 1)
throw new Exception("incorrect TLA+ JSON: expected expression, but none found")
else if(ourKeys > 1)
Expand All @@ -66,6 +72,9 @@ object JsonReader {
OperEx(unaryOps(unary.head), parseJson(m(unary.head)))
else if(nary.nonEmpty)
OperEx(naryOps(nary.head), parseArray(m(nary.head)):_*)
else if(naryPair.nonEmpty) {
OperEx(naryPairOps(naryPair.head), parsePairs(m(naryPair.head)) :_*)
}
else if(functional.nonEmpty) {
if(!m.contains("where"))
throw new Exception("incorrect TLA+ JSON: expecting 'where'")
Expand All @@ -82,41 +91,62 @@ object JsonReader {
throw new Exception("incorrect TLA+ JSON: expecting 'that'")
OperEx(boundedPredOps(boundedPred.head), nameSet(0), nameSet(1), parseJson(m("that")))
}
else if(stutter.nonEmpty) {
if(!m.contains("vars"))
throw new Exception("incorrect TLA+ JSON: expecting 'vars'")
OperEx(stutterOps(stutter.head), parseJson(m(stutter.head)), parseJson(m("vars")))
}
else if(fairness.nonEmpty) {
if(!m.contains("vars"))
throw new Exception("incorrect TLA+ JSON: expecting 'vars'")
OperEx(fairnessOps(fairness.head), parseJson(m("vars")), parseJson(m(fairness.head)))
}
else if(other.nonEmpty) {
if(other.head == "str")
ValEx(TlaStr(parseStr(m("str"))))
else if(other.head == "int")
ValEx(TlaInt(BigInt(parseStr(m("int")))))
else if(other.head == "set") {
val set = parseStr(m("set"))
if(sets.contains(set))
ValEx(sets(set))
else
throw new Exception("can't parse TLA+ JSON: reference to unknown set")
}
else if(other.head == "apply-fun") {
if(!m.contains("arg"))
throw new Exception("incorrect TLA+ JSON: expecting 'arg'")
OperEx(TlaFunOper.app, parseJson(m("apply-fun")), parseJson(m("arg")))
}
else if(other.head == "apply-op") {
if(!m.contains("args"))
throw new Exception("incorrect TLA+ JSON: expecting 'args'")
val name = parseStr(m("apply-op"))
val args = parseArray(m("args"))
if(name == "rec-fun-ref") {
if(args.nonEmpty)
throw new Exception("incorrect TLA+ JSON: found arguments for 'rec-fun-ref'")
OperEx(TlaFunOper.recFunRef)
other.head match {
case "str" => ValEx(TlaStr(parseStr(m("str"))))
case "int" => ValEx(TlaInt(BigInt(parseStr(m("int")))))
case "set" => {
val set = parseStr(m("set"))
if(sets.contains(set))
ValEx(sets(set))
else
throw new Exception("can't parse TLA+ JSON: reference to unknown set")
}
case "apply-fun" => {
if(!m.contains("arg"))
throw new Exception("incorrect TLA+ JSON: expecting 'arg'")
OperEx(TlaFunOper.app, parseJson(m("apply-fun")), parseJson(m("arg")))
}
case "apply-op" => {
if(!m.contains("args"))
throw new Exception("incorrect TLA+ JSON: expecting 'args'")
val name = parseStr(m("apply-op"))
val args = parseArray(m("args"))
if(name == "rec-fun-ref") {
if(args.nonEmpty)
throw new Exception("incorrect TLA+ JSON: found arguments for 'rec-fun-ref'")
OperEx(TlaFunOper.recFunRef)
}
else
OperEx(TlaOper.apply, NameEx(name) +: args:_*)
}
case "IF" => {
if(!m.contains("THEN") || !m.contains("ELSE"))
throw new Exception("incorrect TLA+ JSON: malformed 'IF'")
OperEx(TlaControlOper.ifThenElse, parseJson(m("IF")), parseJson(m("THEN")), parseJson(m("ELSE")))
}
case "CASE" => {
if(m.contains("OTHER"))
OperEx(TlaControlOper.caseWithOther, parseJson(m("OTHER")) +: parsePairs(m("CASE")) :_*)
else
OperEx(TlaControlOper.caseNoOther, parsePairs(m("CASE")):_*)
}
else
OperEx(TlaOper.apply, NameEx(name) +: args:_*)
case _ =>
throw new Exception("can't parse TLA+ JSON: unknown JSON key")
}
else
throw new Exception("can't parse TLA+ JSON: unknown JSON key")
}
else
throw new Exception("can't parse TLA+ JSON: unknown JSON key")
throw new Exception("can't parse TLA+ JSON: cannot find a known JSON key")
}

// expect ujson.Value to be a string
Expand Down

0 comments on commit bd57c12

Please sign in to comment.