Update scalafmt-core to 3.7.0 (#2356)

* Update scalafmt-core to 3.7.0 * Reformat with scalafmt 3.7.0 Executed command: scalafmt --non-interactive * Add 'Reformat with scalafmt 3.7.0' to .git-blame-ignore-revs Co-authored-by: Shon Feder <[email protected]>
apalache-mc · Jan 23, 2023 · fcb206c · fcb206c
1 parent a249bbf
commit fcb206c
Show file tree

Hide file tree

Showing 12 changed files with 67 additions and 55 deletions.
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
@@ -1,2 +1,5 @@
 # Scala Steward: Reformat with scalafmt 3.6.1
 630ce4a77cc49017919a9a17eec16a5177e0aa23
+
+# Scala Steward: Reformat with scalafmt 3.7.0
+940cde8dd83d26a64657982c4b59ec1de2df94e4
diff --git a/.scalafmt.conf b/.scalafmt.conf
@@ -1,4 +1,4 @@
-version = "3.6.1"
+version = "3.7.0"
 
 runner.dialect = scala213
 fileOverride {

diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SymbTransGenerator.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SymbTransGenerator.scala
@@ -66,7 +66,7 @@ class SymbTransGenerator(tracker: TransformationTracker) {
       case OperEx(TlaBoolOper.and, args @ _*) =>
         /** Unify all child maps, keysets are disjoint by construction */
         val unifiedMap = (args
-              .map {
+          .map {
             allSelections(_, letInMap)
           })
           .fold(Map.empty[UID, AssignmentSelections]) {
@@ -85,7 +85,7 @@ class SymbTransGenerator(tracker: TransformationTracker) {
        */
       case OperEx(TlaBoolOper.or, args @ _*) =>
         val unifiedMap = (args
-              .map {
+          .map {
             allSelections(_, letInMap)
           })
           .fold(Map.empty[UID, AssignmentSelections]) {
@@ -113,7 +113,7 @@ class SymbTransGenerator(tracker: TransformationTracker) {
        */
       case OperEx(TlaControlOper.ifThenElse, _, thenAndElse @ _*) =>
         val unifiedMap = (thenAndElse
-              .map {
+          .map {
             allSelections(_, letInMap)
           })
           .fold(Map.empty[UID, AssignmentSelections]) {

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala
@@ -97,7 +97,9 @@ class FunCtorRule(rewriter: SymbStateRewriter) extends RewritingRule {
       state: SymbState,
       mapEx: TlaEx,
       varName: String,
-      oldCells: Seq[ArenaCell]): (SymbState, Seq[ArenaCell]) = {
+      oldCells: Seq[ArenaCell]): (
+      SymbState,
+      Seq[ArenaCell]) = {
     var nextState = state
 
     def mapOne(cell: ArenaCell): ArenaCell = {

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MapBase.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MapBase.scala
@@ -82,7 +82,9 @@ class MapBase(rewriter: SymbStateRewriter) {
       mapEx: TlaEx,
       varNames: Seq[String],
       setsAsCells: Seq[ArenaCell],
-      cellsIter: Iterator[Seq[ArenaCell]]): (SymbState, Iterable[ArenaCell]) = {
+      cellsIter: Iterator[Seq[ArenaCell]]): (
+      SymbState,
+      Iterable[ArenaCell]) = {
     // we could have done it with foldLeft, but that would be even less readable
     var newState = state
 
@@ -124,7 +126,10 @@ class MapBase(rewriter: SymbStateRewriter) {
       mapEx: TlaEx,
       varNames: Seq[String],
       setsAsCells: Seq[ArenaCell],
-      valuesAsCells: Seq[ArenaCell]): (SymbState, ArenaCell, TlaEx) = {
+      valuesAsCells: Seq[ArenaCell]): (
+      SymbState,
+      ArenaCell,
+      TlaEx) = {
     // bind the variables to the corresponding cells
     val newBinding: Binding = varNames.zip(valuesAsCells).foldLeft(state.binding)((m, p) => Binding(m.toMap + p))
     val mapState = state.setBinding(newBinding).setRex(mapEx)

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala
@@ -248,7 +248,9 @@ class ProtoSeqOps(rewriter: SymbStateRewriter) {
       arena: PureArenaAdapter,
       seqT: TlaType1,
       protoSeq: ArenaCell,
-      len: ArenaCell): (PureArenaAdapter, ArenaCell) = {
+      len: ArenaCell): (
+      PureArenaAdapter,
+      ArenaCell) = {
     var newArena = arena.appendCell(seqT)
     val seq = newArena.topCell
     // note that we do not track in SMT the relation between the sequence, the proto sequence, and its length

diff --git a/...ala/at/forsyte/apalache/tla/bmcmt/TestCollectCounterexamplesSeqModelCheckerListener.scala b/...ala/at/forsyte/apalache/tla/bmcmt/TestCollectCounterexamplesSeqModelCheckerListener.scala
@@ -30,7 +30,9 @@ class TestCollectCounterexamplesModelCheckerListener extends AnyFunSuite {
       initTrans: List[TlaEx],
       nextTrans: List[TlaEx],
       inv: TlaEx,
-      maxErrors: Int): (CollectCounterexamplesModelCheckerListener, SeqModelChecker[IncrementalExecutionContextSnapshot]) = {
+      maxErrors: Int): (
+      CollectCounterexamplesModelCheckerListener,
+      SeqModelChecker[IncrementalExecutionContextSnapshot]) = {
     // construct checker input + parameters
     val notInv = not(inv).typed(types, "b")
     val checkerInput = new CheckerInput(module, initTrans, nextTrans, None, CheckerInputVC(List((inv, notInv))))

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/vmt/TestJudgement.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/vmt/TestJudgement.scala
@@ -22,10 +22,10 @@ class TestJudgement extends AnyFunSuite {
   )
 
   val allowed: Seq[TlaEx] = (Seq(
-          tla.intSet(),
-          tla.natSet(),
-          tla.booleanSet(),
-      ).map { _.untyped() }) ++ (constantMap.keys.toSeq.map { tla.name(_).untyped() })
+      tla.intSet(),
+      tla.natSet(),
+      tla.booleanSet(),
+  ).map { _.untyped() }) ++ (constantMap.keys.toSeq.map { tla.name(_).untyped() })
 
   val disallowed: Seq[TlaEx] = Seq(
       ValEx(TlaRealSet),

diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestConstSimplifier.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestConstSimplifier.scala
@@ -507,8 +507,9 @@ class TestConstSimplifier extends AnyFunSuite with BeforeAndAfterEach with Check
               // FALSE \/ x \/ y = x \/ y
               (tla.or(tla.bool(false).as(BoolT1), e1, e2).as(BoolT1)) -> (tla.or(e1, e2).as(BoolT1)),
               // IF x THEN FALSE ELSE y = !x /\ y
-              (tla.ite(e1, tla.bool(false).as(BoolT1), e2).as(BoolT1)) -> (
-                  tla.and(tla.not(e1).as(BoolT1), e2).as(BoolT1)),
+              (tla
+                .ite(e1, tla.bool(false).as(BoolT1), e2)
+                .as(BoolT1)) -> (tla.and(tla.not(e1).as(BoolT1), e2).as(BoolT1)),
               // IF x THEN TRUE ELSE y = x \/ y
               (tla.ite(e1, tla.bool(true).as(BoolT1), e2).as(BoolT1)) -> (tla.or(e1, e2).as(BoolT1)),
               // x \notin y = !(x \in y)

diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSourceLocator.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSourceLocator.scala
@@ -125,12 +125,12 @@ class TestSourceLocator extends AnyFunSuite {
   // Arbitrary assignment, all exs get a unique position equal to their UID
   val sourceMap: SourceMap =
     ((exs.map(allUidsBelow) ++ decls.map(_.body).map(allUidsBelow))
-          .foldLeft(Set.empty[UID]) {
-            _ ++ _
-          }
-          .map { x =>
-            x -> generateLoc(x)
-          })
+      .foldLeft(Set.empty[UID]) {
+        _ ++ _
+      }
+      .map { x =>
+        x -> generateLoc(x)
+      })
       .toMap
 
   val exMap = new mutable.HashMap[UID, TlaEx]()

diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/BuilderTest.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/BuilderTest.scala
@@ -396,16 +396,15 @@ trait BuilderTest extends AnyFunSuite with BeforeAndAfter with Checkers with App
       op: TlaOper,
       mkWellTyped: TypeParameterization => T,
       toSeq: T => Seq[TBuilderResult],
-      resType: TypeParameterization => TlaType1): TypeParameterization => TBuilderResult => Boolean = {
-    tparam =>
-      { resEx =>
-        resEx.eqTyped(
-            OperEx(
-                op,
-                toSeq(mkWellTyped(tparam)): _*
-            )(Typed(resType(tparam)))
-        )
-      }
+      resType: TypeParameterization => TlaType1): TypeParameterization => TBuilderResult => Boolean = { tparam =>
+    { resEx =>
+      resEx.eqTyped(
+          OperEx(
+              op,
+              toSeq(mkWellTyped(tparam)): _*
+          )(Typed(resType(tparam)))
+      )
+    }
   }
 
   /**

diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala
@@ -31,18 +31,17 @@ class TestHybrid extends BuilderTest {
           ),
       )
 
-    def resultIsExpected: TlaType1 => TBuilderResult => Boolean = {
-      tt =>
-        { resEx =>
-          val (x, y) = mkWellTyped(tt)
-          resEx.eqTyped(
-              OperEx(
-                  TlaOper.eq,
-                  OperEx(TlaActionOper.prime, x)(Typed(tt)),
-                  y,
-              )(Typed(BoolT1))
-          )
-        }
+    def resultIsExpected: TlaType1 => TBuilderResult => Boolean = { tt =>
+      { resEx =>
+        val (x, y) = mkWellTyped(tt)
+        resEx.eqTyped(
+            OperEx(
+                TlaOper.eq,
+                OperEx(TlaActionOper.prime, x)(Typed(tt)),
+                y,
+            )(Typed(BoolT1))
+        )
+      }
     }
 
     checkRun(Generators.singleTypeGen)(
@@ -116,18 +115,17 @@ class TestHybrid extends BuilderTest {
     def expectEqTypedDecl[T](
         mkWellTyped: TParam => (String, TBuilderInstruction, T),
         exParams: TParam => List[OperParam],
-        exType: TParam => TlaType1): TParam => TlaOperDecl => Boolean = {
-      tparam =>
-        { resDecl =>
-          val (name, body, _) = mkWellTyped(tparam)
-          resDecl.eqTyped(
-              TlaOperDecl(
-                  name,
-                  exParams(tparam),
-                  body,
-              )(Typed(exType(tparam)))
-          )
-        }
+        exType: TParam => TlaType1): TParam => TlaOperDecl => Boolean = { tparam =>
+      { resDecl =>
+        val (name, body, _) = mkWellTyped(tparam)
+        resDecl.eqTyped(
+            TlaOperDecl(
+                name,
+                exParams(tparam),
+                body,
+            )(Typed(exType(tparam)))
+        )
+      }
     }
 
     def paramArity(tt: TlaType1): Int = tt match {