diff --git a/client/package-lock.json b/client/package-lock.json index 6a7e976b..9be232b1 100644 --- a/client/package-lock.json +++ b/client/package-lock.json @@ -1,12 +1,12 @@ { "name": "liquid-java", - "version": "0.0.88", + "version": "0.0.90", "lockfileVersion": 2, "requires": true, "packages": { "": { "name": "liquid-java", - "version": "0.0.88", + "version": "0.0.90", "license": "MIT", "dependencies": { "@vscode/codicons": "^0.0.45" diff --git a/client/package.json b/client/package.json index c972394a..3f9b7ce5 100644 --- a/client/package.json +++ b/client/package.json @@ -2,7 +2,7 @@ "name": "liquid-java", "displayName": "LiquidJava", "description": "Extending Java with Liquid Types", - "version": "0.0.88", + "version": "0.0.90", "publisher": "AlcidesFonseca", "repository": { "type": "git", diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts index 0300adf4..787f6567 100644 --- a/client/src/services/webview.ts +++ b/client/src/services/webview.ts @@ -9,6 +9,7 @@ import type { DiagnosticRevealTarget } from "../types/diagnostics"; */ export function registerWebview(context: vscode.ExtensionContext) { extension.webview = new LiquidJavaWebviewProvider(context.extensionUri); + let pendingDiagnosticReveal: DiagnosticRevealTarget | undefined; // webview provider context.subscriptions.push( @@ -17,8 +18,15 @@ export function registerWebview(context: vscode.ExtensionContext) { // show view command context.subscriptions.push( vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget) => { + const isVisible = extension.webview?.isVisible(); await vscode.commands.executeCommand("liquidJavaView.focus"); - if (diagnostic) extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic }); + if (!diagnostic) return; + + if (isVisible) { + extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic }); + } else { + pendingDiagnosticReveal = diagnostic; + } }) ); // listen for messages from the webview @@ -30,6 +38,10 @@ export function registerWebview(context: vscode.ExtensionContext) { if (extension.context) extension.webview?.sendMessage({ type: "context", context: extension.context , errorAtCursor: extension.errorAtCursor }); if (extension.stateMachine) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine }); if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status }); + if (pendingDiagnosticReveal) { + extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic: pendingDiagnosticReveal }); + pendingDiagnosticReveal = undefined; + } } }) ); diff --git a/client/src/types/derivation-nodes.ts b/client/src/types/derivation-nodes.ts deleted file mode 100644 index f06386c6..00000000 --- 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 4d518193..1ed3f32f 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 @@ -25,6 +25,7 @@ export type LJWarning = CustomWarning | ExternalClassNotFoundWarning | ExternalM type BaseDiagnostic = { title: string; message: string; + details: string; file: string; position: SourcePosition | null; } @@ -57,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; } @@ -74,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 00000000..a6750edb --- /dev/null +++ b/client/src/types/vc-implications.ts @@ -0,0 +1,12 @@ +export type VCImplication = { + name: string | null; + type: string | null; + predicate: string; + next: VCImplication | null; +} + +export type VCSimplificationResult = { + implication: VCImplication; + origin: VCSimplificationResult | null; + simplification: string | null; +} diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 78762de1..afc428ca 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,23 +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)) { - updateView(); - } + handleVCImplicationStepClick(vcImplicationStepButton); return; } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 29f35d33..769ab1f9 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -161,7 +161,7 @@ export function getStyles(): string { } .diagnostic-item { background-color: var(--vscode-textCodeBlock-background); - padding: 0.5rem 5rem 0.5rem 1rem; + padding: 0.5rem 1rem; margin-bottom: 1rem; border-radius: 4px; position: relative; @@ -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,154 @@ export function getStyles(): string { .clickable:hover { font-weight: bold; } - .derivation-container { + .vc-container { display: flex; + flex-direction: column; + gap: 0.375rem; + margin: 0.5rem 0; + } + .vc-step-header { + display: flex; + align-items: center; justify-content: space-between; + gap: 0.75rem; + min-width: 0; + padding-bottom: 0.25rem; + border-bottom: 1px solid var(--vscode-widget-border, var(--vscode-panel-border)); + font-family: var(--vscode-font-family); + font-size: 0.8rem; + line-height: 1.25rem; + } + .vc-step-name { + min-width: 0; + overflow: hidden; + color: var(--vscode-descriptionForeground); + font-weight: 600; + text-overflow: ellipsis; + white-space: nowrap; + } + .vc-step-navigation { + display: inline-flex; align-items: center; - gap: 1rem; + gap: 0.25rem; + flex-shrink: 0; + } + .vc-step-position { + min-width: 2.5rem; + color: var(--vscode-descriptionForeground); + font-variant-numeric: tabular-nums; + text-align: right; + } + .vc-chain { + display: grid; + grid-template-columns: fit-content(40%) minmax(0, 1fr); + row-gap: 0.25rem; + width: 100%; + min-width: 0; + } + .counterexample-container .vc-chain { + display: flex; + flex-direction: column; + gap: 0.25rem; + } + .counterexample-line { + overflow-wrap: anywhere; + } + .vc-line { + display: contents; } - .reset-btn { + .vc-binder-cell, + .vc-predicate-cell { + min-width: 0; + padding: 0.0625rem 0.25rem; + overflow-wrap: anywhere; + } + .vc-binder-cell { + min-height: 1.2em; + padding-right: 0.75rem; + color: var(--vscode-descriptionForeground); + white-space: normal; + } + .vc-predicate-cell { + color: var(--vscode-editor-foreground); + } + .vc-predicate-cell:only-child { + grid-column: 1 / -1; + } + .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-change-line .vc-node { + border-radius: 2px; + animation: vc-change-line-fade 1.4s ease-out; + } + .vc-change-fragment { + border-radius: 2px; + animation: vc-change-fragment-fade 1.4s ease-out; + } + @keyframes vc-change-line-fade { + 0% { + background-color: rgba(255, 255, 96, 0.68); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.38); + } + 18% { + background-color: rgba(255, 255, 0, 0.4); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.2); + } + 100% { + background-color: transparent; + box-shadow: none; + } + } + @keyframes vc-change-fragment-fade { + 0% { + background-color: rgba(255, 255, 96, 0.68); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.38); + } + 18% { + background-color: rgba(255, 255, 0, 0.4); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.2); + } + 100% { + background-color: transparent; + box-shadow: none; + } + } + @media (prefers-reduced-motion: reduce) { + .vc-change-line .vc-node { + background-color: rgba(255, 255, 0, 0.3); + animation: none; + } + .vc-change-fragment { + background-color: rgba(255, 255, 0, 0.3); + animation: 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 +480,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; + opacity: 1; background-color: transparent; } - .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 209bde8c..89324e5d 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -2,10 +2,9 @@ import { LJVariable } from "../../../types/context"; import { RefinementMismatchError } from "../../../types/diagnostics"; import { renderHighlightedInlineExpression } from "../../highlighting"; import { escapeHtml, getSimpleName } from "../../utils"; -import { renderToggleSection, renderHighlightButton, renderDiagnosticRevealButton } from "../sections"; +import { renderToggleSection, renderVariableHighlightButton, 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*/`
@@ -25,15 +24,14 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool ${variables.map(variable => { - const displayName = getSimpleName(variable.name); const isRelevant = relevantNames.has(variable.name); return /*html*/` - ${renderHighlightButton(variable.position!, displayName)} + ${renderVariableHighlightButton(variable)} ${renderHighlightedInlineExpression(variable.refinement)} `}).join('')} - ${errorAtCursor ? renderFailingRefinement(errorAtCursor, expected!) : ''} + ${errorAtCursor ? renderFailingRefinement(errorAtCursor) : ''} `: '

No variables declared at the cursor position

'} @@ -42,11 +40,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/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts new file mode 100644 index 00000000..6d80f766 --- /dev/null +++ b/client/src/webview/views/diagnostics/counterexample.ts @@ -0,0 +1,25 @@ +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 ""; + + return /*html*/` +
+
+ ${lines.map(line => /*html*/` +
+ ${renderHighlightedInlineExpression(line)} +
+ `).join("")} +
+
+ `; +} 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 b755cb58..00000000 --- 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 e042d1e4..5035bafd 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 b3d07048..ac48c74d 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -1,5 +1,6 @@ import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton } from "../sections"; -import { renderDerivationNode } from "./derivation-nodes"; +import { renderCounterexample } from "./counterexample"; +import { renderVCImplication } from "./vc-implications"; import type { ArgumentMismatchError, CustomError, @@ -34,13 +35,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'))} - ${e.counterexample ? renderExpressionSection('Counterexample', e.counterexample) : ''} + ${renderExpressionSection('Expected', e.expected)} + ${renderCustomSection('Found', renderVCImplication(e, e.found))} + ${e.counterexample ? renderCustomSection('Counterexample', renderCounterexample(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-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts new file mode 100644 index 00000000..67fa0ab1 --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -0,0 +1,215 @@ +import type { VCImplication } from "../../../types/vc-implications"; +import { renderHighlightedInlineExpression } from "../../highlighting"; +import { escapeHtml } from "../../utils"; + +type ChangeKind = "unchanged" | "removed" | "added"; +type DiffOperation = { kind: ChangeKind; value: T }; + +const MIN_LINE_SIMILARITY = 0.3; +const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu; +const WHITESPACE_PATTERN = /^\s+$/u; +const VC_LINE_SEPARATOR = "\t"; + +function hasBinder(node: VCImplication): boolean { + return typeof node.name === "string" && node.name.length > 0; +} + +function formatImplicationLine(node: VCImplication): string { + const binder = hasBinder(node) ? `∀${node.name}` : ""; + const type = typeof node.type === "string" ? node.type : ""; + return [binder, type, node.predicate].join(VC_LINE_SEPARATOR); +} + +function parseImplicationLine(line: string): { binder: string; type: string; predicate: string } { + const [binder = "", type = "", predicate = ""] = line.split(VC_LINE_SEPARATOR); + return { binder, type, predicate }; +} + +function getImplicationLines(node: VCImplication): string[] { + const lines: string[] = []; + for (let current: VCImplication | null = node; current; current = current.next) { + if (current.next && !hasBinder(current)) continue; + lines.push(formatImplicationLine(current)); + } + return lines; +} + +export function renderVCLine(line: string, className = "", predicateContent?: string): string { + const { binder, type, predicate } = parseImplicationLine(line); + return /*html*/` +
+ ${binder ? /*html*/`
${escapeHtml(binder)}
` : ""} +
${predicateContent ?? renderHighlightedInlineExpression(predicate)}
+
+ `; +} + +function createMatrix(rows: number, columns: number): number[][] { + return Array.from({ length: rows + 1 }, () => new Array(columns + 1).fill(0)); +} + +function diffSequence(before: T[], after: T[]): DiffOperation[] { + const lengths = createMatrix(before.length, after.length); + + for (let beforeIndex = before.length - 1; beforeIndex >= 0; beforeIndex -= 1) { + for (let afterIndex = after.length - 1; afterIndex >= 0; afterIndex -= 1) { + lengths[beforeIndex][afterIndex] = before[beforeIndex] === after[afterIndex] + ? lengths[beforeIndex + 1][afterIndex + 1] + 1 + : Math.max(lengths[beforeIndex + 1][afterIndex], lengths[beforeIndex][afterIndex + 1]); + } + } + + const operations: DiffOperation[] = []; + let beforeIndex = 0; + let afterIndex = 0; + while (beforeIndex < before.length && afterIndex < after.length) { + if (before[beforeIndex] === after[afterIndex]) { + operations.push({ kind: "unchanged", value: before[beforeIndex] }); + beforeIndex++; + afterIndex++; + } else if (lengths[beforeIndex + 1][afterIndex] >= lengths[beforeIndex][afterIndex + 1]) { + operations.push({ kind: "removed", value: before[beforeIndex++] }); + } else { + operations.push({ kind: "added", value: after[afterIndex++] }); + } + } + operations.push( + ...before.slice(beforeIndex).map(value => ({ kind: "removed" as const, value })), + ...after.slice(afterIndex).map(value => ({ kind: "added" as const, value })), + ); + return operations; +} + +function tokenizeExpression(expression: string): string[] { + return expression.match(TOKEN_PATTERN) || []; +} + +function renderChangedFragment(content: string): string { + return `${renderHighlightedInlineExpression(content)}`; +} + +function renderDestinationTokenDiff(before: string, after: string): { content: string; hasAddedContent: boolean } { + const operations = diffSequence(tokenizeExpression(before), tokenizeExpression(after)); + let html = ""; + let changedContent = ""; + let hasAddedContent = false; + + const flushChangedContent = () => { + if (!changedContent) return; + const trailingWhitespace = changedContent.match(/\s+$/u)?.[0] ?? ""; + const content = changedContent.slice(0, changedContent.length - trailingWhitespace.length); + if (content) html += renderChangedFragment(content); + html += trailingWhitespace; + changedContent = ""; + }; + + operations.forEach((operation, index) => { + if (operation.kind === "added") { + changedContent += operation.value; + hasAddedContent = true; + return; + } + if (operation.kind === "unchanged") { + if (WHITESPACE_PATTERN.test(operation.value) && changedContent && operations[index + 1]?.kind === "added") { + changedContent += operation.value; + return; + } + flushChangedContent(); + html += renderHighlightedInlineExpression(operation.value); + } + }); + flushChangedContent(); + return { content: html, hasAddedContent }; +} + +function getLineSimilarity(before: string, after: string): number { + const beforeTokens = tokenizeExpression(before).filter(token => !WHITESPACE_PATTERN.test(token)); + const afterTokens = tokenizeExpression(after).filter(token => !WHITESPACE_PATTERN.test(token)); + const unchangedLength = diffSequence(beforeTokens, afterTokens) + .filter(operation => operation.kind === "unchanged") + .reduce((length, operation) => length + operation.value.length, 0); + const totalLength = Math.max(beforeTokens.join("").length, afterTokens.join("").length); + return totalLength === 0 ? 0 : unchangedLength / totalLength; +} + +function alignChangedLines(removed: string[], added: string[]): Array<[string | undefined, string | undefined]> { + const similarities = removed.map(before => added.map(after => getLineSimilarity(before, after))); + const scores = createMatrix(removed.length, added.length); + + for (let i = removed.length - 1; i >= 0; i -= 1) { + for (let j = added.length - 1; j >= 0; j -= 1) { + const similarity = similarities[i][j]; + scores[i][j] = Math.max( + scores[i + 1][j], + scores[i][j + 1], + similarity >= MIN_LINE_SIMILARITY ? similarity + scores[i + 1][j + 1] : 0, + ); + } + } + + const lines: Array<[string | undefined, string | undefined]> = []; + let i = 0; + let j = 0; + while (i < removed.length && j < added.length) { + const similarity = similarities[i][j]; + if ( + similarity >= MIN_LINE_SIMILARITY + && scores[i][j] === similarity + scores[i + 1][j + 1] + ) { + lines.push([removed[i++], added[j++]]); + } else if (scores[i][j + 1] >= scores[i + 1][j]) { + lines.push([undefined, added[j++]]); + } else { + lines.push([removed[i++], undefined]); + } + } + while (i < removed.length) lines.push([removed[i++], undefined]); + while (j < added.length) lines.push([undefined, added[j++]]); + return lines; +} + +function renderChangedDestinationLines(removed: string[], added: string[]): string { + if (added.length === 0) return ""; + + return alignChangedLines(removed, added) + .map(([before, after]) => { + if (after === undefined) return ""; + if (before === undefined) return renderVCLine(after, "vc-change-line"); + const change = renderDestinationTokenDiff( + parseImplicationLine(before).predicate, + parseImplicationLine(after).predicate, + ); + return renderVCLine(after, change.hasAddedContent ? "" : "vc-change-line", change.content); + }) + .join(""); +} + +export function renderImplication(node: VCImplication): string { + return getImplicationLines(node) + .map(line => renderVCLine(line)) + .join(""); +} + +export function renderImplicationChange(before: VCImplication, after: VCImplication): string { + const operations = diffSequence(getImplicationLines(before), getImplicationLines(after)); + let html = ""; + const changed = { removed: [] as string[], added: [] as string[] }; + + const flushChanges = () => { + html += renderChangedDestinationLines(changed.removed, changed.added); + changed.removed.length = 0; + changed.added.length = 0; + }; + + for (const operation of operations) { + if (operation.kind === "unchanged") { + flushChanges(); + html += renderVCLine(operation.value); + continue; + } + changed[operation.kind].push(operation.value); + } + + flushChanges(); + return html; +} 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 00000000..c2b76e61 --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -0,0 +1,111 @@ +import type { RefinementMismatchError } from "../../../types/diagnostics"; +import type { VCSimplificationResult } from "../../../types/vc-implications"; +import { renderHighlightedExpression } from "../../highlighting"; +import { renderCodicon } from "../../icons"; +import { escapeHtml } from "../../utils"; +import { renderImplication, renderImplicationChange } from "./vc-changes"; + +const stepIndexes = new Map(); // errorId => step index, preserved across re-renders +const simplificationSteps = new Map(); // errorId => simplification steps + +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 ``; +} + +function renderStepHeader( + errorId: string, + current: VCSimplificationResult, + index: number, + stepCount: number, +): string { + const currStep = stepCount - index; + const simplification = current.simplification?.trim(); + const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original"); + + return /*html*/` +
+ ${label} +
+ + ${currStep}/${stepCount} + +
+ ${renderStepButton(errorId, "previous", index === stepCount - 1)} + ${renderStepButton(errorId, "next", index === 0)} +
+
+
+ `; +} + +function getTargetStepIndex(errorId: string, step: string | null): number | undefined { + const steps = simplificationSteps.get(errorId); + if (!steps) return; + + const index = stepIndexes.get(errorId) ?? 0; + const targetIndex = step === "previous" ? index + 1 : step === "next" ? index - 1 : -1; + if (targetIndex < 0 || targetIndex >= steps.length) return; + return targetIndex; +} + +function renderSelectedStep(errorId: string, previousIndex?: number): string { + const steps = simplificationSteps.get(errorId); + if (!steps) return ""; + + const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1); + const current = steps[index]; + const previous = previousIndex === undefined ? undefined : steps[previousIndex]; + const implication = previous + ? `
${renderImplicationChange(previous.implication, current.implication)}
` + : `
${renderImplication(current.implication)}
`; + + return /*html*/` + ${steps.length > 1 ? renderStepHeader(errorId, current, index, steps.length) : ""} + ${implication} + `; +} + +export function handleVCImplicationStepClick(target: Element): boolean { + const errorId = target.getAttribute("data-error-id"); + const step = target.getAttribute("data-vc-step"); + if (!errorId || (target as HTMLButtonElement).disabled) return false; + + const currentIndex = stepIndexes.get(errorId) ?? 0; + const targetIndex = getTargetStepIndex(errorId, step); + const container = target.closest?.(".vc-container"); + if (targetIndex === undefined) return false; + + stepIndexes.set(errorId, targetIndex); + if (container) container.innerHTML = renderSelectedStep(errorId, currentIndex); + 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 steps: VCSimplificationResult[] = []; + for (let current: VCSimplificationResult | null = result; current; current = current.origin) { + steps.push(current); + } + simplificationSteps.set(errorId, steps); + + const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1); + stepIndexes.set(errorId, index); + + return /*html*/ ` +
+ ${renderSelectedStep(errorId)} +
+ `; +} diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index fba3f274..2b8c16e3 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -1,8 +1,9 @@ import type { LJDiagnostic, SourcePosition } from "../../types/diagnostics"; -import { escapeHtml } from "../utils"; +import { escapeHtml, getSimpleName } from "../utils"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; import { renderCodicon, renderCodiconButton } from "../icons"; +import { LJVariable } from "../../types/context"; export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
@@ -40,17 +41,21 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => { return renderCustomSection("Location", /*html*/`
${renderLocationLink(diagnostic.position)}
`); }; -export function renderHighlightButton(position: SourcePosition, content: string, error: boolean = false): string { +export function renderVariableHighlightButton(variable: LJVariable): string { + const displayName = getSimpleName(variable.name); + const position = variable.position; + if (!position || !position.file) return `${displayName}`; return /*html*/` `; } diff --git a/server/pom.xml b/server/pom.xml index 640a1298..a4ccaac8 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -172,7 +172,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.25 + 0.0.28 tools.aqua diff --git a/server/src/main/java/LJDiagnosticsService.java b/server/src/main/java/LJDiagnosticsService.java index 35397ab7..6ee9ed79 100644 --- a/server/src/main/java/LJDiagnosticsService.java +++ b/server/src/main/java/LJDiagnosticsService.java @@ -29,6 +29,7 @@ public class LJDiagnosticsService implements TextDocumentService, WorkspaceServi private LJLanguageClient client; private String workspaceRoot; + private boolean initialVerification; private final Set publishedDiagnosticUris = new HashSet<>(); private final ExecutorService diagnosticsExecutor = Executors.newSingleThreadExecutor(r -> { Thread thread = new Thread(r, "liquidjava-diagnostics"); @@ -120,14 +121,15 @@ private void clearPublishedDiagnostics(String uri) { } /** - * Checks diagnostics when a document is opened + * Checks diagnostics when the first document is opened * @param params */ @Override public void didOpen(DidOpenTextDocumentParams params) { String uri = params.getTextDocument().getUri(); - if (!PathUtils.isFileInDirectory(uri, workspaceRoot)) return; - System.out.println("Document opened — checking diagnostics"); + if (!PathUtils.isFileInDirectory(uri, workspaceRoot) || initialVerification) return; + initialVerification = true; + System.out.println("First document opened — checking diagnostics"); generateDiagnosticsAsync(uri); } diff --git a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java index 7ae1de37..83d8d88d 100644 --- a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java +++ b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java @@ -5,10 +5,33 @@ /** * DTO for serializing LJDiagnostic instances to JSON */ -public record LJDiagnosticDTO(String title, String message, String details, String file, SourcePositionDTO position) { +public class LJDiagnosticDTO { - public static LJDiagnosticDTO from(LJDiagnostic diagnostic) { - return new LJDiagnosticDTO(diagnostic.getTitle(), diagnostic.getMessage(), diagnostic.getDetails(), + public final String category; + public final String type; + public final String title; + public final String message; + public final String details; + public final String file; + public final SourcePositionDTO position; + + public LJDiagnosticDTO(String category, String type, LJDiagnostic diagnostic) { + this(category, type, diagnostic.getTitle(), diagnostic.getMessage(), diagnostic.getDetails(), diagnostic.getFile(), SourcePositionDTO.from(diagnostic.getPosition())); } + + public LJDiagnosticDTO(String category, String type, String title, String message, String details, String file, + SourcePositionDTO position) { + this.category = category; + this.type = type; + this.title = title; + this.message = message; + this.details = details; + this.file = file; + this.position = position; + } + + public static LJDiagnosticDTO from(LJDiagnostic diagnostic) { + return new LJDiagnosticDTO(null, null, diagnostic); + } } 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 00000000..5489f40e --- /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 00000000..80027434 --- /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 00000000..4bc76f4b --- /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 00000000..0dc9d262 --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java @@ -0,0 +1,20 @@ +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, String simplification) { + + public static VCSimplificationResultDTO from(VCSimplificationResult result) { + if (result == null) + return null; + + return new VCSimplificationResultDTO( + VCImplicationDTO.from(result.getImplication()), + from(result.getOrigin()), + result.getSimplification() + ); + } +} diff --git a/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java b/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java index 710520c6..6f700b00 100644 --- a/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java +++ b/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java @@ -1,16 +1,17 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.errors.ArgumentMismatchError; /** * DTO for serializing ArgumentMismatchErrorDTO instances to JSON */ -public record ArgumentMismatchErrorDTO(String category, String type, String title, String message, String file, - SourcePositionDTO position) { +public class ArgumentMismatchErrorDTO extends LJErrorDTO { + + public ArgumentMismatchErrorDTO(ArgumentMismatchError error) { + super("argument-mismatch-error", error); + } public static ArgumentMismatchErrorDTO from(ArgumentMismatchError error) { - return new ArgumentMismatchErrorDTO("error", "argument-mismatch-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition())); + return new ArgumentMismatchErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/CustomErrorDTO.java b/server/src/main/java/dtos/errors/CustomErrorDTO.java index 38b4e048..e8c48d25 100644 --- a/server/src/main/java/dtos/errors/CustomErrorDTO.java +++ b/server/src/main/java/dtos/errors/CustomErrorDTO.java @@ -1,15 +1,17 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.errors.CustomError; /** * DTO for serializing CustomError instances to JSON */ -public record CustomErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position) { +public class CustomErrorDTO extends LJErrorDTO { + + public CustomErrorDTO(CustomError error) { + super("custom-error", error); + } public static CustomErrorDTO from(CustomError error) { - return new CustomErrorDTO("error", "custom-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition())); + return new CustomErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java b/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java index d2695f6e..08af9829 100644 --- a/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java +++ b/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java @@ -1,16 +1,17 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.errors.IllegalConstructorTransitionError; /** * DTO for serializing IllegalConstructorTransitionError instances to JSON */ -public record IllegalConstructorTransitionErrorDTO(String category, String type, String title, String message, String file, - SourcePositionDTO position) { +public class IllegalConstructorTransitionErrorDTO extends LJErrorDTO { + + public IllegalConstructorTransitionErrorDTO(IllegalConstructorTransitionError error) { + super("illegal-constructor-transition-error", error); + } public static IllegalConstructorTransitionErrorDTO from(IllegalConstructorTransitionError error) { - return new IllegalConstructorTransitionErrorDTO("error", "illegal-constructor-transition-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition())); + return new IllegalConstructorTransitionErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java b/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java index a669da4e..7e745d48 100644 --- a/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java @@ -1,16 +1,20 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.errors.InvalidRefinementError; /** * DTO for serializing InvalidRefinementError instances to JSON */ -public record InvalidRefinementErrorDTO(String category, String type, String title, String message, String file, - SourcePositionDTO position, String refinement) { +public class InvalidRefinementErrorDTO extends LJErrorDTO { + + public final String refinement; + + public InvalidRefinementErrorDTO(InvalidRefinementError error) { + super("invalid-refinement-error", error); + this.refinement = error.getRefinement(); + } public static InvalidRefinementErrorDTO from(InvalidRefinementError error) { - return new InvalidRefinementErrorDTO("error", "invalid-refinement-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition()), error.getRefinement()); + return new InvalidRefinementErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/LJErrorDTO.java b/server/src/main/java/dtos/errors/LJErrorDTO.java index 67c0865d..82efc118 100644 --- a/server/src/main/java/dtos/errors/LJErrorDTO.java +++ b/server/src/main/java/dtos/errors/LJErrorDTO.java @@ -1,5 +1,6 @@ package dtos.errors; +import dtos.diagnostics.LJDiagnosticDTO; import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.TranslationTableDTO; import liquidjava.diagnostics.errors.LJError; @@ -7,11 +8,27 @@ /** * DTO for serializing LJError instances to JSON */ -public record LJErrorDTO(String title, String message, String file, SourcePositionDTO position, - TranslationTableDTO translationTable) { +public class LJErrorDTO extends LJDiagnosticDTO { + + public final TranslationTableDTO translationTable; + + public LJErrorDTO(String type, LJError error) { + super("error", type, error); + this.translationTable = TranslationTableDTO.from(error.getTranslationTable()); + } + + protected LJErrorDTO(String category, String type, LJError error) { + super(category, type, error); + this.translationTable = TranslationTableDTO.from(error.getTranslationTable()); + } + + public LJErrorDTO(String category, String type, String title, String message, String details, String file, + SourcePositionDTO position, TranslationTableDTO translationTable) { + super(category, type, title, message, details, file, position); + this.translationTable = translationTable; + } public static LJErrorDTO from(LJError error) { - return new LJErrorDTO(error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable())); + return new LJErrorDTO(null, error); } } diff --git a/server/src/main/java/dtos/errors/NotFoundErrorDTO.java b/server/src/main/java/dtos/errors/NotFoundErrorDTO.java index bc8ae7a3..72f0cf94 100644 --- a/server/src/main/java/dtos/errors/NotFoundErrorDTO.java +++ b/server/src/main/java/dtos/errors/NotFoundErrorDTO.java @@ -1,17 +1,22 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; -import dtos.diagnostics.TranslationTableDTO; import liquidjava.diagnostics.errors.NotFoundError; /** * DTO for serializing NotFoundError instances to JSON */ -public record NotFoundErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position, - TranslationTableDTO translationTable, String name, String kind) { +public class NotFoundErrorDTO extends LJErrorDTO { + + public final String name; + public final String kind; + + public NotFoundErrorDTO(NotFoundError error) { + super("not-found-error", error); + this.name = error.getName(); + this.kind = error.getKind(); + } public static NotFoundErrorDTO from(NotFoundError error) { - return new NotFoundErrorDTO("error", "not-found-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getName(), error.getKind()); + return new NotFoundErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/RefinementErrorDTO.java b/server/src/main/java/dtos/errors/RefinementErrorDTO.java index 18f1d7af..599fd21f 100644 --- a/server/src/main/java/dtos/errors/RefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/RefinementErrorDTO.java @@ -1,18 +1,28 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; -import dtos.diagnostics.TranslationTableDTO; +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 record RefinementErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position, - TranslationTableDTO translationTable, ValDerivationNode expected, ValDerivationNode found, String customMessage, String counterexample) { +public class RefinementErrorDTO extends LJErrorDTO { + + 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() == null ? null : ExpressionFormatter.format(error.getExpected()); + this.found = VCSimplificationResultDTO.from(error.getFound()); + this.customMessage = error.getCustomMessage(); + this.counterexample = error.getCounterExampleString(); + } public static RefinementErrorDTO from(RefinementError error) { - return new RefinementErrorDTO("error", "refinement-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(), error.getFound(), error.getCustomMessage(), error.getCounterExampleString()); + return new RefinementErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/StateConflictErrorDTO.java b/server/src/main/java/dtos/errors/StateConflictErrorDTO.java index 402e1bd4..db58642c 100644 --- a/server/src/main/java/dtos/errors/StateConflictErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateConflictErrorDTO.java @@ -1,17 +1,20 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; -import dtos.diagnostics.TranslationTableDTO; import liquidjava.diagnostics.errors.StateConflictError; /** * DTO for serializing StateConflictError instances to JSON */ -public record StateConflictErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position, - TranslationTableDTO translationTable, String state) { +public class StateConflictErrorDTO extends LJErrorDTO { + + public final String state; + + public StateConflictErrorDTO(StateConflictError error) { + super("state-conflict-error", error); + this.state = error.getState(); + } public static StateConflictErrorDTO from(StateConflictError error) { - return new StateConflictErrorDTO("error", "state-conflict-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getState()); + return new StateConflictErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index efcf369f..a985e2fe 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java @@ -1,19 +1,26 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; -import dtos.diagnostics.TranslationTableDTO; +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 record StateRefinementErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position, - TranslationTableDTO translationTable, ValDerivationNode expected, ValDerivationNode found, String customMessage) { +public class StateRefinementErrorDTO extends LJErrorDTO { + + 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() == null ? null : ExpressionFormatter.format(error.getExpected()); + this.found = VCSimplificationResultDTO.from(error.getFoundSimplification()); + this.customMessage = error.getCustomMessage(); + } public static StateRefinementErrorDTO from(StateRefinementError error) { - return new StateRefinementErrorDTO("error", "state-refinement-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(), - error.getFound(), error.getCustomMessage()); + return new StateRefinementErrorDTO(error); } } diff --git a/server/src/main/java/dtos/errors/SyntaxErrorDTO.java b/server/src/main/java/dtos/errors/SyntaxErrorDTO.java index e4268232..e08cd84d 100644 --- a/server/src/main/java/dtos/errors/SyntaxErrorDTO.java +++ b/server/src/main/java/dtos/errors/SyntaxErrorDTO.java @@ -1,16 +1,20 @@ package dtos.errors; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.errors.SyntaxError; /** * DTO for serializing SyntaxError instances to JSON */ -public record SyntaxErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position, - String refinement) { +public class SyntaxErrorDTO extends LJErrorDTO { + + public final String refinement; + + public SyntaxErrorDTO(SyntaxError error) { + super("syntax-error", error); + this.refinement = error.getRefinement(); + } public static SyntaxErrorDTO from(SyntaxError error) { - return new SyntaxErrorDTO("error", "syntax-error", error.getTitle(), error.getMessage(), error.getFile(), - SourcePositionDTO.from(error.getPosition()), error.getRefinement()); + return new SyntaxErrorDTO(error); } } diff --git a/server/src/main/java/dtos/warnings/CustomWarningDTO.java b/server/src/main/java/dtos/warnings/CustomWarningDTO.java index 5e021224..740351e4 100644 --- a/server/src/main/java/dtos/warnings/CustomWarningDTO.java +++ b/server/src/main/java/dtos/warnings/CustomWarningDTO.java @@ -1,15 +1,17 @@ package dtos.warnings; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.warnings.CustomWarning; /** * DTO for serializing CustomError instances to JSON */ -public record CustomWarningDTO(String category, String type, String title, String message, String file, SourcePositionDTO position) { +public class CustomWarningDTO extends LJWarningDTO { + + public CustomWarningDTO(CustomWarning warning) { + super("custom-warning", warning); + } public static CustomWarningDTO from(CustomWarning warning) { - return new CustomWarningDTO("warning", "custom-warning", warning.getTitle(), warning.getMessage(), warning.getFile(), - SourcePositionDTO.from(warning.getPosition())); + return new CustomWarningDTO(warning); } } diff --git a/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java b/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java index 36a0d86f..e380c31e 100644 --- a/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java +++ b/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java @@ -1,16 +1,20 @@ package dtos.warnings; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; /** * DTO for serializing ExternalClassNotFoundWarning instances to JSON */ -public record ExternalClassNotFoundWarningDTO(String category, String type, String title, String message, String file, - SourcePositionDTO position, String className) { +public class ExternalClassNotFoundWarningDTO extends LJWarningDTO { + + public final String className; + + public ExternalClassNotFoundWarningDTO(ExternalClassNotFoundWarning warning) { + super("external-class-not-found-warning", warning); + this.className = warning.getClassName(); + } public static ExternalClassNotFoundWarningDTO from(ExternalClassNotFoundWarning warning) { - return new ExternalClassNotFoundWarningDTO("warning", "external-class-not-found-warning", warning.getTitle(), warning.getMessage(), warning.getFile(), - SourcePositionDTO.from(warning.getPosition()), warning.getClassName()); + return new ExternalClassNotFoundWarningDTO(warning); } } diff --git a/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java b/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java index 495d198a..c5d695d5 100644 --- a/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java +++ b/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java @@ -1,16 +1,24 @@ package dtos.warnings; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; /** * DTO for serializing ExternalMethodNotFoundWarning instances to JSON */ -public record ExternalMethodNotFoundWarningDTO(String category, String type, String title, String message, String file, - SourcePositionDTO position, String signature, String className, String[] overloads) { +public class ExternalMethodNotFoundWarningDTO extends LJWarningDTO { + + public final String signature; + public final String className; + public final String[] overloads; + + public ExternalMethodNotFoundWarningDTO(ExternalMethodNotFoundWarning warning) { + super("external-method-not-found-warning", warning); + this.signature = warning.getSignature(); + this.className = warning.getClassName(); + this.overloads = warning.getOverloads(); + } public static ExternalMethodNotFoundWarningDTO from(ExternalMethodNotFoundWarning warning) { - return new ExternalMethodNotFoundWarningDTO("warning", "external-method-not-found-warning", warning.getTitle(), warning.getMessage(), warning.getFile(), - SourcePositionDTO.from(warning.getPosition()), warning.getSignature(), warning.getClassName(), warning.getOverloads()); + return new ExternalMethodNotFoundWarningDTO(warning); } } diff --git a/server/src/main/java/dtos/warnings/LJWarningDTO.java b/server/src/main/java/dtos/warnings/LJWarningDTO.java index acd598ac..6e41d990 100644 --- a/server/src/main/java/dtos/warnings/LJWarningDTO.java +++ b/server/src/main/java/dtos/warnings/LJWarningDTO.java @@ -1,14 +1,22 @@ package dtos.warnings; -import dtos.diagnostics.SourcePositionDTO; +import dtos.diagnostics.LJDiagnosticDTO; import liquidjava.diagnostics.warnings.LJWarning; /** * DTO for serializing LJWarning instances to JSON */ -public record LJWarningDTO(String title, String message, String file, SourcePositionDTO position) { +public class LJWarningDTO extends LJDiagnosticDTO { + + public LJWarningDTO(String type, LJWarning warning) { + super("warning", type, warning); + } + + protected LJWarningDTO(String category, String type, LJWarning warning) { + super(category, type, warning); + } public static LJWarningDTO from(LJWarning warning) { - return new LJWarningDTO(warning.getTitle(), warning.getMessage(), warning.getFile(), SourcePositionDTO.from(warning.getPosition())); + return new LJWarningDTO(null, warning); } } diff --git a/server/src/main/java/dtos/warnings/UnsatisfiableRefinementWarningDTO.java b/server/src/main/java/dtos/warnings/UnsatisfiableRefinementWarningDTO.java index d72fb012..a127460a 100644 --- a/server/src/main/java/dtos/warnings/UnsatisfiableRefinementWarningDTO.java +++ b/server/src/main/java/dtos/warnings/UnsatisfiableRefinementWarningDTO.java @@ -1,17 +1,20 @@ package dtos.warnings; -import dtos.diagnostics.SourcePositionDTO; import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning; /** * DTO for serializing UnsatisfiableRefinementWarning instances to JSON */ -public record UnsatisfiableRefinementWarningDTO(String category, String type, String title, String message, String file, - SourcePositionDTO position, String refinement) { +public class UnsatisfiableRefinementWarningDTO extends LJWarningDTO { + + public final String refinement; + + public UnsatisfiableRefinementWarningDTO(UnsatisfiableRefinementWarning warning) { + super("unsatisfiable-refinement-warning", warning); + this.refinement = warning.getRefinement(); + } public static UnsatisfiableRefinementWarningDTO from(UnsatisfiableRefinementWarning warning) { - return new UnsatisfiableRefinementWarningDTO("warning", "unsatisfiable-refinement-warning", warning.getTitle(), - warning.getMessage(), warning.getFile(), SourcePositionDTO.from(warning.getPosition()), - warning.getRefinement()); + return new UnsatisfiableRefinementWarningDTO(warning); } } diff --git a/server/src/main/java/fsm/StateMachineParser.java b/server/src/main/java/fsm/StateMachineParser.java index a8c6a9e2..5a8dfb32 100644 --- a/server/src/main/java/fsm/StateMachineParser.java +++ b/server/src/main/java/fsm/StateMachineParser.java @@ -226,9 +226,7 @@ private static List getTransitionSources(Expression expr, List return List.of(new TransitionSource(state, null)); } - if (expr instanceof GroupExpression group) { - return getTransitionSources(group.getExpression(), states, stateOnlyDisjunctions); - } else if (expr instanceof BinaryExpression bin) { + if (expr instanceof BinaryExpression bin) { String op = bin.getOperator(); if (op.equals("&&")) { return getConjunctionSources(bin, states, stateOnlyDisjunctions); @@ -369,8 +367,6 @@ private static List getStateExpressions(Expression expr, List st String state = getStateName(expr, states); if (state != null) { stateExpressions.add(state); - } else if (expr instanceof GroupExpression group) { - stateExpressions.addAll(getStateExpressions(group.getExpression(), states)); } else if (expr instanceof BinaryExpression bin) { stateExpressions.addAll(getStateExpressions(bin.getFirstOperand(), states)); stateExpressions.addAll(getStateExpressions(bin.getSecondOperand(), states));