From a8e2ab427a94ed7501481b9d3c8d494c8d1e4faf Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 26 Jun 2026 10:49:10 +0100 Subject: [PATCH 1/5] Use Table Layout for VCs --- client/src/webview/styles.ts | 31 ++++++++----- .../webview/views/diagnostics/vc-changes.ts | 45 ++++++++++++++----- 2 files changed, 53 insertions(+), 23 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 2780fa5..93186c2 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -361,23 +361,32 @@ export function getStyles(): string { text-align: right; } .vc-chain { - display: flex; - flex-direction: column; - gap: 0.25rem; + display: table; + width: 100%; + border-spacing: 0 0.25rem; min-width: 0; } .vc-line { - display: flex; - align-items: flex-start; - gap: 0.5rem; - min-width: 0; - padding: 0.0625rem 0.25rem; - border-radius: 3px; + display: table-row; } - .vc-line-content { - flex: 0 1 auto; + .vc-binder-cell, + .vc-predicate-cell { + display: table-cell; min-width: 0; + padding: 0.0625rem 0.25rem; overflow-wrap: anywhere; + vertical-align: top; + } + .vc-binder-cell { + min-height: 1.2em; + padding-right: 0.75rem; + color: var(--vscode-descriptionForeground); + white-space: nowrap; + width: 1%; + } + .vc-predicate-cell { + color: var(--vscode-editor-foreground); + width: 99%; } .vc-node { display: inline; diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 928f14c..c026a57 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -1,5 +1,6 @@ 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 }; @@ -7,23 +8,40 @@ 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 - && (current.name === null || current.type === null || current.predicate === "true") - ) continue; - lines.push(current.predicate); + if (current.next && !hasBinder(current)) continue; + lines.push(formatImplicationLine(current)); } return lines; } -function renderVCLine(content: string, className = ""): string { +function renderVCLine(line: string, className = "", predicateContent?: string): string { + const { binder, type, predicate } = parseImplicationLine(line); + const title = binder && type ? ` title="${escapeHtml(`${binder.slice(1)}: ${type}`)}"` : ""; + return /*html*/`
-
${content}
+
${escapeHtml(binder)}
+
${predicateContent ?? renderHighlightedInlineExpression(predicate)}
`; } @@ -158,16 +176,19 @@ function renderChangedDestinationLines(removed: string[], added: string[]): stri return alignChangedLines(removed, added) .map(([before, after]) => { if (after === undefined) return ""; - if (before === undefined) return renderVCLine(renderChangedFragment(after)); - const change = renderDestinationTokenDiff(before, after); - return renderVCLine(change.content, change.hasAddedContent ? "" : "vc-change-line"); + 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(predicate => renderVCLine(renderHighlightedInlineExpression(predicate))) + .map(line => renderVCLine(line)) .join(""); } @@ -185,7 +206,7 @@ export function renderImplicationChange(before: VCImplication, after: VCImplicat for (const operation of operations) { if (operation.kind === "unchanged") { flushChanges(); - html += renderVCLine(renderHighlightedInlineExpression(operation.value)); + html += renderVCLine(operation.value); continue; } changed[operation.kind].push(operation.value); From 47c7b76c347733291e9acc5311505589e6a496f8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 26 Jun 2026 11:08:47 +0100 Subject: [PATCH 2/5] Show Binder Type on Hover --- client/src/webview/views/diagnostics/vc-changes.ts | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index c026a57..611d26c 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -36,11 +36,9 @@ function getImplicationLines(node: VCImplication): string[] { function renderVCLine(line: string, className = "", predicateContent?: string): string { const { binder, type, predicate } = parseImplicationLine(line); - const title = binder && type ? ` title="${escapeHtml(`${binder.slice(1)}: ${type}`)}"` : ""; - return /*html*/`
-
${escapeHtml(binder)}
+
${escapeHtml(binder)}
${predicateContent ?? renderHighlightedInlineExpression(predicate)}
`; From b657d6313e9d3307867c51f6c01f860b30b7006e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 25 Jun 2026 10:36:08 +0100 Subject: [PATCH 3/5] Display Counterexample Assignments by Line --- .../views/diagnostics/counterexample.ts | 22 +++++++++++++++++++ .../src/webview/views/diagnostics/errors.ts | 3 ++- .../webview/views/diagnostics/vc-changes.ts | 2 +- 3 files changed, 25 insertions(+), 2 deletions(-) create mode 100644 client/src/webview/views/diagnostics/counterexample.ts diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts new file mode 100644 index 0000000..4202612 --- /dev/null +++ b/client/src/webview/views/diagnostics/counterexample.ts @@ -0,0 +1,22 @@ +import { renderHighlightedInlineExpression } from "../../highlighting"; +import { renderVCLine } from "./vc-changes"; + +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 => renderVCLine(renderHighlightedInlineExpression(line))).join("")} +
+
+ `; +} diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index c777a32..ac48c74 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -1,4 +1,5 @@ import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton } from "../sections"; +import { renderCounterexample } from "./counterexample"; import { renderVCImplication } from "./vc-implications"; import type { ArgumentMismatchError, @@ -36,7 +37,7 @@ const errorContentRenderers: ErrorRendererMap = { 'refinement-error': (e: RefinementError) => /*html*/ ` ${renderExpressionSection('Expected', e.expected)} ${renderCustomSection('Found', renderVCImplication(e, e.found))} - ${e.counterexample ? renderExpressionSection('Counterexample', e.counterexample) : ''} + ${e.counterexample ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample)) : ''} `, 'state-refinement-error': (e: StateRefinementError) => /*html*/ ` ${renderExpressionSection('Expected', e.expected)} diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 611d26c..34a0333 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -34,7 +34,7 @@ function getImplicationLines(node: VCImplication): string[] { return lines; } -function renderVCLine(line: string, className = "", predicateContent?: string): string { +export function renderVCLine(line: string, className = "", predicateContent?: string): string { const { binder, type, predicate } = parseImplicationLine(line); return /*html*/`
From a55d975563cf26f4a3ba0dc96c49eeef76e6140b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 25 Jun 2026 10:46:54 +0100 Subject: [PATCH 4/5] Display Simplified in Last Simplification Step --- client/src/webview/views/diagnostics/vc-implications.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 0942178..c2b76e6 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -22,7 +22,7 @@ function renderStepHeader( ): string { const currStep = stepCount - index; const simplification = current.simplification?.trim(); - const label = escapeHtml(simplification || "Original"); + const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original"); return /*html*/`
From c6d6486c71afed8ad917453bdbcda2a2570d3306 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 26 Jun 2026 11:40:30 +0100 Subject: [PATCH 5/5] Fix Counterexample Rendering --- client/src/webview/styles.ts | 8 ++++++++ client/src/webview/views/diagnostics/counterexample.ts | 7 +++++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 93186c2..f8dfbd9 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -366,6 +366,14 @@ export function getStyles(): string { border-spacing: 0 0.25rem; min-width: 0; } + .counterexample-container .vc-chain { + display: flex; + flex-direction: column; + gap: 0.25rem; + } + .counterexample-line { + overflow-wrap: anywhere; + } .vc-line { display: table-row; } diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts index 4202612..6d80f76 100644 --- a/client/src/webview/views/diagnostics/counterexample.ts +++ b/client/src/webview/views/diagnostics/counterexample.ts @@ -1,5 +1,4 @@ import { renderHighlightedInlineExpression } from "../../highlighting"; -import { renderVCLine } from "./vc-changes"; function getCounterexampleLines(counterexample: string): string[] { return counterexample @@ -15,7 +14,11 @@ export function renderCounterexample(counterexample: string): string { return /*html*/`
- ${lines.map(line => renderVCLine(renderHighlightedInlineExpression(line))).join("")} + ${lines.map(line => /*html*/` +
+ ${renderHighlightedInlineExpression(line)} +
+ `).join("")}
`;