diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts index 0310287..3b50bf1 100644 --- a/client/src/webview/highlighting.ts +++ b/client/src/webview/highlighting.ts @@ -98,6 +98,103 @@ export function renderHighlightedExpression(expression: string): string { return renderExpression(expression, true); } +const WEAKER_THAN_AND = ["||", "-->", "?"]; + +// the positions of the characters outside parentheses and string or character literals +function topLevelIndices(expression: string): number[] { + const indices: number[] = []; + let depth = 0; + let quote: string | null = null; + for (let i = 0; i < expression.length; i++) { + if (quote) { + if (expression[i] === "\\") i++; + else if (expression[i] === quote) quote = null; + } + else if (expression[i] === '"' || expression[i] === "'") quote = expression[i]; + else if (expression[i] === "(") depth++; + else if (expression[i] === ")") depth--; + else if (depth === 0) indices.push(i); + } + return indices; +} + +/** + * Splits an expression at its top-level &&, keeping the && at the end of each conjunct but the last. An && inside + * parentheses or a literal stays in its conjunct, and nothing is split when a weaker operator (||, -->, ?:) + * outside them would make the parts look like conjuncts of the whole expression + */ +function splitConjuncts(expression: string): string[] { + const indices = topLevelIndices(expression); + if (indices.some(i => WEAKER_THAN_AND.some(operator => expression.startsWith(operator, i)))) return [expression.trim()]; + + const conjuncts: string[] = []; + let start = 0; + for (const i of indices) { + if (i < start || !expression.startsWith("&&", i)) continue; + conjuncts.push(expression.slice(start, i + 2).trim()); + start = i + 2; + } + const last = expression.slice(start).trim(); + return last ? [...conjuncts, last] : conjuncts; +} + +// the condition and the two branches of an expression that is a conditional outside parentheses, or null +function splitConditional(expression: string): [string, string, string] | null { + const indices = topLevelIndices(expression); + const question = indices.find(i => expression[i] === "?"); + if (question === undefined) return null; + + let nested = 0; + for (const i of indices.filter(i => i > question)) { + if (expression[i] === "?") nested++; + else if (expression[i] === ":" && nested-- === 0) + return [expression.slice(0, question), expression.slice(question + 1, i), expression.slice(i + 1)] + .map(part => part.trim()) as [string, string, string]; + } + return null; +} + +export type ExpressionLine = { text: string; branch: boolean }; + +/** + * The lines an expression is shown on: one per top-level conjunct, and a conditional's condition with each branch + * on a line of its own, indented + */ +export function getExpressionLines(expression: string): ExpressionLine[] { + return splitConjuncts(expression).flatMap(conjunct => { + const conditional = splitConditional(conjunct); + if (!conditional) return [{ text: conjunct, branch: false }]; + const [condition, then, otherwise] = conditional; + return [{ text: condition, branch: false }, { text: `? ${then}`, branch: true }, { text: `: ${otherwise}`, branch: true }]; + }); +} + +/** + * Renders the lines of an expression, each of which wraps with a hanging indent + * @param renderText renders the text of the line at an index, highlighted by default + * @param trailing html shown at the end of the last line + */ +export function renderExpressionLines( + lines: ExpressionLine[], + renderText: (text: string, index: number) => string = renderHighlightedContent, + trailing = "", +): string { + return lines.map((line, index) => { + const end = index === lines.length - 1 ? trailing : ""; + return `${renderText(line.text, index)}${end}`; + }).join(""); +} + +/** + * Renders an expression on the lines of getExpressionLines, in an expression block as renderHighlightedExpression does + */ +export function renderHighlightedLines(expression: string): string { + if (!expression) return ""; + + const html = renderExpressionLines(getExpressionLines(expression)); + return `
${html}
`; +} + export function renderHighlightedInlineExpression(expression: string): string { return renderExpression(expression, false); } diff --git a/client/src/webview/styles.spec.ts b/client/src/webview/styles.spec.ts index 722e3d0..70408c9 100644 --- a/client/src/webview/styles.spec.ts +++ b/client/src/webview/styles.spec.ts @@ -105,6 +105,14 @@ describe('state error styles', () => { } }); + it('breaks a Found line inside a name only when the name alone is wider than the line', () => { + render(''); + document.body.insertAdjacentHTML('beforeend', '
'); + + expect(style('.vc-binder-cell').overflowWrap).toBe('break-word'); + expect(style('.vc-predicate-cell').overflowWrap).toBe('break-word'); + }); + it('keeps other states with the default outline', () => { render(state('')); diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index e682ed1..2bed3ab 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -392,6 +392,14 @@ export function getStyles(): string { background: transparent !important; background-color: transparent !important; } + .lj-line { + display: block; + padding-left: 2ch; + text-indent: -2ch; + } + .lj-line-branch { + padding-left: 4ch; + } .lj-token-keyword { color: var(--lj-token-keyword); } @@ -479,7 +487,7 @@ export function getStyles(): string { gap: 0.25rem; } .counterexample-line { - overflow-wrap: anywhere; + overflow-wrap: break-word; } .vc-line { display: contents; @@ -488,7 +496,7 @@ export function getStyles(): string { .vc-predicate-cell { min-width: 0; padding: 0.0625rem 0.25rem; - overflow-wrap: anywhere; + overflow-wrap: break-word; } .vc-binder-cell { min-height: 1.2em; @@ -499,6 +507,23 @@ export function getStyles(): string { .vc-predicate-cell { color: var(--vscode-editor-foreground); } + /* a narrow panel puts each binder above its predicate, so that the predicate gets the whole width */ + @media (max-width: 420px) { + .diagnostic-item { + padding-inline: 0.5rem; + } + .vc-container { + padding-inline: 0.25rem; + } + .vc-chain { + grid-template-columns: minmax(0, 1fr); + line-height: 1.4; + } + .vc-binder-cell, + .vc-predicate-cell { + padding-inline: 0; + } + } .vc-arrow { font-size: 1.5em; line-height: 0; diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index 0e58ed4..72c4875 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, renderDiagnosticStateMachineButton, renderHints } from "../sections"; import { renderCounterexample } from "./counterexample"; +import { renderHighlightedLines } from "../../highlighting"; import { renderVCImplication } from "./vc-implications"; import type { ArgumentMismatchError, @@ -38,14 +39,14 @@ type ErrorRendererMap = { [E in LJError as E['type']]: (error: E) => string }; const errorContentRenderers: ErrorRendererMap = { 'refinement-error': (e: RefinementError) => /*html*/ ` - ${renderExpressionSection('Expected', e.expected)} + ${renderCustomSection('Expected', renderHighlightedLines(e.expected))} ${renderCustomSection('Found', renderVCImplication(e, e.found))} ${e.counterexample.assignments.length > 0 ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample)) : ''} `, 'state-refinement-error': (e: StateRefinementError) => /*html*/ ` - ${renderExpressionSection('Expected', e.expected)} + ${renderCustomSection('Expected', renderHighlightedLines(e.expected))} ${renderCustomSection('Found', renderVCImplication(e, e.found))} `, 'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/ ` diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts index 06527fb..2028727 100644 --- a/client/src/webview/views/diagnostics/vc-changes.spec.ts +++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts @@ -25,7 +25,30 @@ describe('verification implications', () => { expect(document.querySelector('.vc-line:last-child')?.textContent?.trim()).toBe('x > 0'); expect(Array.from(document.querySelectorAll('.vc-predicate-cell')).map(cell => cell.textContent?.trim())) .toEqual(['x == 1 →', 'y == 2 →', 'x > 0']); - expect(document.querySelectorAll('.vc-predicate-cell > .vc-arrow')).toHaveLength(2); + expect(document.querySelectorAll('.vc-predicate-cell .vc-arrow')).toHaveLength(2); + }); + it('puts each top-level conjunct and each branch of a conditional on a line of its own', () => { + document.body.innerHTML = renderImplication({ + name: 'h', type: 'Frame', predicate: 'a > 0 && (b || c) && s == "x && y"', + next: { ...conclusion, predicate: "p && q ? d(h) == on : (c == ':' ? d(h) == off : d(h) == on)" }, + }); + + const lines = (cell: Element) => Array.from(cell.querySelectorAll('.lj-line')) + .map(line => [line.textContent, line.classList.contains('lj-line-branch')]); + const [fact, conditional] = document.querySelectorAll('.vc-predicate-cell'); + expect(lines(fact)).toEqual([['a > 0 &&', false], ['(b || c) &&', false], ['s == "x && y" →', false]]); + expect(lines(conditional)).toEqual([ + ['p && q', false], ['? d(h) == on', true], [": (c == ':' ? d(h) == off : d(h) == on)", true], + ]); + }); + it('keeps a conjunct per line in a predicate that a simplification changed, marking a repeated conjunct it adds', () => { + document.body.innerHTML = renderImplicationChange( + { ...conclusion, predicate: 'x > 0' }, { ...conclusion, predicate: 'x > 0 && x > 0' }, + ); + + expect(Array.from(document.querySelectorAll('.lj-line')).map(line => line.textContent)).toEqual(['x > 0 &&', 'x > 0']); + expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.textContent)) + .toEqual(['x > 0 &&']); }); it.each([ ['initial rendering', () => renderImplication({ ...implication, next: null })], diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index a5c0d37..24f2e74 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -1,6 +1,6 @@ import type { VCImplication } from "../../../types/vc-implications"; import type { TranslationTable } from "../../../types/diagnostics"; -import { renderHighlightedInlineExpression } from "../../highlighting"; +import { getExpressionLines, renderExpressionLines, renderHighlightedInlineExpression } from "../../highlighting"; import { escapeHtml } from "../../utils"; import { renderSourceHighlightButton } from "../sections"; @@ -49,17 +49,22 @@ function renderBinder(binder: string, type: string, translationTable?: Translati ); } +/** + * Renders a line of a VC chain, its predicate on the lines of getExpressionLines + * @param renderText renders the text of the line at an index, highlighted by default + */ export function renderVCLine( line: string, className = "", - predicateContent?: string, + renderText?: (text: string, index: number) => string, translationTable?: TranslationTable, ): string { const { binder, type, predicate, hasNext } = parseImplicationLine(line); + const arrow = hasNext ? ' →' : ""; return /*html*/`
${binder ? /*html*/`
${renderBinder(binder, type, translationTable)}
` : ""} -
${predicateContent ?? renderHighlightedInlineExpression(predicate)}${hasNext ? ' →' : ""}
+
${renderExpressionLines(getExpressionLines(predicate), renderText, arrow)}
`; } @@ -188,6 +193,18 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string | return lines; } +// each line of a changed predicate, diffed against the line of the old predicate it replaces, or all marked if none +function renderChangedPredicateLines(before: string, after: string): string[] { + const lines = (predicate: string) => getExpressionLines(predicate).map(line => line.text); + return alignChangedLines(lines(before), lines(after)) + .flatMap(([beforeLine, afterLine]) => { + if (afterLine === undefined) return []; + return [beforeLine === undefined + ? renderChangedFragment(afterLine) + : renderDestinationTokenDiff(beforeLine, afterLine).content]; + }); +} + function renderChangedDestinationLines( removed: string[], added: string[], @@ -199,14 +216,14 @@ function renderChangedDestinationLines( .map(([before, after]) => { if (after === undefined) return ""; if (before === undefined) return renderVCLine(after, "vc-change-line", undefined, translationTable); - const change = renderDestinationTokenDiff( - parseImplicationLine(before).predicate, - parseImplicationLine(after).predicate, - ); + const beforePredicate = parseImplicationLine(before).predicate; + const afterPredicate = parseImplicationLine(after).predicate; + const change = renderDestinationTokenDiff(beforePredicate, afterPredicate); + const lines = renderChangedPredicateLines(beforePredicate, afterPredicate); return renderVCLine( after, change.hasAddedContent ? "" : "vc-change-line", - change.content, + (_text, index) => lines[index], translationTable, ); })