Add Counterexample DTO (#105)

Author: rcosta358

client/src/types/diagnostics.ts

@@ -62,10 +62,19 @@ export type RefinementError = BaseDiagnostic & {
     expected: string;
     found: VCSimplificationResult;
     customMessage: string;
-    counterexample: string;
+    counterexample: Counterexample;
     declarationPosition: SourcePosition | null;
 }
 
+export type Counterexample = {
+    assignments: CounterexampleAssignment[];
+}
+
+export type CounterexampleAssignment = {
+    variable: string;
+    value: string;
+}
+
 export type StateConflictError = BaseDiagnostic & {
     category: 'error';
     type: 'state-conflict-error';

client/src/webview/views/diagnostics/counterexample.ts

@@ -1,22 +1,17 @@
+import type { Counterexample } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression } from "../../highlighting";
 
-function getCounterexampleLines(counterexample: string): string[] {
-    return counterexample
-        .split("&&")
-        .map(assignment => assignment.trim())
-        .filter(Boolean);
-}
-
-export function renderCounterexample(counterexample: string): string {
-    const lines = getCounterexampleLines(counterexample);
-    if (lines.length === 0) return "";
+export function renderCounterexample(counterexample: Counterexample): string {
+    if (counterexample.assignments.length === 0) return "";
 
     return /*html*/`
         <div class="container vc-container counterexample-container">
             <div class="vc-chain">
-                ${lines.map(line => /*html*/`
+                ${counterexample.assignments.map(assignment => /*html*/`
                     <div class="counterexample-line">
-                        <span class="vc-node">${renderHighlightedInlineExpression(line)}</span>
+                        <span class="vc-node">${renderHighlightedInlineExpression(
+                            `${assignment.variable} == ${assignment.value}`
+                        )}</span>
                     </div>
                 `).join("")}
             </div>

client/src/webview/views/diagnostics/errors.ts

@@ -40,7 +40,9 @@ const errorContentRenderers: ErrorRendererMap = {
     'refinement-error': (e: RefinementError) => /*html*/ `
         ${renderExpressionSection('Expected', e.expected)}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
-        ${e.counterexample ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample)) : ''}
+        ${e.counterexample.assignments.length > 0
+            ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample))
+            : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/ `
         ${renderExpressionSection('Expected', e.expected)}

server/src/main/java/dtos/diagnostics/CounterexampleDTO.java

@@ -0,0 +1,27 @@
+package dtos.diagnostics;
+
+import java.util.List;
+
+import liquidjava.rj_language.ast.formatter.VariableFormatter;
+import liquidjava.smt.Counterexample;
+
+/**
+ * DTO for serializing counterexample assignments.
+ */
+public record CounterexampleDTO(List<AssignmentDTO> assignments) {
+
+    public static CounterexampleDTO from(Counterexample counterexample) {
+        if (counterexample == null)
+            return null;
+
+        List<AssignmentDTO> assignments = counterexample.assignments().stream()
+                .map(assignment -> new AssignmentDTO(
+                        VariableFormatter.format(assignment.first()),
+                        assignment.second()))
+                .toList();
+        return new CounterexampleDTO(assignments);
+    }
+
+    public record AssignmentDTO(String variable, String value) {
+    }
+}

server/src/main/java/dtos/errors/RefinementErrorDTO.java

@@ -1,5 +1,6 @@
 package dtos.errors;
 
+import dtos.diagnostics.CounterexampleDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.VCSimplificationResultDTO;
 import liquidjava.diagnostics.errors.RefinementError;
@@ -13,15 +14,15 @@ public class RefinementErrorDTO extends LJErrorDTO {
     public final String expected;
     public final VCSimplificationResultDTO found;
     public final String customMessage;
-    public final String counterexample;
+    public final CounterexampleDTO counterexample;
     public final SourcePositionDTO declarationPosition;
 
     public RefinementErrorDTO(RefinementError error) {
         super("refinement-error", error);
         this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected());
         this.found = VCSimplificationResultDTO.from(error.getFound());
         this.customMessage = error.getCustomMessage();
-        this.counterexample = error.getCounterExampleString();
+        this.counterexample = CounterexampleDTO.from(error.getCounterexample());
         this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
     }