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..3f097d4c 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.formatter.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/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index a5112c8c..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 @@ -41,13 +41,13 @@ public boolean isArithmeticOperation() { } @Override - public T accept(ExpressionVisitor visitor) throws LJError { - return visitor.visitBinaryExpression(this); + public String toString() { + return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString(); } @Override - public String toString() { - return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString(); + 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..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,6 +11,7 @@ import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.AliasDTO; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; 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 ExpressionFormatter.format(this); + } + List children = new ArrayList<>(); public void addChild(Expression e) { 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/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java new file mode 100644 index 00000000..668f72d0 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -0,0 +1,153 @@ +package liquidjava.rj_language.ast.formatter; + +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; +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; + +/** + * 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 { + + public static String format(Predicate predicate) { + return format(predicate.getExpression()); + } + + public static String format(Expression expression) { + return new ExpressionFormatter().formatExpression(expression); + } + + private String formatExpression(Expression expression) { + return expression.accept(this); + } + + private String formatParentheses(Expression child, boolean shouldWrap) { + if (shouldWrap) + return "(" + formatExpression(child) + ")"; + if (child instanceof GroupExpression group) + return "(" + formatExpression(group.getExpression()) + ")"; + return formatExpression(child); + } + + 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 formatCondition(Expression child) { + return formatParentheses(child, child instanceof Ite); + } + + private String formatArguments(List args) { + return args.stream().map(expression -> formatParentheses(expression, false)).collect(Collectors.joining(", ")); + } + + private boolean needsParentheses(Expression parent, Expression child) { + return ExpressionPrecedence.of(child).isLowerThan(ExpressionPrecedence.of(parent)); + } + + private boolean needsRightParentheses(BinaryExpression parent, Expression child) { + if (needsParentheses(parent, child)) + return true; + + if (ExpressionPrecedence.of(child) != ExpressionPrecedence.of(parent)) + return false; + + if (child instanceof BinaryExpression right) + return !isAssociative(parent.getOperator()) || !parent.getOperator().equals(right.getOperator()); + + return false; + } + + private boolean isAssociative(String operator) { + return operator.equals("&&") || operator.equals("||") || operator.equals("+") || 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()); + } + + @Override + public String visitFunctionInvocation(FunctionInvocation fun) { + return Utils.getSimpleName(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")"; + } + + @Override + public String visitGroupExpression(GroupExpression exp) { + return "(" + formatExpression(exp.getExpression()) + ")"; + } + + @Override + public String visitIte(Ite ite) { + return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : " + + formatOperand(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 lit.toString(); + } + + @Override + public String visitLiteralChar(LiteralChar lit) { + return lit.toString(); + } + + @Override + public String visitLiteralReal(LiteralReal lit) { + return lit.toString(); + } + + @Override + public String visitLiteralString(LiteralString lit) { + return lit.toString(); + } + + @Override + public String visitUnaryExpression(UnaryExpression exp) { + return exp.getOp() + formatOperand(exp, exp.getExpression()); + } + + @Override + public String visitVar(Var var) { + return VariableFormatter.format(var.getName()); + } +} 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 new file mode 100644 index 00000000..fbaa95cb --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java @@ -0,0 +1,39 @@ +package liquidjava.rj_language.ast.formatter; + +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, UNARY, 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 UNARY; + 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/utils/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/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/formatter/VariableFormatter.java index 0629fbff..625aa619 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java @@ -1,14 +1,16 @@ -package liquidjava.utils; +package liquidjava.rj_language.ast.formatter; 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 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 +24,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 +38,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/ExpressionFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java new file mode 100644 index 00000000..da8ce038 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -0,0 +1,88 @@ +package liquidjava.rj_language.ast; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import org.junit.jupiter.api.Test; + +class ExpressionFormatterTest { + + @Test + void formatsUnaryAtoms() { + assertEquals("!x", new UnaryExpression("!", new Var("x")).toDisplayString()); + assertEquals("!false", new UnaryExpression("!", new LiteralBoolean(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()); + } + + @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()); + } + + @Test + void formatsBinaryPrecedence() { + Expression sum = new BinaryExpression(new Var("a"), "+", new Var("b")); + Expression product = new BinaryExpression(new Var("b"), "*", new Var("c")); + + assertEquals("(a + b) * c", new BinaryExpression(sum, "*", new Var("c")).toDisplayString()); + assertEquals("a * (a + b)", new BinaryExpression(new Var("a"), "*", sum).toDisplayString()); + assertEquals("a + b * c", new BinaryExpression(new Var("a"), "+", product).toDisplayString()); + assertEquals("a - (a + b)", new BinaryExpression(new Var("a"), "-", sum).toDisplayString()); + assertEquals("a + b + c", new BinaryExpression(sum, "+", new Var("c")).toDisplayString()); + assertEquals("b * c * c", new BinaryExpression(product, "*", new Var("c")).toDisplayString()); + } + + @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()); + } + + @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()); + } + + @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()); + } +} 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..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 @@ -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().toDisplayString(), "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().toDisplayString(), "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().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"); - } -}