diff --git a/client/src/types/derivation-nodes.ts b/client/src/types/derivation-nodes.ts deleted file mode 100644 index f06386c..0000000 --- a/client/src/types/derivation-nodes.ts +++ /dev/null @@ -1,35 +0,0 @@ -// Type definitions used in refinement errors for expanding node simplifications - -export type DerivationNode = - | ValDerivationNode - | VarDerivationNode - | BinaryDerivationNode - | UnaryDerivationNode - | IteDerivationNode; - -export type ValDerivationNode = { - value: any; - origin: DerivationNode; -} - -export type VarDerivationNode = { - var: string; - origin?: DerivationNode; -} - -export type BinaryDerivationNode = { - op: string; - left: ValDerivationNode; - right: ValDerivationNode; -} - -export type UnaryDerivationNode = { - op: string; - operand: ValDerivationNode; -} - -export type IteDerivationNode = { - condition: ValDerivationNode; - thenBranch: ValDerivationNode; - elseBranch: ValDerivationNode; -} diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 02314e3..1ed3f32 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -1,5 +1,5 @@ -import type { ValDerivationNode } from './derivation-nodes'; import type { Range } from './context'; +import type { VCSimplificationResult } from './vc-implications'; // Type definitions used for LiquidJava diagnostics @@ -58,8 +58,8 @@ export type RefinementError = BaseDiagnostic & { category: 'error'; type: 'refinement-error'; translationTable: TranslationTable; - expected: ValDerivationNode; - found: ValDerivationNode; + expected: string; + found: VCSimplificationResult; customMessage: string; counterexample: string; } @@ -75,8 +75,8 @@ export type StateRefinementError = BaseDiagnostic & { category: 'error'; type: 'state-refinement-error'; translationTable: TranslationTable; - expected: ValDerivationNode; - found: ValDerivationNode; + expected: string; + found: VCSimplificationResult; customMessage: string; } diff --git a/client/src/types/vc-implications.ts b/client/src/types/vc-implications.ts new file mode 100644 index 0000000..2ecc53a --- /dev/null +++ b/client/src/types/vc-implications.ts @@ -0,0 +1,11 @@ +export type VCImplication = { + name: string | null; + type: string | null; + predicate: string; + next: VCImplication | null; +} + +export type VCSimplificationResult = { + implication: VCImplication; + origin: VCSimplificationResult | null; +} diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 78762de..ca33de4 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -1,4 +1,4 @@ -import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/diagnostics/derivation-nodes"; +import { handleVCImplicationStepClick } from "./views/diagnostics/vc-implications"; import { renderLoading } from "./views/loading"; import { renderStopped } from "./views/stopped"; import { renderStateMachineView } from "./views/fsm/fsm"; @@ -131,21 +131,11 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) return; } - // derivation expansion click - const derivableNode = target.closest?.('.derivable-node'); - if (derivableNode) { + // VC implication simplification step buttons + const vcImplicationStepButton = target.closest?.('.vc-step-btn'); + if (vcImplicationStepButton) { e.stopPropagation(); - if (handleDerivableNodeClick(derivableNode)) { - updateView(); - } - return; - } - - // derivation reset button - const derivationResetButton = target.closest?.('.derivation-reset-btn'); - if (derivationResetButton) { - e.stopPropagation(); - if (handleDerivationResetClick(derivationResetButton)) { + if (handleVCImplicationStepClick(vcImplicationStepButton)) { updateView(); } return; diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 29f35d3..fe9ee25 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -271,18 +271,6 @@ export function getStyles(): string { .link:hover { text-decoration: underline; } - .node-var { - color: var(--lj-token-identifier); - } - .node-value { - color: var(--vscode-editor-foreground); - } - .node-number { - color: var(--lj-token-number); - } - .node-boolean { - color: var(--lj-token-boolean); - } .lj-expression, .lj-expression-code { font-family: var(--vscode-editor-font-family); @@ -334,19 +322,59 @@ export function getStyles(): string { .clickable:hover { font-weight: bold; } - .derivation-container { + .vc-container { display: flex; justify-content: space-between; - align-items: center; + align-items: flex-start; gap: 1rem; + margin: 0.5rem 0; } - .reset-btn { + .vc-chain { + flex: 1; + display: flex; + flex-direction: column; + gap: 0.25rem; + min-width: 0; + } + .vc-line { + display: flex; + align-items: flex-start; + gap: 0.5rem; + min-width: 0; + } + .vc-line-content { + flex: 0 1 auto; + min-width: 0; + overflow-wrap: anywhere; + } + .vc-node { + display: inline; + padding: 0; + border: none; + background: none; + color: var(--vscode-editor-foreground); + font: inherit; + text-align: left; + } + .vc-node:hover { + background: none; + } + .vc-binder { + color: var(--vscode-descriptionForeground); + } + .vc-step-controls { + display: inline-flex; + align-items: center; + gap: 0.125rem; + flex-shrink: 0; + } + .vc-step-btn { margin: 0; display: inline-flex; align-items: center; justify-content: center; - width: 1.75rem; - height: 1.75rem; + width: 1.5rem; + height: 1.25rem; padding: 0; background-color: transparent; color: var(--vscode-button-foreground); @@ -357,12 +385,17 @@ export function getStyles(): string { flex-shrink: 0; opacity: 0.7; } - .reset-btn:hover { + .vc-step-btn .codicon { + font-size: 1.5rem; + } + .vc-step-btn:hover { font-weight: bold; background-color: transparent; + opacity: 1; } - .reset-btn:disabled { - opacity: 0.5; + .vc-step-btn:disabled { + cursor: default; + opacity: 0.35; } button { padding: 0.2rem 0.6rem; diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 209bde8..ae1d763 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -5,7 +5,6 @@ import { escapeHtml, getSimpleName } from "../../utils"; import { renderToggleSection, renderHighlightButton, renderDiagnosticRevealButton } from "../sections"; export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string { - const expected = errorAtCursor ? errorAtCursor.expected.value : undefined; const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {})); return /*html*/`
@@ -33,7 +32,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool ${renderHighlightedInlineExpression(variable.refinement)} `}).join('')} - ${errorAtCursor ? renderFailingRefinement(errorAtCursor, expected!) : ''} + ${errorAtCursor ? renderFailingRefinement(errorAtCursor) : ''} `: '

