Fix Expression Formatter

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);

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

@@ -40,60 +40,73 @@ private String formatExpression(Expression expression) {
         return expression.accept(this);
     }
 
-    private String formatParentheses(Expression child, boolean shouldWrap) {
+    private String formatExpression(Expression expression, boolean shouldWrap) {
+        expression = unwrapGroup(expression);
         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 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, child instanceof Ite);
+        return formatExpression(child, unwrapGroup(child) instanceof Ite);
     }
 
     private String formatArguments(List<Expression> args) {
-        return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", "));
+        return args.stream().map(expression -> formatExpression(expression, false)).collect(Collectors.joining(", "));
     }
 
-    private boolean needsParentheses(Expression parent, Expression child) {
-        return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent));
+    private Expression unwrapGroup(Expression expression) {
+        while (expression instanceof GroupExpression group)
+            expression = group.getExpression();
+        return expression;
     }
 
-    private boolean needsRightParentheses(BinaryExpression 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;
-
-        if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent))
+        if (childPrecedence != parentPrecedence)
             return false;
 
-        if (child instanceof BinaryExpression right)
-            return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator());
+        if (parent instanceof BinaryExpression parentBinary && child instanceof BinaryExpression childBinary)
+            return needsBinaryParentheses(parentBinary, childBinary, rightOperand);
+
+        if (parent instanceof UnaryExpression parentUnary && child instanceof UnaryExpression childUnary)
+            return parentUnary.getOp().equals("-") && childUnary.getOp().equals("-");
 
         return false;
     }
 
+    private boolean needsBinaryParentheses(BinaryExpression parent, BinaryExpression child, boolean rightOperand) {
+        if (rightOperand)
+            return !isRightAssociative(parent.getOperator())
+                    && (!isAssociative(parent.getOperator()) || !parent.getOperator().equals(child.getOperator()));
+        return isRightAssociative(parent.getOperator());
+    }
+
     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()) + ")";
     }
 
     @Override
     public String visitBinaryExpression(BinaryExpression exp) {
-        return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " "
-                + formatRightOperand(exp, exp.getSecondOperand());
+        return formatOperand(exp, exp.getFirstOperand(), false) + " " + exp.getOperator() + " "
+                + formatOperand(exp, exp.getSecondOperand(), true);
     }
 
     @Override
@@ -103,13 +116,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());
+                + formatOperand(ite, ite.getElse(), true);
     }
 
     @Override
@@ -144,7 +157,7 @@ public String visitLiteralString(LiteralString lit) {
 
     @Override
     public String visitUnaryExpression(UnaryExpression exp) {
-        return exp.getOp() + formatOperand(exp, exp.getExpression());
+        return exp.getOp() + formatOperand(exp, exp.getExpression(), true);
     }
 
     @Override

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());
     }