diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index fb7b35f326..b5eeee18a9 100644 --- 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 index 2406ded2ca..81f1f55910 100644 --- 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 index fb057d3046..29bb6eaabe 100644 --- 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 index ff3fbac11a..cd76187966 100644 --- 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 index 2f5a4862d6..f824e98072 100644 --- 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 index a962293a8b..c93d69698e 100644 --- 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/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCollectCounterexamplesSeqModelCheckerListener.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCollectCounterexamplesSeqModelCheckerListener.scala index daff197e46..e4af2ab931 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCollectCounterexamplesSeqModelCheckerListener.scala +++ b/tla-bmcmt/src/test/scala/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 index c2b52afa97..a4ba9db66a 100644 --- 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 index 1b4b7a53eb..150110b1c3 100644 --- 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 index 3fe958ef1b..4128e54d44 100644 --- 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 index f1f94eb5e5..ee3b04fd39 100644 --- 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 index dad14f98be..0b6400fd95 100644 --- 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 {