Expand Expressions in State Refinement Errors

client/src/types/diagnostics.ts

@@ -74,8 +74,8 @@ export type StateRefinementError = BaseDiagnostic & {
     category: 'error';
     type: 'state-refinement-error';
     translationTable: TranslationTable;
-    expected: string;
-    found: string;
+    expected: ValDerivationNode;
+    found: ValDerivationNode;
     customMessage: string;
 }
 

client/src/webview/views/context/variables.ts

@@ -5,7 +5,7 @@ import { escapeHtml } from "../../utils";
 import { renderToggleSection, renderHighlightButton, renderDiagnosticRevealButton } from "../sections";
 
 export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string {
-    const expected  = errorAtCursor ? errorAtCursor.type == "refinement-error" ? errorAtCursor.expected.value : errorAtCursor.expected : undefined;
+    const expected = errorAtCursor ? errorAtCursor.expected.value : undefined;
     return /*html*/`
         <div class="context-section">
             ${renderToggleSection('Variables', 'context-vars', isExpanded)}

client/src/webview/views/diagnostics/derivation-nodes.ts

@@ -1,4 +1,4 @@
-import type { LJError, RefinementError } from "../../../types/diagnostics";
+import type { LJError, RefinementMismatchError } from "../../../types/diagnostics";
 import type { DerivationNode, ValDerivationNode } from "../../../types/derivation-nodes";
 import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../../highlighting";
 import { escapeHtml } from "../../utils";
@@ -19,7 +19,7 @@ function renderToken(token: string): string {
 }
 
 function renderJsonTree(
-    error: RefinementError,
+    error: RefinementMismatchError,
     node: DerivationNode | undefined,
     errorId: string,
     path: string,
@@ -123,10 +123,11 @@ export function handleDerivationResetClick(target?: any): boolean {
 }
 
 export function renderDerivationNode(
-    error: RefinementError,
+    error: RefinementMismatchError,
     node: ValDerivationNode,
     scope: "expected" | "found"
 ): string {
+    if (!node || typeof node !== "object" || !("value" in node)) return renderHighlightedExpression(String(node)); // primitive value without derivation
     if (!node.origin) return renderHighlightedExpression(String(node.value)); // no derivation available
 
     const errorId = hashError(error, scope);

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

@@ -36,8 +36,8 @@ const errorContentRenderers: Partial<Record<LJError['type'], (error: LJError) =>
         ${e.counterexample ? renderExpressionSection('Counterexample', e.counterexample) : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/`
-        ${renderExpressionSection('Expected', e.expected)}
-        ${renderExpressionSection('Found', e.found)}
+        ${renderCustomSection('Expected', renderDerivationNode(e, e.expected, 'expected'))}
+        ${renderCustomSection('Found', renderDerivationNode(e, e.found, 'found'))}
     `,
     'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/`
         ${renderExpressionSection('Refinement', e.refinement)}

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

@@ -3,12 +3,13 @@
 import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.TranslationTableDTO;
 import liquidjava.diagnostics.errors.StateRefinementError;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 
 /**
  * DTO for serializing StateRefinementError instances to JSON
  */
 public record StateRefinementErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position,
-        TranslationTableDTO translationTable, String expected, String found, String customMessage) {
+        TranslationTableDTO translationTable, ValDerivationNode expected, ValDerivationNode found, String customMessage) {
 
     public static StateRefinementErrorDTO from(StateRefinementError error) {
         return new StateRefinementErrorDTO("error", "state-refinement-error", error.getTitle(), error.getMessage(), error.getFile(),