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,79 @@ 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 Ite && child instanceof Ite)
+            return true;
+
+        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) {
+            if (isRightAssociative(parent.getOperator()))
+                return true;
+            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 +122,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 +163,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,93 +1,100 @@
 package liquidjava.rj_language.ast;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
+
 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", 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());
+    }
 
-        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());
+    @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());
     }
 
     @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("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
     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(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 --> 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());
     }
 
     @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 ? d : (e ? f : g))", parse("a ? b : c ? d : e ? f : g").toDisplayString());
+        assertEquals("a ? b : c", parse("a ? b : c").toDisplayString());
     }
 }