Replace Details Field with Method

rcosta358 · rcosta358 · commit d243c73f2e8e · 2025-11-20T11:51:29.000Z
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
@@ -10,15 +10,13 @@ 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() != 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() {
@@ -63,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");
         }
 
@@ -128,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)));
@@ -138,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;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java
@@ -10,14 +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 position) {
-        super("Error", message, null, position, null);
-    }
-
-    public CustomError(String message, SourcePosition position, String details) {
-        super("Error", message, details, position, null);
+        super("Error", message, position, null);
     }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java
@@ -10,7 +10,6 @@
 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);
     }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java
@@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError {
     private final String refinement;
 
     public InvalidRefinementError(SourcePosition position, String message, String refinement) {
-        super("Invalid Refinement", message, "", position, null);
+        super("Invalid Refinement", message, position, null);
         this.refinement = refinement;
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java
@@ -12,9 +12,9 @@ public abstract class LJError extends LJDiagnostic {
 
     private final TranslationTable translationTable;
 
-    public LJError(String title, String message, String details, SourcePosition pos,
+    public LJError(String title, String message, SourcePosition pos,
             TranslationTable translationTable) {
-        super(title, message, details, pos, Colors.BOLD_RED);
+        super(title, message, pos, Colors.BOLD_RED);
         this.translationTable = translationTable != null ? translationTable : new TranslationTable();
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java
@@ -16,7 +16,7 @@ public class NotFoundError extends LJError {
 
     public NotFoundError(SourcePosition position, String message, String name, String kind,
             TranslationTable translationTable) {
-        super("Not Found Error", message, "", position, translationTable);
+        super("Not Found Error", message, position, translationTable);
         this.name = Utils.getSimpleName(name);
         this.kind = kind;
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
@@ -18,7 +18,7 @@ public class RefinementError extends LJError {
     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()), "",
+                String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()),
                 position, translationTable);
         this.expected = expected.toSimplifiedString();
         this.found = found;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java
@@ -14,8 +14,7 @@ public class StateConflictError extends LJError {
     private final String state;;
 
     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);
+        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();
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
@@ -17,7 +17,7 @@ public class StateRefinementError extends LJError {
     public StateRefinementError(SourcePosition position, Expression expected, Expression found,
             TranslationTable translationTable) {
         super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(),
-                found.toSimplifiedString()), null, position, translationTable);
+                found.toSimplifiedString()), position, translationTable);
         this.expected = expected.toSimplifiedString();
         this.found = found.toSimplifiedString();
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java b/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;
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/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, null, element.getPosition());
+        super(message, element.getPosition());
         this.className = className;
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java
@@ -13,9 +13,9 @@ public class ExternalMethodNotFoundWarning extends LJWarning {
     private final String className;
     private final String[] overloads;
 
-    public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName,
+    public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName,
             String className, String[] overloads) {
-        super(message, details, element.getPosition());
+        super(message, element.getPosition());
         this.methodName = methodName;
         this.className = className;
         this.overloads = overloads;
@@ -32,4 +32,9 @@ public String getClassName() {
     public String[] getOverloads() {
         return overloads;
     }
+
+    @Override
+    public String getDetails() {
+        return overloads.length > 0 ? String.format("Available overloads:\n  %s", String.join("\n  ", overloads)) : "";
+    }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java b/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);
     }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
@@ -71,20 +71,15 @@ public <R> void visitCtMethod(CtMethod<R> method) {
                 String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(),
                         prefix);
                 String[] overloads = getOverloads(targetType, method);
-                String details = overloads.length == 0 ? null
-                        : "Available constructors:\n  " + String.join("\n  ", overloads);
-
-                diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(),
+                diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(),
                         prefix, overloads));
             }
         } else {
             if (!methodExists(targetType, method)) {
                 String message = String.format("Could not find method '%s %s' for '%s'",
                         method.getType().getSimpleName(), method.getSignature(), prefix);
                 String[] overloads = getOverloads(targetType, method);
-                String details = overloads.length == 0 ? null
-                        : "Available overloads:\n  " + String.join("\n  ", overloads);
-                diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(),
+                diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(),
                         prefix, overloads));
                 return;
             }

Original file line number	Diff line number	Diff line change
`@@ -10,14 +10,10 @@`
`10`	`10`	`public class CustomError extends LJError {`
`11`	`11`
`12`	`12`	`public CustomError(String message) {`
`13`		`- super("Error", message, null, null, null);`
	`13`	`+ super("Error", message, null, null);`
