Renaming

liquid-java · rcosta358 · Apr 11, 2026 · Mar 31, 2026 · Mar 31, 2026 · Mar 31, 2026
commit 1a128375205ee070adffb9a3ee45ecb180636dd6
diff --git 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
@@ -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<Expression> children = new ArrayList<>();

diff --git a/...ast/prettyprinting/ExpressionPrinter.java → ...ge/ast/formatter/ExpressionFormatter.java b/...ast/prettyprinting/ExpressionPrinter.java → ...ge/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<String> {
+public class ExpressionFormatter implements ExpressionVisitor<String> {
 
-    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<Expression> args) {
-        return args.stream().map(expression -> renderWithOptionalParentheses(expression, false))
+    private String formatArguments(List<Expression> 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/.../prettyprinting/ExpressionPrecedence.java → ...e/ast/formatter/ExpressionPrecedence.java b/.../prettyprinting/ExpressionPrecedence.java → ...e/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/...ast/prettyprinting/VariableFormatter.java → ...uage/ast/formatter/VariableFormatter.java b/...ast/prettyprinting/VariableFormatter.java → ...uage/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;