From 35743d9377ae7b140fb1a4b471a8de8e44c6651c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 17:21:07 +0000 Subject: [PATCH 1/4] Found: show only readable simplification steps, under plain step names Older steps of Found are shown only when their chain uses no generated name (#if_condition, extended#1), one step per run of the same pass, and none that looks like the step before. The step header says Original, Simplified or the name of a display step such as Relevant to Expected, with an (i) tooltip that tells in plain words what changed since the step before, instead of the raw pass names. Each line of a step is laid out as the panel lays out any Found line, one conjunct per line. Co-Authored-By: Claude Opus 5.5 --- client/src/webview/styles.ts | 11 ++ .../webview/views/diagnostics/vc-changes.ts | 2 +- .../views/diagnostics/vc-implications.spec.ts | 79 ++++++++++++++ .../views/diagnostics/vc-implications.ts | 101 +++++++++++++++--- 4 files changed, 176 insertions(+), 17 deletions(-) create mode 100644 client/src/webview/views/diagnostics/vc-implications.spec.ts diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 9956790..c8c10e0 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -600,6 +600,17 @@ export function getStyles(): string { .vc-binder { color: var(--vscode-descriptionForeground); } + .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; diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 24f2e74..aa79bd6 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -27,7 +27,7 @@ function parseImplicationLine(line: string): { binder: string; type: string; pre return { binder, type, predicate, hasNext: next === "next" }; } -function getImplicationLines(node: VCImplication): string[] { +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; diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts new file mode 100644 index 0000000..cfaa896 --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -0,0 +1,79 @@ +import { afterEach, describe, expect, it } from 'vitest'; +import type { 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): VCImplication { + return rows.reduceRight( + (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( + (origin, [simplification, implication]) => ({ implication, origin, simplification }), null, + ) as VCSimplificationResult; +} + +function render(found: VCSimplificationResult, message = 'found ... but expected ...'): void { + const error = { + file: 'A.java', position: null, title: 'Refinement Error', message, + } 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(), + // each line of the chain, its binder and the lines its predicate is laid out on + lines: Array.from(document.querySelectorAll('.vc-line'), line => Array.from( + line.querySelectorAll('.vc-binder, .lj-line'), part => part.textContent?.replace(/\s+/gu, ' ').trim(), + ).join(' ')), + }; +} + +function previous(): void { + handleVCImplicationStepClick(document.querySelector('.vc-step-previous-btn')!); +} + +afterEach(() => { document.body.innerHTML = ''; }); + +describe('Found', () => { + it('names a simplified step and tells what changed, instead of the pass', () => { + render(derivation( + [null, chain(['failures', 'failures == this.failures'], ['n', 'n == size(failures)'])], + ['Substitution', chain(['n', 'n == size(this.failures)'])], + )); + + expect(shown()).toEqual({ + label: 'Simplified', info: 'Replaced variables with the values they are equal to.', position: '2/2', + lines: ['∀n n == size(this.failures)'], + }); + previous(); + expect(shown()).toMatchObject({ label: 'Original', info: 'What is known here, before simplifying.', position: '1/2' }); + }); + + 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 ${states}`], + }); + }); +}); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index f433e2b..9dec664 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -1,38 +1,70 @@ import type { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics"; -import type { VCSimplificationResult } from "../../../types/vc-implications"; +import type { VCImplication, VCSimplificationResult } from "../../../types/vc-implications"; import { renderHighlightedExpression } from "../../highlighting"; import { renderCodicon } from "../../icons"; import { escapeHtml } from "../../utils"; -import { renderImplication, renderImplicationChange } from "./vc-changes"; +import { getImplicationLines, renderImplication, renderImplicationChange } from "./vc-changes"; + +// A step of Found as it is shown: its chain, and the passes that changed it since the step before +type VCStep = { + implication: VCImplication; + passes: string[]; +}; // state to preserve across re-renders type VCState = { - steps: VCSimplificationResult[]; + steps: VCStep[]; translationTable: TranslationTable; stepIndex: number; }; const vcStates = new Map(); // errorId => VCState +// What each simplification pass of the verifier does, in the words of the step's tooltip; any other step, such as +// "Relevant to Expected", is a display step and is shown by its name +const PASS_DESCRIPTIONS: Record = { + "Substitution": "Replaced variables with the values they are equal to.", + "Function Substitution": "Replaced calls with the values they are equal to.", + "Binder": "Removed facts that say nothing, and conditions that Expected does not depend on.", + "Known Enum Values": "Decided comparisons of variables whose enum value is known.", + "Folding": "Computed constant expressions.", + "Arithmetic": "Simplified arithmetic.", + "Logical": "Simplified logical operators.", + "Constraint": "Removed facts that other facts already imply.", +}; +const DISPLAY_STEP_DESCRIPTIONS: Record = { + "Relevant to Expected": "Kept only the facts that share a term with Expected.", +}; +const ORIGINAL_DESCRIPTION = "What is known here, before simplifying."; +// names the verifier makes up (#if_condition) or numbers (x#1), which do not appear in the code +const GENERATED_NAME = /#\w/u; + 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 { +function getStepLabel(step: VCStep): { label: string; description: string } { + if (step.passes.length === 0) return { label: "Original", description: ORIGINAL_DESCRIPTION }; + const displayStep = step.passes.find(pass => !(pass in PASS_DESCRIPTIONS)); + const description = step.passes + .map(pass => PASS_DESCRIPTIONS[pass] ?? DISPLAY_STEP_DESCRIPTIONS[pass]) + .filter(Boolean) + .join(" "); + return { label: displayStep ?? "Simplified", description }; +} + +function renderStepHeader(errorId: string, step: VCStep, index: number, stepCount: number): string { const currStep = stepCount - index; - const simplification = current.simplification?.trim(); - const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original"); + const { label, description } = getStepLabel(step); return /*html*/`
- ${label} + + ${escapeHtml(label)} + ${description ? /*html*/`${renderCodicon("info")}` : ""} +
${currStep}/${stepCount} @@ -46,6 +78,46 @@ function renderStepHeader( `; } +/** + * The steps of a derivation worth showing, newest first. The newest is always shown; an older one only when its lines + * use no generated name, and not when it looks like the step after it or only continues the same pass. Each step keeps + * the passes that changed the lines since the step before it + */ +function getVCSteps(result: VCSimplificationResult): VCStep[] { + const derivation: VCSimplificationResult[] = []; + for (let current: VCSimplificationResult | null = result; current; current = current.origin) { + derivation.unshift(current); + } + const lines = derivation.map(current => getImplicationLines(current.implication)); + + const shown: number[] = []; + lines.forEach((stepLines, index) => { + const isNewest = index === derivation.length - 1; + if (!isNewest && stepLines.some(line => GENERATED_NAME.test(line))) return; + const last: number | undefined = shown[shown.length - 1]; + if (last !== undefined && (sameLines(lines[last], stepLines) + || (last > 0 && derivation[last].simplification === derivation[index].simplification))) { + shown.pop(); + } + shown.push(index); + }); + + let previous = 0; + return shown.map(index => { + const passes = new Set(); + for (let i = previous + 1; i <= index; i++) { + const pass = derivation[i].simplification; + if (pass && !sameLines(lines[i - 1], lines[i])) passes.add(pass); + } + previous = index; + return { implication: derivation[index].implication, passes: [...passes] }; + }).reverse(); +} + +function sameLines(a: string[], b: string[]): boolean { + return a.length === b.length && a.every((line, i) => line === b[i]); +} + function getTargetStepIndex(state: VCState, step: string | null): number | undefined { const targetIndex = step === "previous" ? state.stepIndex + 1 @@ -97,6 +169,7 @@ export function renderVCImplication( result: VCSimplificationResult ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); + const steps = getVCSteps(result); const errorId = encodeURIComponent(JSON.stringify([ error.file, @@ -104,10 +177,6 @@ export function renderVCImplication( error.title, error.message ])); - const steps: VCSimplificationResult[] = []; - for (let current: VCSimplificationResult | null = result; current; current = current.origin) { - steps.push(current); - } const stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1); vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex }); From 14f5d91fc892a94483ab567f13ccb75012c939bc Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 17:21:07 +0000 Subject: [PATCH 2/4] Found: open on a summary step when the verifier could not prove Expected When the message says "expected ... but could not prove it", nothing found is about what Expected constrains. Found then opens on a Summary step that says "Nothing is known here that could prove Expected.", and the arrows go back to the chain, also when there was only one step. The message is what decides it: the verifier's Unknown category differs from it for some state errors, e.g. when found states only a ghost of the receiver. Co-Authored-By: Claude Opus 5.5 --- client/src/webview/styles.ts | 6 +++++ .../views/diagnostics/vc-implications.spec.ts | 16 +++++++++++++ .../views/diagnostics/vc-implications.ts | 24 +++++++++++++++---- 3 files changed, 41 insertions(+), 5 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index c8c10e0..755de72 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -600,6 +600,12 @@ 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; diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts index cfaa896..2599671 100644 --- a/client/src/webview/views/diagnostics/vc-implications.spec.ts +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -76,4 +76,20 @@ describe('Found', () => { lines: [`∀p ${states}`], }); }); + + it('says that nothing known proves Expected when the verifier could not prove it, with the steps a step back', () => { + render( + derivation([null, chain(['undoManager', 'undoManager == #getUndoManager_result'])]), + 'expected `redoState(undoManager) == redoable` but could not prove it', + ); + + 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: ['∀undoManager undoManager == #getUndoManager_result'], + }); + }); }); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 9dec664..42c69ad 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -9,6 +9,8 @@ import { getImplicationLines, renderImplication, renderImplicationChange } from type VCStep = { implication: VCImplication; passes: string[]; + // a summary in front of the newest step, which says that nothing known proves Expected instead of showing the chain + nothingKnown?: boolean; }; // state to preserve across re-renders @@ -36,6 +38,10 @@ const DISPLAY_STEP_DESCRIPTIONS: Record = { "Relevant to Expected": "Kept only the facts that share a term with Expected.", }; const ORIGINAL_DESCRIPTION = "What is known here, before simplifying."; +const NOTHING_KNOWN = "Nothing is known here that could prove Expected."; +const NOTHING_KNOWN_DESCRIPTION = "Go back to see what is known here."; +// the end of the verifier's message when nothing it found is about what Expected constrains +const NOT_PROVEN = / but could not prove it$/u; // names the verifier makes up (#if_condition) or numbers (x#1), which do not appear in the code const GENERATED_NAME = /#\w/u; @@ -46,6 +52,7 @@ function renderStepButton(errorId: string, step: "previous" | "next", disabled: } function getStepLabel(step: VCStep): { label: string; description: string } { + if (step.nothingKnown) return { label: "Summary", description: NOTHING_KNOWN_DESCRIPTION }; if (step.passes.length === 0) return { label: "Original", description: ORIGINAL_DESCRIPTION }; const displayStep = step.passes.find(pass => !(pass in PASS_DESCRIPTIONS)); const description = step.passes @@ -134,10 +141,13 @@ function renderSelectedStep(errorId: string, previousIndex?: number): string { const { steps, translationTable, stepIndex } = state; const current = steps[stepIndex]; - const previous = previousIndex === undefined ? undefined : steps[previousIndex]; - const implication = previous - ? `
${renderImplicationChange(previous.implication, current.implication, translationTable)}
` - : `
${renderImplication(current.implication, translationTable)}
`; + // a change is shown from a step whose chain was shown + const previous = previousIndex === undefined || steps[previousIndex].nothingKnown ? undefined : steps[previousIndex]; + const implication = current.nothingKnown + ? `

${NOTHING_KNOWN}

` + : previous + ? `
${renderImplicationChange(previous.implication, current.implication, translationTable)}
` + : `
${renderImplication(current.implication, translationTable)}
`; return /*html*/` ${steps.length > 1 ? renderStepHeader(errorId, current, stepIndex, steps.length) : ""} @@ -169,7 +179,11 @@ export function renderVCImplication( result: VCSimplificationResult ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); - const steps = getVCSteps(result); + const derivedSteps = getVCSteps(result); + // when the verifier could not prove Expected, Found opens on a summary that says so, with the steps a step back + const steps = NOT_PROVEN.test(error.message) + ? [{ ...derivedSteps[0], passes: [], nothingKnown: true }, ...derivedSteps] + : derivedSteps; const errorId = encodeURIComponent(JSON.stringify([ error.file, From 55510f84fa3e8bfb7e9f08920df11276cc7ace38 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 17:31:18 +0000 Subject: [PATCH 3/4] Found: say that Relevant to Expected keeps the facts linked to Expected through other facts too Co-Authored-By: Claude Opus 5.5 --- client/src/webview/views/diagnostics/vc-implications.spec.ts | 2 +- client/src/webview/views/diagnostics/vc-implications.ts | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts index 2599671..50958d0 100644 --- a/client/src/webview/views/diagnostics/vc-implications.spec.ts +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -67,7 +67,7 @@ describe('Found', () => { ), 'found compression(p) == compressionNotExplicit but expected ...'); expect(shown()).toEqual({ - label: 'Relevant to Expected', info: 'Kept only the facts that share a term with Expected.', + label: 'Relevant to Expected', info: 'Kept only the facts that Expected depends on, directly or through other facts.', position: '2/2', lines: ['∀p compression(p) == compressionNotExplicit'], }); previous(); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 42c69ad..b5391e2 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -35,7 +35,7 @@ const PASS_DESCRIPTIONS: Record = { "Constraint": "Removed facts that other facts already imply.", }; const DISPLAY_STEP_DESCRIPTIONS: Record = { - "Relevant to Expected": "Kept only the facts that share a term with Expected.", + "Relevant to Expected": "Kept only the facts that Expected depends on, directly or through other facts.", }; const ORIGINAL_DESCRIPTION = "What is known here, before simplifying."; const NOTHING_KNOWN = "Nothing is known here that could prove Expected."; From af43c9c21312d69bc2b0fa2a3f5a4915dc76ab3d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 18:21:15 +0000 Subject: [PATCH 4/4] Found: show every step the verifier sends Older steps whose facts use generated names are no longer hidden, runs of the same pass are no longer merged into one step, and steps that look like the one before are no longer left out. Each step keeps its plain header (Original, Simplified or the display step's name) and the tooltip of the pass that produced it. The verifier never records a step equal to the one before it, so no step is identical to the previous one. Co-Authored-By: Claude Opus 5.5 --- .../webview/views/diagnostics/vc-changes.ts | 2 +- .../views/diagnostics/vc-implications.spec.ts | 35 ++++---- .../views/diagnostics/vc-implications.ts | 80 ++++--------------- 3 files changed, 31 insertions(+), 86 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index aa79bd6..24f2e74 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -27,7 +27,7 @@ function parseImplicationLine(line: string): { binder: string; type: string; pre return { binder, type, predicate, hasNext: next === "next" }; } -export function getImplicationLines(node: VCImplication): string[] { +function getImplicationLines(node: VCImplication): string[] { const lines: string[] = []; for (let current: VCImplication | null = node; current; current = current.next) { if (current.next && !hasBinder(current)) continue; diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts index 50958d0..6fa0b6a 100644 --- a/client/src/webview/views/diagnostics/vc-implications.spec.ts +++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts @@ -43,37 +43,30 @@ function previous(): void { afterEach(() => { document.body.innerHTML = ''; }); describe('Found', () => { - it('names a simplified step and tells what changed, instead of the pass', () => { - render(derivation( - [null, chain(['failures', 'failures == this.failures'], ['n', 'n == size(failures)'])], - ['Substitution', chain(['n', 'n == size(this.failures)'])], - )); - - expect(shown()).toEqual({ - label: 'Simplified', info: 'Replaced variables with the values they are equal to.', position: '2/2', - lines: ['∀n n == size(this.failures)'], - }); - previous(); - expect(shown()).toMatchObject({ label: 'Original', info: 'What is known here, before simplifying.', position: '1/2' }); - }); - - it('shows a display step by name and skips steps with generated names or the same pass', () => { + it('shows every step of the verifier, each under its name with what changed in the tooltip', () => { 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])], + [null, chain(['#if_condition', '#if_condition'], ['p', states])], + ['Binder', chain(['#if_condition', 'true'], ['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 Expected depends on, directly or through other facts.', - position: '2/2', lines: ['∀p compression(p) == compressionNotExplicit'], + position: '4/4', lines: ['∀p compression(p) == compressionNotExplicit'], + }); + previous(); + expect(shown()).toMatchObject({ + label: 'Simplified', info: 'Removed facts that say nothing, and conditions that Expected does not depend on.', + position: '3/4', }); previous(); + expect(shown()).toMatchObject({ label: 'Simplified', position: '2/4' }); + previous(); expect(shown()).toMatchObject({ - label: 'Simplified', position: '1/2', - lines: [`∀p ${states}`], + label: 'Original', info: 'What is known here, before simplifying.', position: '1/4', + lines: ['∀#if_condition #if_condition →', `∀p ${states}`], }); }); diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index b5391e2..990342b 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -1,17 +1,13 @@ import type { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics"; -import type { VCImplication, VCSimplificationResult } from "../../../types/vc-implications"; +import type { VCSimplificationResult } from "../../../types/vc-implications"; import { renderHighlightedExpression } from "../../highlighting"; import { renderCodicon } from "../../icons"; import { escapeHtml } from "../../utils"; -import { getImplicationLines, renderImplication, renderImplicationChange } from "./vc-changes"; - -// A step of Found as it is shown: its chain, and the passes that changed it since the step before -type VCStep = { - implication: VCImplication; - passes: string[]; - // a summary in front of the newest step, which says that nothing known proves Expected instead of showing the chain - nothingKnown?: boolean; -}; +import { renderImplication, renderImplicationChange } from "./vc-changes"; + +// A step of Found as it is shown: a step of the verifier, or a summary in front of the newest one, which says that +// nothing known proves Expected instead of showing the chain +type VCStep = VCSimplificationResult & { nothingKnown?: boolean }; // state to preserve across re-renders type VCState = { @@ -42,8 +38,6 @@ const NOTHING_KNOWN = "Nothing is known here that could prove Expected."; const NOTHING_KNOWN_DESCRIPTION = "Go back to see what is known here."; // the end of the verifier's message when nothing it found is about what Expected constrains const NOT_PROVEN = / but could not prove it$/u; -// names the verifier makes up (#if_condition) or numbers (x#1), which do not appear in the code -const GENERATED_NAME = /#\w/u; function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string { const label = `${step === "previous" ? "Previous" : "Next"} simplification`; @@ -53,13 +47,10 @@ function renderStepButton(errorId: string, step: "previous" | "next", disabled: function getStepLabel(step: VCStep): { label: string; description: string } { if (step.nothingKnown) return { label: "Summary", description: NOTHING_KNOWN_DESCRIPTION }; - if (step.passes.length === 0) return { label: "Original", description: ORIGINAL_DESCRIPTION }; - const displayStep = step.passes.find(pass => !(pass in PASS_DESCRIPTIONS)); - const description = step.passes - .map(pass => PASS_DESCRIPTIONS[pass] ?? DISPLAY_STEP_DESCRIPTIONS[pass]) - .filter(Boolean) - .join(" "); - return { label: displayStep ?? "Simplified", description }; + const pass = step.simplification?.trim(); + if (!pass) return { label: "Original", description: ORIGINAL_DESCRIPTION }; + if (pass in PASS_DESCRIPTIONS) return { label: "Simplified", description: PASS_DESCRIPTIONS[pass] }; + return { label: pass, description: DISPLAY_STEP_DESCRIPTIONS[pass] ?? "" }; } function renderStepHeader(errorId: string, step: VCStep, index: number, stepCount: number): string { @@ -85,46 +76,6 @@ function renderStepHeader(errorId: string, step: VCStep, index: number, stepCoun `; } -/** - * The steps of a derivation worth showing, newest first. The newest is always shown; an older one only when its lines - * use no generated name, and not when it looks like the step after it or only continues the same pass. Each step keeps - * the passes that changed the lines since the step before it - */ -function getVCSteps(result: VCSimplificationResult): VCStep[] { - const derivation: VCSimplificationResult[] = []; - for (let current: VCSimplificationResult | null = result; current; current = current.origin) { - derivation.unshift(current); - } - const lines = derivation.map(current => getImplicationLines(current.implication)); - - const shown: number[] = []; - lines.forEach((stepLines, index) => { - const isNewest = index === derivation.length - 1; - if (!isNewest && stepLines.some(line => GENERATED_NAME.test(line))) return; - const last: number | undefined = shown[shown.length - 1]; - if (last !== undefined && (sameLines(lines[last], stepLines) - || (last > 0 && derivation[last].simplification === derivation[index].simplification))) { - shown.pop(); - } - shown.push(index); - }); - - let previous = 0; - return shown.map(index => { - const passes = new Set(); - for (let i = previous + 1; i <= index; i++) { - const pass = derivation[i].simplification; - if (pass && !sameLines(lines[i - 1], lines[i])) passes.add(pass); - } - previous = index; - return { implication: derivation[index].implication, passes: [...passes] }; - }).reverse(); -} - -function sameLines(a: string[], b: string[]): boolean { - return a.length === b.length && a.every((line, i) => line === b[i]); -} - function getTargetStepIndex(state: VCState, step: string | null): number | undefined { const targetIndex = step === "previous" ? state.stepIndex + 1 @@ -179,11 +130,6 @@ export function renderVCImplication( result: VCSimplificationResult ): string { if (!result?.implication) return renderHighlightedExpression(String(result)); - const derivedSteps = getVCSteps(result); - // when the verifier could not prove Expected, Found opens on a summary that says so, with the steps a step back - const steps = NOT_PROVEN.test(error.message) - ? [{ ...derivedSteps[0], passes: [], nothingKnown: true }, ...derivedSteps] - : derivedSteps; const errorId = encodeURIComponent(JSON.stringify([ error.file, @@ -191,6 +137,12 @@ export function renderVCImplication( error.title, error.message ])); + const steps: VCStep[] = []; + // when the verifier could not prove Expected, Found opens on a summary that says so, with the steps a step back + if (NOT_PROVEN.test(error.message)) steps.push({ ...result, nothingKnown: true }); + for (let current: VCSimplificationResult | null = result; current; current = current.origin) { + steps.push(current); + } const stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1); vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex });