From 80799a4d39ed9384302e9a21af57d731fd6b1699 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 10 May 2026 14:29:04 +0100 Subject: [PATCH 1/5] Fix Expression Formatting --- .../RefinementTypeChecker.java | 2 +- .../ast/formatter/ExpressionFormatter.java | 54 ++++++++++++++----- .../ast/ExpressionFormatterTest.java | 23 +++++++- 3 files changed, 62 insertions(+), 17 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 09095f35..e5655d5a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) { thenRefs = Predicate.createConjunction(expRefs, freshIsTrue); elseRefs = Predicate.createConjunction(expRefs, freshIsFalse); } - + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); } vcChecker.addPathVariable(freshRV); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index 80e03261..b40a1c6a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -41,15 +41,14 @@ private String formatExpression(Expression expression) { } private String formatParentheses(Expression child, boolean shouldWrap) { + Expression expression = unwrapGroup(child); if (shouldWrap) - return "(" + formatExpression(child) + ")"; - if (child instanceof GroupExpression group) - return "(" + formatExpression(group.getExpression()) + ")"; - return formatExpression(child); + return "(" + formatExpression(expression) + ")"; + return formatExpression(expression); } - private String formatOperand(Expression parent, Expression child) { - return formatParentheses(child, needsParentheses(parent, child)); + private String formatLeftOperand(Expression parent, Expression child) { + return formatParentheses(child, needsLeftParentheses(parent, child)); } private String formatRightOperand(BinaryExpression parent, Expression child) { @@ -57,26 +56,46 @@ private String formatRightOperand(BinaryExpression parent, Expression child) { } private String formatCondition(Expression child) { - return formatParentheses(child, child instanceof Ite); + return formatParentheses(child, unwrapGroup(child) instanceof Ite); } private String formatArguments(List args) { return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", ")); } + private Expression unwrapGroup(Expression expression) { + while (expression instanceof GroupExpression group) + expression = group.getExpression(); + return expression; + } + private boolean needsParentheses(Expression parent, Expression child) { return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent)); } + private boolean needsLeftParentheses(Expression parent, Expression child) { + if (needsParentheses(parent, child)) + return true; + + Expression unwrappedChild = unwrapGroup(child); + if (ExpressionPrecedence.of(unwrappedChild) != ExpressionPrecedence.of(parent)) + return false; + + return parent instanceof BinaryExpression binary && isRightAssociative(binary.getOperator()) + && unwrappedChild instanceof BinaryExpression; + } + private boolean needsRightParentheses(BinaryExpression parent, Expression child) { if (needsParentheses(parent, child)) return true; - if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent)) + Expression unwrappedChild = unwrapGroup(child); + if (ExpressionPrecedence.of(unwrappedChild) != ExpressionPrecedence.of(parent)) return false; - if (child instanceof BinaryExpression right) - return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator()); + if (unwrappedChild instanceof BinaryExpression right) + return !isRightAssociative(parent.getOperator()) + && (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator())); return false; } @@ -85,6 +104,10 @@ private boolean isAssociative(String operator) { return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*"); } + private boolean isRightAssociative(String operator) { + return operator.equals("-->"); + } + @Override public String visitAliasInvocation(AliasInvocation alias) { return alias.getName() + "(" + formatArguments(alias.getArgs()) + ")"; @@ -92,7 +115,7 @@ public String visitAliasInvocation(AliasInvocation alias) { @Override public String visitBinaryExpression(BinaryExpression exp) { - return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " " + return formatLeftOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " " + formatRightOperand(exp, exp.getSecondOperand()); } @@ -103,13 +126,13 @@ public String visitFunctionInvocation(FunctionInvocation fun) { @Override public String visitGroupExpression(GroupExpression exp) { - return "(" + formatExpression(exp.getExpression()) + ")"; + return formatExpression(exp.getExpression()); } @Override public String visitIte(Ite ite) { return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : " - + formatOperand(ite, ite.getElse()); + + formatLeftOperand(ite, ite.getElse()); } @Override @@ -144,7 +167,10 @@ public String visitLiteralString(LiteralString lit) { @Override public String visitUnaryExpression(UnaryExpression exp) { - return exp.getOp() + formatOperand(exp, exp.getExpression()); + Expression child = unwrapGroup(exp.getExpression()); + boolean nestedMinus = child instanceof UnaryExpression unary && exp.getOp().equals("-") + && unary.getOp().equals("-"); + return exp.getOp() + formatParentheses(child, needsParentheses(exp, child) || nestedMinus); } @Override diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java index 25db19ab..98e0c7c2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -1,6 +1,9 @@ package liquidjava.rj_language.ast; import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.List; + import org.junit.jupiter.api.Test; class ExpressionFormatterTest { @@ -48,6 +51,19 @@ void formatsBinaryPrecedence() { assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toDisplayString()); } + @Test + void omitsUnnecessaryGroupParentheses() { + Expression comparison = new BinaryExpression(new FunctionInvocation("size", List.of(new Var("#stack_294"))), + ">", new LiteralInt(0)); + Expression groupedComparison = new GroupExpression(comparison); + + assertEquals("size(stack²⁹⁴) > 0", groupedComparison.toDisplayString()); + assertEquals("size(stack²⁹⁴) > 0 && ready", + new BinaryExpression(groupedComparison, "&&", new Var("ready")).toDisplayString()); + assertEquals("ready && size(stack²⁹⁴) > 0", + new BinaryExpression(new Var("ready"), "&&", groupedComparison).toDisplayString()); + } + @Test void formatsRightGrouping() { Expression groupedSum = new GroupExpression(new BinaryExpression(new Var("b"), "+", new Var("c"))); @@ -66,7 +82,10 @@ void formatsLogicalExpressions() { assertEquals("a && b || c", new BinaryExpression(andExpression, "||", new Var("c")).toDisplayString()); assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toDisplayString()); - assertEquals("a --> (b --> c)", new BinaryExpression(new Var("a"), "-->", implication).toDisplayString()); + assertEquals("a --> b --> c", new BinaryExpression(new Var("a"), "-->", implication).toDisplayString()); + assertEquals("(a --> b) --> c", + new BinaryExpression(new BinaryExpression(new Var("a"), "-->", new Var("b")), "-->", new Var("c")) + .toDisplayString()); assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toDisplayString()); assertEquals("a || b || c", new BinaryExpression(new BinaryExpression(new Var("a"), "||", new Var("b")), "||", new Var("c")) @@ -86,7 +105,7 @@ void formatsTernaryExpressions() { assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toDisplayString()); assertEquals("(a ? b : c) ? d : e", new Ite(new GroupExpression(ite), new Var("d"), new Var("e")).toDisplayString()); - assertEquals("a ? b : (c ? d : e)", + assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), new GroupExpression(nestedElse)).toDisplayString()); assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toDisplayString()); } From f9e52205a3ce5b2cc465cc6b5e662a1b3c2adc52 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 10 May 2026 14:31:43 +0100 Subject: [PATCH 2/5] Refactor Expression Formatter --- .../ast/formatter/ExpressionFormatter.java | 65 ++++++++----------- 1 file changed, 26 insertions(+), 39 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index b40a1c6a..61baa61b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -40,27 +40,24 @@ private String formatExpression(Expression expression) { return expression.accept(this); } - private String formatParentheses(Expression child, boolean shouldWrap) { - Expression expression = unwrapGroup(child); + private String formatExpression(Expression expression, boolean shouldWrap) { + expression = unwrapGroup(expression); if (shouldWrap) return "(" + formatExpression(expression) + ")"; return formatExpression(expression); } - private String formatLeftOperand(Expression parent, Expression child) { - return formatParentheses(child, needsLeftParentheses(parent, child)); - } - - private String formatRightOperand(BinaryExpression parent, Expression child) { - return formatParentheses(child, needsRightParentheses(parent, child)); + private String formatOperand(Expression parent, Expression child, boolean rightOperand) { + child = unwrapGroup(child); + return formatExpression(child, needsParentheses(parent, child, rightOperand)); } private String formatCondition(Expression child) { - return formatParentheses(child, unwrapGroup(child) instanceof Ite); + return formatExpression(child, unwrapGroup(child) instanceof Ite); } private String formatArguments(List args) { - return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", ")); + return args.stream().map(expression -> formatExpression(expression, false)).collect(Collectors.joining(", ")); } private Expression unwrapGroup(Expression expression) { @@ -69,35 +66,28 @@ private Expression unwrapGroup(Expression expression) { return expression; } - private boolean needsParentheses(Expression parent, Expression child) { - return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent)); - } - - private boolean needsLeftParentheses(Expression parent, Expression child) { - if (needsParentheses(parent, child)) + private boolean needsParentheses(Expression parent, Expression child, boolean rightOperand) { + ExpressionPrecedence parentPrecedence = ExpressionPrecedence.of(parent); + ExpressionPrecedence childPrecedence = ExpressionPrecedence.of(child); + if (childPrecedence.isLowerThan(parentPrecedence)) return true; - - Expression unwrappedChild = unwrapGroup(child); - if (ExpressionPrecedence.of(unwrappedChild) != ExpressionPrecedence.of(parent)) + if (childPrecedence != parentPrecedence) return false; - return parent instanceof BinaryExpression binary && isRightAssociative(binary.getOperator()) - && unwrappedChild instanceof BinaryExpression; - } + if (parent instanceof BinaryExpression parentBinary && child instanceof BinaryExpression childBinary) + return needsBinaryParentheses(parentBinary, childBinary, rightOperand); - private boolean needsRightParentheses(BinaryExpression parent, Expression child) { - if (needsParentheses(parent, child)) - return true; + if (parent instanceof UnaryExpression parentUnary && child instanceof UnaryExpression childUnary) + return parentUnary.getOp().equals("-") && childUnary.getOp().equals("-"); - Expression unwrappedChild = unwrapGroup(child); - if (ExpressionPrecedence.of(unwrappedChild) != ExpressionPrecedence.of(parent)) - return false; + return false; + } - if (unwrappedChild instanceof BinaryExpression right) + private boolean needsBinaryParentheses(BinaryExpression parent, BinaryExpression child, boolean rightOperand) { + if (rightOperand) return !isRightAssociative(parent.getOperator()) - && (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator())); - - return false; + && (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(child.getOperator())); + return isRightAssociative(parent.getOperator()); } private boolean isAssociative(String operator) { @@ -115,8 +105,8 @@ public String visitAliasInvocation(AliasInvocation alias) { @Override public String visitBinaryExpression(BinaryExpression exp) { - return formatLeftOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " " - + formatRightOperand(exp, exp.getSecondOperand()); + return formatOperand(exp, exp.getFirstOperand(), false) + " " + exp.getOperator() + " " + + formatOperand(exp, exp.getSecondOperand(), true); } @Override @@ -132,7 +122,7 @@ public String visitGroupExpression(GroupExpression exp) { @Override public String visitIte(Ite ite) { return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : " - + formatLeftOperand(ite, ite.getElse()); + + formatOperand(ite, ite.getElse(), true); } @Override @@ -167,10 +157,7 @@ public String visitLiteralString(LiteralString lit) { @Override public String visitUnaryExpression(UnaryExpression exp) { - Expression child = unwrapGroup(exp.getExpression()); - boolean nestedMinus = child instanceof UnaryExpression unary && exp.getOp().equals("-") - && unary.getOp().equals("-"); - return exp.getOp() + formatParentheses(child, needsParentheses(exp, child) || nestedMinus); + return exp.getOp() + formatOperand(exp, exp.getExpression(), true); } @Override From 8c473f713d255c2d36aa0703807d4e52fb2fca9b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 11 May 2026 15:22:14 +0100 Subject: [PATCH 3/5] Refactor ExpressionFormatterTest --- .../ast/ExpressionFormatterTest.java | 109 +++++++----------- 1 file changed, 41 insertions(+), 68 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java index 98e0c7c2..c09ccae2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -2,111 +2,84 @@ import static org.junit.jupiter.api.Assertions.assertEquals; -import java.util.List; - import org.junit.jupiter.api.Test; +import liquidjava.rj_language.parsing.RefinementsParser; + class ExpressionFormatterTest { + private static Expression parse(String refinement) { + return RefinementsParser.createAST(refinement, ""); + } + @Test void formatsUnaryAtoms() { - assertEquals("!x", new UnaryExpression("!", new Var("x")).toDisplayString()); - assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toDisplayString()); + assertEquals("!x", parse("!x").toDisplayString()); + assertEquals("!false", parse("!false").toDisplayString()); } @Test void formatsInternalVariables() { - assertEquals("x", new Var("x").toDisplayString()); - assertEquals("x²", new Var("#x_2").toDisplayString()); - assertEquals("#fresh¹²", new Var("#fresh_12").toDisplayString()); - assertEquals("#ret³", new Var("#ret_3").toDisplayString()); - assertEquals("this#Class", new Var("this#Class").toDisplayString()); + assertEquals("x", parse("x").toDisplayString()); + assertEquals("x²", parse("#x_2").toDisplayString()); + assertEquals("#fresh¹²", parse("#fresh_12").toDisplayString()); + assertEquals("#ret³", parse("#ret_3").toDisplayString()); + assertEquals("this#Class", parse("this#Class").toDisplayString()); } @Test void formatsEnums() { - assertEquals("Color.RED", new Enum("Color", "RED").toDisplayString()); + assertEquals("Color.RED", parse("Color.RED").toDisplayString()); } @Test void formatsUnaryCompounds() { - Expression comparison = new BinaryExpression(new Var("x"), ">", new LiteralInt(0)); - - assertEquals("x > 0", comparison.toDisplayString()); - assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toDisplayString()); - assertEquals("-(-x)", new UnaryExpression("-", new GroupExpression(new UnaryExpression("-", new Var("x")))) - .toDisplayString()); + assertEquals("x > 0", parse("x > 0").toDisplayString()); + assertEquals("!(x > 0)", parse("!(x > 0)").toDisplayString()); + assertEquals("-(-x)", parse("-(-x)").toDisplayString()); } @Test void formatsBinaryPrecedence() { - Expression sum = new BinaryExpression(new Var("a"), "+", new Var("b")); - Expression product = new BinaryExpression(new Var("b"), "*", new Var("c")); - - assertEquals("(a + b) * c", new BinaryExpression(sum, "*", new Var("c")).toDisplayString()); - assertEquals("a * (a + b)", new BinaryExpression(new Var("a"), "*", sum).toDisplayString()); - assertEquals("a + b * c", new BinaryExpression(new Var("a"), "+", product).toDisplayString()); - assertEquals("a - (a + b)", new BinaryExpression(new Var("a"), "-", sum).toDisplayString()); - assertEquals("a + b + c", new BinaryExpression(sum, "+", new Var("c")).toDisplayString()); - assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toDisplayString()); + assertEquals("(a + b) * c", parse("(a + b) * c").toDisplayString()); + assertEquals("a * (a + b)", parse("a * (a + b)").toDisplayString()); + assertEquals("a + b * c", parse("a + b * c").toDisplayString()); + assertEquals("a - (a + b)", parse("a - (a + b)").toDisplayString()); + assertEquals("a + b + c", parse("a + b + c").toDisplayString()); + assertEquals("b * c * c", parse("b * c * c").toDisplayString()); } @Test void omitsUnnecessaryGroupParentheses() { - Expression comparison = new BinaryExpression(new FunctionInvocation("size", List.of(new Var("#stack_294"))), - ">", new LiteralInt(0)); - Expression groupedComparison = new GroupExpression(comparison); - - assertEquals("size(stack²⁹⁴) > 0", groupedComparison.toDisplayString()); - assertEquals("size(stack²⁹⁴) > 0 && ready", - new BinaryExpression(groupedComparison, "&&", new Var("ready")).toDisplayString()); - assertEquals("ready && size(stack²⁹⁴) > 0", - new BinaryExpression(new Var("ready"), "&&", groupedComparison).toDisplayString()); + assertEquals("size(stack²⁹⁴) > 0", parse("(size(#stack_294) > 0)").toDisplayString()); + assertEquals("size(stack²⁹⁴) > 0 && ready", parse("(size(#stack_294) > 0) && ready").toDisplayString()); + assertEquals("ready && size(stack²⁹⁴) > 0", parse("ready && (size(#stack_294) > 0)").toDisplayString()); } @Test void formatsRightGrouping() { - Expression groupedSum = new GroupExpression(new BinaryExpression(new Var("b"), "+", new Var("c"))); - Expression groupedComparison = new GroupExpression( - new BinaryExpression(new LiteralInt(1), ">", new LiteralInt(0))); - - assertEquals("a - (b + c)", new BinaryExpression(new Var("a"), "-", groupedSum).toDisplayString()); - assertEquals("x == (1 > 0)", new BinaryExpression(new Var("x"), "==", groupedComparison).toDisplayString()); + assertEquals("a - (b + c)", parse("a - (b + c)").toDisplayString()); + assertEquals("x == (1 > 0)", parse("x == (1 > 0)").toDisplayString()); } @Test void formatsLogicalExpressions() { - Expression andExpression = new BinaryExpression(new Var("a"), "&&", new Var("b")); - Expression orExpression = new BinaryExpression(new Var("b"), "||", new Var("c")); - Expression implication = new BinaryExpression(new Var("b"), "-->", new Var("c")); - - assertEquals("a && b || c", new BinaryExpression(andExpression, "||", new Var("c")).toDisplayString()); - assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toDisplayString()); - assertEquals("a --> b --> c", new BinaryExpression(new Var("a"), "-->", implication).toDisplayString()); - assertEquals("(a --> b) --> c", - new BinaryExpression(new BinaryExpression(new Var("a"), "-->", new Var("b")), "-->", new Var("c")) - .toDisplayString()); - assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toDisplayString()); - assertEquals("a || b || c", - new BinaryExpression(new BinaryExpression(new Var("a"), "||", new Var("b")), "||", new Var("c")) - .toDisplayString()); + assertEquals("a && b || c", parse("a && b || c").toDisplayString()); + assertEquals("a && (b || c)", parse("a && (b || c)").toDisplayString()); + assertEquals("a --> b --> c", parse("a --> b --> c").toDisplayString()); + assertEquals("(a --> b) --> c", parse("(a --> b) --> c").toDisplayString()); + assertEquals("a && b && c", parse("a && b && c").toDisplayString()); + assertEquals("a || b || c", parse("a || b || c").toDisplayString()); } @Test void formatsTernaryExpressions() { - Expression ite = new Ite(new Var("a"), new Var("b"), new Var("c")); - Expression nestedElse = new Ite(new Var("c"), new Var("d"), new Var("e")); - - assertEquals("(a ? b : c) + d", new BinaryExpression(ite, "+", new Var("d")).toDisplayString()); - assertEquals("(a ? b : c) ? d : e", new Ite(ite, new Var("d"), new Var("e")).toDisplayString()); - assertEquals("a ? (b ? c : d) : e", - new Ite(new Var("a"), new Ite(new Var("b"), new Var("c"), new Var("d")), new Var("e")) - .toDisplayString()); - assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toDisplayString()); - assertEquals("(a ? b : c) ? d : e", - new Ite(new GroupExpression(ite), new Var("d"), new Var("e")).toDisplayString()); - assertEquals("a ? b : c ? d : e", - new Ite(new Var("a"), new Var("b"), new GroupExpression(nestedElse)).toDisplayString()); - assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toDisplayString()); + assertEquals("(a ? b : c) + d", parse("(a ? b : c) + d").toDisplayString()); + assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString()); + assertEquals("a ? (b ? c : d) : e", parse("a ? (b ? c : d) : e").toDisplayString()); + assertEquals("a ? b : c ? d : e", parse("a ? b : c ? d : e").toDisplayString()); + assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString()); + assertEquals("a ? b : c ? d : e", parse("a ? b : (c ? d : e)").toDisplayString()); + assertEquals("a ? b : c", parse("a ? b : c").toDisplayString()); } } From aa7bf01b3dc00da1c22d35070b6e9b79e898d180 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 11 May 2026 15:26:37 +0100 Subject: [PATCH 4/5] Add Parentheses to Right Associative Expressions --- .../rj_language/ast/formatter/ExpressionFormatter.java | 8 +++++++- .../rj_language/ast/ExpressionFormatterTest.java | 9 ++++++--- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index 61baa61b..cf6e4fdc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -77,6 +77,9 @@ private boolean needsParentheses(Expression parent, Expression child, boolean ri if (parent instanceof BinaryExpression parentBinary && child instanceof BinaryExpression childBinary) return needsBinaryParentheses(parentBinary, childBinary, rightOperand); + if (parent instanceof Ite && child instanceof Ite) + return true; + if (parent instanceof UnaryExpression parentUnary && child instanceof UnaryExpression childUnary) return parentUnary.getOp().equals("-") && childUnary.getOp().equals("-"); @@ -84,9 +87,12 @@ private boolean needsParentheses(Expression parent, Expression child, boolean ri } private boolean needsBinaryParentheses(BinaryExpression parent, BinaryExpression child, boolean rightOperand) { - if (rightOperand) + if (rightOperand) { + if (isRightAssociative(parent.getOperator())) + return true; return !isRightAssociative(parent.getOperator()) && (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(child.getOperator())); + } return isRightAssociative(parent.getOperator()); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java index c09ccae2..9bcfd80a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -66,7 +66,9 @@ void formatsRightGrouping() { void formatsLogicalExpressions() { assertEquals("a && b || c", parse("a && b || c").toDisplayString()); assertEquals("a && (b || c)", parse("a && (b || c)").toDisplayString()); - assertEquals("a --> b --> c", parse("a --> b --> c").toDisplayString()); + assertEquals("a --> (b --> c)", parse("a --> b --> c").toDisplayString()); + assertEquals("a --> (b --> c)", parse("a --> (b --> c)").toDisplayString()); + assertEquals("a --> (b --> (c --> d))", parse("a --> b --> c --> d").toDisplayString()); assertEquals("(a --> b) --> c", parse("(a --> b) --> c").toDisplayString()); assertEquals("a && b && c", parse("a && b && c").toDisplayString()); assertEquals("a || b || c", parse("a || b || c").toDisplayString()); @@ -77,9 +79,10 @@ void formatsTernaryExpressions() { assertEquals("(a ? b : c) + d", parse("(a ? b : c) + d").toDisplayString()); assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString()); assertEquals("a ? (b ? c : d) : e", parse("a ? (b ? c : d) : e").toDisplayString()); - assertEquals("a ? b : c ? d : e", parse("a ? b : c ? d : e").toDisplayString()); + assertEquals("a ? b : (c ? d : e)", parse("a ? b : c ? d : e").toDisplayString()); assertEquals("(a ? b : c) ? d : e", parse("(a ? b : c) ? d : e").toDisplayString()); - assertEquals("a ? b : c ? d : e", parse("a ? b : (c ? d : e)").toDisplayString()); + assertEquals("a ? b : (c ? d : e)", parse("a ? b : (c ? d : e)").toDisplayString()); + assertEquals("a ? b : (c ? d : (e ? f : g))", parse("a ? b : c ? d : e ? f : g").toDisplayString()); assertEquals("a ? b : c", parse("a ? b : c").toDisplayString()); } } From c9d684e22aa41669f6326057818dc64067f5026a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 11 May 2026 17:50:08 +0100 Subject: [PATCH 5/5] Add More Test Cases --- .../rj_language/ast/ExpressionFormatterTest.java | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java index 9bcfd80a..ad96edad 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -51,6 +51,14 @@ void formatsBinaryPrecedence() { @Test void omitsUnnecessaryGroupParentheses() { + assertEquals("x", parse("(x)").toDisplayString()); + assertEquals("x", parse("((x))").toDisplayString()); + assertEquals("1", parse("(1)").toDisplayString()); + assertEquals("a > 0", parse("(a > 0)").toDisplayString()); + assertEquals("a + b + c", parse("a + (b + c)").toDisplayString()); + assertEquals("a + b * c", parse("a + (b * c)").toDisplayString()); + assertEquals("a && b > 0", parse("a && (b > 0)").toDisplayString()); + assertEquals("a && b && c", parse("a && (b && c)").toDisplayString()); assertEquals("size(stack²⁹⁴) > 0", parse("(size(#stack_294) > 0)").toDisplayString()); assertEquals("size(stack²⁹⁴) > 0 && ready", parse("(size(#stack_294) > 0) && ready").toDisplayString()); assertEquals("ready && size(stack²⁹⁴) > 0", parse("ready && (size(#stack_294) > 0)").toDisplayString()); @@ -59,7 +67,11 @@ void omitsUnnecessaryGroupParentheses() { @Test void formatsRightGrouping() { assertEquals("a - (b + c)", parse("a - (b + c)").toDisplayString()); + assertEquals("a - (b - c)", parse("a - (b - c)").toDisplayString()); + assertEquals("a / (b * c)", parse("a / (b * c)").toDisplayString()); + assertEquals("(a || b) && c", parse("(a || b) && c").toDisplayString()); assertEquals("x == (1 > 0)", parse("x == (1 > 0)").toDisplayString()); + assertEquals("a == (b == c)", parse("a == (b == c)").toDisplayString()); } @Test