Skip to content

Commit 063fbfa

Browse files
committed
Fix weird identlhs formatting
1 parent 0074f87 commit 063fbfa

File tree

4 files changed

+18
-35
lines changed

4 files changed

+18
-35
lines changed

src/main/java/me/fponzi/tlaplusformatter/constructs/impl/IdentLHSConstruct.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
4747

4848
Doc content = elementDocs.get(0);
4949
for (int i = 1; i < elementDocs.size(); i++) {
50-
content = content.append(Doc.text(",")).appendLineOrSpace(elementDocs.get(i));
50+
content = content.append(Doc.text(",")).appendSpace(elementDocs.get(i));
5151
}
5252

5353
return

src/test/resources/outputs/AllConstructs.tla

Lines changed: 7 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -29,11 +29,9 @@ vars == << x, y, z, f, r, s, q >>
2929
(****************************************************************)
3030
Zero == 0
3131

32-
Add(a,
33-
b) == a + b
32+
Add(a, b) == a + b
3433

35-
Equal(a,
36-
b) == a = b
34+
Equal(a, b) == a = b
3735

3836
RECURSIVE Fact(_)
3937
Fact(n) == IF n = 0 THEN 1 ELSE n * Fact(n - 1)
@@ -42,15 +40,11 @@ MapPlusOne(U) == LET plus1(t) == t + 1 IN {plus1(t): t \in U}
4240

4341
IdFun(U) == [u \in U |-> u]
4442

45-
Bump(f_,
46-
k) == [f_ EXCEPT ![k] = @ + 1]
43+
Bump(f_, k) == [f_ EXCEPT ![k] = @ + 1]
4744

48-
Rec(a,
49-
b) == [ a |-> a, b |-> b ]
45+
Rec(a, b) == [ a |-> a, b |-> b ]
5046

51-
Tuple3(a,
52-
b,
53-
c) == << a, b, c >>
47+
Tuple3(a, b, c) == << a, b, c >>
5448

5549
Power(U) == SUBSET U
5650

@@ -60,9 +54,7 @@ CaseExample(u) == CASE u \in Nat -> u + 1
6054
[] u \in Int \ Nat -> - u
6155
[] OTHER-> 0
6256

63-
IfElseExample(b,
64-
e1,
65-
e2) == IF b THEN e1 ELSE e2
57+
IfElseExample(b, e1, e2) == IF b THEN e1 ELSE e2
6658

6759
ChooseAnyFrom(U) == CHOOSE u \in U: TRUE
6860

@@ -72,8 +64,7 @@ Dom(f_) == DOMAIN f_
7264

7365
Range(f_) == {f_[i]: i \in DOMAIN f_}
7466

75-
ConstFun(U,
76-
v) == [U -> { v }]
67+
ConstFun(U, v) == [U -> { v }]
7768

7869
SeqStuff(U) ==
7970
LET s0 == <<>> \o << 1 >> \o << 2, 3 >>

src/test/resources/outputs/Stones.tla

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,7 @@ ASSUME W \in Nat /\ N \in 1 .. W
5959
(* definition. *)
6060
(***************************************************************************)
6161
RECURSIVE Partitions(_,_)
62-
Partitions(seq,
63-
wt) ==
62+
Partitions(seq, wt) ==
6463
IF Len(seq) = N
6564
THEN { seq }
6665
ELSE LET r == N - Len(seq)
@@ -75,8 +74,7 @@ wt) ==
7574
(* For convenience, we define Weighs(seq, wt) to be true if the elements *)
7675
(* of the sequence seq sum to wt. *)
7776
(***************************************************************************)
78-
Weighs(seq,
79-
wt) ==
77+
Weighs(seq, wt) ==
8078
\E coef \in [1 .. N -> - 1 .. 1]:
8179
SeqSum([i \in 1 .. N |-> coef[i] * seq[i]]) = wt
8280

src/test/resources/outputs/TowerOfHanoi.tla

Lines changed: 8 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -59,36 +59,30 @@ IsEmptyTower(tower) == tower = 0
5959
(***************************************************************************)
6060
(* TRUE iff the disk is located on the given tower *)
6161
(***************************************************************************)
62-
IsOnTower(tower,
63-
disk) == /\ tower & disk = disk
62+
IsOnTower(tower, disk) == /\ tower & disk = disk
6463

6564
(***************************************************************************)
6665
(* TRUE iff disk is the smallest disk on tower *)
6766
(***************************************************************************)
68-
IsSmallestDisk(tower,
69-
disk) == /\ IsOnTower(tower, disk)
70-
/\ tower & ( disk - 1 ) = 0
67+
IsSmallestDisk(tower, disk) == /\ IsOnTower(tower, disk)
68+
/\ tower & ( disk - 1 ) = 0
7169
\* All less significant bits are 0
7270
(***************************************************************************)
7371
(* TRUE iff disk can be moved off of tower *)
7472
(***************************************************************************)
75-
CanMoveOff(tower,
76-
disk) == /\ IsOnTower(tower, disk)
77-
/\ IsSmallestDisk(tower, disk)
73+
CanMoveOff(tower, disk) == /\ IsOnTower(tower, disk)
74+
/\ IsSmallestDisk(tower, disk)
7875

7976
(***************************************************************************)
8077
(* TRUE iff disk can be moved to the tower *)
8178
(***************************************************************************)
82-
CanMoveTo(tower,
83-
disk) == \/ tower & ( disk - 1 ) = 0
84-
\/ IsEmptyTower(tower)
79+
CanMoveTo(tower, disk) == \/ tower & ( disk - 1 ) = 0
80+
\/ IsEmptyTower(tower)
8581

8682
(***************************************************************************)
8783
(* *)
8884
(***************************************************************************)
89-
Move(from,
90-
to,
91-
disk) ==
85+
Move(from, to, disk) ==
9286
/\ CanMoveOff(towers[from], disk)
9387
/\ CanMoveTo(towers[to], disk)
9488
/\ towers' =

0 commit comments

Comments
 (0)