Skip to content

Commit 9f1c367

Browse files
rcosta358rcosta358
authored
Fix Expression Formatter (#217)
1 parent b98a110 commit 9f1c367

2 files changed

Lines changed: 105 additions & 79 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java‎

Lines changed: 45 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -40,60 +40,79 @@ private String formatExpression(Expression expression) {
4040
return expression.accept(this);
4141
}
4242

43-
private String formatParentheses(Expression child, boolean shouldWrap) {
43+
private String formatExpression(Expression expression, boolean shouldWrap) {
44+
expression = unwrapGroup(expression);
4445
if (shouldWrap)
45-
return "(" + formatExpression(child) + ")";
46-
if (child instanceof GroupExpression group)
47-
return "(" + formatExpression(group.getExpression()) + ")";
48-
return formatExpression(child);
46+
return "(" + formatExpression(expression) + ")";
47+
return formatExpression(expression);
4948
}
5049

51-
private String formatOperand(Expression parent, Expression child) {
52-
return formatParentheses(child, needsParentheses(parent, child));
53-
}
54-
55-
private String formatRightOperand(BinaryExpression parent, Expression child) {
56-
return formatParentheses(child, needsRightParentheses(parent, child));
50+
private String formatOperand(Expression parent, Expression child, boolean rightOperand) {
51+
child = unwrapGroup(child);
52+
return formatExpression(child, needsParentheses(parent, child, rightOperand));
5753
}
5854

5955
private String formatCondition(Expression child) {
60-
return formatParentheses(child, child instanceof Ite);
56+
return formatExpression(child, unwrapGroup(child) instanceof Ite);
6157
}
6258

6359
private String formatArguments(List<Expression> args) {
64-
return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", "));
60+
return args.stream().map(expression -> formatExpression(expression, false)).collect(Collectors.joining(", "));
6561
}
6662

67-
private boolean needsParentheses(Expression parent, Expression child) {
68-
return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent));
63+
private Expression unwrapGroup(Expression expression) {
64+
while (expression instanceof GroupExpression group)
65+
expression = group.getExpression();
66+
return expression;
6967
}
7068

71-
private boolean needsRightParentheses(BinaryExpression parent, Expression child) {
72-
if (needsParentheses(parent, child))
69+
private boolean needsParentheses(Expression parent, Expression child, boolean rightOperand) {
70+
ExpressionPrecedence parentPrecedence = ExpressionPrecedence.of(parent);
71+
ExpressionPrecedence childPrecedence = ExpressionPrecedence.of(child);
72+
if (childPrecedence.isLowerThan(parentPrecedence))
7373
return true;
74-
75-
if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent))
74+
if (childPrecedence != parentPrecedence)
7675
return false;
7776

78-
if (child instanceof BinaryExpression right)
79-
return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator());
77+
if (parent instanceof BinaryExpression parentBinary && child instanceof BinaryExpression childBinary)
78+
return needsBinaryParentheses(parentBinary, childBinary, rightOperand);
79+
80+
if (parent instanceof Ite && child instanceof Ite)
81+
return true;
82+
83+
if (parent instanceof UnaryExpression parentUnary && child instanceof UnaryExpression childUnary)
84+
return parentUnary.getOp().equals("-") && childUnary.getOp().equals("-");
8085

8186
return false;
8287
}
8388

89+
private boolean needsBinaryParentheses(BinaryExpression parent, BinaryExpression child, boolean rightOperand) {
90+
if (rightOperand) {
91+
if (isRightAssociative(parent.getOperator()))
92+
return true;
93+
return !isRightAssociative(parent.getOperator())
94+
&& (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(child.getOperator()));
95+
}
96+
return isRightAssociative(parent.getOperator());
97+
}
98+
8499
private boolean isAssociative(String operator) {
85100
return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*");
86101
}
87102

103+
private boolean isRightAssociative(String operator) {
104+
return operator.equals("-->");
105+
}
106+
88107
@Override
89108
public String visitAliasInvocation(AliasInvocation alias) {
90109
return alias.getName() + "(" + formatArguments(alias.getArgs()) + ")";
91110
}
92111

93112
@Override
94113
public String visitBinaryExpression(BinaryExpression exp) {
95-
return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " "
96-
+ formatRightOperand(exp, exp.getSecondOperand());
114+
return formatOperand(exp, exp.getFirstOperand(), false) + " " + exp.getOperator() + " "
115+
+ formatOperand(exp, exp.getSecondOperand(), true);
97116
}
98117

