Skip to content

Commit 80799a4

Browse files
rcosta358rcosta358
committed
Fix Expression Formatting
1 parent ef48c5f commit 80799a4

3 files changed

Lines changed: 62 additions & 17 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) {
379379
thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
380380
elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
381381
}
382-
382+
383383
freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
384384
}
385385
vcChecker.addPathVariable(freshRV);

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

Lines changed: 40 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -41,42 +41,61 @@ private String formatExpression(Expression expression) {
4141
}
4242

4343
private String formatParentheses(Expression child, boolean shouldWrap) {
44+
Expression expression = unwrapGroup(child);
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));
50+
private String formatLeftOperand(Expression parent, Expression child) {
51+
return formatParentheses(child, needsLeftParentheses(parent, child));
5352
}
5453

5554
private String formatRightOperand(BinaryExpression parent, Expression child) {
5655
return formatParentheses(child, needsRightParentheses(parent, child));
5756
}
5857

5958
private String formatCondition(Expression child) {
60-
return formatParentheses(child, child instanceof Ite);
59+
return formatParentheses(child, unwrapGroup(child) instanceof Ite);
6160
}
6261

6362
private String formatArguments(List<Expression> args) {
6463
return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", "));
6564
}
6665

66+
private Expression unwrapGroup(Expression expression) {
67+
while (expression instanceof GroupExpression group)
68+
expression = group.getExpression();
69+
return expression;
70+
}
71+
6772
private boolean needsParentheses(Expression parent, Expression child) {
6873
return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent));
6974
}
7075

76+
private boolean needsLeftParentheses(Expression parent, Expression child) {
77+
if (needsParentheses(parent, child))
78+
return true;
79+
80+
Expression unwrappedChild = unwrapGroup(child);
81+
if (ExpressionPrecedence.of(unwrappedChild) != ExpressionPrecedence.of(parent))
82+
return false;
83+
84+
return parent instanceof BinaryExpression binary && isRightAssociative(binary.getOperator())
85+
&& unwrappedChild instanceof BinaryExpression;
86+
}
87+
7188
private boolean needsRightParentheses(BinaryExpression parent, Expression child) {
7289
if (needsParentheses(parent, child))
7390
return true;
7491

75-
if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent))
92+
Expression unwrappedChild = unwrapGroup(child);
93+
if (ExpressionPrecedence.of(unwrappedChild) != ExpressionPrecedence.of(parent))
7694
return false;
7795

78-
if (child instanceof BinaryExpression right)
79-
return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator());
96+
if (unwrappedChild instanceof BinaryExpression right)
97+
return !isRightAssociative(parent.getOperator())
98+
&& (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator()));
8099

81100
return false;
82101
}
@@ -85,14 +104,18 @@ private boolean isAssociative(String operator) {
85104
return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*");
86105
}
87106

107+
private boolean isRightAssociative(String operator) {
108+
return operator.equals("-->");
109+
}
110+
88111
@Override
89112
public String visitAliasInvocation(AliasInvocation alias) {
90113
return alias.getName() + "(" + formatArguments(alias.getArgs()) + ")";
91114
}
92115

93116
@Override
94117
public String visitBinaryExpression(BinaryExpression exp) {
95-
return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " "
118+
return formatLeftOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " "
96119
+ formatRightOperand(exp, exp.getSecondOperand());
97120
}
98121

@@ -103,13 +126,13 @@ public String visitFunctionInvocation(FunctionInvocation fun) {
103126

104127
@Override
105128
public String visitGroupExpression(GroupExpression exp) {
106-
return "(" + formatExpression(exp.getExpression()) + ")";
129+
return formatExpression(exp.getExpression());
107130
}
108131

109132
@Override
110133
public String visitIte(Ite ite) {
111134
return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : "
112-
+ formatOperand(ite, ite.getElse());
135+
+ formatLeftOperand(ite, ite.getElse());
113136
}
114137

115138
@Override
@@ -144,7 +167,10 @@ public String visitLiteralString(LiteralString lit) {
144167

145168
@Override
146169
public String visitUnaryExpression(UnaryExpression exp) {
147-
return exp.getOp() + formatOperand(exp, exp.getExpression());
170+
Expression child = unwrapGroup(exp.getExpression());
171+
boolean nestedMinus = child instanceof UnaryExpression unary && exp.getOp().equals("-")
172+
&& unary.getOp().equals("-");
173+
return exp.getOp() + formatParentheses(child, needsParentheses(exp, child) || nestedMinus);
148174
}
149175

150176
@Override

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

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
package liquidjava.rj_language.ast;
22

33
import static org.junit.jupiter.api.Assertions.assertEquals;
4+
5+
import java.util.List;
6+
47
import org.junit.jupiter.api.Test;
58

69
class ExpressionFormatterTest {
@@ -48,6 +51,19 @@ void formatsBinaryPrecedence() {
4851
assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toDisplayString());
4952
}
5053

54+
@Test
55+
void omitsUnnecessaryGroupParentheses() {
56+
Expression comparison = new BinaryExpression(new FunctionInvocation("size", List.of(new Var("#stack_294"))),
57+
">", new LiteralInt(0));
58+
Expression groupedComparison = new GroupExpression(comparison);
59+
60+
assertEquals("size(stack²⁹⁴) > 0", groupedComparison.toDisplayString());
61+
assertEquals("size(stack²⁹⁴) > 0 && ready",
62+
new BinaryExpression(groupedComparison, "&&", new Var("ready")).toDisplayString());
63+
assertEquals("ready && size(stack²⁹⁴) > 0",
64+
new BinaryExpression(new Var("ready"), "&&", groupedComparison).toDisplayString());
65+
}
66+
5167
@Test
5268
void formatsRightGrouping() {
5369
Expression groupedSum = new GroupExpression(new BinaryExpression(new Var("b"), "+", new Var("c")));
@@ -66,7 +82,10 @@ void formatsLogicalExpressions() {
6682

6783
assertEquals("a && b || c", new BinaryExpression(andExpression, "||", new Var("c")).toDisplayString());
6884
assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toDisplayString());
69-
assertEquals("a --> (b --> c)", new BinaryExpression(new Var("a"), "-->", implication).toDisplayString());
85+
assertEquals("a --> b --> c", new BinaryExpression(new Var("a"), "-->", implication).toDisplayString());
86+
assertEquals("(a --> b) --> c",
87+
new BinaryExpression(new BinaryExpression(new Var("a"), "-->", new Var("b")), "-->", new Var("c"))
88+
.toDisplayString());
7089
assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toDisplayString());
7190
assertEquals("a || b || c",
7291
new BinaryExpression(new BinaryExpression(new Var("a"), "||", new Var("b")), "||", new Var("c"))
@@ -86,7 +105,7 @@ void formatsTernaryExpressions() {
86105
assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toDisplayString());
87106
assertEquals("(a ? b : c) ? d : e",
88107
new Ite(new GroupExpression(ite), new Var("d"), new Var("e")).toDisplayString());
89-
assertEquals("a ? b : (c ? d : e)",
108+
assertEquals("a ? b : c ? d : e",
90109
new Ite(new Var("a"), new Var("b"), new GroupExpression(nestedElse)).toDisplayString());
91110
assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toDisplayString());
92111
}

0 commit comments

Comments
 (0)