Simplify Unambiguous Qualified Names (#284)

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,49 @@
+package liquidjava.rj_language.ast.formatter;
+
+import java.util.HashSet;
+import java.util.Set;
+import java.util.function.Function;
+
+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) {
+        String formatted = VariableFormatter.format(name);
+        return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted
+                : Utils.getSimpleName(formatted);
+    }
+
+    public String resolveFunction(String name) {
+        return isAmbiguous(name, functions, Utils::getSimpleName) ? name : Utils.getSimpleName(name);
+    }
+
+    private void collect(Expression expression) {
+        if (expression instanceof Var var)
+            variables.add(var.getName());
+        else if (expression instanceof FunctionInvocation fun)
+            functions.add(fun.getName());
+        expression.getChildren().forEach(this::collect);
+    }
+
+    private static String getVariableSimpleName(String name) {
+        return Utils.getSimpleName(VariableFormatter.withoutInstance(name));
+    }
+
+    private static boolean isAmbiguous(String name, Set<String> names, Function<String, String> getSimpleName) {
+        String simpleName = getSimpleName.apply(name);
+        return names.stream().anyMatch(other -> !other.equals(name) && getSimpleName.apply(other).equals(simpleName));
+    }
+}

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

@@ -24,6 +24,11 @@ public static String format(String name) {
         return prefix + baseName + toSuperscript(counter);
     }
 
+    public static String withoutInstance(String name) {
+        Matcher matcher = INSTACE_VAR_PATTERN.matcher(name);
+        return matcher.matches() ? matcher.group(1) : name;
+    }
+
     private static String toSuperscript(String number) {
         StringBuilder sb = new StringBuilder(number.length());
         for (char c : number.toCharArray()) {
@@ -38,4 +43,4 @@ private static String toSuperscript(String number) {
     private static boolean isSpecialIdentifier(String id) {
         return id.equals("fresh") || id.equals("ret");
     }
-}
+}

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

@@ -13,20 +13,11 @@ private static Expression parse(String refinement) {
     }
 
     @Test
-    void formatsUnaryAtoms() {
+    void formatsUnary() {
         assertEquals("!x", parse("!x").toDisplayString());
         assertEquals("!false", parse("!false").toDisplayString());
     }
 
-    @Test
-    void formatsInternalVariables() {
-        assertEquals("x", parse("x").toDisplayString());
-        assertEquals("x²", parse("#x_2").toDisplayString());
-        assertEquals("#fresh¹²", parse("#fresh_12").toDisplayString());
-        assertEquals("#ret³", parse("#ret_3").toDisplayString());
-        assertEquals("this#Class", parse("this#Class").toDisplayString());
-    }
-
     @Test
     void formatsEnums() {
         assertEquals("Color.RED", parse("Color.RED").toDisplayString());
@@ -50,7 +41,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 +88,5 @@ 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());
     }
+
 }

liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java

@@ -0,0 +1,45 @@
+package liquidjava.rj_language.ast.formatter;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.parsing.RefinementsParser;
+
+class ExpressionNameResolverTest {
+
+    private static Expression parse(String refinement, String prefix) {
+        return RefinementsParser.createAST(refinement, prefix);
+    }
+
+    @Test
+    void stripsQualifiedNamesWhenUnambiguous() {
+        ExpressionNameResolver resolver = ExpressionNameResolver
+                .forExpression(parse("size(this) == size(this)", "java.util.List"));
+
+        assertEquals("size", resolver.resolveFunction("java.util.List.size"));
+    }
+
+    @Test
+    void keepsQualifiedNamesForDifferentPrefixes() {
+        Expression expression = new BinaryExpression(parse("size(this)", "java.util.ArrayList"), "==",
+                parse("size(this)", "java.util.ArrayDeque"));
+        ExpressionNameResolver resolver = ExpressionNameResolver.forExpression(expression);
+
+        assertEquals("java.util.ArrayList.size", resolver.resolveFunction("java.util.ArrayList.size"));
+        assertEquals("java.util.ArrayDeque.size", resolver.resolveFunction("java.util.ArrayDeque.size"));
+    }
+
+    @Test
+    void keepsQualifiedNamesForDifferentInstances() {
+        Predicate differentInstances = Predicate.createEquals(Predicate.createVar("#java.util.ArrayList.size_1"),
+                Predicate.createVar("#java.util.ArrayDeque.size_2"));
+        ExpressionNameResolver resolver = ExpressionNameResolver.forExpression(differentInstances.getExpression());
+
+        assertEquals("java.util.ArrayList.size¹", resolver.resolveVariable("#java.util.ArrayList.size_1"));
+        assertEquals("java.util.ArrayDeque.size²", resolver.resolveVariable("#java.util.ArrayDeque.size_2"));
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java

@@ -0,0 +1,17 @@
+package liquidjava.rj_language.ast.formatter;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import org.junit.jupiter.api.Test;
+
+class VariableFormatterTest {
+
+    @Test
+    void formatsVariables() {
+        assertEquals("x", VariableFormatter.format("x"));
+        assertEquals("x²", VariableFormatter.format("#x_2"));
+        assertEquals("#fresh¹²", VariableFormatter.format("#fresh_12"));
+        assertEquals("#ret³", VariableFormatter.format("#ret_3"));
+        assertEquals("this#Class", VariableFormatter.format("this#Class"));
+    }
+}