99118
@Override
@@ -103,13 +122,13 @@ public String visitFunctionInvocation(FunctionInvocation fun) {
103122

104123
@Override
105124
public String visitGroupExpression(GroupExpression exp) {
106-
return "(" + formatExpression(exp.getExpression()) + ")";
125+
return formatExpression(exp.getExpression());
107126
}
108127

109128
@Override
110129
public String visitIte(Ite ite) {
111130
return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : "
112-
+ formatOperand(ite, ite.getElse());
131+
+ formatOperand(ite, ite.getElse(), true);
113132
}
114133

115134
@Override
@@ -144,7 +163,7 @@ public String visitLiteralString(LiteralString lit) {
144163

145164
@Override
146165
public String visitUnaryExpression(UnaryExpression exp) {
147-
return exp.getOp() + formatOperand(exp, exp.getExpression());
166+
return exp.getOp() + formatOperand(exp, exp.getExpression(), true);
148167
}
149168

150169
@Override

‎liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java‎

Lines changed: 60 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,93 +1,100 @@
11
package liquidjava.rj_language.ast;
22

33
import static org.junit.jupiter.api.Assertions.assertEquals;
4+
45
import org.junit.jupiter.api.Test;
56

7+
import liquidjava.rj_language.parsing.RefinementsParser;
8+
69
class ExpressionFormatterTest {
710

11+
private static Expression parse(String refinement) {
12+
return RefinementsParser.createAST(refinement, "");
13+
}
14+
815
@Test
916
void formatsUnaryAtoms() {
10-
assertEquals("!x", new UnaryExpression("!", new Var("x")).toDisplayString());
11-
assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toDisplayString());
17+
assertEquals("!x", parse("!x").toDisplayString());
18+
assertEquals("!false", parse("!false").toDisplayString());
1219
}
1320

1421
@Test
1522
void formatsInternalVariables() {
16-
assertEquals("x", new Var("x").toDisplayString());
17-
assertEquals("x²", new Var("#x_2").toDisplayString());
18-
assertEquals("#fresh¹²", new Var("#fresh_12").toDisplayString());
19-
assertEquals("#ret³", new Var("#ret_3").toDisplayString());
20-
assertEquals("this#Class", new Var("this#Class").toDisplayString());
23+
assertEquals("x", parse("x").toDisplayString());
24+
assertEquals("x²", parse("#x_2").toDisplayString());
25+
assertEquals("#fresh¹²", parse("#fresh_12").toDisplayString());
26+
assertEquals("#ret³", parse("#ret_3").toDisplayString());
27+
assertEquals("this#Class", parse("this#Class").toDisplayString());
2128
}
2229

2330
@Test
2431
void formatsEnums() {
25-
assertEquals("Color.RED", new Enum("Color", "RED").toDisplayString());
32+
assertEquals("Color.RED", parse("Color.RED").toDisplayString());
2633
}
2734

2835
@Test
2936
void formatsUnaryCompounds() {
30-
Expression comparison = new BinaryExpression(new Var("x"), ">", new LiteralInt(0));
31-
32-
assertEquals("x > 0", comparison.toDisplayString());
33-
assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toDisplayString());
34-
assertEquals("-(-x)", new UnaryExpression("-", new GroupExpression(new UnaryExpression("-", new Var("x"))))
35-
.toDisplayString());
37+
assertEquals("x > 0", parse("x > 0").toDisplayString());
38+
assertEquals("!(x > 0)", parse("!(x > 0)").toDisplayString());
39+
assertEquals("-(-x)", parse("-(-x)").toDisplayString());
3640
}
3741

3842
@Test
3943
void formatsBinaryPrecedence() {
40-
Expression sum = new BinaryExpression(new Var("a"), "+", new Var("b"));
41-
Expression product = new BinaryExpression(new Var("b"), "*", new Var("c"));
44+
assertEquals("(a + b) * c", parse("(a + b) * c").toDisplayString());
45+
assertEquals("a * (a + b)", parse("a * (a + b)").toDisplayString());
46+
assertEquals("a + b * c", parse("a + b * c").toDisplayString());
47+
assertEquals("a - (a + b)", parse("a - (a + b)").toDisplayString());
48+
assertEquals("a + b + c", parse("a + b + c").toDisplayString());
49+
assertEquals("b * c * c", parse("b * c * c").toDisplayString());
50+
}
4251

43-
assertEquals("(a + b) * c", new BinaryExpression(sum, "*", new Var("c")).toDisplayString());
44-
assertEquals("a * (a + b)", new BinaryExpression(new Var("a"), "*", sum).toDisplayString());
45-
assertEquals("a + b * c", new BinaryExpression(new Var("a"), "+", product).toDisplayString());
46-
assertEquals("a - (a + b)", new BinaryExpression(new Var("a"), "-", sum).toDisplayString());
47-
assertEquals("a + b + c", new BinaryExpression(sum, "+", new Var("c")).toDisplayString());
48-
assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toDisplayString());
52+
@Test
53+
void omitsUnnecessaryGroupParentheses() {
54+
assertEquals("x", parse("(x)").toDisplayString());
55+
assertEquals("x", parse("((x))").toDisplayString());
56+
assertEquals("1", parse("(1)").toDisplayString());
57+
assertEquals("a > 0", parse("(a > 0)").toDisplayString());
58+
assertEquals("a + b + c", parse("a + (b + c)").toDisplayString());
59+
assertEquals("a + b * c", parse("a + (b * c)").toDisplayString());
60+
assertEquals("a && b > 0", parse("a && (b > 0)").toDisplayString());
61+
assertEquals("a && b && c", parse("a && (b && c)").toDisplayString());
62+
assertEquals("size(stack²⁹⁴) > 0", parse("(size(#stack_294) > 0)").toDisplayString());
63+
assertEquals("size(stack²⁹⁴) > 0 && ready", parse("(size(#stack_294) > 0) && ready").toDisplayString());
64+
assertEquals("ready && size(stack²⁹⁴) > 0", parse("ready && (size(#stack_294) > 0)").toDisplayString());
4965
}
5066

