Cleaning up the operator names (#726)

* closes #634: cleaning up the operator names * using qualified names in the test * add changelog entry * Update tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala Co-authored-by: Shon Feder <[email protected]> * Update tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaTempOper.scala Co-authored-by: Shon Feder <[email protected]> * fix formatting Co-authored-by: Shon Feder <[email protected]>
apalache-mc · Apr 13, 2021 · 9587968 · 9587968
1 parent 5ea3738
commit 9587968
Show file tree

Hide file tree

Showing 16 changed files with 252 additions and 179 deletions.
diff --git a/UNRELEASED.md b/UNRELEASED.md
@@ -10,3 +10,7 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Features
+
+* IR: made consistent the names of IR operators (may break JSON compatibility),
+  see #634
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetExpandRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetExpandRule.scala
@@ -14,7 +14,7 @@ import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaSetOper}
 class SetExpandRule(rewriter: SymbStateRewriter) extends RewritingRule {
   override def isApplicable(symbState: SymbState): Boolean = {
     symbState.ex match {
-      case OperEx(ApalacheOper.expand, OperEx(TlaSetOper.SUBSET, _))    => true
+      case OperEx(ApalacheOper.expand, OperEx(TlaSetOper.powerset, _))  => true
       case OperEx(ApalacheOper.expand, OperEx(TlaSetOper.funSet, _, _)) => true
       case _                                                            => false
     }
@@ -25,7 +25,7 @@ class SetExpandRule(rewriter: SymbStateRewriter) extends RewritingRule {
       case ex @ OperEx(ApalacheOper.expand, OperEx(TlaSetOper.funSet, _, _)) =>
         throw new RewriterException("Trying to expand a set of functions. This will blow up the solver.", ex)
 
-      case ex @ OperEx(ApalacheOper.expand, OperEx(TlaSetOper.SUBSET, basesetEx)) =>
+      case ex @ OperEx(ApalacheOper.expand, OperEx(TlaSetOper.powerset, basesetEx)) =>
         var nextState = rewriter.rewriteUntilDone(state.setRex(basesetEx))
         new PowSetCtor(rewriter).confringo(nextState, nextState.asCell)
 

diff --git a/tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala b/tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala
@@ -612,7 +612,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
         "Implies",
         OperEx(TlaBoolOper.implies, ValEx(TlaBool(false)), ValEx(TlaBool(true)))
     )
-    expectDecl("Subset", OperEx(TlaSetOper.SUBSET, NameEx("x")))
+    expectDecl("Subset", OperEx(TlaSetOper.powerset, NameEx("x")))
     expectDecl("Union", OperEx(TlaSetOper.union, NameEx("x")))
     expectDecl("Domain", OperEx(TlaFunOper.domain, NameEx("x")))
     expectDecl(

diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
@@ -337,7 +337,7 @@ class ToEtcExpr(annotationStore: AnnotationStore, aliasSubstitution: ConstSubsti
         val opsig = OperT1(List(SetT1(a), SetT1(a)), BoolT1())
         mkExRefApp(opsig, args)
 
-      case OperEx(TlaSetOper.SUBSET, args @ _*) =>
+      case OperEx(TlaSetOper.powerset, args @ _*) =>
         // SUBSET S
         val a = varPool.fresh
         val opsig = OperT1(List(SetT1(a)), SetT1(SetT1(a)))

diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaActionOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaActionOper.scala
@@ -13,29 +13,29 @@ object TlaActionOper {
    * The prime operator. By the TLA+ restrictions, we cannot apply it twice, e.g., (x')' is illegal.
    */
   object prime extends TlaActionOper {
-    override val name: String = "'"
+    override val name: String = "PRIME"
 
     override def arity: OperArity = FixedArity(1)
 
     override def precedence: (Int, Int) = (15, 15)
   }
 
   /**
-   * The operator that executes an action or keeps the variable values.
+   * The operator that executes an action or keeps the variable values. It has the form `[A]_e`.
    */
   object stutter extends TlaActionOper {
-    override val name: String = "[A]_e"
+    override val name: String = "STUTTER"
 
     override def arity: OperArity = FixedArity(2)
 
     override def precedence: (Int, Int) = (4, 15)
   }
 
   /**
-   * The operator that executes an action and enforces the values to change.
+   * The operator that executes an action and enforces the values to change. It has the form `<A>_e`.
    */
   object nostutter extends TlaActionOper {
-    override val name: String = "<A>_e"
+    override val name: String = "NO_STUTTER"
 
     override def arity: OperArity = FixedArity(2)
 
@@ -65,13 +65,10 @@ object TlaActionOper {
   }
 
   /**
-   * The sequential composition of operators.
-   *
-   * [email protected]: Arity 2?
-   * [email protected]: Arity 2. Fixed.
+   * The sequential composition of operators, which usually has the name `\cdot`.
    */
   object composition extends TlaActionOper {
-    override val name: String = "\\cdot"
+    override val name: String = "COMPOSE"
     override def arity: OperArity = FixedArity(2)
     override def precedence: (Int, Int) = (13, 13)
   }

diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaArithOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaArithOper.scala
@@ -27,123 +27,133 @@ abstract class TlaArithOper extends TlaOper {
 object TlaArithOper {
 
   /**
-   * A binary addition.
+   * A binary addition: `a + b`.
    */
   object plus extends TlaArithOper {
     override val arity = FixedArity(2)
-    override val name = "(+)"
+    override val name = "PLUS"
     override val precedence: (Int, Int) = (10, 10)
   }
 
   /**
-   * A unary minus. Note that Naturals do not have unary minus.
+   * A unary minus: `-a`. Note that Naturals do not have unary minus.
    */
   object uminus extends TlaArithOper {
     override val arity = FixedArity(1)
-    override val name = "-."
+    override val name = "UNARY_MINUS"
     override val precedence: (Int, Int) = (12, 12)
   }
 
   /**
-   * A binary minus.
+   * A binary minus: `a - b`.
    */
   object minus extends TlaArithOper {
     override val arity = FixedArity(2)
-    override val name = "(-)"
+    override val name = "MINUS"
     override val precedence: (Int, Int) = (11, 11)
   }
 
   /**
-   * A multiplication.
+   * A multiplication: `a * b`.
    */
   object mult extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(*)"
+
+    override val name: String = "MULT"
     override val precedence: (Int, Int) = (13, 13)
   }
 
   /**
-   * Integer division.
+   * Integer division: `a \div b`.
    */
   object div extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(\\div)"
+
+    override val name: String = "DIV"
     override val precedence: (Int, Int) = (13, 13)
   }
 
   /**
-   * Remainder of an integer division.
+   * Remainder of an integer division: `a % b`
    */
   object mod extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(%)"
+
+    override val name: String = "MOD"
     override val precedence: (Int, Int) = (10, 11)
   }
 
   /**
-   * Real division.
+   * Real division, defined in `Reals`: `a / b`
    */
   object realDiv extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(/)"
+
+    override val name: String = "REAL_DIV"
     override val precedence: (Int, Int) = (13, 13)
   }
 
   /**
-   * Exponent, i.e., x^y gives us x multiplied by itself (y-1) times.
+   * Exponent, i.e., `x^y` gives us `x` multiplied by itself `y - 1` times.
    */
   object exp extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(^)"
+
+    override val name: String = "POW"
     override val precedence: (Int, Int) = (14, 14)
   }
 
   /**
-   * An integer/natural range, that is, a..b = {a,...,b}
+   * An integer/natural range as a set: `a..b`. Both `a` and `b` are included. It can be understood as
+   * `{ i \in Int: a <= i /\ i <= b }`.
    */
   object dotdot extends TlaArithOper {
     override val arity = FixedArity(2)
-    override val name = "_.._"
+    override val name = "INT_RANGE"
     override val precedence: (Int, Int) = (9, 9)
   }
 
   /**
-   * Less than.
+   * Less than: `a < b`.
    */
   object lt extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(<)"
+
+    override val name: String = "LT"
     override val precedence: (Int, Int) = (5, 5)
   }
 
   /**
-   * Greater than.
+   * Greater than: `a > b`.
    */
   object gt extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(>)"
+
+    override val name: String = "GT"
     override val precedence: (Int, Int) = (5, 5)
   }
 
   /**
-   * Less than or equals.
+   * Less than or equals: `a <= b`.
    */
   object le extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(<=)"
+
+    override val name: String = "LE"
     override val precedence: (Int, Int) = (5, 5)
   }
 
   /**
-   * Greater than or equals.
+   * Greater than or equals: `a >= b`.
    */
   object ge extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(>=)"
+
+    override val name: String = "GE"
     override val precedence: (Int, Int) = (5, 5)
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaBoolOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaBoolOper.scala
@@ -18,7 +18,7 @@ object TlaBoolOper {
    */
   object and extends TlaBoolOper {
     override def arity = AnyArity()
-    override val name = "/\\"
+    override val name = "AND"
     override val precedence: (Int, Int) = (3, 3)
   }
 
@@ -30,7 +30,8 @@ object TlaBoolOper {
    */
   object or extends TlaBoolOper {
     override def arity: OperArity = AnyArity()
-    override val name: String = "\\/"
+
+    override val name: String = "OR"
     override val precedence: (Int, Int) = (3, 3)
   }
 
@@ -39,7 +40,8 @@ object TlaBoolOper {
    */
   object not extends TlaBoolOper {
     override def arity: OperArity = FixedArity(1)
-    override val name: String = "~"
+
+    override val name: String = "NOT"
     override val precedence: (Int, Int) = (4, 4)
   }
 
@@ -48,7 +50,8 @@ object TlaBoolOper {
    */
   object implies extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "=>"
+
+    override val name: String = "IMPLIES"
     override val precedence: (Int, Int) = (1, 1)
   }
 
@@ -57,35 +60,48 @@ object TlaBoolOper {
    */
   object equiv extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "<=>"
+
+    override val name: String = "EQUIV"
     override val precedence: (Int, Int) = (2, 2)
   }
 
-  /** \A x \in S : p */
+  /**
+   * A universal quantifier over a set: `\A x \in S : p`.
+   */
   object forall extends TlaBoolOper {
     override def arity: OperArity = FixedArity(3)
-    override val name: String = "\\A3"
+
+    override val name: String = "FORALL3"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 
-  /** \A x : p */
+  /**
+   * A universal quantifier over the whole universe: `\A x : p`.
+   */
   object forallUnbounded extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "\\A2"
+
+    override val name: String = "FORALL2"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 
-  /** \E x \in S : p */
+  /**
+   * An existential quantifier over a set: `\E x \in S : p`.
+   */
   object exists extends TlaBoolOper {
     override def arity: OperArity = FixedArity(3)
-    override val name: String = "\\E3"
+
+    override val name: String = "EXISTS3"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 
-  /** \E x : p */
+  /**
+   * An existential quantifier over the whole universe: `\E x : p`.
+   */
   object existsUnbounded extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "\\E2"
+
+    override val name: String = "EXISTS2"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaControlOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaControlOper.scala
@@ -29,7 +29,7 @@ object TlaControlOper {
    * The rationale is that by using args.tail, one obtains a list similar to the caseOper.
    */
   object caseWithOther extends TlaControlOper {
-    override val name: String = "CASE-OTHER"
+    override val name: String = "CASE_OTHER"
     override val arity: OperArity = MinimalArity(3) && AnyOddArity() //new OperArity( k => k >= 3 && k % 2 == 1 )
     override val interpretation: Interpretation.Value = Interpretation.Predefined
     override val precedence: (Int, Int) = (0, 0)
@@ -39,7 +39,7 @@ object TlaControlOper {
    * The "IF A THEN B ELSE C" operator. The arguments have the following structure: A, B, C.
    */
   object ifThenElse extends TlaControlOper {
-    override val name: String = "IF-THEN-ELSE"
+    override val name: String = "IF_THEN_ELSE"
     override val arity: OperArity = FixedArity(3)
     override val interpretation: Interpretation.Value = Interpretation.Predefined
     override val precedence: (Int, Int) = (0, 0)

diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFiniteSetOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFiniteSetOper.scala
@@ -12,20 +12,20 @@ abstract class TlaFiniteSetOper extends TlaOper {
 object TlaFiniteSetOper {
 
   /**
-   * The operator that checks, whether a set is finite.
+   * The operator that checks, whether a set is finite: `IsFiniteSet(S)`.
    */
   object isFiniteSet extends TlaFiniteSetOper {
     override val arity = FixedArity(1)
-    override val name = "IsFiniteSet"
+    override val name = "FiniteSets!IsFiniteSet"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   /**
-   * The operator that returns the cardinality of a finite set.
+   * The operator that returns the cardinality of a finite set: `Cardinality(S)`.
    */
   object cardinality extends TlaFiniteSetOper {
     override val arity = FixedArity(1)
-    override val name = "Cardinality"
+    override val name = "FiniteSets!Cardinality"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }