Merge branch 'main' into ro/update_doc

.unreleased/bug-fixes/2542-quint-row-recs.md

@@ -0,0 +1,2 @@
+Fix conversion of quint records. See #2542.
+

Makefile

@@ -3,7 +3,7 @@
 # Markdown files used for integration tests
 TEST_MD_FILES := $(wildcard test/tla/*.md)
 
-.PHONY: default all apalache package compile test test-coverage integration docker dist fmt-check fmt-fix clean run docs docs-view tla-io/src/test/resources/tictactoe.json
+.PHONY: default all apalache package compile test test-coverage integration docker dist fmt-check fmt-fix clean run docs docs-view quint-fixtures tla-io/src/test/resources/tictactoe.json test/tla/booleans.qnt.json
 
 default: package
 
@@ -39,11 +39,20 @@ test-coverage:
 integration: package
 	test/mdx-test.py --debug "$(TEST_FILTER)"
 
-TEMP_QNT_FILE := $(shell mktemp)
+# Generate fixtures needed to test quint integration
+quint-fixtures: tla-io/src/test/resources/tictactoe.json test/tla/booleans.qnt.json
+
+TEMP_QNT_TTT_FILE := $(shell mktemp)
 tla-io/src/test/resources/tictactoe.json:
-	curl https://raw.githubusercontent.com/informalsystems/quint/main/examples/puzzles/tictactoe/tictactoe.qnt > $(TEMP_QNT_FILE)
-	quint typecheck --out $@ $(TEMP_QNT_FILE)
-	rm $(TEMP_QNT_FILE)
+	curl https://raw.githubusercontent.com/informalsystems/quint/main/examples/puzzles/tictactoe/tictactoe.qnt > $(TEMP_QNT_TTT_FILE)
+	quint typecheck --out $@ $(TEMP_QNT_TTT_FILE)
+	rm $(TEMP_QNT_TTT_FILE)
+
+TEMP_QNT_BOOL_FILE := $(shell mktemp)
+test/tla/booleans.qnt.json:
+	curl https://raw.githubusercontent.com/informalsystems/quint/main/examples/language-features/booleans.qnt > $(TEMP_QNT_BOOL_FILE)
+	quint typecheck --out $@ $(TEMP_QNT_BOOL_FILE)
+	rm $(TEMP_QNT_BOOL_FILE)
 
 # Build the docker image
 docker:

test/tla/cli-integration-tests.md

@@ -3893,7 +3893,7 @@ The Apalache server is running on port 8888. Press Ctrl-C to stop.
 
 ### quint input: quint spec can be checked
 
-`booleans.qnt.json` is parsed using `quint` from https://github.com/informalsystems/quint/blob/main/examples/language-features/booleans.qnt
+`booleans.qnt.json` updated via `make quint-fixtures`
 
 ```sh
 $ apalache-mc check booleans.qnt.json | sed 's/[IEW]@.*//'

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

@@ -39,6 +39,8 @@ 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.typecomp.TBuilderScopeException
+import at.forsyte.apalache.tla.typecomp.TBuilderTypeException
 
 class Quint(moduleData: QuintOutput) {
   protected val module = moduleData.modules(0)
@@ -395,7 +397,7 @@ class Quint(moduleData: QuintOutput) {
             })
 
       // Create a TLA record
-      val record: Converter = {
+      def record(rowVar: Option[String]): Converter = {
         case Seq() => throw new QuintUnsupportedError("Given empty record, but Apalache doesn't support empty records.")
         case quintArgs =>
           // The quint Rec operator takes its field and value arguments
@@ -404,7 +406,7 @@ class Quint(moduleData: QuintOutput) {
           //
           //    Rec("f1", 1, "f2", 2)
           //
-          // So we first separate out the filed names from the values, so we
+          // So we first separate out the field names from the values, so we
           // can make use of the existing combinator for variadic operators.
           val (fieldNames, quintVals) = quintArgs
             .grouped(2)
@@ -415,7 +417,7 @@ class Quint(moduleData: QuintOutput) {
             }
           variadicApp { tlaVals =>
             val fieldsAndArgs = fieldNames.zip(tlaVals)
-            tla.rec(fieldsAndArgs: _*)
+            tla.rowRec(rowVar, fieldsAndArgs: _*)
           }(quintVals)
 
       }
@@ -517,7 +519,13 @@ class Quint(moduleData: QuintOutput) {
           case "tuples" => variadicApp(tla.times)
 
           // Records
-          case "Rec"        => MkTla.record
+          case "Rec" =>
+            val rowVar = types(id).typ match {
+              case r: QuintRecordT => r.rowVar
+              case invalidType =>
+                throw new QuintIRParseError(s"Invalid type given for Rec operator application ${invalidType}")
+            }
+            MkTla.record(rowVar)
           case "field"      => binaryApp(opName, tla.app)
           case "fieldNames" => unaryApp(opName, tla.dom)
           case "with"       => ternaryApp(opName, tla.except)
@@ -651,9 +659,21 @@ class Quint(moduleData: QuintOutput) {
         // no methods for them are provided by the ScopedBuilder.
         case QuintConst(id, name, _) => Some(TlaConstDecl(name)(typeTagOfId(id)))
         case QuintVar(id, name, _)   => Some(TlaVarDecl(name)(typeTagOfId(id)))
-        case op: QuintOpDef          => Some(build(opDefConverter(op).run(Set())._1))
+        case op: QuintOpDef =>
+          try {
+            val nullaryOpNameContext = Set[String]()
+            Some(build(opDefConverter(op).run(nullaryOpNameContext)._1))
+          } catch {
+            // If the builder fails, then we've done something wrong in our
+            // conversion logic
+            case err @ (_: TBuilderScopeException | _: TBuilderTypeException) =>
+              throw new QuintIRParseError(
+                  s"Conversion failed while building operator definition ${op}: ${err.getMessage()}")
+          }
+
         case QuintAssume(id, _, quintEx) =>
-          val tlaEx = build(tlaExpression(quintEx).run(Set()))
+          val nullaryOpNameContext = Set[String]()
+          val tlaEx = build(tlaExpression(quintEx).run(nullaryOpNameContext))
           Some(TlaAssumeDecl(tlaEx)(typeTagOfId(id)))
       }
     }
@@ -710,7 +730,11 @@ object Quint {
     val vars = mutable.Map[String, Int]()
     def getVarNo(varName: String): Int = {
       vars.get(varName) match {
-        case None    => val v = varNo; varNo += 1; v
+        case None =>
+          val v = varNo
+          vars += varName -> v
+          varNo += 1
+          v
         case Some(n) => n
       }
     }

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

@@ -31,12 +31,21 @@ private[quint] class QuintIRParseError(errMsg: String)
 // User facing error
 class QuintUnsupportedError(errMsg: String) extends Exception("Unsupported quint input: " + errMsg)
 
+private[quint] case class QuintLookupTableEntry(
+    kind: String,
+    reference: Int)
+private[quint] object QuintLookupTableEntry {
+  implicit val rw: RW[QuintLookupTableEntry] = macroRW
+}
+
 /** The JSON output produced by quint parse */
 private[quint] case class QuintOutput(
     stage: String,
     modules: Seq[QuintModule],
     // Maps source IDs to types, see the `WithId` trait
-    types: Map[Int, QuintTypeScheme])
+    types: Map[Int, QuintTypeScheme],
+    // Maps name IDs to declaration IDs
+    table: Map[Int, QuintLookupTableEntry])
 
 private[quint] object QuintOutput {
   implicit val rw: RW[QuintOutput] = macroRW
@@ -355,7 +364,19 @@ private[quint] object QuintType {
     }
   }
 
-  @key("rec") case class QuintRecordT(fields: Row) extends QuintType
+  @key("rec") case class QuintRecordT(fields: Row) extends QuintType {
+
+    // `r.rowVar` is `Some(s)` if it is an open row and `s` is the name of the row variable.
+    // Otherwise it is `None`.
+    def rowVar: Option[String] = getVar(fields)
+
+    private val getVar: Row => Option[String] = {
+      case Row.Var(v)           => Some(v)
+      case Row.Nil()            => None
+      case Row.Cell(_, moreRow) => getVar(moreRow)
+    }
+  }
+
   object QuintRecordT {
     implicit val rw: RW[QuintRecordT] = macroRW
 
@@ -364,6 +385,12 @@ private[quint] object QuintType {
       val fields = fieldTypes.map { case (f, t) => RecordField(f, t) }
       QuintRecordT(Row.Cell(fields, Row.Nil()))
     }
+
+    // Helper for manually constructing record type with free row variable
+    def ofFieldTypes(rowVar: String, fieldTypes: (String, QuintType)*): QuintRecordT = {
+      val fields = fieldTypes.map { case (f, t) => RecordField(f, t) }
+      QuintRecordT(Row.Cell(fields, Row.Var(rowVar)))
+    }
   }
 
   case class UnionRecord(tagValue: String, fields: Row)

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

@@ -1,6 +1,7 @@
 package at.forsyte.apalache.io.quint
 
 import at.forsyte.apalache.tla.lir.IntT1
+import at.forsyte.apalache.tla.lir.OperT1
 import at.forsyte.apalache.tla.lir.SetT1
 import at.forsyte.apalache.tla.lir.Typed
 import org.junit.runner.RunWith
@@ -9,6 +10,9 @@ import org.scalatestplus.junit.JUnitRunner
 
 import QuintType._
 import QuintEx._
+import at.forsyte.apalache.tla.lir.RecRowT1
+import at.forsyte.apalache.tla.lir.RowT1
+import at.forsyte.apalache.tla.lir.VarT1
 
 // You can run all these tests in watch mode in the
 // sbt console with
@@ -53,12 +57,25 @@ class TestQuintEx extends AnyFunSuite {
       e(QuintApp(uid, name, args), retType)
     }
 
+    def opDef(name: String, body: QuintEx): QuintDef.QuintOpDef = {
+      QuintDef.QuintOpDef(body.id, name, "def", body, None)
+    }
+
     def param(name: String, typ: QuintType): QuintLambdaParameter = {
       val id = uid
       typeMap += (id -> typ)
       QuintLambdaParameter(id, name)
     }
 
+    def lam(params: Seq[(String, QuintType)], body: QuintEx, typ: QuintType): QuintLambda = {
+      val opTyp = QuintOperT(params.map(_._2), typ)
+      e(QuintLambda(uid, params.map { case (n, t) => param(n, t) }, "def", body), opTyp)
+    }
+
+    def nam(s: String, t: QuintType): QuintName = {
+      e(QuintName(uid, s), t)
+    }
+
     // Scalar values
     val tt = e(QuintBool(uid, true), QuintBoolT())
     val _0 = e(QuintInt(uid, 0), QuintIntT())
@@ -122,12 +139,13 @@ class TestQuintEx extends AnyFunSuite {
 
     // We construct a converter supplied with the needed type map
     def quint = new Quint(QuintOutput(
-            "typechecking",
-            List(QuintModule(0, "MockedModule", List())),
-            typeMap.map { case (id, typ) =>
+            stage = "typechecking",
+            modules = List(QuintModule(0, "MockedModule", List())),
+            types = typeMap.map { case (id, typ) =>
               // Wrap each type in the TypeScheme required by the Quint IR
               id -> QuintTypeScheme(typ)
             }.toMap,
+            table = Map(),
         ))
 
   }
@@ -464,15 +482,26 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(Q.app("Rec", Q.s, Q._1, Q.t, Q._2)(typ)) == """["s" ↦ 1, "t" ↦ 2]""")
   }
 
-  test("convert builtin Rec operator constructing empty record fails") {
+  test("converting builtin Rec operator constructing empty record fails") {
     val exn = intercept[QuintUnsupportedError] {
-      val typ = QuintRecordT.ofFieldTypes(("s", QuintIntT()), ("t", QuintIntT()))
+      val typ = QuintRecordT.ofFieldTypes()
       convert(Q.app("Rec")(typ))
     }
     assert(exn.getMessage.contains(
             "Unsupported quint input: Given empty record, but Apalache doesn't support empty records."))
   }
 
+  test("can convert row-polymorphic record") {
+    val typ = QuintRecordT.ofFieldTypes("a", ("s", QuintIntT()), ("t", QuintIntT()))
+    val quintEx = Q.app("Rec", Q.s, Q._1, Q.t, Q._2)(typ)
+    val exp = Q.quint.exToTla(quintEx).get
+    val expectedTlaType = RecRowT1(RowT1(VarT1("a"), ("s", IntT1), ("t", IntT1)))
+
+    assert(Quint.typeToTlaType(typ) == expectedTlaType)
+    assert(exp.typeTag == Typed(expectedTlaType))
+    assert(exp.toString == """["s" ↦ 1, "t" ↦ 2]""")
+  }
+
   test("can convert builtin field operator application") {
     val rec = {
       val typ = QuintRecordT.ofFieldTypes(("s", QuintIntT()), ("t", QuintIntT()))
@@ -495,6 +524,21 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(Q.app("with", rec, Q.s, Q._42)(typ)) == """[["s" ↦ 1, "t" ↦ 2] EXCEPT ![<<"s">>] = 42]""")
   }
 
+  test("operator def conversion preserves row-typing") {
+    // def updateF1(r) : {s: int | a} => {s: int | a} = r.with("s", 1)
+    val recType = QuintRecordT.ofFieldTypes("a", ("s", QuintIntT()))
+    val opType = QuintOperT(Seq(recType), recType)
+    val rName = Q.nam("r", recType)
+    val body = Q.app("with", rName, Q.s, Q._1)(recType)
+    val abs = Q.lam(Seq(("r", recType)), body, recType)
+    val opDef = Q.opDef("updateF1", abs)
+    val tlaOpDef = Q.quint.defToTla(opDef).get
+    val tlaRecTyp = RecRowT1(RowT1(VarT1("a"), ("s", IntT1)))
+    val expectedTlaType = OperT1(Seq(tlaRecTyp), tlaRecTyp)
+    assert(Quint.typeToTlaType(opType) == expectedTlaType)
+    assert(tlaOpDef.typeTag == Typed(expectedTlaType))
+  }
+
   test("can convert builtin Tup operator application") {
     assert(convert(Q.app("Tup", Q._0, Q._1)(QuintTupleT.ofTypes(QuintIntT(), QuintIntT()))) == "<<0, 1>>")
   }

tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala

@@ -6,6 +6,7 @@ import at.forsyte.apalache.tla.typecomp.{TBuilderInstruction, TBuilderInternalSt
 import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeFunBuilder
 import scalaz._
 import scalaz.Scalaz._
+import at.forsyte.apalache.tla.lir.VarT1
 
 /**
  * Scope-safe builder for TlaFunOper expressions.
@@ -26,6 +27,18 @@ trait FunBuilder {
     ks = args.map(_._1)
   } yield unsafeBuilder.rec(ks.zip(vs): _*)
 
+  /**
+   * Like [[rec]] but using `RowRecT1` types
+   *
+   * @param rowVar
+   *   The name of a free row variable
+   */
+  def rowRec(rowVar: Option[String], args: (String, TBuilderInstruction)*): TBuilderInstruction = for {
+    vs <- buildSeq(args.map(_._2))
+    ks = args.map(_._1)
+    v = rowVar.map(VarT1(_))
+  } yield unsafeBuilder.rowRec(v, ks.zip(vs): _*)
+
   /**
    * {{{[ args[0] |-> args[1], ..., args[n-1] |-> args[n] ]}}}
    * @param args