Merge pull request #2782 from informalsystems/2774/catch-nonnondet-oneOf

Add case to handle oneOf outside of nondet

tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

@@ -409,6 +409,15 @@ class Quint(quintOutput: QuintOutput) {
       val applicationBuilder: Seq[QuintEx] => NullaryOpReader[TBuilderInstruction] = opName match {
         // First we check for application of builtin operators
 
+        // Illegal builtins
+        // We expect that these builins will be eliminated in earlier stages
+        // of the translation (e.g., inside special forms like `nondet`) or
+        // via rewrites in quint.
+        case "oneOf" =>
+          // See https://github.com/informalsystems/apalache/issues/2774
+          throw new QuintIRParseError(
+              s"`oneOf` can only occur as the principle operator of a `nondet` declaration: `oneOf` operator with id ${id} applied to ${quintArgs}")
+
         // Booleans
         case "eq"      => binaryApp(opName, tla.eql)
         case "neq"     => binaryApp(opName, tla.neql)

tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala

@@ -751,4 +751,10 @@ class TestQuintEx extends AnyFunSuite {
     // And if our conversion logic is correct, we can convert this to Apalache's IR:
     assert(convert(expr) == """LET polyConst1(x) ≜ 1 IN (polyConst1("s")) + (polyConst1(TRUE))""")
   }
+
+  test("oneOf operator occuring outside of a nondet binding is an error") {
+    // See https://github.com/informalsystems/apalache/issues/2774
+    val err = intercept[QuintIRParseError](convert(Q.oneOfSet))
+    assert(err.getMessage().contains("`oneOf` can only occur as the principle operator of a `nondet` declaration"))
+  }
 }