close 615: remove \subset, \supset, \supset (#684)

* close #615: remove subsetProper, supsetProper, supseteq * entry in UNRELEASED.md * fix the unit test
apalache-mc · Mar 25, 2021 · 5312c25 · 5312c25
1 parent 698ea27
commit 5312c25
Show file tree

Hide file tree

Showing 13 changed files with 27 additions and 151 deletions.
diff --git a/UNRELEASED.md b/UNRELEASED.md
@@ -36,6 +36,10 @@
 
 * Intermediate representation: removed TlaArithOper.{sum,prod}, as they are not standard, see #580
 
+### Removed
+
+* Intermediate representation: removed non-standard operators subsetProper, supset, supseteq, see #615
+
 ### Known issues
 
 * Multiple-update expressions `[f EXCEPT ![i1][i2] = e1, ![i1][i3] = e2]` may produce incorrect results, see #647
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
@@ -327,11 +327,8 @@ class ToEtcExpr(annotationStore: AnnotationStore, varPool: TypeVarPool) extends
         val opsig = OperT1(List(a, SetT1(a)), BoolT1())
         mkExRefApp(opsig, args)
 
-      // TODO: scheduled for removal, issue #615: \subset, \supset, \supseteq
-      case OperEx(op, args @ _*)
-          if op == TlaSetOper.subseteq || op == TlaSetOper.subsetProper
-            || op == TlaSetOper.supseteq || op == TlaSetOper.supsetProper =>
-        // S \subseteq T, S \subset T, S \supseteq T, S \supset T
+      case OperEx(op, args @ _*) if op == TlaSetOper.subseteq =>
+        // S \subseteq T
         val a = varPool.fresh
         val opsig = OperT1(List(SetT1(a), SetT1(a)), BoolT1())
         mkExRefApp(opsig, args)

diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/types/SignatureGenerator.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/types/SignatureGenerator.scala
@@ -39,7 +39,7 @@ class SignatureGenerator {
     case TlaSetOper.in | TlaSetOper.notin =>
       val t = typeVarGenerator.getUnique
       List(PolyOperT(List(t), OperT(TupT(t, SetT(t)), BoolT)))
-    case TlaSetOper.supsetProper | TlaSetOper.subsetProper | TlaSetOper.supseteq | TlaSetOper.subseteq =>
+    case TlaSetOper.subseteq =>
       val t = typeVarGenerator.getUnique
       List(PolyOperT(List(t), OperT(TupT(SetT(t), SetT(t)), BoolT)))
     case TlaSetOper.cup | TlaSetOper.cap | TlaSetOper.setminus =>

diff --git a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala
@@ -286,13 +286,10 @@ class TestToEtcExpr extends FunSuite with BeforeAndAfterEach with EtcBuilder {
     assert(mkExpected(parser("(Set(c), Set(c)) => Set(c)")) == gen(tla.setminus(tla.intSet(), tla.intSet())))
   }
 
-  test("\\subseteq, \\subset, \\supseteq, \\supset") {
+  test("\\subseteq") {
     def mkExpected(tt: TlaType1) = mkConstAppByType(tt, parser("Set(Int)"), parser("Set(Int)"))
 
-    assert(mkExpected(parser("(Set(a), Set(a)) => Bool")) == gen(tla.subset(tla.intSet(), tla.intSet())))
-    assert(mkExpected(parser("(Set(b), Set(b)) => Bool")) == gen(tla.subseteq(tla.intSet(), tla.intSet())))
-    assert(mkExpected(parser("(Set(c), Set(c)) => Bool")) == gen(tla.supseteq(tla.intSet(), tla.intSet())))
-    assert(mkExpected(parser("(Set(d), Set(d)) => Bool")) == gen(tla.supset(tla.intSet(), tla.intSet())))
+    assert(mkExpected(parser("(Set(a), Set(a)) => Bool")) == gen(tla.subseteq(tla.intSet(), tla.intSet())))
   }
 
   test("SUBSET") {

diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Builder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Builder.scala
@@ -520,21 +520,6 @@ class Builder {
     BuilderOper(TlaSetOper.subseteq, leftSet, rightSet)
   }
 
-  // FIXME: scheduled for removal in #615
-  def subset(leftSet: BuilderEx, rightSet: BuilderEx): BuilderEx = {
-    BuilderOper(TlaSetOper.subsetProper, leftSet, rightSet)
-  }
-
-  // FIXME: scheduled for removal in #615
-  def supset(leftSet: BuilderEx, rightSet: BuilderEx): BuilderEx = {
-    BuilderOper(TlaSetOper.supsetProper, leftSet, rightSet)
-  }
-
-  // FIXME: scheduled for removal in #615
-  def supseteq(leftSet: BuilderEx, rightSet: BuilderEx): BuilderEx = {
-    BuilderOper(TlaSetOper.supseteq, leftSet, rightSet)
-  }
-
   def setminus(leftSet: BuilderEx, rightSet: BuilderEx): BuilderEx = {
     BuilderOper(TlaSetOper.setminus, leftSet, rightSet)
   }
@@ -683,9 +668,6 @@ class Builder {
         TlaSetOper.seqSet.name -> TlaSetOper.seqSet,
         TlaSetOper.setminus.name -> TlaSetOper.setminus,
         TlaSetOper.subseteq.name -> TlaSetOper.subseteq,
-        TlaSetOper.subsetProper.name -> TlaSetOper.subsetProper,
-        TlaSetOper.supseteq.name -> TlaSetOper.supseteq,
-        TlaSetOper.supsetProper.name -> TlaSetOper.supsetProper,
         TlaSetOper.times.name -> TlaSetOper.times,
         TlaSetOper.union.name -> TlaSetOper.union
     )

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
@@ -323,9 +323,6 @@ object JsonWriter {
       TlaSetOper.cup -> "cup",
       TlaSetOper.setminus -> "setminus",
       TlaSetOper.subseteq -> "subseteq",
-      TlaSetOper.subsetProper -> "subset",
-      TlaSetOper.supseteq -> "supseteq",
-      TlaSetOper.supsetProper -> "supset",
       TlaActionOper.composition -> "composition",
       TlaTempOper.leadsTo -> "leadsTo",
       TlaTempOper.guarantees -> "guarantees",

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
@@ -576,9 +576,6 @@ object PrettyWriter {
         TlaSetOper.cup -> "\\union",
         TlaSetOper.setminus -> "\\",
         TlaSetOper.subseteq -> "\\subseteq",
-        TlaSetOper.subsetProper -> "\\subset",
-        TlaSetOper.supseteq -> "\\supseteq",
-        TlaSetOper.supsetProper -> "\\supset",
         TlaActionOper.composition -> "\\cdot",
         TlaTempOper.leadsTo -> "~>",
         TlaTempOper.guarantees -> "-+->",

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
@@ -171,26 +171,23 @@ object UTFPrinter extends Printer {
           case TlaSeqOper.tail   => mkApp("Tail(%s)", args: _*)
           case TlaSeqOper.len    => mkApp("Len(%s)", args: _*)
 
-          case TlaSetOper.enumSet      => "{%s}".format(str(args))
-          case TlaSetOper.in           => mkOpApp("%%s %s %%s".format(m_in), args: _*)
-          case TlaSetOper.notin        => mkOpApp("%%s %s %%s".format(m_notin), args: _*)
-          case TlaSetOper.cap          => mkOpApp("%%s %s %%s".format(m_cap), args: _*)
-          case TlaSetOper.cup          => mkOpApp("%%s %s %%s".format(m_cup), args: _*)
-          case TlaSetOper.filter       => mkOpApp("{%%s %s %%s: %%s}".format(m_in), args: _*)
-          case TlaSetOper.funSet       => mkOpApp("[%%s %s %%s]".format(m_rarrow), args: _*)
-          case TlaSetOper.map          => "{%s : %s}".format(apply(args.head), opAppStrPairs(args.tail, pad(m_in), ", "))
-          case TlaSetOper.powerset     => mkOpApp("SUBSET %s", args: _*)
-          case TlaSetOper.recSet       => "[" + opAppStrPairs(args, ": ", ", ") + "]"
-          case TlaSetOper.seqSet       => mkApp("Seq(%s)", args: _*)
-          case TlaSetOper.setminus     => mkOpApp("%%s %s %%s".format(m_setminus), args: _*)
-          case TlaSetOper.subseteq     => mkOpApp("%%s %s %%s".format(m_subseteq), args: _*)
-          case TlaSetOper.subsetProper => mkOpApp("%%s %s %%s".format(m_subset), args: _*)
-          case TlaSetOper.supseteq     => mkOpApp("%%s %s %%s".format(m_supseteq), args: _*)
-          case TlaSetOper.supsetProper => mkOpApp("%%s %s %%s".format(m_supset), args: _*)
-          case TlaSetOper.times        => opAppStr(args, pad(m_times))
-          case TlaSetOper.union        => mkOpApp("UNION %s", args: _*)
-          case TlcOper.atat            => str(args, " @@ ")
-          case TlcOper.colonGreater    => "%s :> %s".format(args.head, args(1))
+          case TlaSetOper.enumSet   => "{%s}".format(str(args))
+          case TlaSetOper.in        => mkOpApp("%%s %s %%s".format(m_in), args: _*)
+          case TlaSetOper.notin     => mkOpApp("%%s %s %%s".format(m_notin), args: _*)
+          case TlaSetOper.cap       => mkOpApp("%%s %s %%s".format(m_cap), args: _*)
+          case TlaSetOper.cup       => mkOpApp("%%s %s %%s".format(m_cup), args: _*)
+          case TlaSetOper.filter    => mkOpApp("{%%s %s %%s: %%s}".format(m_in), args: _*)
+          case TlaSetOper.funSet    => mkOpApp("[%%s %s %%s]".format(m_rarrow), args: _*)
+          case TlaSetOper.map       => "{%s : %s}".format(apply(args.head), opAppStrPairs(args.tail, pad(m_in), ", "))
+          case TlaSetOper.powerset  => mkOpApp("SUBSET %s", args: _*)
+          case TlaSetOper.recSet    => "[" + opAppStrPairs(args, ": ", ", ") + "]"
+          case TlaSetOper.seqSet    => mkApp("Seq(%s)", args: _*)
+          case TlaSetOper.setminus  => mkOpApp("%%s %s %%s".format(m_setminus), args: _*)
+          case TlaSetOper.subseteq  => mkOpApp("%%s %s %%s".format(m_subseteq), args: _*)
+          case TlaSetOper.times     => opAppStr(args, pad(m_times))
+          case TlaSetOper.union     => mkOpApp("UNION %s", args: _*)
+          case TlcOper.atat         => str(args, " @@ ")
+          case TlcOper.colonGreater => "%s :> %s".format(args.head, args(1))
           case TlaOper.label =>
             val body = this(args.head)
             val label = this(args.tail.head)

diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSetOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSetOper.scala
@@ -81,30 +81,6 @@ object TlaSetOper {
     override val precedence: (Int, Int) = (5, 5)
   }
 
-  /**
-   * The standard \subset operator.
-   *
-   * WARNING: Do not confuse with SUBSET that is implemented by TlaSetOper.powerset.
-   */
-  object subsetProper extends TlaSetOper {
-    override val arity = FixedArity(2)
-    override val name = "\\subset"
-    override val precedence: (Int, Int) = (5, 5)
-  }
-
-  object supsetProper extends TlaSetOper {
-    override val arity = FixedArity(2)
-    override val name = "\\supset"
-    override val precedence: (Int, Int) = (5, 5)
-  }
-
-  /** the standard \supseteq operator */
-  object supseteq extends TlaSetOper {
-    override val arity = FixedArity(2)
-    override val name = "\\supseteq"
-    override val precedence: (Int, Int) = (5, 5)
-  }
-
   /** the standard set difference */
   object setminus extends TlaSetOper {
     override val arity = FixedArity(2)

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
@@ -74,8 +74,7 @@ trait IrGenerators {
    */
   val setOperators = List(TlaSetOper.cap, TlaSetOper.cup, TlaSetOper.enumSet, TlaSetOper.filter, TlaSetOper.funSet,
       TlaSetOper.in, TlaSetOper.notin, TlaSetOper.map, TlaSetOper.powerset, TlaSetOper.recSet, TlaSetOper.seqSet,
-      TlaSetOper.setminus, TlaSetOper.subseteq, TlaSetOper.subsetProper, TlaSetOper.supseteq, TlaSetOper.supsetProper,
-      TlaSetOper.times, TlaSetOper.union)
+      TlaSetOper.setminus, TlaSetOper.subseteq, TlaSetOper.times, TlaSetOper.union)
 
   def genTypeTag: Gen[TypeTag] = for {
     i <- arbitrary[Int]

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
@@ -1372,22 +1372,9 @@ class TestBuilder extends FunSuite with TestingPredefs {
 
     assert(seqSetBuild == OperEx(TlaSetOper.seqSet, n_a))
 
-    val subsetBuild = bd.subset(n_a, n_b).untyped()
-
-    assert(subsetBuild == OperEx(TlaSetOper.subsetProper, n_a, n_b))
-
     val subseteqBuild = bd.subseteq(n_a, n_b).untyped()
-
     assert(subseteqBuild == OperEx(TlaSetOper.subseteq, n_a, n_b))
 
-    val supsetBuild = bd.supset(n_a, n_b).untyped()
-
-    assert(supsetBuild == OperEx(TlaSetOper.supsetProper, n_a, n_b))
-
-    val supseteqBuild = bd.supseteq(n_a, n_b).untyped()
-
-    assert(supseteqBuild == OperEx(TlaSetOper.supseteq, n_a, n_b))
-
     val setminusBuild = bd.setminus(n_a, n_b).untyped()
 
     assert(setminusBuild == OperEx(TlaSetOper.setminus, n_a, n_b))
@@ -1474,30 +1461,12 @@ class TestBuilder extends FunSuite with TestingPredefs {
     assert(seqSetBuild == OperEx(TlaSetOper.seqSet, n_a))
     assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.seqSet.name, n_a, n_b).untyped())
 
-    val subsetBuild = bd.byName(TlaSetOper.subsetProper.name, n_a, n_b).untyped()
-
-    assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.subsetProper.name, n_a).untyped())
-    assert(subsetBuild == OperEx(TlaSetOper.subsetProper, n_a, n_b))
-    assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.subsetProper.name, n_a, n_b, n_c).untyped())
-
     val subseteqBuild = bd.byName(TlaSetOper.subseteq.name, n_a, n_b).untyped()
 
     assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.subseteq.name, n_a).untyped())
     assert(subseteqBuild == OperEx(TlaSetOper.subseteq, n_a, n_b))
     assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.subseteq.name, n_a, n_b, n_c).untyped())
 
-    val supsetBuild = bd.byName(TlaSetOper.supsetProper.name, n_a, n_b).untyped()
-
-    assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.supsetProper.name, n_a).untyped())
-    assert(supsetBuild == OperEx(TlaSetOper.supsetProper, n_a, n_b))
-    assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.supsetProper.name, n_a, n_b, n_c).untyped())
-
-    val supseteqBuild = bd.byName(TlaSetOper.supseteq.name, n_a, n_b).untyped()
-
-    assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.supseteq.name, n_a).untyped())
-    assert(supseteqBuild == OperEx(TlaSetOper.supseteq, n_a, n_b))
-    assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.supseteq.name, n_a, n_b, n_c).untyped())
-
     val setminusBuild = bd.byName(TlaSetOper.setminus.name, n_a, n_b).untyped()
 
     assertThrows[IllegalArgumentException](bd.byName(TlaSetOper.setminus.name, n_a).untyped())
