Skip to content

Commit a0f32e0

Browse files
committed
Add Simplification Diff
1 parent 2a8e44c commit a0f32e0

4 files changed

Lines changed: 282 additions & 34 deletions

File tree

client/src/webview/script.ts

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import { handleVCImplicationStepClick } from "./views/diagnostics/vc-implications";
1+
import { handleVCDiffToggleClick, handleVCImplicationStepClick } from "./views/diagnostics/vc-implications";
22
import { renderLoading } from "./views/loading";
33
import { renderStopped } from "./views/stopped";
44
import { renderStateMachineView } from "./views/fsm/fsm";
@@ -135,9 +135,14 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
135135
const vcImplicationStepButton = target.closest?.('.vc-step-btn');
136136
if (vcImplicationStepButton) {
137137
e.stopPropagation();
138-
if (handleVCImplicationStepClick(vcImplicationStepButton)) {
139-
updateView();
140-
}
138+
handleVCImplicationStepClick(vcImplicationStepButton);
139+
return;
140+
}
141+
142+
const vcDiffToggleButton = target.closest?.('.vc-diff-toggle-btn');
143+
if (vcDiffToggleButton) {
144+
e.stopPropagation();
145+
handleVCDiffToggleClick(vcDiffToggleButton);
141146
return;
142147
}
143148

client/src/webview/styles.ts

