Error Refactoring

liquidjava-verifier/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.2</version>
+	<version>0.0.4</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -10,16 +10,14 @@ public class LJDiagnostic extends RuntimeException {
 
     private final String title;
     private final String message;
-    private final String details;
     private final String file;
     private final ErrorPosition position;
     private final String accentColor;
 
-    public LJDiagnostic(String title, String message, String details, SourcePosition pos, String accentColor) {
+    public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor) {
         this.title = title;
         this.message = message;
-        this.details = details;
-        this.file = pos != null ? pos.getFile().getPath() : null;
+        this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null;
         this.position = ErrorPosition.fromSpoonPosition(pos);
         this.accentColor = accentColor;
     }
@@ -33,7 +31,7 @@ public String getMessage() {
     }
 
     public String getDetails() {
-        return details;
+        return "";
     }
 
     public ErrorPosition getPosition() {
@@ -44,13 +42,17 @@ public String getFile() {
         return file;
     }
 
+    public String getAccentColor() {
+        return accentColor;
+    }
+
     @Override
     public String toString() {
         StringBuilder sb = new StringBuilder();
 
         // title
-        sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET)
-                .append(message.toLowerCase()).append("\n");
+        sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
+                .append("\n");
 
         // snippet
         String snippet = getSnippet();
@@ -59,7 +61,8 @@ public String toString() {
         }
 
         // details
-        if (details != null && !details.isEmpty()) {
+        String details = getDetails();
+        if (!details.isEmpty()) {
             sb.append(" --> ").append(String.join("\n     ", details.split("\n"))).append("\n");
         }
 
@@ -124,7 +127,6 @@ public boolean equals(Object obj) {
             return false;
         LJDiagnostic other = (LJDiagnostic) obj;
         return title.equals(other.title) && message.equals(other.message)
-                && ((details == null && other.details == null) || (details != null && details.equals(other.details)))
                 && ((file == null && other.file == null) || (file != null && file.equals(other.file)))
                 && ((position == null && other.position == null)
                         || (position != null && position.equals(other.position)));
@@ -134,7 +136,6 @@ public boolean equals(Object obj) {
     public int hashCode() {
         int result = title.hashCode();
         result = 31 * result + message.hashCode();
-        result = 31 * result + (details != null ? details.hashCode() : 0);
         result = 31 * result + (file != null ? file.hashCode() : 0);
         result = 31 * result + (position != null ? position.hashCode() : 0);
         return result;

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

@@ -1,7 +1,6 @@
 package liquidjava.diagnostics.errors;
 
 import spoon.reflect.cu.SourcePosition;
-import spoon.reflect.declaration.CtElement;
 
 /**
  * Custom error with an arbitrary message
@@ -11,18 +10,10 @@
 public class CustomError extends LJError {
 
     public CustomError(String message) {
-        super("Error", message, null, null, null);
+        super("Error", message, null, null);
     }
 
-    public CustomError(String message, SourcePosition pos) {
-        super("Error", message, null, pos, null);
-    }
-
-    public CustomError(String message, String detail, CtElement element) {
-        super("Error", message, detail, element.getPosition(), null);
-    }
-
-    public CustomError(String message, CtElement element) {
-        super("Error", message, null, element.getPosition(), null);
+    public CustomError(String message, SourcePosition position) {
+        super("Error", message, position, null);
     }
 }

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

@@ -10,7 +10,8 @@
 public class IllegalConstructorTransitionError extends LJError {
 
     public IllegalConstructorTransitionError(CtElement element) {
-        super("Illegal Constructor Transition Error", "Found constructor with 'from' state",
-                "Constructor methods should only have a 'to' state", element.getPosition(), null);
+        super("Illegal Constructor Transition Error",
+                "Found constructor with 'from' state: constructors should only have a 'to' state",
+                element.getPosition(), null);
     }
 }

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

@@ -1,6 +1,6 @@
 package liquidjava.diagnostics.errors;
 
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that a refinement is invalid (e.g., not a boolean expression)
@@ -11,8 +11,8 @@ public class InvalidRefinementError extends LJError {
 
     private final String refinement;
 
-    public InvalidRefinementError(CtElement element, String message, String refinement) {
-        super("Invalid Refinement", message, "", element.getPosition(), null);
+    public InvalidRefinementError(SourcePosition position, String message, String refinement) {
+        super("Invalid Refinement", message, position, null);
         this.refinement = refinement;
     }
 

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

@@ -12,9 +12,8 @@ public abstract class LJError extends LJDiagnostic {
 
     private final TranslationTable translationTable;
 
-    public LJError(String title, String message, String details, SourcePosition pos,
-            TranslationTable translationTable) {
-        super(title, message, details, pos, Colors.BOLD_RED);
+    public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) {
+        super(title, message, pos, Colors.BOLD_RED);
         this.translationTable = translationTable != null ? translationTable : new TranslationTable();
     }
 

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

@@ -1,7 +1,8 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import spoon.reflect.declaration.CtElement;
+import liquidjava.utils.Utils;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that an element referenced in a refinement was not found
@@ -10,7 +11,21 @@
  */
 public class NotFoundError extends LJError {
 
-    public NotFoundError(CtElement element, String message, TranslationTable translationTable) {
-        super("Not Found Error", message, "", element.getPosition(), translationTable);
+    private final String name;
+    private final String kind; // "Variable" or "Ghost"
+
+    public NotFoundError(SourcePosition position, String message, String name, String kind,
+            TranslationTable translationTable) {
+        super("Not Found Error", message, position, translationTable);
+        this.name = Utils.getSimpleName(name);
+        this.kind = kind;
+    }
+
+    public String getName() {
+        return name;
+    }
+
+    public String getKind() {
+        return kind;
     }
 }

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

@@ -3,7 +3,7 @@
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that a refinement constraint either was violated or cannot be proven
@@ -15,11 +15,11 @@ public class RefinementError extends LJError {
     private final String expected;
     private final ValDerivationNode found;
 
-    public RefinementError(CtElement element, Expression expected, ValDerivationNode found,
+    public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found,
             TranslationTable translationTable) {
         super("Refinement Error",
-                String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), "",
-                element.getPosition(), translationTable);
+                String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), position,
+                translationTable);
         this.expected = expected.toSimplifiedString();
         this.found = found;
     }

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

@@ -2,7 +2,7 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that two disjoint states were found in a state refinement
@@ -11,22 +11,16 @@
  */
 public class StateConflictError extends LJError {
 
-    private final String state;
-    private final String className;
+    private final String state;;
 
-    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);
+    public StateConflictError(SourcePosition position, Expression state, 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",
+                position, translationTable);
         this.state = state.toSimplifiedString();
-        this.className = className;
     }
 
     public String getState() {
         return state;
     }
-
-    public String getClassName() {
-        return className;
-    }
 }

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

@@ -1,10 +1,8 @@
 package liquidjava.diagnostics.errors;
 
-import java.util.Arrays;
-
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that a state refinement transition was violated
@@ -13,28 +11,18 @@
  */
 public class StateRefinementError extends LJError {
 
-    private final String method;
-    private final String[] expected;
+    private final String expected;
     private final String found;
 
-    public StateRefinementError(CtElement element, String method, Expression[] expected, Expression found,
+    public StateRefinementError(SourcePosition position, Expression expected, Expression found,
             TranslationTable translationTable) {
-        super("State Refinement Error", "State refinement transition violation",
-                String.format("Expected: %s\nFound: %s",
-                        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::toSimplifiedString).toArray(String[]::new);
+        super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(),
+                found.toSimplifiedString()), position, translationTable);
+        this.expected = expected.toSimplifiedString();
         this.found = found.toSimplifiedString();
     }
 
-    public String getMethod() {
-        return method;
-    }
-
-    public String[] getExpected() {
+    public String getExpected() {
         return expected;
     }
 

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

@@ -16,7 +16,7 @@ public SyntaxError(String message, String refinement) {
     }
 
     public SyntaxError(String message, SourcePosition pos, String refinement) {
-        super("Syntax Error", message, "", pos, null);
+        super("Syntax Error", message, pos, null);
         this.refinement = refinement;
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java

@@ -12,7 +12,7 @@ public class ExternalClassNotFoundWarning extends LJWarning {
     private final String className;
 
     public ExternalClassNotFoundWarning(CtElement element, String message, String className) {
-        super(message, "", element.getPosition());
+        super(message, element.getPosition());
         this.className = className;
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java

@@ -11,12 +11,14 @@ public class ExternalMethodNotFoundWarning extends LJWarning {
 
     private final String methodName;
     private final String className;
+    private final String[] overloads;
 
-    public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName,
-            String className) {
-        super(message, details, element.getPosition());
+    public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, String className,
+            String[] overloads) {
+        super(message, element.getPosition());
         this.methodName = methodName;
         this.className = className;
+        this.overloads = overloads;
     }
 
     public String getMethodName() {
@@ -26,4 +28,13 @@ public String getMethodName() {
     public String getClassName() {
         return className;
     }
+
+    public String[] getOverloads() {
+        return overloads;
+    }
+
+    @Override
+    public String getDetails() {
+        return overloads.length > 0 ? String.format("Available overloads:\n  %s", String.join("\n  ", overloads)) : "";
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java

@@ -9,7 +9,7 @@
  */
 public abstract class LJWarning extends LJDiagnostic {
 
-    public LJWarning(String message, String details, SourcePosition pos) {
-        super("Warning", message, details, pos, Colors.BOLD_YELLOW);
+    public LJWarning(String message, SourcePosition pos) {
+        super("Warning", message, pos, Colors.BOLD_YELLOW);
     }
 }