Merge pull request #2916 from konnov/igor/quint-generate

Translate Quint `generate`
apalache-mc · Aug 14, 2024 · 9e6071b · 9e6071b
2 parents 6ba3a45 + 4e48675
commit 9e6071b
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 3 deletions.
diff --git a/.unreleased/features/translate-generate.md b/.unreleased/features/translate-generate.md
@@ -0,0 +1 @@
+Translate Quint's generate into `Apalache!Gen` (#2916)
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
@@ -655,9 +655,13 @@ class Quint(quintOutput: QuintOutput) {
 
   // Convert Quint's nondet variable binding
   //
-  //   val nondet name = oneOf(domain); scope
+  //   nondet name = oneOf(domain); scope
   //   ~~>
   //   \E name \in domain: scope
+  //
+  //   nondet name = generate(sz, typeSet); scope
+  //   ~~>
+  //   \E name \in { Apalache!Gen(sz) }: scope
   private val nondetBinding: (QuintDef.QuintOpDef, QuintEx) => NullaryOpReader[TBuilderInstruction] = {
     case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "oneOf", Seq(domain))), scope) =>
       val elemType = typeConv.convert(types(id).typ)
@@ -666,6 +670,19 @@ class Quint(quintOutput: QuintOutput) {
         tlaDomain <- tlaExpression(domain)
         tlaScope <- tlaExpression(scope)
       } yield tla.exists(tlaName, tlaDomain, tlaScope)
+
+    case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(bound, _))), scope) =>
+      val elemType = typeConv.convert(types(id).typ)
+      val boundIntConst = intFromExpr(bound)
+      if (boundIntConst.isEmpty) {
+        throw new QuintIRParseError(s"nondet $name = generate($bound) ... expects an integer constant")
+      }
+      val genExpr = tla.enumSet(tla.gen(boundIntConst.get, elemType))
+      val tlaName = tla.name(name, elemType)
+      for {
+        tlaScope <- tlaExpression(scope)
+      } yield tla.exists(tlaName, genExpr, tlaScope)
+
     case invalidValue =>
       throw new QuintIRParseError(s"nondet keyword used to bind invalid value ${invalidValue}")
   }
@@ -804,4 +821,14 @@ class Quint(quintOutput: QuintOutput) {
         .reverse // Return the declarations to their original order
     }
   } yield TlaModule(module.name, declarations)
+
+  private def intFromExpr(expr: QuintEx): Option[BigInt] = {
+    expr match {
+      case QuintInt(_, value) =>
+        Some(value)
+
+      case _ =>
+        None
+    }
+  }
 }
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
@@ -172,7 +172,15 @@ class TestQuintEx extends AnyFunSuite {
     val chooseSomeFromIntSet = app("chooseSome", intSet)(QuintIntT())
     val oneOfSet = app("oneOf", intSet)(QuintIntT())
     val nondetBinding =
-      e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintIntT())
+      e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintBoolT())
+    val generateSet = app("generate", _42, app("Set", _42)(QuintSetT(QuintIntT())))(QuintSetT(QuintIntT()))
+    val nondetGenerateId = uid
+    val appGenSet =
+      app("eq", e(QuintName(uid, "S"), QuintSetT(QuintIntT())), app("Set")(QuintSetT(QuintIntT())))(QuintBoolT())
+    val nondetGenerate =
+      e(QuintLet(uid,
+              d(QuintDef.QuintOpDef(nondetGenerateId, "S", "nondet", generateSet),
+                  QuintOperT(Seq(), QuintSetT(QuintIntT()))), appGenSet), QuintBoolT())
     // Requires ID registered with type
     val selectGreaterThanZero = app("select", intList, intIsGreaterThanZero)(QuintSeqT(QuintIntT()))
     val addOne = app("iadd", name, _1)(QuintIntT())
@@ -710,10 +718,14 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(Q.app("put", Q.intMap, Q._3, Q._42)(intMapT)) == expected)
   }
 
-  test("can convert nondet bindings") {
+  test("can convert nondet...oneOf") {
     assert(convert(Q.nondetBinding) == "∃n ∈ {1, 2, 3}: (n > 0)")
   }
 
+  test("can convert nondet...generate") {
+    assert(convert(Q.nondetGenerate) == "∃S ∈ {Apalache!Gen(42)}: (S = {})")
+  }
+
   test("can convert let binding with reference to name in scope") {
     assert(convert(Q.letNbe42inNisGreaterThan0) == "LET n ≜ 42 IN n() > 0")
   }