From 80799a4d39ed9384302e9a21af57d731fd6b1699 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 10 May 2026 14:29:04 +0100 Subject: [PATCH 1/2] 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/2] 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