Add VC Simplification Support (#95)

Author: rcosta358

client/src/types/derivation-nodes.ts

@@ -1,5 +1,5 @@
-import type { ValDerivationNode } from './derivation-nodes';
 import type { Range } from './context';
+import type { VCSimplificationResult } from './vc-implications';
 
 // Type definitions used for LiquidJava diagnostics
 
@@ -58,8 +58,8 @@ export type RefinementError = BaseDiagnostic & {
     category: 'error';
     type: 'refinement-error';
     translationTable: TranslationTable;
-    expected: ValDerivationNode;
-    found: ValDerivationNode;
+    expected: string;
+    found: VCSimplificationResult;
     customMessage: string;
     counterexample: string;
 }
@@ -75,8 +75,8 @@ export type StateRefinementError = BaseDiagnostic & {
     category: 'error';
     type: 'state-refinement-error';
     translationTable: TranslationTable;
-    expected: ValDerivationNode;
-    found: ValDerivationNode;
+    expected: string;
+    found: VCSimplificationResult;
     customMessage: string;
 }
 

client/src/types/diagnostics.ts

@@ -0,0 +1,11 @@
+export type VCImplication = {
+    name: string | null;
+    type: string | null;
+    predicate: string;
+    next: VCImplication | null;
+}
+
+export type VCSimplificationResult = {
+    implication: VCImplication;
+    origin: VCSimplificationResult | null;
+}

client/src/types/vc-implications.ts

@@ -1,4 +1,4 @@
-import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/diagnostics/derivation-nodes";
+import { handleVCImplicationStepClick } from "./views/diagnostics/vc-implications";
 import { renderLoading } from "./views/loading";
 import { renderStopped } from "./views/stopped";
 import { renderStateMachineView } from "./views/fsm/fsm";
@@ -131,21 +131,11 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
             return;
         }
 
-        // derivation expansion click
-        const derivableNode = target.closest?.('.derivable-node');
-        if (derivableNode) {
+        // VC implication simplification step buttons
+        const vcImplicationStepButton = target.closest?.('.vc-step-btn');
+        if (vcImplicationStepButton) {
             e.stopPropagation();
-            if (handleDerivableNodeClick(derivableNode)) {
-                updateView();
-            }
-            return;
-        }
-
-        // derivation reset button
-        const derivationResetButton = target.closest?.('.derivation-reset-btn');
-        if (derivationResetButton) {
-            e.stopPropagation();
-            if (handleDerivationResetClick(derivationResetButton)) {
+            if (handleVCImplicationStepClick(vcImplicationStepButton)) {
                 updateView();
             }
             return;

client/src/webview/script.ts

@@ -271,18 +271,6 @@ export function getStyles(): string {
         .link:hover {
             text-decoration: underline;
         }
-        .node-var {
-            color: var(--lj-token-identifier);
-        }
-        .node-value {
-            color: var(--vscode-editor-foreground);
-        }
-        .node-number {
-            color: var(--lj-token-number);
-        }
-        .node-boolean {
-            color: var(--lj-token-boolean);
-        }
         .lj-expression,
         .lj-expression-code {
             font-family: var(--vscode-editor-font-family);
@@ -334,19 +322,59 @@ export function getStyles(): string {
         .clickable:hover {
             font-weight: bold;
         }
-        .derivation-container {
+        .vc-container {
             display: flex;
             justify-content: space-between;
-            align-items: center;
+            align-items: flex-start;
             gap: 1rem;
+            margin: 0.5rem 0;
         }
-        .reset-btn {
+        .vc-chain {
+            flex: 1;
+            display: flex;
+            flex-direction: column;
+            gap: 0.25rem;
+            min-width: 0;
+        }
+        .vc-line {
+            display: flex;
+            align-items: flex-start;
+            gap: 0.5rem;
+            min-width: 0;
+        }
+        .vc-line-content {
+            flex: 0 1 auto;
+            min-width: 0;
+            overflow-wrap: anywhere;
+        }
+        .vc-node {
+            display: inline;
+            padding: 0;
+            border: none;
+            background: none;
+            color: var(--vscode-editor-foreground);
+            font: inherit;
+            text-align: left;
+        }
+        .vc-node:hover {
+            background: none;
+        }
+        .vc-binder {
+            color: var(--vscode-descriptionForeground);
+        }
+        .vc-step-controls {
+            display: inline-flex;
+            align-items: center;
+            gap: 0.125rem;
+            flex-shrink: 0;
+        }
+        .vc-step-btn {
             margin: 0;
             display: inline-flex;
             align-items: center;
             justify-content: center;
-            width: 1.75rem;
-            height: 1.75rem;
+            width: 1.5rem;
+            height: 1.25rem;
             padding: 0;
             background-color: transparent;
             color: var(--vscode-button-foreground);
@@ -357,12 +385,17 @@ export function getStyles(): string {
             flex-shrink: 0;
             opacity: 0.7;
         }
-        .reset-btn:hover {
+        .vc-step-btn .codicon {
+            font-size: 1.5rem;
+        }
+        .vc-step-btn:hover {
             font-weight: bold;
             background-color: transparent;
+            opacity: 1;
         }
-        .reset-btn:disabled {
-            opacity: 0.5;
+        .vc-step-btn:disabled {
+            cursor: default;
+            opacity: 0.35;
         }
         button {
             padding: 0.2rem 0.6rem;

client/src/webview/styles.ts

@@ -5,7 +5,6 @@ import { escapeHtml, getSimpleName } from "../../utils";
 import { renderToggleSection, renderHighlightButton, renderDiagnosticRevealButton } from "../sections";
 
 export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string {
-    const expected = errorAtCursor ? errorAtCursor.expected.value : undefined;
     const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {}));
     return /*html*/`
         <div class="context-section">
@@ -33,7 +32,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool
                                     <td><code>${renderHighlightedInlineExpression(variable.refinement)}</code></td>
                                 </tr>
                             `}).join('')}
-                            ${errorAtCursor ? renderFailingRefinement(errorAtCursor, expected!) : ''}
+                            ${errorAtCursor ? renderFailingRefinement(errorAtCursor) : ''}
                         </tbody>
                     </table>
                 `: '<p>No variables declared at the cursor position</p>'}
@@ -42,11 +41,11 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool
     `;
 }
 
-function renderFailingRefinement(errorAtCursor: RefinementMismatchError, expected: string): string {
+function renderFailingRefinement(errorAtCursor: RefinementMismatchError): string {
     return /*html*/`
         <tr>
             <td class="failing-refinement tooltip" colspan="2" data-tooltip="${escapeHtml(errorAtCursor.title)}">
-                ${renderDiagnosticRevealButton(errorAtCursor.position!, '⊢ ' + expected)}
+                ${renderDiagnosticRevealButton(errorAtCursor.position!, '⊢ ' + errorAtCursor.expected)}
             </td>
         </tr>
     `;