Simplify Unambiguous Qualified Names

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java

@@ -19,20 +19,25 @@
 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<String> {
 
+    private final ExpressionNameResolver nameResolver;
+
+    private ExpressionFormatter(Expression expression) {
+        this.nameResolver = ExpressionNameResolver.forExpression(expression);
+    }
+
     public static String format(Predicate predicate) {
         return format(predicate.getExpression());
     }
 
     public static String format(Expression expression) {
-        return new ExpressionFormatter().formatExpression(expression);
+        return new ExpressionFormatter(expression).formatExpression(expression);
     }
 
     private String formatExpression(Expression expression) {
@@ -108,7 +113,7 @@ public String visitBinaryExpression(BinaryExpression exp) {
 
     @Override
     public String visitFunctionInvocation(FunctionInvocation fun) {
-        return Utils.getSimpleName(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")";
+        return nameResolver.resolveFunction(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")";
     }
 
     @Override
@@ -159,6 +164,6 @@ public String visitEnum(Enum en) {
 
     @Override
     public String visitVar(Var var) {
-        return VariableFormatter.format(var.getName());
+        return nameResolver.resolveVariable(var.getName());
     }
 }

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java

@@ -0,0 +1,44 @@
+package liquidjava.rj_language.ast.formatter;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.utils.Utils;
+
+/** Simplifies unambiguous qualified names within one expression */
+final class ExpressionNameResolver {
+    private final Set<String> variables = new HashSet<>();
+    private final Set<String> functions = new HashSet<>();
+
+    public static ExpressionNameResolver forExpression(Expression expression) {
+        ExpressionNameResolver resolver = new ExpressionNameResolver();
+        resolver.collect(expression);
+        return resolver;
+    }
+
+    public String resolveVariable(String name) {
+        return resolve(VariableFormatter.format(name), variables);
+    }
+
+    public String resolveFunction(String name) {
+        return resolve(name, functions);
+    }
+
+    private void collect(Expression expression) {
+        if (expression instanceof Var var)
+            variables.add(VariableFormatter.format(var.getName()));
+        else if (expression instanceof FunctionInvocation function)
+            functions.add(function.getName());
+        expression.getChildren().forEach(this::collect);
+    }
+
+    private static String resolve(String name, Set<String> names) {
+        String simpleName = Utils.getSimpleName(name);
+        boolean ambiguous = names.stream()
+                .anyMatch(other -> !other.equals(name) && Utils.getSimpleName(other).equals(simpleName));
+        return ambiguous ? name : simpleName;
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java

@@ -9,11 +9,15 @@
 class ExpressionFormatterTest {
 
     private static Expression parse(String refinement) {
-        return RefinementsParser.createAST(refinement, "");
+        return parse(refinement, "");
+    }
+
+    private static Expression parse(String refinement, String prefix) {
+        return RefinementsParser.createAST(refinement, prefix);
     }
 
     @Test
-    void formatsUnaryAtoms() {
+    void formatsUnary() {
         assertEquals("!x", parse("!x").toDisplayString());
         assertEquals("!false", parse("!false").toDisplayString());
     }
@@ -50,7 +54,7 @@ void formatsBinaryPrecedence() {
     }
 
     @Test
-    void omitsUnnecessaryGroupParentheses() {
+    void formatsGrouping() {
         assertEquals("x", parse("(x)").toDisplayString());
         assertEquals("x", parse("((x))").toDisplayString());
         assertEquals("1", parse("(1)").toDisplayString());
@@ -97,4 +101,18 @@ void formatsTernaryExpressions() {
         assertEquals("a ? b : (c ? d : (e ? f : g))", parse("a ? b : c ? d : e ? f : g").toDisplayString());
         assertEquals("a ? b : c", parse("a ? b : c").toDisplayString());
     }
+
+    @Test
+    void formatsWithQualifiedNames() {
+        Expression exp = new BinaryExpression(parse("size(this)", "java.util.ArrayList"), "==",
+                parse("size(this)", "java.util.ArrayDeque"));
+        assertEquals("java.util.ArrayList.size(this) == java.util.ArrayDeque.size(this)",
+                exp.toDisplayString());
+    }
+
+    @Test
+    void formatsWithoutQualifiedNames() {
+        assertEquals("size(this)", parse("size(this)", "java.util.List").toDisplayString());
+        assertEquals("size(this) == size(this)", parse("size(this) == size(this)", "java.util.List").toDisplayString());
+    }
 }