Lines changed: 48 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -371,6 +371,8 @@ export function getStyles(): string {
371371
align-items: flex-start;
372372
gap: 0.5rem;
373373
min-width: 0;
374+
padding: 0.0625rem 0.25rem;
375+
border-radius: 3px;
374376
}
375377
.vc-line-content {
376378
flex: 0 1 auto;
@@ -389,6 +391,34 @@ export function getStyles(): string {
389391
.vc-node:hover {
390392
background: none;
391393
}
394+
.vc-diff-chain {
395+
gap: 0.125rem;
396+
}
397+
.vc-diff-line-removed {
398+
background-color: var(--vscode-diffEditor-removedLineBackground, #f8514933);
399+
background-color: color-mix(in srgb, var(--vscode-diffEditor-removedLineBackground, #f8514933) 75%, transparent);
400+
}
401+
.vc-diff-line-added {
402+
background-color: var(--vscode-diffEditor-insertedLineBackground, #2ea04333);
403+
background-color: color-mix(in srgb, var(--vscode-diffEditor-insertedLineBackground, #2ea04333) 75%, transparent);
404+
}
405+
.vc-diff-fragment {
406+
border-radius: 2px;
407+
}
408+
.vc-diff-fragment-removed {
409+
background-color: var(--vscode-diffEditor-removedTextBackground, #f8514966);
410+
}
411+
.vc-diff-fragment-added {
412+
background-color: var(--vscode-diffEditor-insertedTextBackground, #2ea04366);
413+
}
414+
.vc-diff-fragment-removed,
415+
.vc-diff-fragment-removed * {
416+
color: var(--vscode-gitDecoration-deletedResourceForeground, #f85149) !important;
417+
}
418+
.vc-diff-fragment-added,
419+
.vc-diff-fragment-added * {
420+
color: var(--vscode-gitDecoration-addedResourceForeground, #2ea043) !important;
421+
}
392422
.vc-binder {
393423
color: var(--vscode-descriptionForeground);
394424
}
@@ -398,7 +428,8 @@ export function getStyles(): string {
398428
gap: 0.125rem;
399429
flex-shrink: 0;
400430
}
401-
.vc-step-btn {
431+
.vc-step-btn,
432+
.vc-diff-toggle-btn {
402433
margin: 0;
403434
display: inline-flex;
404435
align-items: center;
@@ -418,11 +449,25 @@ export function getStyles(): string {
418449
.vc-step-btn .codicon {
419450
font-size: 1.5rem;
420451
}
421-
.vc-step-btn:hover {
452+
.vc-diff-toggle-btn .codicon {
453+
font-size: 1rem;
454+
}
455+
.vc-step-btn:hover,
456+
.vc-diff-toggle-btn:hover {
422457
font-weight: bold;
423-
background-color: transparent;
424458
opacity: 1;
425459
}
460+
.vc-step-btn:hover {
461+
background-color: transparent;
462+
}
463+
.vc-diff-toggle-btn {
464+
width: 1.5rem;
465+
margin-right: 0.25rem;
466+
}
467+
.vc-diff-toggle-btn:hover,
468+
.vc-diff-toggle-btn.active {
469+
background-color: var(--vscode-toolbar-hoverBackground);
470+
}
426471
.vc-step-btn:disabled {
427472
cursor: default;
428473
opacity: 0.35;
Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
import type { VCImplication } from "../../../types/vc-implications";
2+
import { renderHighlightedInlineExpression } from "../../highlighting";
3+
4+
type DiffKind = "unchanged" | "removed" | "added";
5+
6+
type DiffOperation<T> = {
7+
kind: DiffKind;
8+
value: T;
9+
};
10+
11+
function getImplicationLines(node: VCImplication): string[] {
12+
const lines: string[] = [];
13+
for (let current: VCImplication | null = node; current; current = current.next) {
14+
const binder = current.name !== null && current.type !== null;
15+
if (!binder && current.next || current.predicate === "true" && current.next !== null) continue;
16+
lines.push(current.predicate);
17+
}
18+
return lines;
19+
}
20+
21+
function renderVCLine(content: string, className = ""): string {
22+
return /*html*/`
23+
<div class="vc-line ${className}">
24+
<div class="vc-line-content"><span class="vc-node">${content}</span></div>
25+
</div>
26+
`;
27+
}
28+
29+
function diffSequence<T>(before: T[], after: T[]): DiffOperation<T>[] {
30+
const lengths = Array.from(
31+
{ length: before.length + 1 },
32+
() => new Array<number>(after.length + 1).fill(0),
33+
);
34+
35+
for (let beforeIndex = before.length - 1; beforeIndex >= 0; beforeIndex -= 1) {
36+
for (let afterIndex = after.length - 1; afterIndex >= 0; afterIndex -= 1) {
37+
lengths[beforeIndex][afterIndex] = before[beforeIndex] === after[afterIndex]
38+
? lengths[beforeIndex + 1][afterIndex + 1] + 1
39+
: Math.max(lengths[beforeIndex + 1][afterIndex], lengths[beforeIndex][afterIndex + 1]);
40+
}
41+
}
42+
43+
const operations: DiffOperation<T>[] = [];
44+
let beforeIndex = 0;
45+
let afterIndex = 0;
46+
47+
while (beforeIndex < before.length && afterIndex < after.length) {
48+
if (before[beforeIndex] === after[afterIndex]) {
49+
operations.push({ kind: "unchanged", value: before[beforeIndex] });
50+
beforeIndex += 1;
51+
afterIndex += 1;
52+
} else if (lengths[beforeIndex + 1][afterIndex] >= lengths[beforeIndex][afterIndex + 1]) {
53+
operations.push({ kind: "removed", value: before[beforeIndex] });
54+
beforeIndex += 1;
55+
} else {
56+
operations.push({ kind: "added", value: after[afterIndex] });
57+
afterIndex += 1;
58+
}
59+
}
60+
61+
while (beforeIndex < before.length) {
62+
operations.push({ kind: "removed", value: before[beforeIndex] });
63+
beforeIndex += 1;
64+
}
65+
while (afterIndex < after.length) {
66+
operations.push({ kind: "added", value: after[afterIndex] });
67+
afterIndex += 1;
68+
}
69+
70+
return operations;
71+
}
72+
73+
function tokenizeExpression(expression: string): string[] {
74+
return expression.match(
75+
/\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#¹²³]*|\d+(?:\.\d+)?|[^\s]/gu,
76+
) || [];
77+
}
78+
79+
function renderTokenDiff(before: string, after: string): { removed: string; added: string } {
80+
const operations = diffSequence(tokenizeExpression(before), tokenizeExpression(after));
81+
return {
82+
removed: renderDiffSide(operations, "removed"),
83+
added: renderDiffSide(operations, "added"),
84+
};
85+
}
86+
87+
function renderDiffSide(operations: DiffOperation<string>[], changedKind: "removed" | "added"): string {
88+
let html = "";
89+
let changedContent = "";
90+
91+
const flushChangedContent = () => {
92+
if (!changedContent) return;
93+
html += `<span class="vc-diff-fragment vc-diff-fragment-${changedKind}">${renderHighlightedInlineExpression(changedContent)}</span>`;
94+
changedContent = "";
95+
};
96+
97+
for (const operation of operations) {
98+
if (operation.kind === changedKind) {
99+
changedContent += operation.value;
100+
continue;
101+
}
102+
if (operation.kind === "unchanged") {
103+
flushChangedContent();
104+
html += renderHighlightedInlineExpression(operation.value);
105+
}
106+
}
107+
flushChangedContent();
108+
return html;
109+
}
110+
111+
function renderChangedLines(removed: string[], added: string[]): string {
112+
const removedLines: string[] = [];
113+
const addedLines: string[] = [];
114+
const pairedCount = Math.min(removed.length, added.length);
115+
116+
for (let index = 0; index < pairedCount; index += 1) {
117+
const diff = renderTokenDiff(removed[index], added[index]);
118+
removedLines.push(renderVCLine(diff.removed, "vc-diff-line vc-diff-line-removed"));
119+
addedLines.push(renderVCLine(diff.added, "vc-diff-line vc-diff-line-added"));
120+
}
121+
for (let index = pairedCount; index < removed.length; index += 1) {
122+
const content = `<span class="vc-diff-fragment vc-diff-fragment-removed">${renderHighlightedInlineExpression(removed[index])}</span>`;
123+
removedLines.push(renderVCLine(content, "vc-diff-line vc-diff-line-removed"));
124+
}
125+
for (let index = pairedCount; index < added.length; index += 1) {
126+
const content = `<span class="vc-diff-fragment vc-diff-fragment-added">${renderHighlightedInlineExpression(added[index])}</span>`;
127+
addedLines.push(renderVCLine(content, "vc-diff-line vc-diff-line-added"));
128+
}
129+
130+
return [...removedLines, ...addedLines].join("");
131+
}
132+
133+
export function renderImplication(node: VCImplication): string {
134+
return getImplicationLines(node)
135+
.map(predicate => renderVCLine(renderHighlightedInlineExpression(predicate)))
136+
.join("");
137+
}
138+
139+
export function renderImplicationDiff(before: VCImplication, after: VCImplication): string {
140+
const operations = diffSequence(getImplicationLines(before), getImplicationLines(after));
141+
const lines: string[] = [];
142+
let index = 0;
143+
144+
while (index < operations.length) {
145+
const operation = operations[index];
146+
if (operation.kind === "unchanged") {
147+
lines.push(renderVCLine(renderHighlightedInlineExpression(operation.value)));
148+
index += 1;
149+
continue;
150+
}
151+
152+
const removed: string[] = [];
153+
const added: string[] = [];
154+
while (index < operations.length && operations[index].kind !== "unchanged") {
155+
const changedOperation = operations[index];
156+
if (changedOperation.kind === "removed") removed.push(changedOperation.value);
157+
if (changedOperation.kind === "added") added.push(changedOperation.value);
158+
index += 1;
159+
}
160+
lines.push(renderChangedLines(removed, added));
161+
}
162+
163+
return lines.join("");
164+
}

0 commit comments

Comments
 (0)