Add implication arrows after verification predicates

client/src/webview/styles.ts

@@ -415,6 +415,12 @@ export function getStyles(): string {
         .vc-predicate-cell {
             color: var(--vscode-editor-foreground);
         }
+        .vc-arrow {
+            font-size: 1.5em;
+            line-height: 0;
+            vertical-align: middle;
+            color: var(--vscode-descriptionForeground);
+        }
         .vc-predicate-cell:only-child {
             grid-column: 1 / -1;
         }

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

@@ -0,0 +1,40 @@
+import { afterEach, describe, expect, it } from 'vitest';
+import type { VCImplication } from '../../../types/vc-implications';
+import { renderImplication, renderImplicationChange } from './vc-changes';
+
+const conclusion: VCImplication = { name: null, type: null, predicate: 'x > 0', next: null };
+const implication: VCImplication = {
+    name: 'x', type: 'int', predicate: 'x == 1',
+    next: { name: 'y', type: 'int', predicate: 'y == 2', next: conclusion },
+};
+
+afterEach(() => { document.body.innerHTML = ''; });
+
+describe('verification implications', () => {
+    it.each([
+        ['initial rendering', () => renderImplication(implication)],
+        ['simplification change', () => renderImplicationChange(
+            { ...implication, predicate: 'x > 0' }, implication,
+        )],
+    ] as const)('adds an implication arrow after each nonterminal predicate during %s', (_label, render) => {
+        document.body.innerHTML = render();
+
+        const binders = Array.from(document.querySelectorAll('.vc-binder-cell'));
+        expect(binders.map(cell => cell.textContent?.trim())).toEqual(['∀x', '∀y']);
+        expect(binders.map(cell => cell.querySelector('.vc-binder')?.textContent)).toEqual(['∀x', '∀y']);
+        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);
+    });
+    it.each([
+        ['initial rendering', () => renderImplication({ ...implication, next: null })],
+        ['simplification change', () => renderImplicationChange(implication, { ...implication, next: null })],
+    ] as const)('omits the arrow on a terminal node with a binder during %s', (_label, render) => {
+        document.body.innerHTML = render();
+
+        expect(document.querySelector('.vc-binder')?.textContent).toBe('∀x');
+        expect(document.querySelector('.vc-predicate-cell')?.textContent?.trim()).toBe('x == 1');
+        expect(document.querySelector('.vc-arrow')).toBeNull();
+    });
+});

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

@@ -19,12 +19,12 @@ function hasBinder(node: VCImplication): boolean {
 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);
+    return [binder, type, node.predicate, node.next ? "next" : ""].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 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" };
 }
 
 function getImplicationLines(node: VCImplication): string[] {
@@ -55,11 +55,11 @@ export function renderVCLine(
     predicateContent?: string,
     translationTable?: TranslationTable,
 ): string {
-    const { binder, type, predicate } = parseImplicationLine(line);
+    const { binder, type, predicate, hasNext } = parseImplicationLine(line);
     return /*html*/`
         <div class="vc-line ${className}">
             ${binder ? /*html*/`<div class="vc-binder-cell">${renderBinder(binder, type, translationTable)}</div>` : ""}
-            <div class="vc-predicate-cell"><span class="vc-node">${predicateContent ?? renderHighlightedInlineExpression(predicate)}</span></div>
+            <div class="vc-predicate-cell"><span class="vc-node">${predicateContent ?? renderHighlightedInlineExpression(predicate)}</span>${hasNext ? ' <span class="vc-arrow">→</span>' : ""}</div>
         </div>
     `;
 }