diff --git a/.unreleased/bug-fixes/quint-setBy.md b/.unreleased/bug-fixes/quint-setBy.md new file mode 100644 index 0000000000..24e32e9f8e --- /dev/null +++ b/.unreleased/bug-fixes/quint-setBy.md @@ -0,0 +1,2 @@ +Fix conversion of quint `setBy` operator. See #2531. + diff --git a/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/PreproPassImpl.scala b/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/PreproPassImpl.scala index d0ff7cbd28..7370746be6 100644 --- a/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/PreproPassImpl.scala +++ b/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/PreproPassImpl.scala @@ -1,16 +1,16 @@ package at.forsyte.apalache.tla.passes.pp -import at.forsyte.apalache.infra.passes.DerivedPredicates import at.forsyte.apalache.infra.passes.Pass.PassResult -import at.forsyte.apalache.infra.passes.options.OptionGroup -import at.forsyte.apalache.io.lir.TlaWriterFactory import at.forsyte.apalache.tla.imp.src.SourceStore +import at.forsyte.apalache.io.lir.TlaWriterFactory import at.forsyte.apalache.tla.lir.storage.ChangeListener import at.forsyte.apalache.tla.lir.transformations.standard._ import at.forsyte.apalache.tla.lir.transformations.{TlaModuleTransformation, TransformationTracker} import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule} -import at.forsyte.apalache.tla.pp.{Desugarer, Keramelizer, LetInApplier, Normalizer, UniqueNameGenerator} +import at.forsyte.apalache.tla.pp.{Desugarer, Keramelizer, Normalizer, UniqueNameGenerator} import com.google.inject.Inject +import at.forsyte.apalache.infra.passes.options.OptionGroup +import at.forsyte.apalache.infra.passes.DerivedPredicates /** * A preprocessing pass that simplifies TLA+ expression by running multiple transformation. @@ -51,7 +51,6 @@ class PreproPassImpl @Inject() ( List( ("PrimePropagation", createModuleTransformerForPrimePropagation(varSet)), ("Desugarer", ModuleByExTransformer(Desugarer(gen, varSet, tracker))), - ("LetInApplier", ModuleByExTransformer(LetInApplier(tracker))), ("UniqueRenamer", renaming.renameInModule), ("Normalizer", ModuleByExTransformer(Normalizer(tracker))), ("Keramelizer", ModuleByExTransformer(Keramelizer(gen, tracker))), 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 790634a718..b81bcf0f31 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 @@ -39,7 +39,6 @@ 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._, scalaz.syntax.traverse._ -import at.forsyte.apalache.tla.lir.NameEx class Quint(moduleData: QuintOutput) { protected val module = moduleData.modules(0) @@ -309,51 +308,22 @@ class Quint(moduleData: QuintOutput) { // // Since `__e` is free in `__test` the binding in the head of `__QUINT_LAMBDA0` // will bind the element at the appropriate place in the test. - def selectSeq(opName: String, seqType: TlaType1): Converter = quintArgs => { - // `mk(varNam, seq, test)` is an implementation of Apalache's rewired - // version of `SelectSeq` using the variable named 'varName' in the - // append operation over the give `seq` guarded by the given `test`. - // `test` is given the TLA name constructed with the given `varName`, - // so that the test can be applied to that element if needed. - def mk(elemVarName: String, seq: T, test: T => T): T = { - val elemType = seqType match { - case SeqT1(elem) => elem - case invalidType => throw new QuintIRParseError(s"sequence ${seq} has invalid type ${invalidType}") - } - val resultParam = tla.param(uniqueVarName(), seqType) - val elemParam = tla.param(elemVarName, elemType) - val result = tla.name(resultParam._1.name, resultParam._2) - val elem = tla.name(elemParam._1.name, elemParam._2) - val ite = tla.ite(test(elem), tla.append(result, elem), result) - val testLambda = tla.lambda(uniqueLambdaName(), ite, resultParam, elemParam) - tla.foldSeq(testLambda, tla.emptySeq(elemType), seq) - } - - quintArgs match { - case Seq(_, _: QuintLambda) => - binaryBindingApp(opName, - (x, seq, testBody) => { - // When the test operator is given as a lambda we derive - // the element variable name from the lambda's parameter - val elemNameStr = build[TlaEx](x) match { - case NameEx(n) => n - case exp => throw new QuintIRParseError(s"binaryBindingApp did not provide ${exp} as a name") - } - // The element is ignored in the test, since the variable - // is already present n the testBody - val test = ((_: T) => testBody) - mk(elemNameStr, seq, test) - })(quintArgs) - case _ => { - binaryApp(opName, - (seq, testOp) => { - // When the test operator is given by name, we apply it to the element. - val test = (elem: T) => tla.appOp(testOp, elem) - mk(uniqueVarName(), seq, test) - })(quintArgs) - } - } - } + def selectSeq(opName: String, seqType: TlaType1): Converter = + binaryApp(opName, + (seq, testOp) => { + // When the test operator is given by name, we apply it to the element. + val elemType = seqType match { + case SeqT1(elem) => elem + case invalidType => throw new QuintIRParseError(s"sequence ${seq} has invalid type ${invalidType}") + } + val resultParam = tla.param(uniqueVarName(), seqType) + val elemParam = tla.param(uniqueLambdaName(), elemType) + val result = tla.name(resultParam._1.name, resultParam._2) + val elem = tla.name(elemParam._1.name, elemParam._2) + val ite = tla.ite(tla.appOp(testOp, elem), tla.append(result, elem), result) + val testLambda = tla.lambda(uniqueLambdaName(), ite, resultParam, elemParam) + tla.foldSeq(testLambda, tla.emptySeq(elemType), seq) + }) def exceptWithUpdate(opName: String, id: Int): Converter = // f.setBy(x, op) ~~> 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 6b5e461cf3..7a304b8cf5 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 @@ -444,13 +444,13 @@ class TestQuintEx extends AnyFunSuite { test("can convert builtin select operator application") { val expected = - "Apalache!ApaFoldSeqLeft(LET __QUINT_LAMBDA0(__quint_var0, n) ≜ IF (n > 0) THEN (Append(__quint_var0, n)) ELSE __quint_var0 IN __QUINT_LAMBDA0, <<>>, <<1, 2, 3>>)" + "Apalache!ApaFoldSeqLeft(LET __QUINT_LAMBDA2(__quint_var0, __QUINT_LAMBDA1) ≜ IF LET __QUINT_LAMBDA0(n) ≜ n > 0 IN __QUINT_LAMBDA0(__QUINT_LAMBDA1) THEN (Append(__quint_var0, __QUINT_LAMBDA1)) ELSE __quint_var0 IN __QUINT_LAMBDA2, <<>>, <<1, 2, 3>>)" assert(convert(Q.selectGreaterThanZero) == expected) } test("can convert builtin select operator application with named test operator") { val expected = - "Apalache!ApaFoldSeqLeft(LET __QUINT_LAMBDA0(__quint_var1, __quint_var0) ≜ IF (intToBoolOp(__quint_var0)) THEN (Append(__quint_var1, __quint_var0)) ELSE __quint_var1 IN __QUINT_LAMBDA0, <<>>, <<1, 2, 3>>)" + "Apalache!ApaFoldSeqLeft(LET __QUINT_LAMBDA1(__quint_var0, __QUINT_LAMBDA0) ≜ IF (intToBoolOp(__QUINT_LAMBDA0)) THEN (Append(__quint_var0, __QUINT_LAMBDA0)) ELSE __quint_var0 IN __QUINT_LAMBDA1, <<>>, <<1, 2, 3>>)" assert(convert(Q.selectNamedIntToBoolOp) == expected) } @@ -560,7 +560,7 @@ class TestQuintEx extends AnyFunSuite { test("can convert builtin setBy operator") { val expected = """ |LET __quint_var0 ≜ Apalache!SetAsFun({<<0, 1>>, <<3, 42>>}) IN - |[__quint_var0() EXCEPT ![<<1>>] = (LET __QUINT_LAMBDA0(n) ≜ n + 1 IN __QUINT_LAMBDA0(__quint_var0()[1]))] + |[__quint_var0() EXCEPT ![<<1>>] = LET __QUINT_LAMBDA0(n) ≜ n + 1 IN __QUINT_LAMBDA0(__quint_var0()[1])] """.stripMargin.linesIterator.mkString(" ").trim assert(convert(Q.setByExpression) == expected) } diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/LetInApplier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/LetInApplier.scala deleted file mode 100644 index 6026be6cea..0000000000 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/LetInApplier.scala +++ /dev/null @@ -1,44 +0,0 @@ -package at.forsyte.apalache.tla.pp - -import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.lir.oper.TlaOper -import at.forsyte.apalache.tla.lir.transformations._ - -/** - * LetInApplier turns applications of operator-typed LET-expressions, into LET-expressions with applications pushed into - * the body. - * - * Workaround until LAMBDAS are systematically supported (#2534). - * - * @author - * Jure Kukovec - */ -class LetInApplier(tracker: TransformationTracker) extends TlaExTransformation { - override def apply(input: TlaEx): TlaEx = { - transform(input) - } - - private def transform: TlaExTransformation = tracker.trackEx { - case ex @ OperEx(TlaOper.apply, LetInEx(nameEx @ NameEx(operName), decl @ TlaOperDecl(declName, _, _)), args @ _*) - if operName == declName => - LetInEx( - OperEx(TlaOper.apply, nameEx +: args.map(transform): _*)(ex.typeTag), - decl.copy(body = transform(decl.body)), - )(ex.typeTag) - - case ex @ OperEx(op, args @ _*) => - val newArgs = args.map(transform) - if (args == newArgs) ex else OperEx(op, newArgs: _*)(ex.typeTag) - - case ex @ LetInEx(body, defs @ _*) => - val newDefs = defs.map(tracker.trackOperDecl { d => d.copy(body = transform(d.body)) }) - val newBody = transform(body) - if (defs == newDefs && body == newBody) ex else LetInEx(newBody, newDefs: _*)(ex.typeTag) - - case ex @ _ => ex - } -} - -object LetInApplier { - def apply(tracker: TransformationTracker): LetInApplier = new LetInApplier(tracker) -} diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestLetInApplier.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestLetInApplier.scala deleted file mode 100644 index 15c9a09c7a..0000000000 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestLetInApplier.scala +++ /dev/null @@ -1,77 +0,0 @@ -package at.forsyte.apalache.tla.pp - -import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker -import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla._ -import org.junit.runner.RunWith -import org.scalatest.BeforeAndAfterEach -import org.scalatest.funsuite.AnyFunSuite -import org.scalatestplus.junit.JUnitRunner - -@RunWith(classOf[JUnitRunner]) -class TestLetInApplier extends AnyFunSuite with BeforeAndAfterEach { - - private var delambda = new LetInApplier(new IdleTracker) - - override def beforeEach(): Unit = { - delambda = new LetInApplier(new IdleTracker) - } - - val intToIntT: TlaType1 = OperT1(Seq(IntT1), IntT1) - val unitToIntT: TlaType1 = OperT1(Seq.empty, IntT1) - - test("""NoOp on non-(lambda applications) and non-lambda expressions""") { - val values: Seq[TlaEx] = Seq( - int(1), - name("x", StrT1), - appOp(name("Op", intToIntT), int(1)), - appOp(name("Op", unitToIntT)), - // LET F(p) == p + 1 IN F(1) - letIn( - appOp(name("F", intToIntT), int(1)), - decl("F", plus(name("p", IntT1), int(1)), param("p", IntT1)), - ), - ) - - val txdValues = values.map(delambda) - assert(txdValues == values) - } - - test("""Correct transformation on lambda applications""") { - - def letShell(body: TBuilderInstruction, operName: String = "F", paramName: String = "p"): TBuilderInstruction = - letIn( - body, - decl(operName, plus(name(paramName, IntT1), int(1)), param(paramName, IntT1)), - ) - - val lambda1 = letShell(name("F", intToIntT)) - val arg1 = int(1) - val lambdaApp1 = appOp(lambda1, arg1) - val expected1: TlaEx = letShell(appOp(name("F", intToIntT), arg1)) - - assert(delambda(lambdaApp1) == expected1) - assert(delambda(expected1) == expected1) - - val lambda2 = letShell(name("F2", intToIntT), "F2", "p2") - val arg2 = appOp(lambda2, int(1)) - val lambdaApp2 = appOp(lambda1, arg2) - - val expected2: TlaEx = letShell( - appOp( - name("F", intToIntT), - letShell( - appOp(name("F2", intToIntT), int(1)), - "F2", - "p2", - ), - ) - ) - - assert(delambda(lambdaApp2) == expected2) - assert(delambda(expected2) == expected2) - - } - -} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala index 46eb6ae502..400d37f8e2 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala @@ -22,7 +22,17 @@ class UnsafeBaseBuilder extends ProtoBuilder { def neql(lhs: TlaEx, rhs: TlaEx): TlaEx = buildBySignatureLookup(TlaOper.ne, lhs, rhs) /** {{{Op(args[1],...,args[n])}}} */ - def appOp(Op: TlaEx, args: TlaEx*): TlaEx = buildBySignatureLookup(TlaOper.apply, Op +: args: _*) + def appOp(Op: TlaEx, args: TlaEx*): TlaEx = { + Op match { + // This is a workaround for the fact that that we currently de-lambda, + // because lambdas are not supported in the Apalache IR. See + // https://github.com/informalsystems/apalache/issues/2532 + case LetInEx(nameEx @ NameEx(operName), decl) if operName == decl.name => + val appliedByName = buildBySignatureLookup(TlaOper.apply, nameEx +: args: _*) + LetInEx(appliedByName, decl)(appliedByName.typeTag) + case _ => buildBySignatureLookup(TlaOper.apply, Op +: args: _*) + } + } /** * {{{CHOOSE x: p}}}