A builder for TLA expressions. A singleton instance of this class is defined in *.lir.convenience.
@@ -144,7 +144,7 @@ class Builder { /** Declarations */ - def declOp(name: String, body: BuilderEx, params: FormalParam*): BuilderOperDecl = { + def declOp(name: String, body: BuilderEx, params: OperParam*): BuilderOperDecl = { BuilderOperDecl(name, params.toList, body) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/FormalParam.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/FormalParam.scala deleted file mode 100644 index 04f71dfdf0..0000000000 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/FormalParam.scala +++ /dev/null @@ -1,19 +0,0 @@ -package at.forsyte.apalache.tla.lir - -/** - * A formal parameter of an operator. - */ -sealed abstract class FormalParam extends Serializable { - def name: String - - def arity: Int - -} - -/** An ordinary formal parameter, e.g., x used in A(x) == ... */ -case class SimpleFormalParam(name: String) extends FormalParam with Serializable { - override def arity: Int = 0 -} - -/** A function signature, e.g., f(_, _) used in A(f(_, _), x, y) */ -case class OperFormalParam(name: String, arity: Int) extends FormalParam with Serializable {} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/OperParam.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/OperParam.scala new file mode 100644 index 0000000000..c318854db2 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/OperParam.scala @@ -0,0 +1,23 @@ +package at.forsyte.apalache.tla.lir + +/** + * A formal parameter of an operator. A parameter is either: a value (`arity = 0`), or an operator (`arity > 0`). + * Higher-order operators have at least one parameter that is an operator itself. + * We declare `OperParam` as a case class, in order to have `equals` + * and pattern-matching. + */ +case class OperParam(val name: String, val arity: Int) extends Serializable { + + /** + * Is the parameter an operator. + * + * @return true, if the parameter is an operator + */ + def isOperator: Boolean = arity > 0 +} + +object OperParam { + def apply(name: String): OperParam = { + OperParam(name, 0) + } +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TestingPredefs.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TestingPredefs.scala index 34ff4d208e..ca281eca56 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TestingPredefs.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TestingPredefs.scala @@ -8,10 +8,10 @@ import at.forsyte.apalache.tla.lir.UntypedPredefs._ trait TestingPredefs { implicit def name(p_s: String): NameEx = NameEx(p_s) - implicit def sfp(p_s: String): SimpleFormalParam = SimpleFormalParam(p_s) + implicit def sfp(p_s: String): OperParam = OperParam(p_s) - implicit def ofp(p_pair: (String, Int)): OperFormalParam = - OperFormalParam(p_pair._1, p_pair._2) + implicit def ofp(p_pair: (String, Int)): OperParam = + OperParam(p_pair._1, p_pair._2) def n_a: NameEx = "a" diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala index 17b9472169..1dd96dda9c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala @@ -87,7 +87,7 @@ case class TlaAssumeDecl(body: TlaEx)(implicit typeTag: TypeTag) extends TlaDecl * @param formalParams formal parameters * @param body operator definition, that is a TLA+ expression that captures the operator definition */ -case class TlaOperDecl(name: String, formalParams: List[FormalParam], var body: TlaEx)(implicit typeTag: TypeTag) +case class TlaOperDecl(name: String, formalParams: List[OperParam], var body: TlaEx)(implicit typeTag: TypeTag) extends TlaDecl with Serializable { /** @@ -97,7 +97,7 @@ case class TlaOperDecl(name: String, formalParams: List[FormalParam], var body: // Temporary solution, until #345 is resolved def copy( - name: String = this.name, formalParams: List[FormalParam] = this.formalParams, body: TlaEx = this.body + name: String = this.name, formalParams: List[OperParam] = this.formalParams, body: TlaEx = this.body )(implicit copyTypeTag: TypeTag = typeTag): TlaOperDecl = { val ret = TlaOperDecl(name, formalParams, body)(copyTypeTag) ret.isRecursive = this.isRecursive diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/aux/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/aux/package.scala index 669989a27f..3770e1c045 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/aux/package.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/aux/package.scala @@ -90,19 +90,19 @@ package object aux { case (NameEx(n1), NameEx(n2)) if n1 == n2 => ex1 case (LetInEx(b1, decls1 @ _*), LetInEx(b2, decls2 @ _*)) => val defaultDecl = TlaOperDecl("Null", List.empty, NullEx) - val defaultParam = SimpleFormalParam("diffParam") + val defaultParam = OperParam("diffParam") val declDiff = decls1.zipAll(decls2, defaultDecl, defaultDecl) map { case (d1, d2) => if (d1.name == d2.name && d1.formalParams == d2.formalParams) d1.copy(body = diff(d1.body, d2.body)) else { val name = s"DiffDecl_${d1.name}_${d2.name}" val params = d1.formalParams.zipAll(d2.formalParams, defaultParam, defaultParam) map { - case (par1 @ SimpleFormalParam(p1), SimpleFormalParam(p2)) if p1 == p2 => + case (par1 @ OperParam(p1, 0), OperParam(p2, 0)) if p1 == p2 => par1 - case (par1 @ OperFormalParam(p1, n1), OperFormalParam(p2, n2)) if p1 == p2 && n1 == n2 => + case (par1 @ OperParam(p1, n1), OperParam(p2, n2)) if p1 == p2 && n1 == n2 => par1 case (par1, par2) => - SimpleFormalParam(s"DiffParam_${par1.name}_${par2.name}") + OperParam(s"DiffParam_${par1.name}_${par2.name}") } TlaOperDecl(name, params, diff(d1.body, d2.body)) } 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 index edeffb5bbb..945207df6d 100644 --- 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 @@ -292,7 +292,7 @@ object JsonReader { } // expect ujson.Value to be an encoding of TLA+ params array - def parseParams(v: ujson.Value): Seq[FormalParam] = { + def parseParams(v: ujson.Value): Seq[OperParam] = { // it should be a JSON array val arr = v.arrOpt match { case Some(value) => value @@ -302,7 +302,7 @@ object JsonReader { } // expect ujson.Value to be an encoding of a parameter - def parseParam(v: ujson.Value): FormalParam = { + def parseParam(v: ujson.Value): OperParam = { // it should be a JSON object val m = v.objOpt match { case Some(value) => value @@ -314,9 +314,6 @@ object JsonReader { ) throw new Exception("incorrect TLA+ JSON: malformed parameter") val arity = m("arity").num.toInt - if (arity == 0) - SimpleFormalParam(m("name").str) - else - OperFormalParam(m("name").str, arity) + OperParam(m("name").str, arity) } } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/JsonWriter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/JsonWriter.scala index c1e8f7c3e8..935f554c11 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/JsonWriter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/JsonWriter.scala @@ -134,7 +134,7 @@ class JsonWriter(writer: PrintWriter, indent: Int = 2)(implicit typeTag: TypeTag Obj("name" -> name, "arity" -> arity) } - private def operatorDef(name: String, params: Seq[FormalParam], body: TlaEx): ujson.Value = { + private def operatorDef(name: String, params: Seq[OperParam], body: TlaEx): ujson.Value = { Obj("operator" -> name, "body" -> toJson(body), "params" -> params.map(toJson)) } @@ -168,13 +168,8 @@ class JsonWriter(writer: PrintWriter, indent: Int = 2)(implicit typeTag: TypeTag } } - private def toJson(param: FormalParam): ujson.Value = { - param match { - case SimpleFormalParam(name) => - operFormalParam(name, 0) - case OperFormalParam(name, arity) => - operFormalParam(name, arity) - } + private def toJson(param: OperParam): ujson.Value = { + operFormalParam(param.name, param.arity) } // TODO: in LIR, do not see anything about function definitions, as allowed by TLA+ grammar (Andrey) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala index 3b34ec3cd0..9bea88326a 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/PrettyWriter.scala @@ -480,7 +480,7 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex if (!tod.isRecursive) text("") else - "RECURSIVE" <> space <> toDoc(OperFormalParam(name, params.length)) <> line + "RECURSIVE" <> space <> toDoc(OperParam(name, params.length)) <> line val paramsDoc = if (params.isEmpty) @@ -491,13 +491,11 @@ class PrettyWriter(writer: PrintWriter, textWidth: Int = 80, indent: Int = 2) ex } } - private def toDoc(param: FormalParam): Doc = { - param match { - case SimpleFormalParam(name) => - name - - case OperFormalParam(name, arity) => - group(name <> parens(ssep(List.fill(arity)("_"), "," <> softline))) + private def toDoc(param: OperParam): Doc = { + if (param.isOperator) { + group(param.name <> parens(ssep(List.fill(param.arity)("_"), "," <> softline))) + } else { + param.name } } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/Printer.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/Printer.scala index 475e9892fb..656e357299 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/Printer.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/Printer.scala @@ -220,7 +220,7 @@ object UTFPrinter extends Printer { * @return a string representation of TLA+ declaration */ override def apply(p_decl: TlaDecl): String = { - def pr_param(p: FormalParam): String = { + def pr_param(p: OperParam): String = { val arity = p.arity val params = if (arity == 0) "" else "(%s)".format(1.to(arity).map(_ => "_").mkString(", ")) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/IncrementalRenaming.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/IncrementalRenaming.scala index 6c136c545f..dd37a06ee2 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/IncrementalRenaming.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/IncrementalRenaming.scala @@ -233,9 +233,8 @@ class IncrementalRenaming @Inject() (tracker: TransformationTracker) extends Tla // Copy preserves typeTag and .isRecursive d.copy( name = opersAndFParamsNameMap(n), - formalParams = ps map { - case SimpleFormalParam(p) => SimpleFormalParam(opersAndFParamsNameMap(p)) - case OperFormalParam(p, a) => OperFormalParam(opersAndFParamsNameMap(p), a) + formalParams = ps map { case OperParam(p, a) => + OperParam(opersAndFParamsNameMap(p), a) }, // We recurse over operator bodies, because newRenamed contains parameter // and operator renamings @@ -281,9 +280,8 @@ class IncrementalRenaming @Inject() (tracker: TransformationTracker) extends Tla // Copy preserves typeTag and .isRecursive d.copy( name = offsetFn(n), - formalParams = params map { - case SimpleFormalParam(p) => SimpleFormalParam(offsetFn(p)) - case OperFormalParam(p, a) => OperFormalParam(offsetFn(p), a) + formalParams = params map { case OperParam(p, a) => + OperParam(offsetFn(p), a) }, body = self(b) ) diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala index f620b0f530..ec17e802b8 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala @@ -219,7 +219,7 @@ trait IrGenerators { nparams <- choose(0, maxArgs) params <- listOfN(nparams, identifier) tt <- genTypeTag - } yield TlaOperDecl(name, params map (n => SimpleFormalParam(n)), body).withTag(tt) + } yield TlaOperDecl(name, params map (n => OperParam(n)), body).withTag(tt) } /** diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala index 508fab4b3c..27eadd5772 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala @@ -15,9 +15,9 @@ class TestAux extends FunSuite with TestingPredefs { val ar0Decl2 = TlaOperDecl("Y", List.empty, n_y) val ar0Decl3 = TlaOperDecl("Z", List.empty, n_z) - val arGe0Decl1 = TlaOperDecl("A", List(SimpleFormalParam("t")), n_a) - val arGe0Decl2 = TlaOperDecl("B", List(SimpleFormalParam("t")), n_b) - val arGe0Decl3 = TlaOperDecl("C", List(SimpleFormalParam("t")), n_c) + val arGe0Decl1 = TlaOperDecl("A", List(OperParam("t")), n_a) + val arGe0Decl2 = TlaOperDecl("B", List(OperParam("t")), n_b) + val arGe0Decl3 = TlaOperDecl("C", List(OperParam("t")), n_c) val pa1 = List(ar0Decl1) -> diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestBuilder.scala index ba9340ab50..f2080ee55e 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestBuilder.scala @@ -39,19 +39,19 @@ class TestBuilder extends FunSuite with TestingPredefs { val decl4 = bd.declOp("A", bd.appOp(n_B, n_x), "x", ("B", 1)).untypedOperDecl() assert(decl1 == TlaOperDecl("A", List(), n_c)) - assert(decl2 == TlaOperDecl("A", List(SimpleFormalParam("x")), n_x)) + assert(decl2 == TlaOperDecl("A", List(OperParam("x")), n_x)) assert( decl3 == TlaOperDecl( "A", - List(OperFormalParam("B", 0)), + List(OperParam("B", 0)), OperEx(TlaOper.apply, n_B) )) assert( decl4 == TlaOperDecl( "A", - List(SimpleFormalParam("x"), OperFormalParam("B", 1)), + List(OperParam("x"), OperParam("B", 1)), OperEx(TlaOper.apply, n_B, n_x) )) diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestLetInExpander.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestLetInExpander.scala index 9f7c05eb13..1fcbbb64ea 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestLetInExpander.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestLetInExpander.scala @@ -20,7 +20,7 @@ class TestLetInExpander extends FunSuite with TestingPredefs { val ex1: TlaEx = n_x val ex2: TlaEx = letIn(appOp(n_A), declOp("A", n_x).untypedOperDecl()) - val ex3: TlaEx = letIn(appOp(n_A, n_x), declOp("A", n_y, SimpleFormalParam("y")).untypedOperDecl()) + val ex3: TlaEx = letIn(appOp(n_A, n_x), declOp("A", n_y, OperParam("y")).untypedOperDecl()) val ex4: TlaEx = letIn( ite( @@ -57,7 +57,7 @@ class TestLetInExpander extends FunSuite with TestingPredefs { val ex1: TlaEx = n_x val ex2: TlaEx = letIn(appOp(n_A), declOp("A", n_x).untypedOperDecl()) - val ex3: TlaEx = letIn(appOp(n_A, n_x), declOp("A", n_y, SimpleFormalParam("y")).untypedOperDecl()) + val ex3: TlaEx = letIn(appOp(n_A, n_x), declOp("A", n_y, OperParam("y")).untypedOperDecl()) val ex4: TlaEx = letIn( ite( @@ -97,7 +97,7 @@ class TestLetInExpander extends FunSuite with TestingPredefs { // this is how we represent LAMBDA in IR val lambdaAsLetIn = tla.letIn(tla.name("LAMBDA"), - tla.declOp("LAMBDA", tla.eql(tla.name("x"), tla.name("e")), SimpleFormalParam("x")).untypedOperDecl()) + tla.declOp("LAMBDA", tla.eql(tla.name("x"), tla.name("e")), OperParam("x")).untypedOperDecl()) val input = OperEx(TlaSeqOper.selectseq, tla.name("s"), lambdaAsLetIn) val output = transformation(input) // there is nothing to expand here, as SelectSeq is the standard operator @@ -109,7 +109,7 @@ class TestLetInExpander extends FunSuite with TestingPredefs { // this is how we represent LAMBDA in IR val lambdaAsLetIn = tla.letIn(tla.name("LAMBDA"), - tla.declOp("LAMBDA", tla.eql(tla.name("x"), tla.name("e")), SimpleFormalParam("x")).untypedOperDecl()) + tla.declOp("LAMBDA", tla.eql(tla.name("x"), tla.name("e")), OperParam("x")).untypedOperDecl()) // in this case, we cannot do anything, as the lambda operator is passed into the built-in operator val input = OperEx(TlaSeqOper.selectseq, tla.name("s"), lambdaAsLetIn) val output = transformation(input) @@ -122,7 +122,7 @@ class TestLetInExpander extends FunSuite with TestingPredefs { // this is how we represent LAMBDA in IR val lambdaAsLetIn = tla.letIn(tla.name("LAMBDA"), - tla.declOp("LAMBDA", tla.eql(tla.name("x"), tla.name("e")), SimpleFormalParam("x")).untypedOperDecl()) + tla.declOp("LAMBDA", tla.eql(tla.name("x"), tla.name("e")), OperParam("x")).untypedOperDecl()) val input = OperEx(TlaOper.apply, lambdaAsLetIn, ValEx(TlaInt(3))) val output = transformation(input) // application of the lambda expression should be replaced with the body diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala index 231282dc46..237969f315 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala @@ -78,7 +78,7 @@ class TestModule extends FunSuite { * /\ UNCHANGED << ackQ, sAck, rBit, rcvd >> */ val SndNewValue = - new TlaOperDecl("SndNewValue", List(SimpleFormalParam("d")), + new TlaOperDecl("SndNewValue", List(OperParam("d")), OperEx( TlaBoolOper.and, OperEx(TlaOper.eq, NameEx("sAck"), NameEx("sBit")), @@ -163,7 +163,7 @@ class TestModule extends FunSuite { * /\ UNCHANGED << sBit, sAck, rBit, sent, rcvd >> */ val Lose = - new TlaOperDecl("Lose", List(SimpleFormalParam("q")), + new TlaOperDecl("Lose", List(OperParam("q")), OperEx(TlaBoolOper.exists, NameEx("i"), OperEx(TlaArithOper.dotdot, ValEx(TlaInt(1)), OperEx(TlaSeqOper.len, NameEx("q"))), OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("q")), diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestPrinter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestPrinter.scala index c91bc90e19..027c4a1090 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestPrinter.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestPrinter.scala @@ -197,7 +197,7 @@ class TestPrinter extends FunSuite with TestingPredefs { // regression test("Test UTF8: OperFormalParam") { - val d = TlaOperDecl("Foo", List(OperFormalParam("Bar", 1)), ValEx(TlaInt(1))) + val d = TlaOperDecl("Foo", List(OperParam("Bar", 1)), ValEx(TlaInt(1))) assert("Foo(Bar(_)) ≜ 1" == UTFPrinter(d)) } } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala index 1838994bf5..658f37e10c 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala @@ -147,7 +147,7 @@ class TestTlaExpr extends FunSuite { test("declaring an order 1 operator") { // A(x, y) == x' /\ y - val odef = TlaOperDecl("A", List(SimpleFormalParam("x"), SimpleFormalParam("y")), + val odef = TlaOperDecl("A", List(OperParam("x"), OperParam("y")), OperEx(TlaBoolOper.and, OperEx(TlaActionOper.prime, NameEx("x")), NameEx("y"))) // this is the way to use a user-defined operator @@ -164,10 +164,10 @@ class TestTlaExpr extends FunSuite { test("declaring an order 2 operator") { // f(_, _) - val fOper = OperFormalParam("f", 2) + val fOper = OperParam("f", 2) // A(f(_, _), x, y) == f(x, y) - val odef = TlaOperDecl("A", List(fOper, SimpleFormalParam("x"), SimpleFormalParam("y")), + val odef = TlaOperDecl("A", List(fOper, OperParam("x"), OperParam("y")), OperEx(TlaOper.apply, NameEx("f"), NameEx("x"), NameEx("y"))) // this is the way to use a user-defined operator 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 index 8793755aa4..8972158745 100644 --- 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 @@ -421,7 +421,7 @@ abstract class TestJson extends FunSuite { test("LET A(x, y) == x + y IN A(1,2)") { // _vars - val decl = TlaOperDecl("A", List(SimpleFormalParam("x"), SimpleFormalParam("y")), plus(name("x"), name("y"))) + val decl = TlaOperDecl("A", List(OperParam("x"), OperParam("y")), plus(name("x"), name("y"))) compare( letIn(appDecl(decl, int(1), int(2)), decl), """{"let":[{"operator":"A","body":{"plus":"x","arg":"y"},"params":[{"name":"x","arity":0},{"name":"y","arity":0}]}],"body":{"applyOp":"A","args":[1,2]}}""" @@ -430,8 +430,8 @@ abstract class TestJson extends FunSuite { test("LET A(x, y) == x + 1 IN B(x, y) == x - y IN A(1, 2) * B(3, 4)") { // _vars - val decl1 = TlaOperDecl("A", List(SimpleFormalParam("x"), SimpleFormalParam("y")), plus(name("x"), name("y"))) - val decl2 = TlaOperDecl("B", List(SimpleFormalParam("x"), SimpleFormalParam("y")), minus(name("x"), name("y"))) + val decl1 = TlaOperDecl("A", List(OperParam("x"), OperParam("y")), plus(name("x"), name("y"))) + val decl2 = TlaOperDecl("B", List(OperParam("x"), OperParam("y")), minus(name("x"), name("y"))) compareMultiLine( letIn(mult(appDecl(decl1, int(1), int(2)), appDecl(decl2, int(3), int(4))), decl1, decl2), """{ @@ -515,7 +515,7 @@ abstract class TestJson extends FunSuite { compareModuleMultiLine( new TlaModule("simpleOperator", List( - TlaOperDecl("A", List(SimpleFormalParam("age")), gt(name("age"), int(42))) + TlaOperDecl("A", List(OperParam("age")), gt(name("age"), int(42))) )), """{ | "module": "simpleOperator", @@ -540,16 +540,15 @@ abstract class TestJson extends FunSuite { test("module level2Operators") { // awesome - val aDecl = TlaOperDecl("A", List(SimpleFormalParam("i"), SimpleFormalParam("j"), OperFormalParam("f", 1)), + val aDecl = TlaOperDecl("A", List(OperParam("i"), OperParam("j"), OperParam("f", 1)), OperEx(TlaOper.apply, NameEx("f"), OperEx(TlaSetOper.cup, NameEx("i"), NameEx("j")))) - val bDecl = TlaOperDecl("B", List(SimpleFormalParam("y")), NameEx("y")) + val bDecl = TlaOperDecl("B", List(OperParam("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)))) + TlaOperDecl("C", List(OperParam("z")), appDecl(aDecl, int(0), NameEx("z"), appDecl(bDecl, int(1)))) )), """{ | "module": "level2Operators", diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala index bdc15226e5..e875e3c5f9 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala @@ -720,8 +720,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { test("a multi-line LET-IN") { val writer = new PrettyWriter(printWriter, 40) val decl = - TlaOperDecl("AVeryLongName", List(SimpleFormalParam("param1"), SimpleFormalParam("param2")), - plus(name("param1"), name("param2"))) + TlaOperDecl("AVeryLongName", List(OperParam("param1"), OperParam("param2")), plus(name("param1"), name("param2"))) val expr = letIn(appDecl(decl, int(1), int(2)), decl) writer.write(expr) printWriter.flush() @@ -736,11 +735,9 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { test("multiple definitions in LET-IN") { val writer = new PrettyWriter(printWriter, 40) val decl1 = - TlaOperDecl("AVeryLongName", List(SimpleFormalParam("param1"), SimpleFormalParam("param2")), - plus(name("param1"), name("param2"))) + TlaOperDecl("AVeryLongName", List(OperParam("param1"), OperParam("param2")), plus(name("param1"), name("param2"))) val decl2 = - TlaOperDecl("BVeryLongName", List(SimpleFormalParam("param1"), SimpleFormalParam("param2")), - plus(name("param1"), name("param2"))) + TlaOperDecl("BVeryLongName", List(OperParam("param1"), OperParam("param2")), plus(name("param1"), name("param2"))) val expr = letIn(mult(appDecl(decl1, int(1), int(2)), appDecl(decl2, int(3), int(4))), decl1, decl2) writer.write(expr) printWriter.flush() @@ -758,7 +755,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { test("a LAMBDA as LET-IN") { val writer = new PrettyWriter(printWriter, 40) - val aDecl = TlaOperDecl("LAMBDA", List(SimpleFormalParam("x")), NameEx("x")) + val aDecl = TlaOperDecl("LAMBDA", List(OperParam("x")), NameEx("x")) val expr = letIn(NameEx("LAMBDA"), aDecl) writer.write(expr) printWriter.flush() @@ -772,12 +769,12 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { val writer = new PrettyWriter(printWriter, 40) // A(LAMBDA y: y + 1, x) val innerDecl = - TlaOperDecl("LAMBDA", List(SimpleFormalParam("y")), tla.name("y")) + TlaOperDecl("LAMBDA", List(OperParam("y")), tla.name("y")) val innerLambda = tla.letIn(tla.name("LAMBDA"), innerDecl) val innerA = tla.appOp(tla.name("A"), innerLambda, tla.name("x")) // A(LAMBDA x: A(LAMBDA y: y + 1, x), z) val outerDecl = - TlaOperDecl("LAMBDA", List(SimpleFormalParam("x")), innerA) + TlaOperDecl("LAMBDA", List(OperParam("x")), innerA) val outerLambda = letIn(NameEx("LAMBDA"), outerDecl) val outerA = tla.appOp(tla.name("A"), outerLambda, tla.name("z")) writer.write(outerA) @@ -794,7 +791,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { val fDecl = TlaOperDecl( "A", - List(SimpleFormalParam("x")), + List(OperParam("x")), body ) /// writer.write(fDecl) @@ -813,7 +810,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { val fDecl = TlaOperDecl( "A", - List(SimpleFormalParam("x")), + List(OperParam("x")), body ) /// fDecl.isRecursive = true @@ -835,7 +832,7 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach { val fDecl = TlaOperDecl( "A", - List(SimpleFormalParam("x")), + List(OperParam("x")), body ) /// fDecl.isRecursive = true diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala index aadb3f7b6c..b263d1273b 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala @@ -1,6 +1,6 @@ package at.forsyte.apalache.tla.lir.transformations.standard -import at.forsyte.apalache.tla.lir.{SimpleFormalParam, TlaModule} +import at.forsyte.apalache.tla.lir.{OperParam, TlaModule} import at.forsyte.apalache.tla.lir.convenience._ import at.forsyte.apalache.tla.lir.UntypedPredefs._ import org.junit.runner.RunWith @@ -23,8 +23,8 @@ class TestFlatLanguagePred extends LanguagePredTestSuite { test("a non-nullary let-in ") { val app = tla.appOp(tla.name("UserOp"), tla.int(3)) - val letIn = tla.letIn(app, - tla.declOp("UserOp", tla.plus(tla.int(1), tla.name("x")), SimpleFormalParam("x")).untypedOperDecl()) + val letIn = + tla.letIn(app, tla.declOp("UserOp", tla.plus(tla.int(1), tla.name("x")), OperParam("x")).untypedOperDecl()) expectFail(pred.isExprOk(app)) } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestKeraLanguagePred.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestKeraLanguagePred.scala index 5ab53a1503..484e369e4e 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestKeraLanguagePred.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestKeraLanguagePred.scala @@ -134,7 +134,7 @@ class TestKeraLanguagePred extends LanguagePredTestSuite { test("a non-nullary let-in ") { val app = appOp(name("UserOp"), int(3)) - val letInDef = letIn(app, declOp("UserOp", plus(int(1), name("x")), SimpleFormalParam("x")).untypedOperDecl()) + val letInDef = letIn(app, declOp("UserOp", plus(int(1), name("x")), OperParam("x")).untypedOperDecl()) expectFail(pred.isExprOk(letInDef)) } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestReplaceFixed.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestReplaceFixed.scala index a65e2af416..8a9cd22400 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestReplaceFixed.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestReplaceFixed.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.lir.convenience.tla import at.forsyte.apalache.tla.lir.oper.TlaArithOper import at.forsyte.apalache.tla.lir.transformations.TlaExTransformation import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker -import at.forsyte.apalache.tla.lir.{FormalParam, NameEx, OperEx, TestingPredefs, TlaEx, TlaOperDecl} +import at.forsyte.apalache.tla.lir.{OperParam, NameEx, OperEx, TestingPredefs, TlaEx, TlaOperDecl} import at.forsyte.apalache.tla.lir.UntypedPredefs._ import org.junit.runner.RunWith import org.scalatest.FunSuite @@ -42,10 +42,10 @@ class TestReplaceFixed extends FunSuite with TestingPredefs { } test("Replace in Let-in") { - val decl = TlaOperDecl("A", List.empty[FormalParam], n_x) + val decl = TlaOperDecl("A", List.empty[OperParam], n_x) val ex = tla.letIn(tla.appDecl(decl), decl) val tr = mkTr(n_x, n_y) - val expectedDecl = TlaOperDecl("A", List.empty[FormalParam], n_y) + val expectedDecl = TlaOperDecl("A", List.empty[OperParam], n_y) val expectedEx = tla.letIn(tla.appDecl(expectedDecl), expectedDecl) assert(tr(ex) == expectedEx.untyped()) }