Refactor FormalParam (#724)

* closes #656: refactor FormalParam

* fix formatting

* fix the comments

* fix formatting

* fix formatting

UNRELEASED.md

@@ -10,7 +10,7 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
-### Features
+### Changed
 
-* IR: made consistent the names of IR operators (may break JSON compatibility),
-  see #634
+* IR: simplified `SimpleFormalParam` and `OperFormalParam` into `OperParam`, see #656
+* IR: made consistent the names of IR operators (may break JSON compatibility), see #634

tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala

@@ -155,18 +155,12 @@ class TlaToJson[T <: JsonRepresentation](factory: JsonFactory[T])(implicit typTa
 
     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
-          )
+      val paramsJsons = formalParams map { case OperParam(paramName, arity) =>
+        factory.mkObj(
+            kindFieldName -> "OperParam",
+            "name" -> paramName,
+            "arity" -> arity
+        )
       }
       factory.mkObj(
           typeFieldName -> typTagPrinter(decl.typeTag),

tla-import/src/main/scala/at/forsyte/apalache/tla/imp/FormalParamTranslator.scala

@@ -1,7 +1,6 @@
 package at.forsyte.apalache.tla.imp
 
-import at.forsyte.apalache.tla.lir.oper.FixedArity
-import at.forsyte.apalache.tla.lir.{FormalParam, OperFormalParam, SimpleFormalParam}
+import at.forsyte.apalache.tla.lir.OperParam
 import tla2sany.semantic.FormalParamNode
 
 /**
@@ -10,12 +9,8 @@ import tla2sany.semantic.FormalParamNode
  * @author konnov
  */
 class FormalParamTranslator {
-  def translate(param: FormalParamNode): FormalParam = {
-    if (param.getArity == 0) {
-      SimpleFormalParam(param.getName.toString.intern())
-    } else {
-      OperFormalParam(param.getName.toString.intern(), param.getArity)
-    }
+  def translate(param: FormalParamNode): OperParam = {
+    OperParam(param.getName.toString.intern(), param.getArity)
   }
 }
 

tla-import/src/main/scala/at/forsyte/apalache/tla/imp/OpApplTranslator.scala

@@ -229,8 +229,7 @@ class OpApplTranslator(
   private def translateFormalParam(node: OpApplNode): TlaEx = {
     val oper = node.getOperator.asInstanceOf[FormalParamNode]
     // FIXME: should we extract the parameter from the context???
-    val formalParam =
-      FormalParamTranslator().translate(oper).asInstanceOf[OperFormalParam]
+    val formalParam = FormalParamTranslator().translate(oper)
     val exTran = ExprOrOpArgNodeTranslator(
         sourceStore,
         annotationStore,

tla-import/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithAnnotations.scala

@@ -55,7 +55,7 @@ class TestPrettyWriterWithAnnotations extends FunSuite with BeforeAndAfterEach {
   }
 
   test("operator declaration") {
-    val decl = TlaOperDecl("MyOper", List(SimpleFormalParam("x"), SimpleFormalParam("y")), tla.bool(true))
+    val decl = TlaOperDecl("MyOper", List(OperParam("x"), OperParam("y")), tla.bool(true))
     val store = createAnnotationStore()
     store += decl.ID -> List(Annotation("type", AnnotationStr("(Int, Str) -> Bool")))
 

tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala

@@ -121,16 +121,18 @@ class TestTlaToUJson extends FunSuite with BeforeAndAfterEach with TestingPredef
     assert(!jsonNullary("isRecursive").bool)
 
     assert(jsonUnary("formalParams").arr.size == 1)
-    assert(jsonUnary("formalParams")(0)(kindField).str == "SimpleFormalParam")
+    assert(jsonUnary("formalParams")(0)(kindField).str == "OperParam")
     assert(jsonUnary("formalParams")(0)("name").str == "p")
+    assert(jsonUnary("formalParams")(0)("arity").num == 0)
     assert(!jsonUnary("isRecursive").bool)
 
     assert(jsonHO("formalParams").arr.size == 2)
-    assert(jsonHO("formalParams")(0)(kindField).str == "OperFormalParam")
+    assert(jsonHO("formalParams")(0)(kindField).str == "OperParam")
     assert(jsonHO("formalParams")(0)("name").str == "A")
     assert(jsonHO("formalParams")(0)("arity").num == 1)
-    assert(jsonHO("formalParams")(1)(kindField).str == "SimpleFormalParam")
+    assert(jsonHO("formalParams")(1)(kindField).str == "OperParam")
     assert(jsonHO("formalParams")(1)("name").str == "b")
+    assert(jsonHO("formalParams")(1)("arity").num == 0)
     assert(!jsonHO("isRecursive").bool)
 
     assert(jsonRec("isRecursive").bool)

tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala

@@ -69,7 +69,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
   }
 
   def expectOperDecl(
-      name: String, params: List[FormalParam], body: TlaEx
+      name: String, params: List[OperParam], body: TlaEx
   ): (TlaDecl => Unit) = {
     case d: TlaOperDecl =>
       assert(name == d.name)
@@ -91,7 +91,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
   }
 
   def findAndExpectOperDecl(
-      mod: TlaModule, name: String, params: List[FormalParam], body: TlaEx
+      mod: TlaModule, name: String, params: List[OperParam], body: TlaEx
   ): Unit = {
     mod.declarations.find {
       _.name == name
@@ -1029,7 +1029,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
     val mod = expectSingleModule("except", rootName, modules)
     expectSourceInfoInDefs(mod)
 
-    def expectDecl(name: String, params: List[FormalParam], body: TlaEx) =
+    def expectDecl(name: String, params: List[OperParam], body: TlaEx) =
       expectOperDecl(name, params, body)
 
     expectDecl(
@@ -1121,7 +1121,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
     val mod = expectSingleModule("labels", rootName, modules)
     expectSourceInfoInDefs(mod)
 
-    def expectDecl(n: String, p: List[FormalParam], b: TlaEx) =
+    def expectDecl(n: String, p: List[OperParam], b: TlaEx) =
       expectOperDecl(n, p, b)
 
     //    A == {FALSE} \cup (l1 :: {TRUE})
@@ -1171,7 +1171,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
     val mod = expectSingleModule("args", rootName, modules)
     expectSourceInfoInDefs(mod)
 
-    def expectDecl(n: String, p: List[FormalParam], b: TlaEx) =
+    def expectDecl(n: String, p: List[OperParam], b: TlaEx) =
       expectOperDecl(n, p, b)
 
     val expectedABody = OperEx(TlaFunOper.app, NameEx("f"), ValEx(TlaInt(2)))
@@ -1427,17 +1427,17 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
       .loadFromSource("level1Operators", Source.fromString(text))
     val mod = expectSingleModule("level1Operators", rootName, modules)
 
-    def expectDecl(n: String, p: List[FormalParam], b: TlaEx) =
+    def expectDecl(n: String, p: List[OperParam], b: TlaEx) =
       expectOperDecl(n, p, b)
 
     expectDecl(
         "A",
-        List(SimpleFormalParam("i"), SimpleFormalParam("j")),
+        List(OperParam("i"), OperParam("j")),
         OperEx(TlaSetOper.cup, NameEx("i"), NameEx("j"))
     )(mod.declarations(2))
     expectDecl(
         "**",
-        List(SimpleFormalParam("i"), SimpleFormalParam("j")),
+        List(OperParam("i"), OperParam("j")),
         OperEx(TlaSetOper.cap, NameEx("i"), NameEx("j"))
     )(mod.declarations(3))
     val aDecl = mod.declarations(2).asInstanceOf[TlaOperDecl]
@@ -1473,15 +1473,15 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
     val mod = expectSingleModule("level2Operators", rootName, modules)
     expectSourceInfoInDefs(mod)
 
-    def expectDecl(n: String, p: List[FormalParam], b: TlaEx) =
+    def expectDecl(n: String, p: List[OperParam], b: TlaEx) =
       expectOperDecl(n, p, b)
 
     expectDecl(
         "A",
         List(
-            SimpleFormalParam("i"),
-            SimpleFormalParam("j"),
-            OperFormalParam("f", 1)
+            OperParam("i"),
+            OperParam("j"),
+            OperParam("f", 1)
         ),
         OperEx(
             TlaOper.apply,
@@ -1525,15 +1525,15 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
         assert("X" == xDecl.name)
         val yDecl = defs(1)
         assert(
-            TlaOperDecl("Y", List(SimpleFormalParam("a")), NameEx("a")) == yDecl
+            TlaOperDecl("Y", List(OperParam("a")), NameEx("a")) == yDecl
         )
         assert(sourceStore.contains(yDecl.body.ID)) // and source file information has been saved
 
         val zDecl = defs(2)
         zDecl match {
           case TlaOperDecl(
                   "Z",
-                  List(OperFormalParam("f", 1), SimpleFormalParam("a")),
+                  List(OperParam("f", 1), OperParam("a", 0)),
                   _
               ) =>
             assert(
@@ -1578,7 +1578,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
                   NameEx("LAMBDA"),
                   TlaOperDecl(
                       "LAMBDA",
-                      List(SimpleFormalParam("x")),
+                      List(OperParam("x", 0)),
                       OperEx(TlaOper.eq, NameEx("x"), ValEx(TlaInt(_)))
                   )
               ) =>
@@ -1676,7 +1676,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
           // The caveat here is that the formal parameter R does not appear in the list of the R's formal parameters,
           // but it is accessible via the field recParam.
           assert(d.isRecursive)
-          val recParam = OperFormalParam(name, nparams)
+          val recParam = OperParam(name, nparams)
           assert(d.body == expectedBody)
           assert(sourceStore.contains(d.body.ID)) // and source file information has been saved
 
@@ -1721,7 +1721,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
         // The caveat here is that the formal parameter F does not appear in the list of the F's formal parameters,
         // but it is accessible via the field recParam.
         assert(d.isRecursive)
-        val recParam = OperFormalParam("F", 1)
+        val recParam = OperParam("F", 1)
         val ite = OperEx(
             TlaControlOper.ifThenElse,
             OperEx(TlaOper.eq, NameEx("n"), ValEx(TlaInt(0))),
@@ -1853,8 +1853,8 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
               )
           ) =>
         assert(params.length == 1)
-        assert(params.head.isInstanceOf[SimpleFormalParam])
-        assert("x" == params.head.asInstanceOf[SimpleFormalParam].name)
+        assert(params.head.isInstanceOf[OperParam])
+        assert("x" == params.head.asInstanceOf[OperParam].name)
 
       case e =>
         fail("expected the body for J!F, found: " + e)
@@ -1875,9 +1875,9 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
       case Some(TlaOperDecl(_, params,
           OperEx(TlaArithOper.plus, NameEx("x"), NameEx("K")))) =>
         assert(params.length == 3)
-        assert(params.head == SimpleFormalParam("V"))
-        assert(params(1) == SimpleFormalParam("K"))
-        assert(params(2) == SimpleFormalParam("x"))
+        assert(params.head == FormalParam("V"))
+        assert(params(1) == FormalParam("K"))
+        assert(params(2) == FormalParam("x"))
 
       case _ =>
         fail("expected the body for I!F")
@@ -1887,7 +1887,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
     root.declarations.find { _.name == "B2!C2!H" } match {
       case Some(TlaOperDecl(_, params, NameEx("x"))) =>
         assert(params.length == 1)
-        assert(params.head == SimpleFormalParam("x"))
+        assert(params.head == OperParam("x"))
 
       case _ =>
         fail("expected the body for B2!C2!H")

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ParameterNormalizer.scala

@@ -72,12 +72,12 @@ class ParameterNormalizer(
   }
 
   /** Iteratively introduces a new operator for each formal parameter */
-  private def normalizeParametersInEx(paramNames: Seq[FormalParam], paramTypes: Seq[TlaType1]): TlaExTransformation =
+  private def normalizeParametersInEx(paramNames: Seq[OperParam], paramTypes: Seq[TlaType1]): TlaExTransformation =
     tracker.trackEx { ex =>
       paramNames.zip(paramTypes).foldLeft(ex) { case (partialEx, (fParam, fParamType)) =>
         val paramOperName = nameGenerator.newName()
         (fParam, fParamType) match {
-          case (SimpleFormalParam(name), paramType) =>
+          case (OperParam(name, 0), paramType) =>
             // case 1: a normal parameter, not a higher-order one.
             // We replace all instances of `fParam` with `paramOperName()`
             // however, since paramOperName is an operator, we have to replace with application
@@ -96,7 +96,7 @@ class ParameterNormalizer(
               .letIn(replaced, letInDef)
               .typed(types, "p")
 
-          case (OperFormalParam(name, arity), paramType) =>
+          case (OperParam(name, arity), paramType) =>
             // case 2: a higher-order parameter.
             // We again replace all instances of `fParam` with `paramOperName`
             // As both are operators, we don't need to introduce application
@@ -123,7 +123,7 @@ class ParameterNormalizer(
                     )
                     .typed(resType)
                 val letInDef = tla
-                  .declOp(paramOperName, newBody, freshParams map SimpleFormalParam: _*)
+                  .declOp(paramOperName, newBody, freshParams.map(n => OperParam(n)): _*)
                   .typedOperDecl(paramType)
                 tla.letIn(replaced, letInDef).typed(resType)
 

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestConstAndDefRewriter.scala

@@ -3,10 +3,10 @@ package at.forsyte.apalache.tla.pp
 import at.forsyte.apalache.io.annotations.store._
 import at.forsyte.apalache.tla.imp.SanyImporter
 import at.forsyte.apalache.tla.imp.src.SourceStore
+import at.forsyte.apalache.tla.lir.UntypedPredefs._
 import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
-import at.forsyte.apalache.tla.lir.{IntT1, OperT1, SimpleFormalParam, TlaModule, TlaOperDecl, Typed}
-import at.forsyte.apalache.tla.lir.UntypedPredefs._
+import at.forsyte.apalache.tla.lir._
 import org.junit.runner.RunWith
 import org.scalatest.junit.JUnitRunner
 import org.scalatest.{BeforeAndAfterEach, FunSuite}
@@ -105,7 +105,7 @@ class TestConstAndDefRewriter extends FunSuite with BeforeAndAfterEach {
     assert(rewritten.constDeclarations.isEmpty)
     assert(rewritten.operDeclarations.size == 1)
     val expected =
-      TlaOperDecl("BoolMin", List(SimpleFormalParam("S")), tla.choose(tla.name("x"), tla.name("S"), tla.bool(true)))
+      TlaOperDecl("BoolMin", List(OperParam("S")), tla.choose(tla.name("x"), tla.name("S"), tla.bool(true)))
     assert(expected == rewritten.operDeclarations.head)
   }
 

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestDesugarer.scala

@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.lir.TypedPredefs._
 import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.{
-  BoolT1, FunT1, IntT1, OperT1, RecT1, SeqT1, SetT1, SimpleFormalParam, StrT1, TlaEx, TlaType1, TupT1
+  BoolT1, FunT1, IntT1, OperT1, RecT1, SeqT1, SetT1, OperParam, StrT1, TlaEx, TlaType1, TupT1
 }
 import org.junit.runner.RunWith
 import org.scalatest.junit.JUnitRunner
@@ -711,7 +711,7 @@ class TestDesugarer extends FunSuite with BeforeAndAfterEach {
     val types = Map("i" -> IntT1(), "F" -> OperT1(Seq(), IntT1()))
     // Foo(1)
     val fooDef = tla
-      .declOp("Foo", tla.name("x") ? "i", SimpleFormalParam("x"))
+      .declOp("Foo", tla.name("x") ? "i", OperParam("x"))
       .typedOperDecl(types, "F")
     val input = tla
       .letIn(tla.appOp(tla.name("Foo") ? "F", tla.int(1) ? "i") ? "i", fooDef)

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestInlinerofUserOper.scala

@@ -1,11 +1,11 @@
 package at.forsyte.apalache.tla.pp
 
+import at.forsyte.apalache.tla.lir.TypedPredefs._
 import at.forsyte.apalache.tla.lir.convenience.tla
 import at.forsyte.apalache.tla.lir.storage.BodyMapFactory
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.transformations.standard.InlinerOfUserOper
-import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, OperT1, SimpleFormalParam, TestingPredefs}
-import at.forsyte.apalache.tla.lir.TypedPredefs._
+import at.forsyte.apalache.tla.lir.{BoolT1, OperParam, IntT1, OperT1, TestingPredefs}
 import org.junit.runner.RunWith
 import org.scalatest.FunSuite
 import org.scalatest.junit.JUnitRunner
@@ -23,7 +23,7 @@ class TestInlinerofUserOper extends FunSuite with TestingPredefs {
     // C(x) == x + 1
     // B == k
     // A == B()
-    val cDecl = declOp("C", cBody, SimpleFormalParam("x"))
+    val cDecl = declOp("C", cBody, OperParam("x"))
       .typedOperDecl(types, "C")
     val aDecl = declOp("A", appOp(tla.name("B") ? "U") ? "i")
       .typedOperDecl(types, "U")

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestParameterNormalizer.scala

@@ -45,7 +45,7 @@ class TestParameterNormalizer extends FunSuite with BeforeAndAfterEach with Test
     val output = parNorm.normalizeDeclaration(input)
 
     output match {
-      case d @ TlaOperDecl(name, List(SimpleFormalParam(p)), body) =>
+      case d @ TlaOperDecl(name, List(OperParam(p, 0)), body) =>
         assert(input.typeTag == d.typeTag)
 
         body match {
@@ -88,12 +88,12 @@ class TestParameterNormalizer extends FunSuite with BeforeAndAfterEach with Test
     //  LET NewName(p) == T(p) IN
     //    NewName(0)
     output match {
-      case d @ TlaOperDecl(name, List(OperFormalParam(opName, 1)), body) =>
+      case d @ TlaOperDecl(_, List(OperParam(opName, 1)), body) =>
         assert(input.typeTag == d.typeTag)
 
         body match {
-          case letin @ LetInEx(letInBody, TlaOperDecl(newName, List(SimpleFormalParam(intermediateParam)),
-                      appex @ OperEx(TlaOper.apply, nex @ NameEx(appliedOperName), NameEx(arg)))) =>
+          case letin @ LetInEx(letInBody, TlaOperDecl(newName, List(OperParam(intermediateParam, 0)), appex @ OperEx(
+                          TlaOper.apply, nex @ NameEx(appliedOperName), NameEx(arg)))) =>
             assert(opName == appliedOperName)
             assert(arg == intermediateParam)
             assert(Typed(IntT1()) == letin.typeTag)

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestUnroller.scala

@@ -214,7 +214,7 @@ class TestUnroller extends FunSuite with BeforeAndAfterEach with TestingPredefs
           case LetInEx(letBody, TlaOperDecl(declName, params, unrolled)) =>
             assert(appEx == letBody)
             assert(letInOpName == declName)
-            assert(List(SimpleFormalParam("p")) == params)
+            assert(List(OperParam("p")) == params)
             assert(aUnrolledBody == unrolled)
 
           case _ =>