List Found as facts and show only readable simplification steps

client/src/types/diagnostics.ts

@@ -27,6 +27,9 @@ export type LJWarning = CustomWarning | ExternalClassNotFoundWarning | ExternalM
 export type LJHintKind = 'general' | 'deciding-argument' | 'call-sequence' | 'available-calls' | 'unreachable-state'
     | 'path-dependent-state' | 'final-state' | 'reaching-calls';
 
+// the kind of mistake an error shows, as the verifier names it, e.g. 'unknown' when nothing known could prove what was expected
+export type LJErrorCategory = 'out-of-order' | 'out-of-domain' | 'argument-picks-the-state' | 'path-dependent-state' | 'unknown';
+
 export type LJHint = {
     kind: LJHintKind;
     message: string;
@@ -68,6 +71,8 @@ export type RefinementError = BaseDiagnostic & {
     category: 'error';
     type: 'refinement-error';
     translationTable: TranslationTable;
+    // absent when the verifier gives none, as lsp4j leaves out null fields
+    errorCategory?: LJErrorCategory;
     expected: string;
     found: VCSimplificationResult;
     customMessage: string;
@@ -95,6 +100,8 @@ export type StateRefinementError = BaseDiagnostic & {
     category: 'error';
     type: 'state-refinement-error';
     translationTable: TranslationTable;
+    // absent when the verifier gives none, as lsp4j leaves out null fields
+    errorCategory?: LJErrorCategory;
     expected: string;
     found: VCSimplificationResult;
     customMessage: string;

client/src/webview/styles.ts

@@ -569,6 +569,23 @@ export function getStyles(): string {
         .vc-binder {
             color: var(--vscode-descriptionForeground);
         }
+        .vc-nothing-known {
+            margin: 0;
+            padding: 0.0625rem 0.25rem;
+            color: var(--vscode-descriptionForeground);
+            font-family: var(--vscode-font-family);
+        }
+        .vc-step-title {
+            display: inline-flex;
+            align-items: center;
+            gap: 0.25rem;
+            min-width: 0;
+        }
+        .vc-step-info {
+            display: inline-flex;
+            color: var(--vscode-descriptionForeground);
+            cursor: help;
+        }
         .vc-step-controls {
             display: inline-flex;
             align-items: center;

client/src/webview/views/diagnostics/vc-changes.spec.ts

@@ -37,4 +37,16 @@ describe('verification implications', () => {
         expect(document.querySelector('.vc-predicate-cell')?.textContent?.trim()).toBe('x == 1');
         expect(document.querySelector('.vc-arrow')).toBeNull();
     });
+    it('puts each conjunct outside parentheses and strings on its own line', () => {
+        document.body.innerHTML = renderImplication({ ...conclusion, predicate: 'a > 0 && (b || c && d) && s == "x&&y"' });
+
+        expect(Array.from(document.querySelectorAll('.vc-predicate-cell'), cell => cell.textContent?.trim()))
+            .toEqual(['a > 0 &&', '(b || c && d) &&', 's == "x&&y"']);
+    });
+
+    it.each(['a || b && c', 'a && b --> c', 'a && b ? c : d'])('keeps %s on one line', predicate => {
+        document.body.innerHTML = renderImplication({ ...conclusion, predicate });
+
+        expect(document.querySelectorAll('.vc-predicate-cell')).toHaveLength(1);
+    });
 });

client/src/webview/views/diagnostics/vc-changes.ts

@@ -11,27 +11,65 @@ 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";
+const WEAKER_THAN_AND = ["||", "-->", "?"];
 
 function hasBinder(node: VCImplication): boolean {
     return typeof node.name === "string" && node.name.length > 0;
 }
 
-function formatImplicationLine(node: VCImplication): string {
+// one line per conjunct of a node's predicate; the lines after the first keep its binder to tell nodes apart, but do not show it
+function formatImplicationLines(node: VCImplication): string[] {
     const binder = hasBinder(node) ? `∀${node.name}` : "";
     const type = typeof node.type === "string" ? node.type : "";
-    return [binder, type, node.predicate, node.next ? "next" : ""].join(VC_LINE_SEPARATOR);
+    const conjuncts = splitConjuncts(node.predicate);
+    return conjuncts.map((conjunct, index) => {
+        const isLast = index === conjuncts.length - 1;
+        const predicate = isLast ? conjunct : `${conjunct} &&`;
+        return [binder, type, predicate, isLast && node.next ? "next" : "", index > 0 ? "continued" : ""]
+            .join(VC_LINE_SEPARATOR);
+    });
+}
+
+function parseImplicationLine(line: string): {
+    binder: string; type: string; predicate: string; hasNext: boolean; isContinued: boolean;
+} {
+    const [binder = "", type = "", predicate = "", next = "", continued = ""] = line.split(VC_LINE_SEPARATOR);
+    return { binder, type, predicate, hasNext: next === "next", isContinued: continued === "continued" };
 }
 
-function parseImplicationLine(line: string): { binder: string; type: string; predicate: string; hasNext: boolean } {
-    const [binder = "", type = "", predicate = "", next = ""] = line.split(VC_LINE_SEPARATOR);
-    return { binder, type, predicate, hasNext: next === "next" };
+// splits a predicate on the && outside parentheses and string literals, unless a weaker operator outside them
+// (||, -->, ?:) would make its parts look like conjuncts of the whole predicate
+function splitConjuncts(predicate: string): string[] {
+    const conjuncts: string[] = [];
+    let depth = 0;
+    let start = 0;
+    let inString = false;
+    for (let i = 0; i < predicate.length; i++) {
+        if (inString) {
+            if (predicate[i] === "\\") i++;
+            else if (predicate[i] === '"') inString = false;
+        }
+        else if (predicate[i] === '"') inString = true;
+        else if (predicate[i] === "(") depth++;
+        else if (predicate[i] === ")") depth--;
+        else if (depth > 0) continue;
+        else if (WEAKER_THAN_AND.some(operator => predicate.startsWith(operator, i))) return [predicate];
+        else if (predicate.startsWith("&&", i)) {
+            conjuncts.push(predicate.slice(start, i).trim());
+            start = i + 2;
+        }
+    }
+    return [...conjuncts, predicate.slice(start).trim()];
 }
 
-function getImplicationLines(node: VCImplication): string[] {
+/**
+ * The lines of a VC chain: one per conjunct of each node with a binder, and of the conclusion
+ */
+export 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));
+        lines.push(...formatImplicationLines(current));
     }
     return lines;
 }
@@ -55,10 +93,11 @@ export function renderVCLine(
     predicateContent?: string,
     translationTable?: TranslationTable,
 ): string {
-    const { binder, type, predicate, hasNext } = parseImplicationLine(line);
+    const { binder, type, predicate, hasNext, isContinued } = parseImplicationLine(line);
+    const binderCell = isContinued ? "" : renderBinder(binder, type, translationTable);
     return /*html*/`
         <div class="vc-line ${className}">
-            ${binder ? /*html*/`<div class="vc-binder-cell">${renderBinder(binder, type, translationTable)}</div>` : ""}
+            ${binder ? /*html*/`<div class="vc-binder-cell">${binderCell}</div>` : ""}
             <div class="vc-predicate-cell"><span class="vc-node">${predicateContent ?? renderHighlightedInlineExpression(predicate)}</span>${hasNext ? ' <span class="vc-arrow">→</span>' : ""}</div>
         </div>
     `;

client/src/webview/views/diagnostics/vc-implications.spec.ts

@@ -0,0 +1,96 @@
+import { afterEach, describe, expect, it } from 'vitest';
+import type { LJErrorCategory, RefinementError } from '../../../types/diagnostics';
+import type { VCImplication, VCSimplificationResult } from '../../../types/vc-implications';
+import { handleVCImplicationStepClick, renderVCImplication } from './vc-implications';
+
+// a VC chain from its rows, each a binder and its predicate
+function chain(...rows: ReadonlyArray<readonly [string, string]>): VCImplication {
+    return rows.reduceRight<VCImplication | null>(
+        (next, [name, predicate]) => ({ name, type: 'int', predicate, next }), null,
+    ) as VCImplication;
+}
+
+// a derivation from its steps, oldest first, each the pass that produced it and its chain
+function derivation(...steps: Array<[string | null, VCImplication]>): VCSimplificationResult {
+    return steps.reduce<VCSimplificationResult | null>(
+        (origin, [simplification, implication]) => ({ implication, origin, simplification }), null,
+    ) as VCSimplificationResult;
+}
+
+function render(found: VCSimplificationResult, message = 'found ... but expected ...', errorCategory?: LJErrorCategory): void {
+    const error = {
+        file: 'A.java', position: null, title: 'Refinement Error', message, errorCategory,
+    } as unknown as RefinementError;
+    document.body.innerHTML = renderVCImplication(error, found);
+}
+
+function shown() {
+    return {
+        label: document.querySelector('.vc-step-name')?.textContent,
+        info: document.querySelector('.vc-step-info')?.getAttribute('title'),
+        position: document.querySelector('.vc-step-position')?.textContent?.trim(),
+        lines: Array.from(document.querySelectorAll('.vc-line')).map(line => line.textContent?.replace(/\s+/gu, ' ').trim()),
+    };
+}
+
+function previous(): void {
+    handleVCImplicationStepClick(document.querySelector('.vc-step-previous-btn')!);
+}
+
+afterEach(() => { document.body.innerHTML = ''; });
+
+describe('Found', () => {
+    it('keeps the binders and implications, with a line per conjunct', () => {
+        const size = 'failures.size() == size(this.failures) && failures.size() >= 0';
+        render(derivation(
+            [null, chain(['this.failures', 'true'], ['failures', 'failures == this.failures'],
+                ['failures.size()', 'failures.size() == size(failures) && failures.size() >= 0'])],
+            ['Substitution', chain(['this.failures', 'true'], ['failures.size()', size])],
+        ));
+
+        expect(shown()).toEqual({
+            label: 'Simplified', info: 'Replaced variables with the values they are equal to.', position: '2/2',
+            lines: ['∀this.failures true →', '∀failures.size() failures.size() == size(this.failures) &&', 'failures.size() >= 0'],
+        });
+        // a conjunct after the first sits under its binder, which is shown once
+        expect(Array.from(document.querySelectorAll('.vc-binder'), binder => binder.textContent))
+            .toEqual(['∀this.failures', '∀failures.size()']);
+        previous();
+        expect(shown()).toMatchObject({ label: 'Original', position: '1/2' });
+        expect(shown().lines).toContain('∀failures failures == this.failures →');
+    });
+
+    it('shows a display step by name and skips steps with generated names or the same pass', () => {
+        const states = 'tiling(p) == tilingNotExplicit && compression(p) == compressionNotExplicit';
+        render(derivation(
+            [null, chain(['#if_condition', '#if_condition'], ['x', 'x > 0'], ['p', states])],
+            ['Binder', chain(['x', 'x > 0'], ['p', states])],
+            ['Binder', chain(['p', states])],
+            ['Relevant to Expected', chain(['p', 'compression(p) == compressionNotExplicit'])],
+        ), 'found compression(p) == compressionNotExplicit but expected ...');
+
+        expect(shown()).toEqual({
+            label: 'Relevant to Expected', info: 'Kept only the facts that share a term with Expected.',
+            position: '2/2', lines: ['∀p compression(p) == compressionNotExplicit'],
+        });
+        previous();
+        expect(shown()).toMatchObject({
+            label: 'Simplified', position: '1/2',
+            lines: ['∀p tiling(p) == tilingNotExplicit &&', 'compression(p) == compressionNotExplicit'],
+        });
+    });
+
+    it.each([
+        ['its category is unknown', [['undoManager', 'undoManager == undoManager@12']], 'unknown'],
+        ['found states nothing', [['timeout', 'true']], undefined],
+    ] as const)('says that nothing known proves Expected when %s, with the steps a step back', (label, rows, errorCategory) => {
+        render(derivation([null, chain(...rows)]), `found ${label}`, errorCategory);
+
+        expect(shown()).toMatchObject({ label: 'Summary', info: 'Go back to see what is known here.', position: '2/2', lines: [] });
+        expect(document.querySelector('.vc-nothing-known')?.textContent)
+            .toBe('Nothing is known here that could prove Expected.');
+        previous();
+        expect(document.querySelector('.vc-nothing-known')).toBeNull();
+        expect(shown()).toMatchObject({ label: 'Original', position: '1/2', lines: [`∀${rows[0][0]} ${rows[0][1]}`] });
+    });
+});