No variables declared at the cursor position

'} @@ -42,11 +41,11 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool `; } -function renderFailingRefinement(errorAtCursor: RefinementMismatchError, expected: string): string { +function renderFailingRefinement(errorAtCursor: RefinementMismatchError): string { return /*html*/` - ${renderDiagnosticRevealButton(errorAtCursor.position!, '⊢ ' + expected)} + ${renderDiagnosticRevealButton(errorAtCursor.position!, '⊢ ' + errorAtCursor.expected)} `; diff --git a/client/src/webview/views/diagnostics/derivation-nodes.ts b/client/src/webview/views/diagnostics/derivation-nodes.ts deleted file mode 100644 index b755cb5..0000000 --- a/client/src/webview/views/diagnostics/derivation-nodes.ts +++ /dev/null @@ -1,137 +0,0 @@ -import type { LJError, RefinementMismatchError } from "../../../types/diagnostics"; -import type { DerivationNode, ValDerivationNode } from "../../../types/derivation-nodes"; -import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../../highlighting"; -import { renderCodicon } from "../../icons"; -import { escapeHtml } from "../../utils"; - -// Handles rendering and interaction of derivation nodes in refinement errors - -const expansionsMap = new Map>(); - -function getExpansions(errorId: string): Set { - if (!expansionsMap.has(errorId)) { - expansionsMap.set(errorId, new Set()); - } - return expansionsMap.get(errorId)!; -} - -function renderToken(token: string): string { - return renderHighlightedInlineExpression(token); -} - -function renderJsonTree( - error: RefinementMismatchError, - node: DerivationNode | undefined, - errorId: string, - path: string, - expandedPaths: Set -): string { - if (!node) - return 'undefined'; - - const hasOrigin = Boolean("origin" in node && node.origin); - const isExpanded = expandedPaths.has(path); - if (hasOrigin && isExpanded && "origin" in node) { - return renderJsonTree(error, node.origin, errorId, `${path}.origin`, expandedPaths); - } - - // VarDerivationNode - if ("var" in node) { - const classes = `node-var ${hasOrigin ? "derivable-node clickable" : ""}`.trim(); - const attrs = hasOrigin ? ` data-node-path="${path}" data-error-id="${errorId}"` : ""; - return `${renderHighlightedInlineExpression(node.var)}`; - } - - // ValDerivationNode - if ("value" in node) { - const valueNode = node as ValDerivationNode; - const valClass = typeof valueNode.value === "number" ? "node-number" : typeof valueNode.value === "boolean" ? "node-boolean" : "node-value"; - const clickableClass = hasOrigin ? "derivable-node clickable" : ""; - const pathAttr = hasOrigin ? `data-node-path="${path}"` : ""; - const idAttr = hasOrigin ? `data-error-id="${errorId}"` : ""; - return `${renderHighlightedInlineExpression(String(valueNode.value))}`; - } - - // BinaryDerivationNode - if ("left" in node && "right" in node) { - const leftHtml = renderJsonTree(error, node.left, errorId, `${path}.left`, expandedPaths); - const rightHtml = renderJsonTree(error, node.right, errorId, `${path}.right`, expandedPaths); - return `${leftHtml} ${renderToken(node.op)} ${rightHtml}`; - } - - // UnaryDerivationNode - if ("operand" in node) { - const operandHtml = renderJsonTree(error, node.operand, errorId, `${path}.operand`, expandedPaths); - return node.op === "-" - ? `${renderToken(node.op)}${renderToken("(")}${operandHtml}${renderToken(")")}` - : `${renderToken(node.op)}${operandHtml}`; - } - - // IteDerivationNode - if ("condition" in node && "thenBranch" in node && "elseBranch" in node) { - const conditionHtml = renderJsonTree(error, node.condition, errorId, `${path}.condition`, expandedPaths); - const thenBranchHtml = renderJsonTree(error, node.thenBranch, errorId, `${path}.thenBranch`, expandedPaths); - const elseBranchHtml = renderJsonTree(error, node.elseBranch, errorId, `${path}.elseBranch`, expandedPaths); - return `${conditionHtml} ${renderToken("?")} ${thenBranchHtml} ${renderToken(":")} ${elseBranchHtml}`; - } - - // fallback - return `${escapeHtml(JSON.stringify(node))}`; -} - -function hashError(error: LJError, scope: string): string { - const content = `${error.title}|${error.message}|${error.file}|${error.position?.lineStart ?? 0}|${scope}`; - let hash = 0; - for (let i = 0; i < content.length; i++) { - const char = content.charCodeAt(i); - hash = ((hash << 5) - hash) + char; - hash = hash & hash; // Convert to 32bit integer - } - return `error_${Math.abs(hash)}`; -} - -export function handleDerivableNodeClick(target?: any): boolean { - if (!target) return false; - - const nodePath = target.getAttribute("data-node-path"); - const errorId = target.getAttribute("data-error-id"); - if (nodePath && errorId !== null) { - const paths = getExpansions(errorId); - if (!paths.has(nodePath)) { - paths.add(nodePath); - } - return true; - } - return false; -} - -export function handleDerivationResetClick(target?: any): boolean { - if (!target) return false; - - const errorId = target.getAttribute("data-error-id"); - if (errorId !== null) { - expansionsMap.delete(errorId); - return true; - } - return false; -} - -export function renderDerivationNode( - 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); - const expansions = getExpansions(errorId); - return /*html*/ ` -
-
- ${renderJsonTree(error, node, errorId, "root", expansions)} -
- -
- `; -} diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index e042d1e..5035baf 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -1,4 +1,5 @@ import { LJDiagnostic, LJError, LJWarning } from "../../../types/diagnostics"; +import type { VCImplication, VCSimplificationResult } from "../../../types/vc-implications"; import { copyToClipboard } from "../../clipboard"; import { renderCodiconButton } from "../../icons"; import { renderErrors } from "./errors"; @@ -106,13 +107,35 @@ function formatClipboardValue(value: unknown): string { return values.some(v => v.includes('\n')) ? `\n${values.join('\n')}` : values.join(', '); } - if (typeof value === 'object' && 'value' in value) { - return formatClipboardValue((value as { value: unknown }).value); - } + if (isVCSimplificationResult(value)) return formatVCImplication(value.implication); + if (isVCImplication(value)) return formatVCImplication(value); return JSON.stringify(value); } +function isVCSimplificationResult(value: unknown): value is VCSimplificationResult { + return typeof value === 'object' + && value !== null + && 'implication' in value + && 'origin' in value; +} + +function isVCImplication(value: unknown): value is VCImplication { + return typeof value === 'object' + && value !== null + && 'predicate' in value + && 'next' in value; +} + +function formatVCImplication(node: VCImplication | null): string { + if (!node) return ''; + + const binder = node.name !== null && node.type !== null ? `∀${node.name}:${node.type}, ` : ''; + const current = `${binder}${node.predicate}`; + const next = formatVCImplication(node.next); + return next ? `${current}\n=> ${next}` : current; +} + function formatDiagnosticLocation(diagnostic: LJDiagnostic): string { if (!diagnostic.file || !diagnostic.position) return ''; diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index b3d0704..c777a32 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -1,5 +1,5 @@ import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton } from "../sections"; -import { renderDerivationNode } from "./derivation-nodes"; +import { renderVCImplication } from "./vc-implications"; import type { ArgumentMismatchError, CustomError, @@ -34,13 +34,13 @@ type ErrorRendererMap = { [E in LJError as E['type']]: (error: E) => string }; const errorContentRenderers: ErrorRendererMap = { 'refinement-error': (e: RefinementError) => /*html*/ ` - ${renderCustomSection('Expected', renderDerivationNode(e, e.expected, 'expected'))} - ${renderCustomSection('Found', renderDerivationNode(e, e.found, 'found'))} + ${renderExpressionSection('Expected', e.expected)} + ${renderCustomSection('Found', renderVCImplication(e, e.found))} ${e.counterexample ? renderExpressionSection('Counterexample', e.counterexample) : ''} `, 'state-refinement-error': (e: StateRefinementError) => /*html*/ ` - ${renderCustomSection('Expected', renderDerivationNode(e, e.expected, 'expected'))} - ${renderCustomSection('Found', renderDerivationNode(e, e.found, 'found'))} + ${renderExpressionSection('Expected', e.expected)} + ${renderCustomSection('Found', renderVCImplication(e, e.found))} `, 'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/ ` ${renderExpressionSection('Refinement', e.refinement)} diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts new file mode 100644 index 0000000..848220b --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -0,0 +1,73 @@ +import type { RefinementMismatchError } from "../../../types/diagnostics"; +import type { VCImplication, VCSimplificationResult } from "../../../types/vc-implications"; +import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../../highlighting"; +import { renderCodicon } from "../../icons"; +import { escapeHtml } from "../../utils"; + +const stepIndexes = new Map(); // step index => errorId to preserve step state across re-renders + +function renderImplication(node: VCImplication): string { + const lines: string[] = []; + + for (let current: VCImplication | null = node; current; current = current.next) { + const binder = current.name !== null && current.type !== null; + if (!binder && current.next || current.predicate === "true" && current.next !== null) continue; + + const content = /*binder + ? `∀${escapeHtml(current.name!)}: ${escapeHtml(current.type!)}. ${renderHighlightedInlineExpression(current.predicate)}` + :*/ renderHighlightedInlineExpression(current.predicate); + lines.push(`
${content}
`); + } + + return lines.join(""); +} + +function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string { + const label = `${step === "previous" ? "Previous" : "Next"} simplification`; + const icon = step === "previous" ? "arrow-small-left" : "arrow-small-right"; + return ``; +} + +export function handleVCImplicationStepClick(target: Element): boolean { + const errorId = target.getAttribute("data-error-id"); + const step = target.getAttribute("data-vc-step"); + if (!errorId || target.hasAttribute("disabled")) return false; + + const index = stepIndexes.get(errorId) ?? 0; + const nextIndex = step === "previous" ? index + 1 : step === "next" ? index - 1 : -1; + if (nextIndex < 0) return false; + + stepIndexes.set(errorId, nextIndex); + return true; +} + +export function renderVCImplication( + error: RefinementMismatchError, + result: VCSimplificationResult +): string { + if (!result?.implication) return renderHighlightedExpression(String(result)); + + const errorId = encodeURIComponent(JSON.stringify([ + error.file, + error.position?.lineStart, + error.title, + error.message + ])); + const history: VCSimplificationResult[] = []; + for (let current: VCSimplificationResult | null = result; current; current = current.origin) { + history.push(current); + } + + const index = Math.min(stepIndexes.get(errorId) ?? 0, history.length - 1); + stepIndexes.set(errorId, index); + + return /*html*/ ` +
+
${renderImplication(history[index].implication)}
+
+ ${renderStepButton(errorId, "previous", index === history.length - 1)} + ${renderStepButton(errorId, "next", index === 0)} +
+
+ `; +} diff --git a/server/pom.xml b/server/pom.xml index 640a129..d4ba04d 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -172,7 +172,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.25 + 0.0.26 tools.aqua diff --git a/server/src/main/java/dtos/diagnostics/RefinementDTO.java b/server/src/main/java/dtos/diagnostics/RefinementDTO.java new file mode 100644 index 0000000..5489f40 --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/RefinementDTO.java @@ -0,0 +1,17 @@ +package dtos.diagnostics; + +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; + +/** + * DTO for serializing refinement predicates. + */ +public record RefinementDTO(String predicate) { + + public static RefinementDTO from(Predicate refinement) { + if (refinement == null) + return null; + + return new RefinementDTO(ExpressionFormatter.format(refinement)); + } +} diff --git a/server/src/main/java/dtos/diagnostics/VCBinderDTO.java b/server/src/main/java/dtos/diagnostics/VCBinderDTO.java new file mode 100644 index 0000000..8002743 --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/VCBinderDTO.java @@ -0,0 +1,20 @@ +package dtos.diagnostics; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.utils.Utils; + +/** + * DTO for serializing the binder part of a VC implication node. + */ +public record VCBinderDTO(String name, String type) { + + public static VCBinderDTO from(VCImplication implication) { + if (implication == null || !implication.hasBinder()) + return null; + + String qualifiedType = implication.getType().getQualifiedName(); + String simpleType = qualifiedType.contains(".") ? Utils.getSimpleName(qualifiedType) : qualifiedType; + return new VCBinderDTO(VariableFormatter.format(implication.getName()), simpleType); + } +} diff --git a/server/src/main/java/dtos/diagnostics/VCImplicationDTO.java b/server/src/main/java/dtos/diagnostics/VCImplicationDTO.java new file mode 100644 index 0000000..4bc76f4 --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/VCImplicationDTO.java @@ -0,0 +1,28 @@ +package dtos.diagnostics; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.utils.Utils; + +/** + * DTO for serializing a complete VC implication chain. + */ +public record VCImplicationDTO(String name, String type, String predicate, VCImplicationDTO next) { + + public static VCImplicationDTO from(VCImplication implication) { + if (implication == null) + return null; + + String name = null; + String type = null; + if (implication.hasBinder()) { + name = VariableFormatter.format(implication.getName()); + type = Utils.getSimpleName(implication.getType().getQualifiedName()); + } + return new VCImplicationDTO( + name, + type, + implication.getRefinement().getExpression().toDisplayString(), + from(implication.getNext())); + } +} diff --git a/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java new file mode 100644 index 0000000..155c3ac --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java @@ -0,0 +1,18 @@ +package dtos.diagnostics; + +import liquidjava.rj_language.opt.VCSimplificationResult; + +/** + * DTO for serializing a simplified VC and its complete predecessor states. + */ +public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin) { + + public static VCSimplificationResultDTO from(VCSimplificationResult result) { + if (result == null) + return null; + + return new VCSimplificationResultDTO( + VCImplicationDTO.from(result.getImplication()), + from(result.getOrigin())); + } +} diff --git a/server/src/main/java/dtos/errors/RefinementErrorDTO.java b/server/src/main/java/dtos/errors/RefinementErrorDTO.java index 196befa..599fd21 100644 --- a/server/src/main/java/dtos/errors/RefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/RefinementErrorDTO.java @@ -1,22 +1,23 @@ package dtos.errors; +import dtos.diagnostics.VCSimplificationResultDTO; import liquidjava.diagnostics.errors.RefinementError; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; /** * DTO for serializing RefinementError instances to JSON */ public class RefinementErrorDTO extends LJErrorDTO { - public final ValDerivationNode expected; - public final ValDerivationNode found; + public final String expected; + public final VCSimplificationResultDTO found; public final String customMessage; public final String counterexample; public RefinementErrorDTO(RefinementError error) { super("refinement-error", error); - this.expected = error.getExpected(); - this.found = error.getFound(); + this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected()); + this.found = VCSimplificationResultDTO.from(error.getFound()); this.customMessage = error.getCustomMessage(); this.counterexample = error.getCounterExampleString(); } diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index ab1a217..a985e2f 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java @@ -1,21 +1,22 @@ package dtos.errors; +import dtos.diagnostics.VCSimplificationResultDTO; import liquidjava.diagnostics.errors.StateRefinementError; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; /** * DTO for serializing StateRefinementError instances to JSON */ public class StateRefinementErrorDTO extends LJErrorDTO { - public final ValDerivationNode expected; - public final ValDerivationNode found; + public final String expected; + public final VCSimplificationResultDTO found; public final String customMessage; public StateRefinementErrorDTO(StateRefinementError error) { super("state-refinement-error", error); - this.expected = error.getExpected(); - this.found = error.getFound(); + this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected()); + this.found = VCSimplificationResultDTO.from(error.getFoundSimplification()); this.customMessage = error.getCustomMessage(); }