From b0a2559091103bed4b4ed3c5e605f0ce897f68bd Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 10 Dec 2024 09:42:56 -0300 Subject: [PATCH 1/3] Fix conversion of Quint nullary polymorphic operators --- .../at/forsyte/apalache/io/quint/Quint.scala | 2 +- .../apalache/io/quint/TestQuintEx.scala | 18 +++++++++++++++--- .../subbuilder/LiteralAndNameBuilder.scala | 8 ++++++++ .../typecomp/TestLiteralAndNameBuilder.scala | 8 ++++++++ 4 files changed, 32 insertions(+), 4 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 index 91ef87fbea..2fb7dbb19b 100644 --- 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 @@ -727,7 +727,7 @@ class Quint(quintOutput: QuintOutput) { val t = typeConv.convert(types(id).typ) Reader { nullaryOpNames => if (nullaryOpNames.contains(name)) { - tla.appOp(tla.name(name, OperT1(Seq(), t))) + tla.appOp(tla.polymorphicName(name, OperT1(Seq(), t))) } else { tla.name(name, t) } 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 index 9245bca5e1..a1b880f9dc 100644 --- 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 @@ -205,7 +205,7 @@ class TestQuintEx extends AnyFunSuite { def translate(qex: QuintEx): TlaEx = { val translator = new Quint(Q.quintOutput) - val nullaryOps = Set[String]() + val nullaryOps = Set[String]("None") val tlaEx = build(translator.tlaExpression(qex).run(nullaryOps)) tlaEx } @@ -793,13 +793,13 @@ class TestQuintEx extends AnyFunSuite { val polyConst1 = "polyConst1" // We want to test that we can use this polymorphic operator by applying it to two - // different values of the same type. + // different values of different types. val appliedToStr = Q.app(polyConst1, Q.s)(QuintIntT(), oper.id) val appliedToBool = Q.app(polyConst1, Q.tt)(QuintIntT(), oper.id) // We'll combine these two applications using addition, just to form a compound expression that includes both val body = Q.app("iadd", appliedToStr, appliedToBool)(QuintIntT()) - // Putting it all to gether, we have the let expression + // Putting it all together, we have the let expression // // ``` // def polyConst1(x): a => int = 1; @@ -811,6 +811,18 @@ class TestQuintEx extends AnyFunSuite { assert(convert(expr) == """LET polyConst1(x) ≜ 1 IN (polyConst1("s")) + (polyConst1(TRUE))""") } + test("can convert nullary polymorphic operator used polymorphically") { + val optionInt = QuintSumT.ofVariantTypes("Some" -> QuintIntT(), "None" -> QuintRecordT.ofFieldTypes()) + val noneInt = Q.nam("None", optionInt) + + val optionBool = QuintSumT.ofVariantTypes("Some" -> QuintBoolT(), "None" -> QuintRecordT.ofFieldTypes()) + val noneBool = Q.nam("None", optionBool) + + val expr = Q.app("Tup", noneInt, noneBool)(QuintTupleT.ofTypes(optionInt, optionBool)) + + assert(convert(expr) == """<>""") + } + 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)) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala index 5fd4178efe..ca3123d7dd 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala @@ -77,6 +77,14 @@ trait LiteralAndNameBuilder { (mi.copy(freeNameScope = scope + (exprName -> finalT), usedNames = mi.usedNames + exprName), ret) } + /** + * {{{exprName: t}}} + * @param exprName + * can take different types under the same scope (polymorphic operator). + */ + def polymorphicName(exprName: String, t: TlaType1): TBuilderInstruction = + unsafeBuilder.name(exprName, t).point[TBuilderInternalState] + /** Attempt to infer the type from the scope. Fails if exprName is not in scope. */ def nameWithInferredType(exprName: String): TBuilderInstruction = get[TBuilderContext].map { mi: TBuilderContext => val scope = mi.freeNameScope diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala index 70c2d6c303..63fc3252cd 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala @@ -152,5 +152,13 @@ class TestLiteralAndNameBuilder extends BuilderTest { } yield () ) } + + // Should not throw with polymorphic names + build( + for { + _ <- builder.polymorphicName("x", IntT1) + _ <- builder.polymorphicName("x", BoolT1) + } yield () + ) } } From afff4366a03ab6fc3b10f1ef5b9b529de0e9d6e1 Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 10 Dec 2024 09:51:11 -0300 Subject: [PATCH 2/3] Add CHANGELOG entry --- .unreleased/bug-fixes/quint-nullary-operators.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/quint-nullary-operators.md diff --git a/.unreleased/bug-fixes/quint-nullary-operators.md b/.unreleased/bug-fixes/quint-nullary-operators.md new file mode 100644 index 0000000000..046a7265a9 --- /dev/null +++ b/.unreleased/bug-fixes/quint-nullary-operators.md @@ -0,0 +1 @@ +Fix a problem when translating Quint nullary operators used polymorphically, see #3044 From e1c2d85343a16e4e74c78ef69e6196747e5b518e Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 13 Dec 2024 10:07:31 -0300 Subject: [PATCH 3/3] Use unsafe builder --- .../at/forsyte/apalache/io/quint/Quint.scala | 15 ++++++++++----- .../subbuilder/LiteralAndNameBuilder.scala | 8 -------- .../tla/typecomp/TestLiteralAndNameBuilder.scala | 8 -------- 3 files changed, 10 insertions(+), 21 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 index 2fb7dbb19b..a9b42ff71e 100644 --- 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 @@ -4,16 +4,14 @@ import at.forsyte.apalache.io.quint.QuintEx._ import at.forsyte.apalache.io.quint.QuintType._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.typecomp._ +import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeLiteralAndNameBuilder import at.forsyte.apalache.tla.types.tla // scalaz is brought in For the Reader monad, which we use for // append-only, context local state for tracking reference to nullary TLA // operators import scalaz._ -// list and traverse give us monadic mapping over lists -// see https://github.com/scalaz/scalaz/blob/88fc7de1c439d152d40fce6b20d90aea33cbb91b/example/src/main/scala-2/scalaz/example/TraverseUsage.scala -import scalaz.std.list._ -import scalaz.syntax.traverse._ +import Scalaz._ import scala.util.{Failure, Success, Try} import at.forsyte.apalache.tla.lir.values.TlaStr @@ -31,6 +29,8 @@ import at.forsyte.apalache.tla.lir.values.TlaStr class Quint(quintOutput: QuintOutput) { private val nameGen = new QuintNameGen // name generator, reused across the entire spec private val typeConv = new QuintTypeConverter + private val unsafeBuilder = new UnsafeLiteralAndNameBuilder {} + private val table = quintOutput.table private val types = quintOutput.types @@ -727,7 +727,12 @@ class Quint(quintOutput: QuintOutput) { val t = typeConv.convert(types(id).typ) Reader { nullaryOpNames => if (nullaryOpNames.contains(name)) { - tla.appOp(tla.polymorphicName(name, OperT1(Seq(), t))) + // Name can be a polymorphic operator, but we need to give it the + // specialized type inferred by Quint to avoid type errors in + // Apalache. So we use the unsafe builder instead, as the safe + // builder enforces that same names have the same types under + // the scope. + tla.appOp(unsafeBuilder.name(name, OperT1(Seq(), t)).point[TBuilderInternalState]) } else { tla.name(name, t) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala index ca3123d7dd..5fd4178efe 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala @@ -77,14 +77,6 @@ trait LiteralAndNameBuilder { (mi.copy(freeNameScope = scope + (exprName -> finalT), usedNames = mi.usedNames + exprName), ret) } - /** - * {{{exprName: t}}} - * @param exprName - * can take different types under the same scope (polymorphic operator). - */ - def polymorphicName(exprName: String, t: TlaType1): TBuilderInstruction = - unsafeBuilder.name(exprName, t).point[TBuilderInternalState] - /** Attempt to infer the type from the scope. Fails if exprName is not in scope. */ def nameWithInferredType(exprName: String): TBuilderInstruction = get[TBuilderContext].map { mi: TBuilderContext => val scope = mi.freeNameScope diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala index 63fc3252cd..70c2d6c303 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala @@ -152,13 +152,5 @@ class TestLiteralAndNameBuilder extends BuilderTest { } yield () ) } - - // Should not throw with polymorphic names - build( - for { - _ <- builder.polymorphicName("x", IntT1) - _ <- builder.polymorphicName("x", BoolT1) - } yield () - ) } }