Apply review fixes

tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala

@@ -190,18 +190,15 @@ class TlaToJson[T <: JsonRepresentation](
 
       case TlaAssumeDecl(definedName, body) =>
         val bodyJson = apply(body)
-        val fields = Array[(String, T)](
+
+        val optionalName: Option[(String, T)] = definedName.map("name" -> _)
+        val fields = Seq[(String, T)](
             typeFieldName -> typeTagPrinter(decl.typeTag),
             kindFieldName -> "TlaAssumeDecl",
             "body" -> bodyJson,
-        )
-
-        val f = definedName match {
-          case None       => fields
-          case Some(name) => fields :+ ("name" -> name: (String, T))
-        }
+        ) ++ optionalName
 
-        withLoc(f.toIndexedSeq: _*)
+        withLoc(fields: _*)
     }
   }
 

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

@@ -314,9 +314,9 @@ private[quint] object QuintDef {
 
     /**
      * @return
-     *   true if this ASSUME clause has no user-defined name, false otherwise
+     *   `true` if this assume declaration has no user-defined name, `false` otherwise
      *
-     * unnamed ASSUME clauses use `_` as a name
+     * anonymous assume declarations are named with the "hole", `_`
      */
     def isUnnamed: Boolean = name == "_"
   }

tla-io/src/main/scala/at/forsyte/apalache/tla/imp/AssumeTranslator.scala

@@ -17,7 +17,8 @@ class AssumeTranslator(
           context,
           OutsideRecursion(),
       ).translate(node.getAssume)
-    TlaAssumeDecl(Option(node.getDef).map(_.getName.toString), body)(Untyped)
+    val name = Option(node.getDef).map(_.getName.toString)
+    TlaAssumeDecl(name, body)(Untyped)
   }
 }
 

tla-io/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithTypes.scala

@@ -99,28 +99,34 @@ class TestPrettyWriterWithTypes extends AnyFunSuite with BeforeAndAfterEach {
   }
 
   test("unnamed assume declaration") {
-    val decl = TlaAssumeDecl(None, tla.eql(tla.name("x"), tla.bool(true)))
+    val decl = TlaAssumeDecl(None, tla.eql(tla.name("x"), tla.bool(true)))(Typed(BoolT1))
     val store = createAnnotationStore()
 
     val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80)
     writer.write(decl)
     printWriter.flush()
     val expected =
-      """ASSUME(x = TRUE)
+      """(*
+        |  @type: Bool;
+        |*)
+        |ASSUME(x = TRUE)
         |
         |""".stripMargin
     assert(expected == stringWriter.toString)
   }
 
   test("named assume declaration") {
-    val decl = TlaAssumeDecl(Some("myAssume"), tla.eql(tla.name("x"), tla.bool(true)))
+    val decl = TlaAssumeDecl(Some("myAssume"), tla.eql(tla.name("x"), tla.bool(true)))(Typed(BoolT1))
     val store = createAnnotationStore()
 
     val writer = new PrettyWriterWithAnnotations(store, printWriter, layout80)
     writer.write(decl)
     printWriter.flush()
     val expected =
-      """ASSUME myAssume == (x = TRUE)
+      """(*
+        |  @type: Bool;
+        |*)
+        |ASSUME myAssume == (x = TRUE)
         |
         |""".stripMargin
     assert(expected == stringWriter.toString)

tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala

@@ -47,7 +47,7 @@ class ToEtcExpr(
         // We have to introduce a lambda abstraction, as the type checker is expecting this form.
         mkLet(
             BlameRef(d.ID),
-            "__Assume_" + d.definedName.getOrElse(d.ID.toString),
+            d.name,
             mkAbs(ExactRef(d.ID), application),
             inScopeEx,
         )

tla-typechecker/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExprDecls.scala

@@ -117,7 +117,7 @@ class TestToEtcExprDecls extends AnyFunSuite with ToEtcExprBase with BeforeAndAf
     // This allows us to check that the assumption has Boolean type.
     val application = mkUniqApp(Seq(parser("Bool => Bool")), assumption)
     val expected =
-      mkUniqLet("__Assume_" + assume.definedName.getOrElse(assume.ID.toString), mkUniqAbs(application), terminal)
+      mkUniqLet(assume.name, mkUniqAbs(application), terminal)
     // Translate the declaration of positive.
     // We have to pass the next expression in scope, which is just TRUE in this case.
     assert(expected == mkToEtcExpr(Map())(assume, terminal))