Code Refactoring

rcosta358 · rcosta358 · commit a08e169f8cb3 · 2026-03-31T21:50:57.000+01:00
diff --git 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
@@ -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
@@ -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> T accept(ExpressionVisitor<T> 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
@@ -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
@@ -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<Expression> 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
@@ -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> T accept(ExpressionVisitor<T> 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
@@ -21,7 +21,7 @@ public <T> T accept(ExpressionVisitor<T> 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
@@ -32,7 +32,7 @@ public <T> T accept(ExpressionVisitor<T> 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
@@ -29,7 +29,7 @@ public <T> T accept(ExpressionVisitor<T> 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/prettyprinting/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/rj_language/ast/prettyprinting/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");
     }
-}
+}
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
@@ -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
@@ -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<String> {
-        @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
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
diff --git a/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java

Original file line number	Diff line number	Diff line change
`@@ -42,7 +42,7 @@ public boolean isArithmeticOperation() {`
`42`	`42`
`43`	`43`	`@Override`
`44`	`44`	`public String toString() {`
`45`		`- return ExpressionPrinter.print(this);`
	`45`	`+ return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();`
`46`	`46`	`}`
`47`	`47`
`48`	`48`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -21,7 +21,7 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {`
`21`	`21`	`}`
`22`	`22`
`23`	`23`	`public String toString() {`
`24`		`- return ExpressionPrinter.print(this);`
	`24`	`+ return getExpression().toString();`
`25`	`25`	`}`
`26`	`26`
`27`	`27`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -32,7 +32,7 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {`
`32`	`32`
`33`	`33`	`@Override`
`34`	`34`	`public String toString() {`
`35`		`- return ExpressionPrinter.print(this);`
	`35`	`+ return getCondition().toString() + " ? " + getThen().toString() + " : " + getElse().toString();`
`36`	`36`	`}`
`37`	`37`
`38`	`38`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -29,7 +29,7 @@ public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {`
`29`	`29`
`30`	`30`	`@Override`
`31`	`31`	`public String toString() {`
`32`		`- return ExpressionPrinter.print(this);`
	`32`	`+ return op + getExpression().toString();`
`33`	`33`	`}`
`34`	`34`
`35`	`35`	`@Override`