From 9c7ed97a5c2cb993afb33b302982c84c20a9b479 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 31 Mar 2026 19:38:27 +0100 Subject: [PATCH 01/13] Fix Expression Parentheses --- .../rj_language/ast/BinaryExpression.java | 23 ++++++- .../rj_language/ast/Expression.java | 33 ++++++++++ .../rj_language/ast/GroupExpression.java | 5 ++ .../java/liquidjava/rj_language/ast/Ite.java | 14 ++++- .../rj_language/ast/UnaryExpression.java | 7 ++- .../ast/ExpressionPrinterTest.java | 63 +++++++++++++++++++ .../opt/ExpressionSimplifierTest.java | 19 +++--- 7 files changed, 147 insertions(+), 17 deletions(-) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index a5112c8c..01f99dec 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java @@ -40,14 +40,31 @@ public boolean isArithmeticOperation() { return !isLogicOperation() && !isBooleanOperation(); } + private boolean isAssociative() { + return op.equals("&&") || op.equals("||") || op.equals("+") || op.equals("*"); + } + @Override - public T accept(ExpressionVisitor visitor) throws LJError { - return visitor.visitBinaryExpression(this); + protected Precedence getPrecedence() { + return Precedence.fromOperator(op); + } + + private String formatRightOperand(Expression operand) { + if (operand.getPrecedence() == getPrecedence() && operand instanceof BinaryExpression right) + if (!isAssociative() || !op.equals(right.getOperator())) + return parenthesize(operand); + + return formatChild(operand); } @Override public String toString() { - return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString(); + return formatChild(getFirstOperand()) + " " + op + " " + formatRightOperand(getSecondOperand()); + } + + @Override + public T accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitBinaryExpression(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 3859c530..2f5a888b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -36,6 +36,39 @@ public abstract class Expression { public abstract String toString(); + protected enum Precedence { + TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, PREFIX, ATOMIC; + + private boolean isLowerThan(Precedence other) { + return ordinal() < other.ordinal(); + } + + protected static Precedence fromOperator(String op) { + return switch (op) { + case "-->" -> IMPLICATION; + case "||" -> OR; + case "&&" -> AND; + case "==", "!=", ">=", ">", "<=", "<" -> COMPARISON; + case "+", "-" -> ADDITIVE; + case "*", "/", "%" -> MULTIPLICATIVE; + default -> ATOMIC; + }; + } + } + + protected Precedence getPrecedence() { + return Precedence.ATOMIC; + } + + protected String parenthesize(Expression expression) { + return "(" + expression.toString() + ")"; + } + + protected String formatChild(Expression child) { + boolean needsParentheses = child.getPrecedence().isLowerThan(getPrecedence()); + return needsParentheses ? parenthesize(child) : child.toString(); + } + List children = new ArrayList<>(); public void addChild(Expression e) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java index 4597a157..3567afd8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java @@ -24,6 +24,11 @@ public String toString() { return getExpression().toString(); } + @Override + protected Precedence getPrecedence() { + return getExpression().getPrecedence(); + } + @Override public void getVariableNames(List toAdd) { getExpression().getVariableNames(toAdd); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java index cf95b730..08542186 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java @@ -30,9 +30,21 @@ public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitIte(this); } + @Override + protected Precedence getPrecedence() { + return Precedence.TERNARY; + } + + private String formatCondition(Expression operand) { + if (operand instanceof Ite) + return parenthesize(operand); + + return formatChild(operand); + } + @Override public String toString() { - return getCondition().toString() + " ? " + getThen().toString() + " : " + getElse().toString(); + return formatCondition(getCondition()) + " ? " + formatCondition(getThen()) + " : " + formatChild(getElse()); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java index 4ffbc2d9..f6af6eae 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java @@ -27,9 +27,14 @@ public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitUnaryExpression(this); } + @Override + protected Precedence getPrecedence() { + return Precedence.PREFIX; + } + @Override public String toString() { - return op + getExpression().toString(); + return op + formatChild(getExpression()); } @Override diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java new file mode 100644 index 00000000..ee20813a --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java @@ -0,0 +1,63 @@ +package liquidjava.rj_language.ast; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import org.junit.jupiter.api.Test; + +class ExpressionPrinterTest { + + @Test + void printsUnaryWithoutExtraParenthesesForAtoms() { + assertEquals("!x", new UnaryExpression("!", new Var("x")).toString()); + assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toString()); + } + + @Test + void printsUnaryWithParenthesesForCompoundOperands() { + Expression comparison = new BinaryExpression(new Var("x"), ">", new LiteralInt(0)); + + assertEquals("x > 0", comparison.toString()); + assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toString()); + } + + @Test + void printsBinaryExpressionsWithOperatorPrecedence() { + 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")).toString()); + assertEquals("a * (a + b)", new BinaryExpression(new Var("a"), "*", sum).toString()); + assertEquals("a + b * c", new BinaryExpression(new Var("a"), "+", product).toString()); + assertEquals("a - (a + b)", new BinaryExpression(new Var("a"), "-", sum).toString()); + assertEquals("a + b + c", new BinaryExpression(sum, "+", new Var("c")).toString()); + assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toString()); + } + + @Test + void printsLogicalExpressionsWithNeededParentheses() { + 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")).toString()); + assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toString()); + assertEquals("a --> (b --> c)", new BinaryExpression(new Var("a"), "-->", implication).toString()); + assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toString()); + assertEquals("a || b || c", + new BinaryExpression(new BinaryExpression(new Var("a"), "||", new Var("b")), "||", new Var("c")) + .toString()); + } + + @Test + void printsTernaryExpressionsWithNeededParentheses() { + 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")).toString()); + assertEquals("(a ? b : c) ? d : e", new Ite(ite, new Var("d"), new Var("e")).toString()); + 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")).toString()); + assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toString()); + assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toString()); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index 6ac20359..845b85f9 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -23,7 +23,7 @@ import org.junit.jupiter.api.Test; /** - * Test suite for expression simplification using constant propagation and folding + * Test suite for expression simplification */ class ExpressionSimplifierTest { @@ -562,8 +562,6 @@ void testTransitive() { @Test void testShouldNotOversimplifyToTrue() { // Given: x > 5 && x == y && y == 10 - // Iteration 1: resolves y == 10, substitutes y -> 10: x > 5 && x == 10 - // Iteration 2: resolves x == 10, substitutes x -> 10: 10 > 5 && 10 == 10 -> true // Expected: x > 5 && x == 10 (should NOT simplify to true) Expression varX = new Var("x"); @@ -592,8 +590,7 @@ void testShouldNotOversimplifyToTrue() { @Test void testShouldUnwrapBooleanInEquality() { // Given: x == (1 > 0) - // Without unwrapping: x == true (unhelpful - hides what "true" came from) - // Expected: x == 1 > 0 (unwrapped to show the original comparison) + // Expected: x == (1 > 0) (unwrapped to show the original comparison) Expression varX = new Var("x"); Expression one = new LiteralInt(1); @@ -606,15 +603,14 @@ void testShouldUnwrapBooleanInEquality() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == 1 > 0", result.getValue().toString(), + assertEquals("x == (1 > 0)", result.getValue().toString(), "Boolean in equality should be unwrapped to show the original comparison"); } @Test void testShouldUnwrapBooleanInEqualityWithPropagation() { // Given: x == (a > b) && a == 3 && b == 1 - // Without unwrapping: x == true (unhelpful) - // Expected: x == 3 > 1 (unwrapped and propagated) + // Expected: x == (3 > 1) (unwrapped and propagated) Expression varX = new Var("x"); Expression varA = new Var("a"); @@ -635,7 +631,7 @@ void testShouldUnwrapBooleanInEqualityWithPropagation() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == 3 > 1", result.getValue().toString(), + assertEquals("x == (3 > 1)", result.getValue().toString(), "Boolean in equality should be unwrapped after propagation"); } @@ -666,8 +662,7 @@ void testShouldNotUnwrapBooleanWithBooleanChildren() { @Test void testShouldUnwrapNestedBooleanInEquality() { // Given: x == (a + b > 10) && a == 3 && b == 5 - // Without unwrapping: x == true (unhelpful) - // Expected: x == 8 > 10 (shows the actual comparison that produced the boolean) + // Expected: x == (8 > 10) (shows the actual comparison that produced the boolean) Expression varX = new Var("x"); Expression varA = new Var("a"); @@ -690,7 +685,7 @@ void testShouldUnwrapNestedBooleanInEquality() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == 8 > 10", result.getValue().toString(), + assertEquals("x == (8 > 10)", result.getValue().toString(), "Boolean in equality should be unwrapped to show the computed comparison"); } From 0aa749a5dd3ce619e6534eb98cf314ee690b9632 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 31 Mar 2026 20:09:59 +0100 Subject: [PATCH 02/13] Add ExpressionPrinter for Pretty Printing --- .../rj_language/ast/AliasInvocation.java | 4 +- .../rj_language/ast/BinaryExpression.java | 19 +- .../rj_language/ast/Expression.java | 33 ---- .../rj_language/ast/ExpressionPrinter.java | 166 ++++++++++++++++++ .../rj_language/ast/FunctionInvocation.java | 5 +- .../rj_language/ast/GroupExpression.java | 7 +- .../java/liquidjava/rj_language/ast/Ite.java | 14 +- .../rj_language/ast/LiteralString.java | 1 + .../rj_language/ast/UnaryExpression.java | 7 +- .../ast/ExpressionPrinterTest.java | 15 ++ 10 files changed, 188 insertions(+), 83 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/ExpressionPrinter.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java index 2c02734f..54621a86 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java @@ -2,8 +2,6 @@ import java.util.ArrayList; import java.util.List; -import java.util.stream.Collectors; - import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; @@ -31,7 +29,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { @Override public String toString() { - return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")) + ")"; + return ExpressionPrinter.print(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index 01f99dec..d08850f5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java @@ -40,26 +40,9 @@ public boolean isArithmeticOperation() { return !isLogicOperation() && !isBooleanOperation(); } - private boolean isAssociative() { - return op.equals("&&") || op.equals("||") || op.equals("+") || op.equals("*"); - } - - @Override - protected Precedence getPrecedence() { - return Precedence.fromOperator(op); - } - - private String formatRightOperand(Expression operand) { - if (operand.getPrecedence() == getPrecedence() && operand instanceof BinaryExpression right) - if (!isAssociative() || !op.equals(right.getOperator())) - return parenthesize(operand); - - return formatChild(operand); - } - @Override public String toString() { - return formatChild(getFirstOperand()) + " " + op + " " + formatRightOperand(getSecondOperand()); + return ExpressionPrinter.print(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 2f5a888b..3859c530 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -36,39 +36,6 @@ public abstract class Expression { public abstract String toString(); - protected enum Precedence { - TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, PREFIX, ATOMIC; - - private boolean isLowerThan(Precedence other) { - return ordinal() < other.ordinal(); - } - - protected static Precedence fromOperator(String op) { - return switch (op) { - case "-->" -> IMPLICATION; - case "||" -> OR; - case "&&" -> AND; - case "==", "!=", ">=", ">", "<=", "<" -> COMPARISON; - case "+", "-" -> ADDITIVE; - case "*", "/", "%" -> MULTIPLICATIVE; - default -> ATOMIC; - }; - } - } - - protected Precedence getPrecedence() { - return Precedence.ATOMIC; - } - - protected String parenthesize(Expression expression) { - return "(" + expression.toString() + ")"; - } - - protected String formatChild(Expression child) { - boolean needsParentheses = child.getPrecedence().isLowerThan(getPrecedence()); - return needsParentheses ? parenthesize(child) : child.toString(); - } - List children = new ArrayList<>(); public void addChild(Expression e) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/ExpressionPrinter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/ExpressionPrinter.java new file mode 100644 index 00000000..047648b5 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/ExpressionPrinter.java @@ -0,0 +1,166 @@ +package liquidjava.rj_language.ast; + +import java.util.stream.Collectors; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.rj_language.visitors.ExpressionVisitor; +import liquidjava.utils.Utils; + +public class ExpressionPrinter implements ExpressionVisitor { + + private enum Precedence { + TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, PREFIX, ATOMIC; + + private boolean isLowerThan(Precedence other) { + return ordinal() < other.ordinal(); + } + } + + public static String print(Expression expression) { + return new ExpressionPrinter().render(expression); + } + + private String render(Expression expression) { + return expression.accept(this); + } + + private String renderChild(Expression child) { + if (child instanceof GroupExpression group) + return "(" + render(group.getExpression()) + ")"; + return render(child); + } + + private String renderOperand(Expression parent, Expression child) { + if (needsParentheses(parent, child)) + return "(" + render(child) + ")"; + return renderChild(child); + } + + private String renderRightOperand(BinaryExpression parent, Expression child) { + if (needsRightParentheses(parent, child)) + return "(" + render(child) + ")"; + return renderChild(child); + } + + private String renderConditionOperand(Expression child) { + if (child instanceof Ite) + return "(" + render(child) + ")"; + return renderChild(child); + } + + private boolean needsParentheses(Expression parent, Expression child) { + if (precedence(child).isLowerThan(precedence(parent))) + return true; + return false; + } + + private boolean needsRightParentheses(BinaryExpression parent, Expression child) { + if (needsParentheses(parent, child)) + return true; + + if (precedence(child) != precedence(parent)) + return false; + + if (child instanceof BinaryExpression right) + return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator()); + + return false; + } + + private Precedence precedence(Expression expression) { + if (expression instanceof GroupExpression group) + return precedence(group.getExpression()); + if (expression instanceof Ite) + return Precedence.TERNARY; + if (expression instanceof UnaryExpression) + return Precedence.PREFIX; + if (expression instanceof BinaryExpression binary) + return precedence(binary.getOperator()); + return Precedence.ATOMIC; + } + + private Precedence precedence(String operator) { + return switch (operator) { + case "-->" -> Precedence.IMPLICATION; + case "||" -> Precedence.OR; + case "&&" -> Precedence.AND; + case "==", "!=", ">=", ">", "<=", "<" -> Precedence.COMPARISON; + case "+", "-" -> Precedence.ADDITIVE; + case "*", "/", "%" -> Precedence.MULTIPLICATIVE; + default -> Precedence.ATOMIC; + }; + } + + private boolean isAssociative(String operator) { + return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*"); + } + + @Override + public String visitAliasInvocation(AliasInvocation alias) { + return alias.getName() + "(" + alias.getArgs().stream().map(this::renderChild).collect(Collectors.joining(", ")) + + ")"; + } + + @Override + public String visitBinaryExpression(BinaryExpression exp) { + return renderOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " " + + renderRightOperand(exp, exp.getSecondOperand()); + } + + @Override + public String visitFunctionInvocation(FunctionInvocation fun) { + return Utils.getSimpleName(fun.getName()) + "(" + + fun.getArgs().stream().map(this::renderChild).collect(Collectors.joining(",")) + ")"; + } + + @Override + public String visitGroupExpression(GroupExpression exp) { + return "(" + render(exp.getExpression()) + ")"; + } + + @Override + public String visitIte(Ite ite) { + return renderConditionOperand(ite.getCondition()) + " ? " + renderConditionOperand(ite.getThen()) + " : " + + renderOperand(ite, ite.getElse()); + } + + @Override + public String visitLiteralInt(LiteralInt lit) { + return Integer.toString(lit.getValue()); + } + + @Override + public String visitLiteralLong(LiteralLong lit) { + return Long.toString(lit.getValue()); + } + + @Override + public String visitLiteralBoolean(LiteralBoolean lit) { + return Boolean.toString(lit.value); + } + + @Override + public String visitLiteralChar(LiteralChar lit) { + return "'" + lit.getValue() + "'"; + } + + @Override + public String visitLiteralReal(LiteralReal lit) { + return Double.toString(lit.getValue()); + } + + @Override + public String visitLiteralString(LiteralString lit) { + return lit.toString(); + } + + @Override + public String visitUnaryExpression(UnaryExpression exp) { + return exp.getOp() + renderOperand(exp, exp.getExpression()); + } + + @Override + public String visitVar(Var var) { + return var.getName(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index d9d53731..c24e6bba 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -2,8 +2,6 @@ import java.util.ArrayList; import java.util.List; -import java.util.stream.Collectors; - import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; @@ -37,8 +35,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { @Override public String toString() { - return Utils.getSimpleName(name) + "(" - + getArgs().stream().map(Expression::toString).collect(Collectors.joining(",")) + ")"; + return ExpressionPrinter.print(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java index 3567afd8..4e697d7a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java @@ -21,12 +21,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { } public String toString() { - return getExpression().toString(); - } - - @Override - protected Precedence getPrecedence() { - return getExpression().getPrecedence(); + return ExpressionPrinter.print(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java index 08542186..d6b178d1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java @@ -30,21 +30,9 @@ public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitIte(this); } - @Override - protected Precedence getPrecedence() { - return Precedence.TERNARY; - } - - private String formatCondition(Expression operand) { - if (operand instanceof Ite) - return parenthesize(operand); - - return formatChild(operand); - } - @Override public String toString() { - return formatCondition(getCondition()) + " ? " + formatCondition(getThen()) + " : " + formatChild(getElse()); + return ExpressionPrinter.print(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java index 1d8d2842..71268537 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java @@ -18,6 +18,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitLiteralString(this); } + @Override public String toString() { return value; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java index f6af6eae..0bb65839 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java @@ -27,14 +27,9 @@ public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitUnaryExpression(this); } - @Override - protected Precedence getPrecedence() { - return Precedence.PREFIX; - } - @Override public String toString() { - return op + formatChild(getExpression()); + return ExpressionPrinter.print(this); } @Override diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java index ee20813a..9a64b1cb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java @@ -18,6 +18,8 @@ void printsUnaryWithParenthesesForCompoundOperands() { assertEquals("x > 0", comparison.toString()); assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toString()); + assertEquals("-(-x)", + new UnaryExpression("-", new GroupExpression(new UnaryExpression("-", new Var("x")))).toString()); } @Test @@ -33,6 +35,16 @@ void printsBinaryExpressionsWithOperatorPrecedence() { assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toString()); } + @Test + void preservesExplicitGroupingOnRightHandSide() { + 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).toString()); + assertEquals("x == (1 > 0)", new BinaryExpression(new Var("x"), "==", groupedComparison).toString()); + } + @Test void printsLogicalExpressionsWithNeededParentheses() { Expression andExpression = new BinaryExpression(new Var("a"), "&&", new Var("b")); @@ -58,6 +70,9 @@ void printsTernaryExpressionsWithNeededParentheses() { 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")).toString()); assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toString()); + assertEquals("(a ? b : c) ? d : e", new Ite(new GroupExpression(ite), new Var("d"), new Var("e")).toString()); + assertEquals("a ? b : (c ? d : e)", + new Ite(new Var("a"), new Var("b"), new GroupExpression(nestedElse)).toString()); assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toString()); } } From a08e169f8cb388572a9c2571266421cb7e630fad Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 31 Mar 2026 21:50:57 +0100 Subject: [PATCH 03/13] Code Refactoring --- .../diagnostics/errors/RefinementError.java | 13 ++-- .../errors/StateRefinementError.java | 9 ++- .../rj_language/ast/AliasInvocation.java | 4 +- .../rj_language/ast/BinaryExpression.java | 2 +- .../rj_language/ast/Expression.java | 5 ++ .../rj_language/ast/FunctionInvocation.java | 5 +- .../rj_language/ast/GroupExpression.java | 2 +- .../java/liquidjava/rj_language/ast/Ite.java | 2 +- .../rj_language/ast/UnaryExpression.java | 2 +- .../ExpressionPrinter.java | 25 +++++-- .../prettyprinting}/VariableFormatter.java | 21 +----- .../derivation_node/ValDerivationNode.java | 6 +- .../derivation_node/VarDerivationNode.java | 18 ----- .../ast/ExpressionPrinterTest.java | 66 +++++++++++-------- .../opt/ExpressionSimplifierTest.java | 6 +- .../VariableFormatterTest.java | 31 --------- 16 files changed, 92 insertions(+), 125 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/{ => prettyprinting}/ExpressionPrinter.java (85%) rename liquidjava-verifier/src/main/java/liquidjava/{utils => rj_language/ast/prettyprinting}/VariableFormatter.java (64%) delete mode 100644 liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 39a81d92..6ba1369b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -5,9 +5,10 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.TranslationTable; +import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.ast.prettyprinting.VariableFormatter; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.smt.Counterexample; -import liquidjava.utils.VariableFormatter; import spoon.reflect.cu.SourcePosition; /** @@ -23,10 +24,8 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, TranslationTable translationTable, Counterexample counterexample, String customMessage) { - super("Refinement Error", - String.format("%s is not a subtype of %s", VariableFormatter.formatText(found.getValue().toString()), - VariableFormatter.formatText(expected.getValue().toString())), - position, translationTable, customMessage); + super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue().toDisplayString(), + expected.getValue().toDisplayString()), position, translationTable, customMessage); this.expected = expected; this.found = found; this.counterexample = counterexample; @@ -50,11 +49,11 @@ public String getCounterExampleString() { // only include variables that appear in the found value .filter(a -> foundVarNames.contains(a.first())) // format as "var == value" - .map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second()) + .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) // join with "&&" .collect(Collectors.joining(" && ")); - String foundString = VariableFormatter.formatText(found.getValue().toString()); + String foundString = found.getValue().toDisplayString(); if (counterexampleString.isEmpty() || counterexampleString.equals(foundString)) return null; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 1e83a2bc..e16d3a18 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -2,7 +2,6 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; -import liquidjava.utils.VariableFormatter; import spoon.reflect.cu.SourcePosition; /** @@ -17,11 +16,11 @@ public class StateRefinementError extends LJError { public StateRefinementError(SourcePosition position, Expression expected, Expression found, TranslationTable translationTable, String customMessage) { - super("State Refinement Error", String.format("Expected state %s but found %s", - VariableFormatter.formatText(expected.toString()), VariableFormatter.formatText(found.toString())), + super("State Refinement Error", + String.format("Expected state %s but found %s", expected.toDisplayString(), found.toDisplayString()), position, translationTable, customMessage); - this.expected = VariableFormatter.formatText(expected.toString()); - this.found = VariableFormatter.formatText(found.toString()); + this.expected = expected.toDisplayString(); + this.found = found.toDisplayString(); } public String getExpected() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java index 54621a86..2c02734f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java @@ -2,6 +2,8 @@ import java.util.ArrayList; import java.util.List; +import java.util.stream.Collectors; + import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; @@ -29,7 +31,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { @Override public String toString() { - return ExpressionPrinter.print(this); + return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")) + ")"; } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index d08850f5..148c0ee8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java @@ -42,7 +42,7 @@ public boolean isArithmeticOperation() { @Override public String toString() { - return ExpressionPrinter.print(this); + return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString(); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 3859c530..9acdf6e3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -11,6 +11,7 @@ import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.AliasDTO; +import liquidjava.rj_language.ast.prettyprinting.ExpressionPrinter; import liquidjava.rj_language.ast.typing.TypeInfer; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; @@ -36,6 +37,10 @@ public abstract class Expression { public abstract String toString(); + public String toDisplayString() { + return ExpressionPrinter.print(this); + } + List children = new ArrayList<>(); public void addChild(Expression e) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index c24e6bba..d9d53731 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -2,6 +2,8 @@ import java.util.ArrayList; import java.util.List; +import java.util.stream.Collectors; + import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; @@ -35,7 +37,8 @@ public T accept(ExpressionVisitor visitor) throws LJError { @Override public String toString() { - return ExpressionPrinter.print(this); + return Utils.getSimpleName(name) + "(" + + getArgs().stream().map(Expression::toString).collect(Collectors.joining(",")) + ")"; } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java index 4e697d7a..4597a157 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java @@ -21,7 +21,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { } public String toString() { - return ExpressionPrinter.print(this); + return getExpression().toString(); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java index d6b178d1..cf95b730 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java @@ -32,7 +32,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { @Override public String toString() { - return ExpressionPrinter.print(this); + return getCondition().toString() + " ? " + getThen().toString() + " : " + getElse().toString(); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java index 0bb65839..4ffbc2d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java @@ -29,7 +29,7 @@ public T accept(ExpressionVisitor visitor) throws LJError { @Override public String toString() { - return ExpressionPrinter.print(this); + return op + getExpression().toString(); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/ExpressionPrinter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java similarity index 85% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/ExpressionPrinter.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java index 047648b5..e7db1adf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/ExpressionPrinter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java @@ -1,8 +1,21 @@ -package liquidjava.rj_language.ast; +package liquidjava.rj_language.ast.prettyprinting; import java.util.stream.Collectors; -import liquidjava.diagnostics.errors.LJError; +import liquidjava.rj_language.ast.AliasInvocation; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralChar; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.LiteralString; +import liquidjava.rj_language.ast.UnaryExpression; +import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; @@ -136,17 +149,17 @@ public String visitLiteralLong(LiteralLong lit) { @Override public String visitLiteralBoolean(LiteralBoolean lit) { - return Boolean.toString(lit.value); + return lit.toString(); } @Override public String visitLiteralChar(LiteralChar lit) { - return "'" + lit.getValue() + "'"; + return lit.toString(); } @Override public String visitLiteralReal(LiteralReal lit) { - return Double.toString(lit.getValue()); + return lit.toString(); } @Override @@ -161,6 +174,6 @@ public String visitUnaryExpression(UnaryExpression exp) { @Override public String visitVar(Var var) { - return var.getName(); + return VariableFormatter.format(var.getName()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java similarity index 64% rename from liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java index 0629fbff..7b43ab67 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java @@ -1,14 +1,13 @@ -package liquidjava.utils; +package liquidjava.rj_language.ast.prettyprinting; import java.util.regex.Matcher; import java.util.regex.Pattern; public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); - private static final Pattern INSTANCE_VAR_TEXT_PATTERN = Pattern.compile("#[^\\s,;:()\\[\\]{}]+_[0-9]+"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; - public static String formatVariable(String name) { + public static String format(String name) { if (name == null) return null; @@ -22,20 +21,6 @@ public static String formatVariable(String name) { return prefix + baseName + toSuperscript(counter); } - public static String formatText(String text) { - if (text == null) - return null; - - Matcher textMatcher = INSTANCE_VAR_TEXT_PATTERN.matcher(text); - StringBuilder sb = new StringBuilder(); - while (textMatcher.find()) { - String token = textMatcher.group(); - textMatcher.appendReplacement(sb, Matcher.quoteReplacement(formatVariable(token))); - } - textMatcher.appendTail(sb); - return sb.toString(); - } - private static String toSuperscript(String number) { StringBuilder sb = new StringBuilder(number.length()); for (char c : number.toCharArray()) { @@ -50,4 +35,4 @@ private static String toSuperscript(String number) { private static boolean isSpecialIdentifier(String id) { return id.equals("fresh") || id.equals("ret"); } -} +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java index be9afb00..02367ee7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -14,8 +14,6 @@ import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; -import liquidjava.rj_language.ast.Var; -import liquidjava.utils.VariableFormatter; public class ValDerivationNode extends DerivationNode { @@ -50,9 +48,7 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo return new JsonPrimitive(v.getValue()); if (exp instanceof LiteralBoolean v) return new JsonPrimitive(v.isBooleanTrue()); - if (exp instanceof Var v) - return new JsonPrimitive(VariableFormatter.formatVariable(v.getName())); - return new JsonPrimitive(VariableFormatter.formatText(exp.toString())); + return new JsonPrimitive(exp.toDisplayString()); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java index a8dce4c5..c134a44e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java @@ -1,18 +1,7 @@ package liquidjava.rj_language.opt.derivation_node; -import java.lang.reflect.Type; - -import com.google.gson.JsonElement; -import com.google.gson.JsonPrimitive; -import com.google.gson.JsonSerializationContext; -import com.google.gson.JsonSerializer; -import com.google.gson.annotations.JsonAdapter; - -import liquidjava.utils.VariableFormatter; - public class VarDerivationNode extends DerivationNode { - @JsonAdapter(VariableNameSerializer.class) private final String var; private final DerivationNode origin; @@ -33,11 +22,4 @@ public String getVar() { public DerivationNode getOrigin() { return origin; } - - private static class VariableNameSerializer implements JsonSerializer { - @Override - public JsonElement serialize(String src, Type typeOfSrc, JsonSerializationContext context) { - return new JsonPrimitive(VariableFormatter.formatVariable(src)); - } - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java index 9a64b1cb..2e2e2a92 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java @@ -1,25 +1,37 @@ package liquidjava.rj_language.ast; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; import org.junit.jupiter.api.Test; class ExpressionPrinterTest { @Test void printsUnaryWithoutExtraParenthesesForAtoms() { - assertEquals("!x", new UnaryExpression("!", new Var("x")).toString()); - assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toString()); + assertEquals("!x", new UnaryExpression("!", new Var("x")).toDisplayString()); + assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toDisplayString()); + } + + @Test + void formatsInternalVariablesWithSuperscripts() { + 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()); } @Test void printsUnaryWithParenthesesForCompoundOperands() { Expression comparison = new BinaryExpression(new Var("x"), ">", new LiteralInt(0)); - assertEquals("x > 0", comparison.toString()); - assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toString()); - assertEquals("-(-x)", - new UnaryExpression("-", new GroupExpression(new UnaryExpression("-", new Var("x")))).toString()); + assertEquals("x > 0", comparison.toDisplayString()); + assertEquals("!(x > 0)", new UnaryExpression("!", comparison).toDisplayString()); + assertEquals("-(-x)", new UnaryExpression("-", new GroupExpression(new UnaryExpression("-", new Var("x")))) + .toDisplayString()); } @Test @@ -27,12 +39,12 @@ void printsBinaryExpressionsWithOperatorPrecedence() { 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")).toString()); - assertEquals("a * (a + b)", new BinaryExpression(new Var("a"), "*", sum).toString()); - assertEquals("a + b * c", new BinaryExpression(new Var("a"), "+", product).toString()); - assertEquals("a - (a + b)", new BinaryExpression(new Var("a"), "-", sum).toString()); - assertEquals("a + b + c", new BinaryExpression(sum, "+", new Var("c")).toString()); - assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toString()); + 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 @@ -41,8 +53,8 @@ void preservesExplicitGroupingOnRightHandSide() { Expression groupedComparison = new GroupExpression( new BinaryExpression(new LiteralInt(1), ">", new LiteralInt(0))); - assertEquals("a - (b + c)", new BinaryExpression(new Var("a"), "-", groupedSum).toString()); - assertEquals("x == (1 > 0)", new BinaryExpression(new Var("x"), "==", groupedComparison).toString()); + assertEquals("a - (b + c)", new BinaryExpression(new Var("a"), "-", groupedSum).toDisplayString()); + assertEquals("x == (1 > 0)", new BinaryExpression(new Var("x"), "==", groupedComparison).toDisplayString()); } @Test @@ -51,13 +63,13 @@ void printsLogicalExpressionsWithNeededParentheses() { 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")).toString()); - assertEquals("a && (b || c)", new BinaryExpression(new Var("a"), "&&", orExpression).toString()); - assertEquals("a --> (b --> c)", new BinaryExpression(new Var("a"), "-->", implication).toString()); - assertEquals("a && b && c", new BinaryExpression(andExpression, "&&", new Var("c")).toString()); + 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")) - .toString()); + .toDisplayString()); } @Test @@ -65,14 +77,16 @@ void printsTernaryExpressionsWithNeededParentheses() { 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")).toString()); - assertEquals("(a ? b : c) ? d : e", new Ite(ite, new Var("d"), new Var("e")).toString()); + 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")).toString()); - assertEquals("a ? b : c ? d : e", new Ite(new Var("a"), new Var("b"), nestedElse).toString()); - assertEquals("(a ? b : c) ? d : e", new Ite(new GroupExpression(ite), new Var("d"), new Var("e")).toString()); + 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)).toString()); - assertEquals("a ? b : c", new Ite(new Var("a"), new Var("b"), new Var("c")).toString()); + 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()); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index 845b85f9..de2c553a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -603,7 +603,7 @@ void testShouldUnwrapBooleanInEquality() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == (1 > 0)", result.getValue().toString(), + assertEquals("x == (1 > 0)", result.getValue().toDisplayString(), "Boolean in equality should be unwrapped to show the original comparison"); } @@ -631,7 +631,7 @@ void testShouldUnwrapBooleanInEqualityWithPropagation() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == (3 > 1)", result.getValue().toString(), + assertEquals("x == (3 > 1)", result.getValue().toDisplayString(), "Boolean in equality should be unwrapped after propagation"); } @@ -685,7 +685,7 @@ void testShouldUnwrapNestedBooleanInEquality() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == (8 > 10)", result.getValue().toString(), + assertEquals("x == (8 > 10)", result.getValue().toDisplayString(), "Boolean in equality should be unwrapped to show the computed comparison"); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java deleted file mode 100644 index 98e52ea0..00000000 --- a/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java +++ /dev/null @@ -1,31 +0,0 @@ -package liquidjava.variable_formatter; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import liquidjava.rj_language.ast.Var; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; -import liquidjava.utils.VariableFormatter; - -import org.junit.jupiter.api.Test; - -class VariableFormatterTest { - - @Test - void testInstanceVariableDisplayNameFormatting() { - assertEquals("x", VariableFormatter.formatVariable("x")); - assertEquals("x²", VariableFormatter.formatVariable("#x_2")); - assertEquals("#fresh¹²", VariableFormatter.formatVariable("#fresh_12")); - assertEquals("#ret³", VariableFormatter.formatVariable("#ret_3")); - assertEquals("this#Class", VariableFormatter.formatVariable("this#Class")); - } - - @Test - void testDerivationNodeUsesSuperscriptNotation() { - ValDerivationNode node = new ValDerivationNode(new Var("#x_2"), new VarDerivationNode("#x_2")); - String serialized = node.toString(); - assertTrue(serialized.contains("\"value\": \"x²\""), "Expected derivation value to use superscript notation"); - assertTrue(serialized.contains("\"var\": \"x²\""), "Expected derivation origin to use superscript notation"); - } -} From 516f795e4340e0b62f0a7f025d97db256cfca902 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 31 Mar 2026 23:26:03 +0100 Subject: [PATCH 04/13] Add Javadocs --- .../rj_language/ast/prettyprinting/ExpressionPrinter.java | 3 +++ .../rj_language/ast/prettyprinting/VariableFormatter.java | 3 +++ 2 files changed, 6 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java index e7db1adf..985d8a10 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java @@ -19,6 +19,9 @@ import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; +/** + * Pretty printer for expressions that preserves only the parentheses required by precedence and associativty + */ public class ExpressionPrinter implements ExpressionVisitor { private enum Precedence { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java index 7b43ab67..38477590 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java @@ -3,6 +3,9 @@ import java.util.regex.Matcher; import java.util.regex.Pattern; +/** + * Formats internal variable names into a cleaner display representation using superscript notation + */ public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; From 2d2fc97a0ff9397314824a9ab5f0cef32bbb8775 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 31 Mar 2026 23:26:45 +0100 Subject: [PATCH 05/13] Update Javadoc --- .../rj_language/ast/prettyprinting/ExpressionPrinter.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java index 985d8a10..ca99f350 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java @@ -20,7 +20,8 @@ import liquidjava.utils.Utils; /** - * Pretty printer for expressions that preserves only the parentheses required by precedence and associativty + * Pretty printer for expressions that preserves only the parentheses required by precedence and associativity rules + * Also formats variable names using {@link VariableFormatter} */ public class ExpressionPrinter implements ExpressionVisitor { From f455e9705032728919350d235f88f1eac3837cd8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 12:02:32 +0100 Subject: [PATCH 06/13] Simplify ExpressionPrinter --- .../ast/prettyprinting/ExpressionPrinter.java | 32 +++++++++---------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java index ca99f350..030bba14 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java @@ -1,5 +1,6 @@ package liquidjava.rj_language.ast.prettyprinting; +import java.util.List; import java.util.stream.Collectors; import liquidjava.rj_language.ast.AliasInvocation; @@ -41,34 +42,28 @@ private String render(Expression expression) { return expression.accept(this); } - private String renderChild(Expression child) { + private String renderWithOptionalParentheses(Expression child, boolean shouldWrap) { + if (shouldWrap) + return "(" + render(child) + ")"; if (child instanceof GroupExpression group) return "(" + render(group.getExpression()) + ")"; return render(child); } private String renderOperand(Expression parent, Expression child) { - if (needsParentheses(parent, child)) - return "(" + render(child) + ")"; - return renderChild(child); + return renderWithOptionalParentheses(child, needsParentheses(parent, child)); } private String renderRightOperand(BinaryExpression parent, Expression child) { - if (needsRightParentheses(parent, child)) - return "(" + render(child) + ")"; - return renderChild(child); + return renderWithOptionalParentheses(child, needsRightParentheses(parent, child)); } private String renderConditionOperand(Expression child) { - if (child instanceof Ite) - return "(" + render(child) + ")"; - return renderChild(child); + return renderWithOptionalParentheses(child, child instanceof Ite); } private boolean needsParentheses(Expression parent, Expression child) { - if (precedence(child).isLowerThan(precedence(parent))) - return true; - return false; + return precedence(child).isLowerThan(precedence(parent)); } private boolean needsRightParentheses(BinaryExpression parent, Expression child) { @@ -114,8 +109,7 @@ private boolean isAssociative(String operator) { @Override public String visitAliasInvocation(AliasInvocation alias) { - return alias.getName() + "(" + alias.getArgs().stream().map(this::renderChild).collect(Collectors.joining(", ")) - + ")"; + return alias.getName() + "(" + renderArguments(alias.getArgs(), ", ") + ")"; } @Override @@ -126,8 +120,7 @@ public String visitBinaryExpression(BinaryExpression exp) { @Override public String visitFunctionInvocation(FunctionInvocation fun) { - return Utils.getSimpleName(fun.getName()) + "(" - + fun.getArgs().stream().map(this::renderChild).collect(Collectors.joining(",")) + ")"; + return Utils.getSimpleName(fun.getName()) + "(" + renderArguments(fun.getArgs(), ",") + ")"; } @Override @@ -180,4 +173,9 @@ public String visitUnaryExpression(UnaryExpression exp) { public String visitVar(Var var) { return VariableFormatter.format(var.getName()); } + + private String renderArguments(List args, String separator) { + return args.stream().map(expression -> renderWithOptionalParentheses(expression, false)) + .collect(Collectors.joining(separator)); + } } From 3db15e9fd49ea614620f17767cbaf617d8a15313 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 12:10:07 +0100 Subject: [PATCH 07/13] Add ExpressionPrecendence --- .../prettyprinting/ExpressionPrecedence.java | 39 +++++++++++++++ .../ast/prettyprinting/ExpressionPrinter.java | 50 ++++--------------- 2 files changed, 48 insertions(+), 41 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrecedence.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrecedence.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrecedence.java new file mode 100644 index 00000000..61447301 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrecedence.java @@ -0,0 +1,39 @@ +package liquidjava.rj_language.ast.prettyprinting; + +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.UnaryExpression; + +public enum ExpressionPrecedence { + TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, PREFIX, ATOMIC; + + public boolean isLowerThan(ExpressionPrecedence other) { + return ordinal() < other.ordinal(); + } + + public static ExpressionPrecedence of(Expression expression) { + if (expression instanceof GroupExpression group) + return of(group.getExpression()); + if (expression instanceof Ite) + return TERNARY; + if (expression instanceof UnaryExpression) + return PREFIX; + if (expression instanceof BinaryExpression binary) + return of(binary.getOperator()); + return ATOMIC; + } + + public static ExpressionPrecedence of(String operator) { + return switch (operator) { + case "-->" -> IMPLICATION; + case "||" -> OR; + case "&&" -> AND; + case "==", "!=", ">=", ">", "<=", "<" -> COMPARISON; + case "+", "-" -> ADDITIVE; + case "*", "/", "%" -> MULTIPLICATIVE; + default -> ATOMIC; + }; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java index 030bba14..ccbbb8b0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java @@ -26,14 +26,6 @@ */ public class ExpressionPrinter implements ExpressionVisitor { - private enum Precedence { - TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, PREFIX, ATOMIC; - - private boolean isLowerThan(Precedence other) { - return ordinal() < other.ordinal(); - } - } - public static String print(Expression expression) { return new ExpressionPrinter().render(expression); } @@ -62,15 +54,20 @@ private String renderConditionOperand(Expression child) { return renderWithOptionalParentheses(child, child instanceof Ite); } + private String renderArguments(List args) { + return args.stream().map(expression -> renderWithOptionalParentheses(expression, false)) + .collect(Collectors.joining(", ")); + } + private boolean needsParentheses(Expression parent, Expression child) { - return precedence(child).isLowerThan(precedence(parent)); + return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent)); } private boolean needsRightParentheses(BinaryExpression parent, Expression child) { if (needsParentheses(parent, child)) return true; - if (precedence(child) != precedence(parent)) + if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent)) return false; if (child instanceof BinaryExpression right) @@ -79,37 +76,13 @@ private boolean needsRightParentheses(BinaryExpression parent, Expression child) return false; } - private Precedence precedence(Expression expression) { - if (expression instanceof GroupExpression group) - return precedence(group.getExpression()); - if (expression instanceof Ite) - return Precedence.TERNARY; - if (expression instanceof UnaryExpression) - return Precedence.PREFIX; - if (expression instanceof BinaryExpression binary) - return precedence(binary.getOperator()); - return Precedence.ATOMIC; - } - - private Precedence precedence(String operator) { - return switch (operator) { - case "-->" -> Precedence.IMPLICATION; - case "||" -> Precedence.OR; - case "&&" -> Precedence.AND; - case "==", "!=", ">=", ">", "<=", "<" -> Precedence.COMPARISON; - case "+", "-" -> Precedence.ADDITIVE; - case "*", "/", "%" -> Precedence.MULTIPLICATIVE; - default -> Precedence.ATOMIC; - }; - } - private boolean isAssociative(String operator) { return operator.equals("&&") || operator.equals("||") || operator.equals("+") || operator.equals("*"); } @Override public String visitAliasInvocation(AliasInvocation alias) { - return alias.getName() + "(" + renderArguments(alias.getArgs(), ", ") + ")"; + return alias.getName() + "(" + renderArguments(alias.getArgs()) + ")"; } @Override @@ -120,7 +93,7 @@ public String visitBinaryExpression(BinaryExpression exp) { @Override public String visitFunctionInvocation(FunctionInvocation fun) { - return Utils.getSimpleName(fun.getName()) + "(" + renderArguments(fun.getArgs(), ",") + ")"; + return Utils.getSimpleName(fun.getName()) + "(" + renderArguments(fun.getArgs()) + ")"; } @Override @@ -173,9 +146,4 @@ public String visitUnaryExpression(UnaryExpression exp) { public String visitVar(Var var) { return VariableFormatter.format(var.getName()); } - - private String renderArguments(List args, String separator) { - return args.stream().map(expression -> renderWithOptionalParentheses(expression, false)) - .collect(Collectors.joining(separator)); - } } From 1a128375205ee070adffb9a3ee45ecb180636dd6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 13:51:39 +0100 Subject: [PATCH 08/13] Renaming --- .../diagnostics/errors/RefinementError.java | 2 +- .../rj_language/ast/Expression.java | 4 +- .../ExpressionFormatter.java} | 52 +++++++++---------- .../ExpressionPrecedence.java | 2 +- .../VariableFormatter.java | 2 +- 5 files changed, 31 insertions(+), 31 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/{prettyprinting/ExpressionPrinter.java => formatter/ExpressionFormatter.java} (65%) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/{prettyprinting => formatter}/ExpressionPrecedence.java (96%) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/{prettyprinting => formatter}/VariableFormatter.java (96%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 6ba1369b..3f097d4c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -6,7 +6,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Var; -import liquidjava.rj_language.ast.prettyprinting.VariableFormatter; +import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.smt.Counterexample; import spoon.reflect.cu.SourcePosition; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 9acdf6e3..e283790b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -11,7 +11,7 @@ import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.AliasDTO; -import liquidjava.rj_language.ast.prettyprinting.ExpressionPrinter; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; import liquidjava.rj_language.ast.typing.TypeInfer; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; @@ -38,7 +38,7 @@ public abstract class Expression { public abstract String toString(); public String toDisplayString() { - return ExpressionPrinter.print(this); + return ExpressionFormatter.format(this); } List children = new ArrayList<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java similarity index 65% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index ccbbb8b0..c24e18f4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrinter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -1,4 +1,4 @@ -package liquidjava.rj_language.ast.prettyprinting; +package liquidjava.rj_language.ast.formatter; import java.util.List; import java.util.stream.Collectors; @@ -21,41 +21,41 @@ import liquidjava.utils.Utils; /** - * Pretty printer for expressions that preserves only the parentheses required by precedence and associativity rules + * Formatter expressions that preserves only the parentheses required by precedence and associativity rules * Also formats variable names using {@link VariableFormatter} */ -public class ExpressionPrinter implements ExpressionVisitor { +public class ExpressionFormatter implements ExpressionVisitor { - public static String print(Expression expression) { - return new ExpressionPrinter().render(expression); + public static String format(Expression expression) { + return new ExpressionFormatter().formatExpression(expression); } - private String render(Expression expression) { + private String formatExpression(Expression expression) { return expression.accept(this); } - private String renderWithOptionalParentheses(Expression child, boolean shouldWrap) { + private String formatParentheses(Expression child, boolean shouldWrap) { if (shouldWrap) - return "(" + render(child) + ")"; + return "(" + formatExpression(child) + ")"; if (child instanceof GroupExpression group) - return "(" + render(group.getExpression()) + ")"; - return render(child); + return "(" + formatExpression(group.getExpression()) + ")"; + return formatExpression(child); } - private String renderOperand(Expression parent, Expression child) { - return renderWithOptionalParentheses(child, needsParentheses(parent, child)); + private String formatOperand(Expression parent, Expression child) { + return formatParentheses(child, needsParentheses(parent, child)); } - private String renderRightOperand(BinaryExpression parent, Expression child) { - return renderWithOptionalParentheses(child, needsRightParentheses(parent, child)); + private String formatRightOperand(BinaryExpression parent, Expression child) { + return formatParentheses(child, needsRightParentheses(parent, child)); } - private String renderConditionOperand(Expression child) { - return renderWithOptionalParentheses(child, child instanceof Ite); + private String formatCondition(Expression child) { + return formatParentheses(child, child instanceof Ite); } - private String renderArguments(List args) { - return args.stream().map(expression -> renderWithOptionalParentheses(expression, false)) + private String formatArguments(List args) { + return args.stream().map(expression -> formatParentheses(expression, false)) .collect(Collectors.joining(", ")); } @@ -82,29 +82,29 @@ private boolean isAssociative(String operator) { @Override public String visitAliasInvocation(AliasInvocation alias) { - return alias.getName() + "(" + renderArguments(alias.getArgs()) + ")"; + return alias.getName() + "(" + formatArguments(alias.getArgs()) + ")"; } @Override public String visitBinaryExpression(BinaryExpression exp) { - return renderOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " " - + renderRightOperand(exp, exp.getSecondOperand()); + return formatOperand(exp, exp.getFirstOperand()) + " " + exp.getOperator() + " " + + formatRightOperand(exp, exp.getSecondOperand()); } @Override public String visitFunctionInvocation(FunctionInvocation fun) { - return Utils.getSimpleName(fun.getName()) + "(" + renderArguments(fun.getArgs()) + ")"; + return Utils.getSimpleName(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")"; } @Override public String visitGroupExpression(GroupExpression exp) { - return "(" + render(exp.getExpression()) + ")"; + return "(" + formatExpression(exp.getExpression()) + ")"; } @Override public String visitIte(Ite ite) { - return renderConditionOperand(ite.getCondition()) + " ? " + renderConditionOperand(ite.getThen()) + " : " - + renderOperand(ite, ite.getElse()); + return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : " + + formatOperand(ite, ite.getElse()); } @Override @@ -139,7 +139,7 @@ public String visitLiteralString(LiteralString lit) { @Override public String visitUnaryExpression(UnaryExpression exp) { - return exp.getOp() + renderOperand(exp, exp.getExpression()); + return exp.getOp() + formatOperand(exp, exp.getExpression()); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrecedence.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java similarity index 96% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrecedence.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java index 61447301..1c330dc9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/ExpressionPrecedence.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java @@ -1,4 +1,4 @@ -package liquidjava.rj_language.ast.prettyprinting; +package liquidjava.rj_language.ast.formatter; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java similarity index 96% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 38477590..625aa619 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/prettyprinting/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java @@ -1,4 +1,4 @@ -package liquidjava.rj_language.ast.prettyprinting; +package liquidjava.rj_language.ast.formatter; import java.util.regex.Matcher; import java.util.regex.Pattern; From 76041fe24606b832e8442d7e9219224e12c79456 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 13:53:37 +0100 Subject: [PATCH 09/13] Formatting --- .../rj_language/ast/formatter/ExpressionFormatter.java | 7 +++---- 1 file changed, 3 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 c24e18f4..0a2f23aa 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 @@ -21,8 +21,8 @@ import liquidjava.utils.Utils; /** - * Formatter expressions that preserves only the parentheses required by precedence and associativity rules - * Also formats variable names using {@link VariableFormatter} + * Formatter for expressions that only adds parentheses when required by precedence and associativity rules and formats + * variable names using {@link VariableFormatter} */ public class ExpressionFormatter implements ExpressionVisitor { @@ -55,8 +55,7 @@ private String formatCondition(Expression child) { } private String formatArguments(List args) { - return args.stream().map(expression -> formatParentheses(expression, false)) - .collect(Collectors.joining(", ")); + return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", ")); } private boolean needsParentheses(Expression parent, Expression child) { From 51024ef46ad341bcfc533991b8bc9aa8fd680c0f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 13:54:23 +0100 Subject: [PATCH 10/13] Rename Test Class --- ...ressionPrinterTest.java => ExpressionFormatterTest.java} | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) rename liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/{ExpressionPrinterTest.java => ExpressionFormatterTest.java} (95%) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java similarity index 95% rename from liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java rename to liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java index 2e2e2a92..9ff50bc1 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionPrinterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -1,13 +1,9 @@ package liquidjava.rj_language.ast; import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; import org.junit.jupiter.api.Test; -class ExpressionPrinterTest { +class ExpressionFormatterTest { @Test void printsUnaryWithoutExtraParenthesesForAtoms() { From 774a4ad34131c7d73751e3b22d64400f9c658830 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 14:05:27 +0100 Subject: [PATCH 11/13] Add Format Predicate Overload --- .../rj_language/ast/formatter/ExpressionFormatter.java | 5 +++++ 1 file changed, 5 insertions(+) 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 0a2f23aa..668f72d0 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 @@ -3,6 +3,7 @@ import java.util.List; import java.util.stream.Collectors; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; @@ -26,6 +27,10 @@ */ public class ExpressionFormatter implements ExpressionVisitor { + public static String format(Predicate predicate) { + return format(predicate.getExpression()); + } + public static String format(Expression expression) { return new ExpressionFormatter().formatExpression(expression); } From 7240cb2aec9455ea282142e864b092d0b3c30451 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 14:14:21 +0100 Subject: [PATCH 12/13] Minor Change --- .../rj_language/ast/formatter/ExpressionPrecedence.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java index 1c330dc9..fbaa95cb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java @@ -7,7 +7,7 @@ import liquidjava.rj_language.ast.UnaryExpression; public enum ExpressionPrecedence { - TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, PREFIX, ATOMIC; + TERNARY, IMPLICATION, OR, AND, COMPARISON, ADDITIVE, MULTIPLICATIVE, UNARY, ATOMIC; public boolean isLowerThan(ExpressionPrecedence other) { return ordinal() < other.ordinal(); @@ -19,7 +19,7 @@ public static ExpressionPrecedence of(Expression expression) { if (expression instanceof Ite) return TERNARY; if (expression instanceof UnaryExpression) - return PREFIX; + return UNARY; if (expression instanceof BinaryExpression binary) return of(binary.getOperator()); return ATOMIC; From 3b05d782e9ea9cc448ef3aed2ab7f7d306b40533 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 14:18:39 +0100 Subject: [PATCH 13/13] Rename Tests --- .../rj_language/ast/ExpressionFormatterTest.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 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 9ff50bc1..da8ce038 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 @@ -6,13 +6,13 @@ class ExpressionFormatterTest { @Test - void printsUnaryWithoutExtraParenthesesForAtoms() { + void formatsUnaryAtoms() { assertEquals("!x", new UnaryExpression("!", new Var("x")).toDisplayString()); assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(false)).toDisplayString()); } @Test - void formatsInternalVariablesWithSuperscripts() { + void formatsInternalVariables() { assertEquals("x", new Var("x").toDisplayString()); assertEquals("x²", new Var("#x_2").toDisplayString()); assertEquals("#fresh¹²", new Var("#fresh_12").toDisplayString()); @@ -21,7 +21,7 @@ void formatsInternalVariablesWithSuperscripts() { } @Test - void printsUnaryWithParenthesesForCompoundOperands() { + void formatsUnaryCompounds() { Expression comparison = new BinaryExpression(new Var("x"), ">", new LiteralInt(0)); assertEquals("x > 0", comparison.toDisplayString()); @@ -31,7 +31,7 @@ void printsUnaryWithParenthesesForCompoundOperands() { } @Test - void printsBinaryExpressionsWithOperatorPrecedence() { + void formatsBinaryPrecedence() { Expression sum = new BinaryExpression(new Var("a"), "+", new Var("b")); Expression product = new BinaryExpression(new Var("b"), "*", new Var("c")); @@ -44,7 +44,7 @@ void printsBinaryExpressionsWithOperatorPrecedence() { } @Test - void preservesExplicitGroupingOnRightHandSide() { + 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))); @@ -54,7 +54,7 @@ void preservesExplicitGroupingOnRightHandSide() { } @Test - void printsLogicalExpressionsWithNeededParentheses() { + 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")); @@ -69,7 +69,7 @@ void printsLogicalExpressionsWithNeededParentheses() { } @Test - void printsTernaryExpressionsWithNeededParentheses() { + 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"));