@@ -1609,14 +1578,6 @@ class TestBuilder extends FunSuite with TestingPredefs {
     assert(seqSetBuild == OperEx(TlaSetOper.seqSet, n_a))
     assert(seqSetBuildBad2 == NullEx)
 
-    val subsetBuildBad1 = bd.byNameOrNull(TlaSetOper.subsetProper.name, n_a).untyped()
-    val subsetBuild = bd.byNameOrNull(TlaSetOper.subsetProper.name, n_a, n_b).untyped()
-    val subsetBuildBad2 = bd.byNameOrNull(TlaSetOper.subsetProper.name, n_a, n_b, n_c).untyped()
-
-    assert(subsetBuildBad1 == NullEx)
-    assert(subsetBuild == OperEx(TlaSetOper.subsetProper, n_a, n_b))
-    assert(subsetBuildBad2 == NullEx)
-
     val subseteqBuildBad1 = bd.byNameOrNull(TlaSetOper.subseteq.name, n_a).untyped()
     val subseteqBuild = bd.byNameOrNull(TlaSetOper.subseteq.name, n_a, n_b).untyped()
     val subseteqBuildBad2 = bd.byNameOrNull(TlaSetOper.subseteq.name, n_a, n_b, n_c).untyped()
@@ -1625,22 +1586,6 @@ class TestBuilder extends FunSuite with TestingPredefs {
     assert(subseteqBuild == OperEx(TlaSetOper.subseteq, n_a, n_b))
     assert(subseteqBuildBad2 == NullEx)
 
-    val supsetBuildBad1 = bd.byNameOrNull(TlaSetOper.supsetProper.name, n_a).untyped()
-    val supsetBuild = bd.byNameOrNull(TlaSetOper.supsetProper.name, n_a, n_b).untyped()
-    val supsetBuildBad2 = bd.byNameOrNull(TlaSetOper.supsetProper.name, n_a, n_b, n_c).untyped()
-
-    assert(supsetBuildBad1 == NullEx)
-    assert(supsetBuild == OperEx(TlaSetOper.supsetProper, n_a, n_b))
-    assert(supsetBuildBad2 == NullEx)
-
-    val supseteqBuildBad1 = bd.byNameOrNull(TlaSetOper.supseteq.name, n_a).untyped()
-    val supseteqBuild = bd.byNameOrNull(TlaSetOper.supseteq.name, n_a, n_b).untyped()
-    val supseteqBuildBad2 = bd.byNameOrNull(TlaSetOper.supseteq.name, n_a, n_b, n_c).untyped()
-
-    assert(supseteqBuildBad1 == NullEx)
-    assert(supseteqBuild == OperEx(TlaSetOper.supseteq, n_a, n_b))
-    assert(supseteqBuildBad2 == NullEx)
-
     val setminusBuildBad1 = bd.byNameOrNull(TlaSetOper.setminus.name, n_a).untyped()
     val setminusBuild = bd.byNameOrNull(TlaSetOper.setminus.name, n_a, n_b).untyped()
     val setminusBuildBad2 = bd.byNameOrNull(TlaSetOper.setminus.name, n_a, n_b, n_c).untyped()

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
@@ -69,14 +69,8 @@ class TestTlaExpr extends FunSuite {
     OperEx(TlaSetOper.notin, x, y)
     // x \setminus y
     OperEx(TlaSetOper.setminus, x, y)
-    // x \subset y
-    OperEx(TlaSetOper.subsetProper, x, y)
     // x \subseteq y
     OperEx(TlaSetOper.subseteq, x, y)
-    // x \supset y
-    OperEx(TlaSetOper.supsetProper, x, y)
-    // x \supseteq y
-    OperEx(TlaSetOper.supseteq, x, y)
     // SUBSET y
     OperEx(TlaSetOper.powerset, y)
     // UNION x
@@ -112,14 +106,8 @@ class TestTlaExpr extends FunSuite {
     expectWrongArity(TlaSetOper.notin, y)
     // x \setminus y
     expectWrongArity(TlaSetOper.setminus, y)
-    // x \subset y
-    expectWrongArity(TlaSetOper.subsetProper, x)
     // x \subseteq y
     expectWrongArity(TlaSetOper.subseteq, x)
-    // x \supset y
-    expectWrongArity(TlaSetOper.supsetProper, x)
-    // x \supseteq y
-    expectWrongArity(TlaSetOper.supseteq, x)
     // SUBSET y
     expectWrongArity(TlaSetOper.powerset, y, x)
     // UNION x

diff --git a/...est/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestKeraLanguagePred.scala b/...est/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestKeraLanguagePred.scala
@@ -96,9 +96,6 @@ class TestKeraLanguagePred extends LanguagePredTestSuite {
     expectFail(pred.isExprOk(cap(enumSet(int(1)), enumSet(int(2)))))
     expectFail(pred.isExprOk(setminus(enumSet(int(1)), enumSet(int(2)))))
     expectFail(pred.isExprOk(notin(int(1), enumSet(int(2)))))
-    expectFail(pred.isExprOk(supseteq(enumSet(int(1)), enumSet(int(2)))))
-    expectFail(pred.isExprOk(subset(enumSet(int(1)), enumSet(int(2)))))
-    expectFail(pred.isExprOk(supset(enumSet(int(1)), enumSet(int(2)))))
   }
 
   test("not a KerA record expression") {