Merge pull request #2536 from informalsystems/2531/setBy

Rewrite applied `LET/IN`s in the builder

.unreleased/bug-fixes/quint-setBy.md

@@ -0,0 +1,2 @@
+Fix conversion of quint `setBy` operator. See #2531.
+

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))),

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) ~~>

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)
   }

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}}}