Exclude Qualified Names in Error Messages

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java

@@ -16,7 +16,7 @@ public class GhostInvocationError extends LJError {
     public GhostInvocationError(String message, SourcePosition pos, Expression expected,
             TranslationTable translationTable) {
         super("Ghost Invocation Error", message, "", pos, translationTable);
-        this.expected = expected.toString();
+        this.expected = expected.toSimplifiedString();
     }
 
     public String getExpected() {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -17,9 +17,10 @@ public class RefinementError extends LJError {
 
     public RefinementError(CtElement element, Expression expected, ValDerivationNode found,
             TranslationTable translationTable) {
-        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), "",
+        super("Refinement Error",
+                String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), "",
                 element.getPosition(), translationTable);
-        this.expected = expected.toString();
+        this.expected = expected.toSimplifiedString();
         this.found = found;
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java

@@ -18,7 +18,7 @@ public StateConflictError(CtElement element, Expression state, String className,
             TranslationTable translationTable) {
         super("State Conflict Error", "Found multiple disjoint states in state transition",
                 "State transition can only go to one state of each state set", element.getPosition(), translationTable);
-        this.state = state.toString();
+        this.state = state.toSimplifiedString();
         this.className = className;
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -22,12 +22,13 @@ public StateRefinementError(CtElement element, String method, Expression[] expec
             TranslationTable translationTable) {
         super("State Refinement Error", "State refinement transition violation",
                 String.format("Expected: %s\nFound: %s",
-                        String.join(", ", Arrays.stream(expected).map(Expression::toString).toArray(String[]::new)),
-                        found.toString()),
+                        String.join(", ",
+                                Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new)),
+                        found.toSimplifiedString()),
                 element.getPosition(), translationTable);
         this.method = method;
-        this.expected = Arrays.stream(expected).map(Expression::toString).toArray(String[]::new);
-        this.found = found.toString();
+        this.expected = Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new);
+        this.found = found.toSimplifiedString();
     }
 
     public String getMethod() {

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java

@@ -33,6 +33,12 @@ public String toString() {
         return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(", ")) + ")";
     }
 
+    @Override
+    public String toSimplifiedString() {
+        return name + "(" + getArgs().stream().map(Expression::toSimplifiedString).collect(Collectors.joining(", "))
+                + ")";
+    }
+
     @Override
     public void getVariableNames(List<String> toAdd) {
         for (Expression e : getArgs())

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java

@@ -49,6 +49,11 @@ public String toString() {
         return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();
     }
 
+    @Override
+    public String toSimplifiedString() {
+        return getFirstOperand().toSimplifiedString() + " " + op + " " + getSecondOperand().toSimplifiedString();
+    }
+
     @Override
     public void getVariableNames(List<String> toAdd) {
         getFirstOperand().getVariableNames(toAdd);

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java

@@ -29,6 +29,17 @@ public abstract class Expression {
 
     public abstract String toString();
 
+    /**
+     * Returns a simplified string representation of this expression with unqualified names (e.g.,
+     * com.example.State.open => open Default implementation delegates to toString() Subclasses that contain qualified
+     * names should override this method
+     * 
+     * @return simplified string representation
+     */
+    public String toSimplifiedString() {
+        return toString();
+    }
+
     List<Expression> children = new ArrayList<>();
 
     public void addChild(Expression e) {

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java

@@ -39,6 +39,13 @@ public String toString() {
         return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(",")) + ")";
     }
 
+    @Override
+    public String toSimplifiedString() {
+        String simpleName = Utils.getSimpleName(name);
+        return simpleName + "("
+                + getArgs().stream().map(Expression::toSimplifiedString).collect(Collectors.joining(",")) + ")";
+    }
+
     @Override
     public void getVariableNames(List<String> toAdd) {
         for (Expression e : getArgs())

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java

@@ -23,6 +23,11 @@ public String toString() {
         return "(" + getExpression().toString() + ")";
     }
 
+    @Override
+    public String toSimplifiedString() {
+        return "(" + getExpression().toSimplifiedString() + ")";
+    }
+
     @Override
     public void getVariableNames(List<String> toAdd) {
         getExpression().getVariableNames(toAdd);

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java

@@ -34,6 +34,12 @@ public String toString() {
         return getCondition().toString() + "?" + getThen().toString() + ":" + getElse().toString();
     }
 
+    @Override
+    public String toSimplifiedString() {
+        return getCondition().toSimplifiedString() + "?" + getThen().toSimplifiedString() + ":"
+                + getElse().toSimplifiedString();
+    }
+
     @Override
     public void getVariableNames(List<String> toAdd) {
         getCondition().getVariableNames(toAdd);