Account for predefined set names (#2603)

Translate name of predefined Bool set
apalache-mc · Jun 16, 2023 · 79900a4 · 79900a4
1 parent ed07563
commit 79900a4
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 7 deletions.
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
@@ -633,13 +633,19 @@ class Quint(moduleData: QuintOutput) {
         case QuintInt(_, i)  => Reader(_ => tla.int(i))
         case QuintStr(_, s)  => Reader(_ => tla.str(s))
         case QuintName(id, name) =>
-          val t = Quint.typeToTlaType(types(id).typ)
-          Reader { nullaryOpNames =>
-            if (nullaryOpNames.contains(name)) {
-              tla.appOp(tla.name(name, OperT1(Seq(), t)))
-            } else {
-              tla.name(name, t)
-            }
+          name match {
+            // special case: predefined set BOOLEAN is Bool in Quint
+            case "Bool" => Reader(_ => tla.booleanSet())
+            // general case: some other name
+            case _ =>
+              val t = Quint.typeToTlaType(types(id).typ)
+              Reader { nullaryOpNames =>
+                if (nullaryOpNames.contains(name)) {
+                  tla.appOp(tla.name(name, OperT1(Seq(), t)))
+                } else {
+                  tla.name(name, t)
+                }
+              }
           }
         case QuintLet(_, binding: QuintDef.QuintOpDef, scope) if binding.qualifier == "nondet" =>
           nondetBinding(binding, scope)

diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
@@ -206,6 +206,12 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(Q.name) == "n")
   }
 
+  test("can convert predefined sets") {
+    assert(convert(Q.nam("Bool", QuintSetT(QuintBoolT()))) == "BOOLEAN")
+    assert(convert(Q.nam("Int", QuintSetT(QuintIntT()))) == "Int")
+    assert(convert(Q.nam("Nat", QuintSetT(QuintIntT()))) == "Nat")
+  }
+
   test("can convert let expression") {
     assert(convert(Q.letFooBeTrueIn42) == "LET foo ≜ TRUE IN 42")
   }