`14`	`14`	`}`
`15`	`15`
`16`	`16`	`public CustomError(String message, SourcePosition position) {`
`17`		`- super("Error", message, null, position, null);`
`18`		`- }`
`19`		`-`
`20`		`- public CustomError(String message, SourcePosition position, String details) {`
`21`		`- super("Error", message, details, position, null);`
	`17`	`+ super("Error", message, position, null);`
`22`	`18`	`}`
`23`	`19`	`}`
Original file line number	Diff line number	Diff line change
`@@ -10,7 +10,6 @@`
`10`	`10`	`public class IllegalConstructorTransitionError extends LJError {`
`11`	`11`
`12`	`12`	`public IllegalConstructorTransitionError(CtElement element) {`
`13`		`- super("Illegal Constructor Transition Error", "Found constructor with 'from' state",`
`14`		`- "Constructor methods should only have a 'to' state", element.getPosition(), null);`
	`13`	`+ super("Illegal Constructor Transition Error", "Found constructor with 'from' state: constructors should only have a 'to' state", element.getPosition(), null);`
`15`	`14`	`}`
`16`	`15`	`}`
Original file line number	Diff line number	Diff line change
`@@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError {`
`12`	`12`	`private final String refinement;`
`13`	`13`
`14`	`14`	`public InvalidRefinementError(SourcePosition position, String message, String refinement) {`
`15`		`- super("Invalid Refinement", message, "", position, null);`
	`15`	`+ super("Invalid Refinement", message, position, null);`
`16`	`16`	`this.refinement = refinement;`
`17`	`17`	`}`
`18`	`18`
Original file line number	Diff line number	Diff line change
`@@ -12,9 +12,9 @@ public abstract class LJError extends LJDiagnostic {`
`12`	`12`
`13`	`13`	`private final TranslationTable translationTable;`
`14`	`14`
`15`		`- public LJError(String title, String message, String details, SourcePosition pos,`
	`15`	`+ public LJError(String title, String message, SourcePosition pos,`
`16`	`16`	`TranslationTable translationTable) {`
`17`		`- super(title, message, details, pos, Colors.BOLD_RED);`
	`17`	`+ super(title, message, pos, Colors.BOLD_RED);`
`18`	`18`	`this.translationTable = translationTable != null ? translationTable : new TranslationTable();`
`19`	`19`	`}`
`20`	`20`
Original file line number	Diff line number	Diff line change
`@@ -16,7 +16,7 @@ public class NotFoundError extends LJError {`
`16`	`16`
`17`	`17`	`public NotFoundError(SourcePosition position, String message, String name, String kind,`
`18`	`18`	`TranslationTable translationTable) {`
`19`		`- super("Not Found Error", message, "", position, translationTable);`
	`19`	`+ super("Not Found Error", message, position, translationTable);`
`20`	`20`	`this.name = Utils.getSimpleName(name);`
`21`	`21`	`this.kind = kind;`
`22`	`22`	`}`
Original file line number	Diff line number	Diff line change
`@@ -14,8 +14,7 @@ public class StateConflictError extends LJError {`
`14`	`14`	`private final String state;;`
`15`	`15`
`16`	`16`	`public StateConflictError(SourcePosition position, Expression state, TranslationTable translationTable) {`
`17`		`- super("State Conflict Error", "Found multiple disjoint states in state transition",`
`18`		`- "State transition can only go to one state of each state set", position, translationTable);`
	`17`	`+ 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);`
`19`	`18`	`this.state = state.toSimplifiedString();`
`20`	`19`	`}`
`21`	`20`
Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,7 @@ public class StateRefinementError extends LJError {`
`17`	`17`	`public StateRefinementError(SourcePosition position, Expression expected, Expression found,`
`18`	`18`	`TranslationTable translationTable) {`
`19`	`19`	`super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(),`
`20`		`- found.toSimplifiedString()), null, position, translationTable);`
	`20`	`+ found.toSimplifiedString()), position, translationTable);`
`21`	`21`	`this.expected = expected.toSimplifiedString();`
`22`	`22`	`this.found = found.toSimplifiedString();`
`23`	`23`	`}`
Original file line number	Diff line number	Diff line change
`@@ -16,7 +16,7 @@ public SyntaxError(String message, String refinement) {`
`16`	`16`	`}`
`17`	`17`
`18`	`18`	`public SyntaxError(String message, SourcePosition pos, String refinement) {`
`19`		`- super("Syntax Error", message, "", pos, null);`
	`19`	`+ super("Syntax Error", message, pos, null);`
`20`	`20`	`this.refinement = refinement;`
`21`	`21`	`}`
`22`	`22`