5167
@Test
5268
void formatsRightGrouping() {
53-
Expression groupedSum = new GroupExpression(new BinaryExpression(new Var("b"), "+", new Var("c")));
54-
Expression groupedComparison = new GroupExpression(
55-
new BinaryExpression(new LiteralInt(1), ">", new LiteralInt(0)));
56-
57-
assertEquals("a - (b + c)", new BinaryExpression(new Var("a"), "-", groupedSum).toDisplayString());
58-
assertEquals("x == (1 > 0)", new BinaryExpression(new Var("x"), "==", groupedComparison).toDisplayString());
69+
assertEquals("a - (b + c)", parse("a - (b + c)").toDisplayString());
70+
assertEquals("a - (b - c)", parse("a - (b - c)").toDisplayString());
71+
assertEquals("a / (b * c)", parse("a / (b * c)").toDisplayString());
72+
assertEquals("(a || b) && c", parse("(a || b) && c").toDisplayString());
73+
assertEquals("x == (1 > 0)", parse("x == (1 > 0)").toDisplayString());
74+
assertEquals("a == (b == c)", parse("a == (b == c)").toDisplayString());
5975
}
6076

6177
@Test
6278
void formatsLogicalExpressions() {
63-
Expression andExpression = new BinaryExpression(new Var("a"), "&&", new Var("b"));
64-
Expression orExpression = new BinaryExpression(new Var("b"), "||", new Var("c"));
65-
Expression implication = new BinaryExpression(new Var("b"), "-->", new Var("c"));
66-
67-
assertEquals("a && b || c", new BinaryExpression(andExpression, "||", new Var("c")).toDisplayString());
68-
assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toDisplayString());
69-
assertEquals("a --> (b --> c)", new BinaryExpression(new Var("a"), "-->", implication).toDisplayString());
70-
assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toDisplayString());
71-
assertEquals("a || b || c",
72-
new BinaryExpression(new BinaryExpression(new Var("a"), "||", new Var("b")), "||", new Var("c"))
73-
.toDisplayString());
79+
assertEquals("a && b || c", parse("a && b || c").toDisplayString());
80+
assertEquals("a && (b || c)", parse("a && (b || c)").toDisplayString());
81+
assertEquals("a --> (b --> c)", parse("a --> b --> c").toDisplayString());
82+
assertEquals("a --> (b --> c)", parse("a --> (b --> c)").toDisplayString());
83+
assertEquals("a --> (b --> (c --> d))", parse("a --> b --> c --> d").toDisplayString());
84+
assertEquals("(a --> b) --> c", parse("(a --> b) --> c").toDisplayString());
85+
assertEquals("a && b && c", parse("a && b && c").toDisplayString());
86+
assertEquals("a || b || c", parse("a || b || c").toDisplayString());
7487
}
7588

7689
@Test
7790
void formatsTernaryExpressions() {
78-
Expression ite = new Ite(new Var("a"), new Var("b"), new Var("c"));
79-
Expression nestedElse = new Ite(new Var("c"), new Var("d"), new Var("e"));
80-
81-
assertEquals("(a ? b : c) + d", new BinaryExpression(ite, "+", new Var("d")).toDisplayString());
82-
assertEquals("(a ? b : c) ? d : e", new Ite(ite, new Var("d"), new Var("e")).toDisplayString());
83-
assertEquals("a ? (b ? c : d) : e",
84-
new Ite(new Var("a"), new Ite(new Var("b"), new Var("c"), new Var("d")), new Var("e"))
85-
.toDisplayString());
86-
assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toDisplayString());
87-
assertEquals("(a ? b : c) ? d : e",
88-
new Ite(new GroupExpression(ite), new Var("d"), new Var("e")).toDisplayString());
89-
assertEquals("a ? b : (c ? d : e)",
90-
new Ite(new Var("a"), new Var("b"), new GroupExpression(nestedElse)).toDisplayString());
91-
assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toDisplayString());
91+
assertEquals("(a ? b : c) + d", parse("(a ? b : c) + d").toDisplayString());
92+
assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString());
93+
assertEquals("a ? (b ? c : d) : e", parse("a ? (b ? c : d) : e").toDisplayString());
94+
assertEquals("a ? b : (c ? d : e)", parse("a ? b : c ? d : e").toDisplayString());
95+
assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString());
96+
assertEquals("a ? b : (c ? d : e)", parse("a ? b : (c ? d : e)").toDisplayString());
97+
assertEquals("a ? b : (c ? d : (e ? f : g))", parse("a ? b : c ? d : e ? f : g").toDisplayString());
98+
assertEquals("a ? b : c", parse("a ? b : c").toDisplayString());
9299
}
93100
}

0 commit comments

Comments
 (0)