Explain the verifier's generated names on hover and link them to their lines

client/src/types/context.ts

@@ -1,4 +1,4 @@
-import { SourcePosition } from "./diagnostics";
+import { SourcePosition, TranslationTable } from "./diagnostics";
 
 // Type definitions used for LiquidJava context information
 
@@ -54,6 +54,7 @@ export type LJContext = {
   visibleVars: LJVariable[]; // variables visible in the current selection
   allVars: LJVariable[]; // instance vars + global vars + vars in scope
   fileScopes: Record<string, Range[]>; // file -> scopes
+  generatedPlaces: TranslationTable; // where each value the verifier introduces, such as #if_condition, comes from
 }
 
 export type Range = {

client/src/webview/generated-names.ts

@@ -0,0 +1,73 @@
+import type { PlacementInCode, SourcePosition } from "../types/diagnostics";
+import { escapeHtml } from "./utils";
+
+// what a value the verifier names stands for, given where it is (" at line 12", or empty when unknown)
+type Description = (at: string) => string;
+
+const NAMED_VALUES = new Map<string, Description>(Object.entries({
+    if_condition: at => `the condition of the if${at}`,
+    loop_condition: at => `the condition of the loop${at}`,
+    ternary_condition: at => `the condition of the ? :${at}`,
+    switch_selector: at => `the value the switch${at} checks`,
+    case_condition: at => `whether the case${at} matches`,
+    try_branch: at => `whether the try block${at} runs to its end, rather than a catch block`,
+    catch_branch: at => `whether this catch block of the try${at} runs, rather than a later one`,
+    array_length: at => `the length of the array created${at}`,
+    operation_result: at => `the result of the operation${at}`,
+    expression_value: at => `the value of the expression${at}`,
+} satisfies Record<string, Description>));
+
+// values named after the code they come from: a call, a new object or a field read
+const VALUES_OF_CODE: [RegExp, (code: string) => Description][] = [
+    [/^new_(\w+)$/, type => at => `the new ${type} object created${at}`],
+    [/^(\w+)_result$/, method => at => `the value returned by the call to ${method}()${at}`],
+    [/^(\w+)_value$/, field => at => `the value of the field ${field} read${at}`],
+];
+
+function describe(name: string): Description | undefined {
+    const kind = name.slice(1);
+    if (!name.startsWith("#") || !kind) return undefined;
+    const named = NAMED_VALUES.get(kind);
+    if (named) return named;
+    for (const [pattern, describeCode] of VALUES_OF_CODE) {
+        const code = pattern.exec(kind)?.[1];
+        if (code) return describeCode(code);
+    }
+    return undefined;
+}
+
+/** Whether a name, written without its line tag, is one the verifier gives a value of the code, such as #if_condition */
+export function isGeneratedName(name: string): boolean {
+    return describe(name) !== undefined;
+}
+
+// says in plain words what a value the verifier names stands for, such as "The condition of the if at line 12"
+function explain(name: string, line?: number): string {
+    const description = describe(name)?.(line === undefined ? "" : ` at line ${line}`) ?? "";
+    return `${description.charAt(0).toUpperCase()}${description.slice(1)}. LiquidJava gives it the name ${name}.`;
+}
+
+/**
+ * The hover text of a name the verifier gives a value of the code: what the value is, and where when it is known
+ * @param name the name without its line tag
+ * @param position where the value comes from, if known; it is a link when it has a file
+ * @param tagLine the line of the name's line tag, used when the position is not known
+ */
+export function generatedNameTitle(name: string, position?: SourcePosition | null, tagLine?: number): string {
+    const explanation = explain(name, position ? position.lineStart + 1 : tagLine);
+    return position?.file ? `${explanation} Click to go to it.` : explanation;
+}
+
+/**
+ * Renders a name the verifier gives a value of the code, explained on hover and, when its place is known, a link to it
+ * @param name the name without its line tag
+ * @param content the name as rendered, with its line tag
+ * @param tagLine the line of its line tag, if it has one
+ * @param place where the value comes from, if known
+ */
+export function renderGeneratedName(name: string, content: string, tagLine?: number, place?: PlacementInCode): string {
+    const position = place?.position;
+    const title = escapeHtml(generatedNameTitle(name, position, tagLine));
+    if (!position?.file) return `<span class="lj-generated-name" title="${title}">${content}</span>`;
+    return /*html*/`<span class="lj-generated-name location-link" title="${title}" data-file="${escapeHtml(position.file)}" data-line="${position.lineStart}" data-column="${position.colStart}">${content}</span>`;
+}

client/src/webview/highlighting.ts

@@ -1,4 +1,6 @@
 import * as liquidJavaGrammar from "../../syntaxes/liquidjava.json";
+import type { TranslationTable } from "../types/diagnostics";
+import { isGeneratedName, renderGeneratedName } from "./generated-names";
 import { escapeHtml } from "./utils";
 
 type GrammarPattern = {
@@ -22,6 +24,8 @@ type ScopeColorRule = {
 // numbered when values share a line or have none, x@12#2 and x#2
 export const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b";
 const LINE_TAG_SCOPE = "line-tag";
+const VARIABLE_SCOPE = "variable.other.liquidjava";
+const LINE_TAG_AT_INDEX = new RegExp(LINE_TAG, "y");
 // string and character literals, whose text is shown as it is even where it looks like a line tag
 export const LITERAL = `"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'`;
 const LINE_TAGS_OUTSIDE_LITERALS = new RegExp(`${LITERAL}|${LINE_TAG}`, "g");
@@ -44,7 +48,7 @@ const expressionPatterns: GrammarPattern[] = [
     { match: "\\bnull\\b", name: "constant.language.null.liquidjava.webview" },
     ...patterns("literals"),
     { match: "[(){}.,;\\[\\]]", name: "punctuation.separator.liquidjava" },
-    { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: "variable.other.liquidjava" }
+    { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: VARIABLE_SCOPE }
 ];
 
 const highlightRules: HighlightRule[] = expressionPatterns
@@ -117,12 +121,38 @@ export function renderLineTags(text: string): string {
     return html + escapeHtml(text.slice(index));
 }
 
+/** The line of the line tag a name ends with, x@12 or x@12#2, if it has one */
+export function lineOfTag(name: string): number | undefined {
+    const line = /@(\d+)(?:#\d+)?$/.exec(name)?.[1];
+    return line === undefined ? undefined : Number(line);
+}
+
 /** The name of a variable without its line tag, as it is written in code */
 export function withoutLineTag(name: string): string {
     return name.replace(new RegExp(`(?:${LINE_TAG})$`), "");
 }
 
-function renderHighlightedContent(expression: string): string {
+function renderToken(content: string, scope: string): string {
+    return `<span style="color:${colorForScope(scope)}">${escapeHtml(content)}</span>`;
+}
+
+/**
+ * Renders a name the verifier gives a value of the code, with the line tag after it if any
+ * @returns the html and the length of the text it renders
+ */
+function renderGeneratedNameAt(expression: string, index: number, name: string, places?: TranslationTable): [string, number] {
+    LINE_TAG_AT_INDEX.lastIndex = index + name.length;
+    const tag = LINE_TAG_AT_INDEX.exec(expression)?.[0] ?? "";
+    const content = renderToken(name, VARIABLE_SCOPE) + (tag ? renderLineTag(tag, name) : "");
+    const html = renderGeneratedName(name, content, lineOfTag(tag), places?.[name + tag]);
+    return [html, name.length + tag.length];
+}
+
+/**
+ * Renders an expression with its tokens colored
+ * @param places where the variables of the expression come from, by name, such as the translation table of an error
+ */
+function renderHighlightedContent(expression: string, places?: TranslationTable): string {
     let html = "";
     let index = 0;
 
@@ -140,25 +170,31 @@ function renderHighlightedContent(expression: string): string {
         const match = matchingRule.regex.exec(expression);
         const content = match?.[0] || expression[index] || "";
 
+        if (matchingRule.scope === VARIABLE_SCOPE && isGeneratedName(content)) {
+            const [generated, length] = renderGeneratedNameAt(expression, index, content, places);
+            html += generated;
+            index += length;
+            continue;
+        }
         html += matchingRule.scope === LINE_TAG_SCOPE
             ? renderLineTag(content, variableBefore(expression, index))
-            : `<span style="color:${colorForScope(matchingRule.scope)}">${escapeHtml(content)}</span>`;
+            : renderToken(content, matchingRule.scope);
         index += content.length;
     }
     return html;
 }
 
-function renderExpression(expression: string, wrap: boolean): string {
+function renderExpression(expression: string, wrap: boolean, places?: TranslationTable): string {
     if (!expression) return "";
 
-    const content = renderHighlightedContent(expression);
+    const content = renderHighlightedContent(expression, places);
     return wrap
         ? `<pre class="lj-expression-block"><code class="lj-expression-code">${content}</code></pre>`
         : content;
 }
 
-export function renderHighlightedExpression(expression: string): string {
-    return renderExpression(expression, true);
+export function renderHighlightedExpression(expression: string, places?: TranslationTable): string {
+    return renderExpression(expression, true, places);
 }
 
 const WEAKER_THAN_AND = ["||", "-->", "?"];
@@ -239,7 +275,7 @@ export function getExpressionLines(expression: string): ExpressionLine[] {
  */
 export function renderExpressionLines(
     lines: ExpressionLine[],
-    renderText: (text: string, index: number) => string = renderHighlightedContent,
+    renderText: (text: string, index: number) => string = text => renderHighlightedContent(text),
     trailing = "",
 ): string {
     return lines.map((line, index) => {
@@ -250,14 +286,19 @@ export function renderExpressionLines(
 
 /**
  * Renders an expression on the lines of getExpressionLines, in an expression block as renderHighlightedExpression does
+ * @param places where the variables of the expression come from, by name
  */
-export function renderHighlightedLines(expression: string): string {
+export function renderHighlightedLines(expression: string, places?: TranslationTable): string {
     if (!expression) return "";
 
-    const html = renderExpressionLines(getExpressionLines(expression));
+    const html = renderExpressionLines(getExpressionLines(expression), text => renderHighlightedContent(text, places));
     return `<pre class="lj-expression-block"><code class="lj-expression-code">${html}</code></pre>`;
 }
 
-export function renderHighlightedInlineExpression(expression: string): string {
-    return renderExpression(expression, false);
+/**
+ * Renders an expression inline, with its tokens colored
+ * @param places where the variables of the expression come from, by name
+ */
+export function renderHighlightedInlineExpression(expression: string, places?: TranslationTable): string {
+    return renderExpression(expression, false, places);
 }

client/src/webview/script.spec.ts

@@ -47,6 +47,7 @@ function context(file = currentFile): LJContext {
         visibleVars: [variable],
         allVars: [variable],
         fileScopes: {},
+        generatedPlaces: {},
     };
 }
 

client/src/webview/styles.ts

@@ -399,6 +399,18 @@ export function getStyles(): string {
             color: var(--vscode-descriptionForeground);
             cursor: help;
         }
+        /* a name LiquidJava gives a value of the code, explained on hover */
+        .lj-generated-name {
+            text-decoration: underline dotted var(--vscode-descriptionForeground);
+            text-underline-offset: 2px;
+            cursor: help;
+        }
+        .lj-generated-name.location-link {
+            cursor: pointer;
+        }
+        .lj-generated-name.location-link:hover {
+            text-decoration-style: solid;
+        }
         .lj-expression,
         .lj-expression-code {
             font-family: var(--vscode-editor-font-family);

client/src/webview/views/context/context.spec.ts

@@ -15,7 +15,7 @@ function ghost(name: string, file = currentFile, stateSet: string | null = null)
 function context(overrides: Partial<LJContext> = {}): LJContext {
     return {
         localVars: [], globalVars: [], ghosts: [], aliases: [], methods: [],
-        visibleVars: [], allVars: [], fileScopes: {}, ...overrides,
+        visibleVars: [], allVars: [], fileScopes: {}, generatedPlaces: {}, ...overrides,
     };
 }
 
@@ -50,6 +50,21 @@ describe('context view', () => {
         expect(document.querySelectorAll('.context-section-content.collapsed')).toHaveLength(0);
     });
 
+    it('links the names LiquidJava gives values of the code in refinements to their lines', () => {
+        document.body.innerHTML = renderContextView(context({
+            allVars: [{
+                name: 'a', displayName: 'a', internalName: 'a', type: 'int', refinement: 'a == #pos_result',
+                mainRefinement: '', position: null, annotationPosition: null,
+            }],
+            generatedPlaces: { '#pos_result': { text: 'pos(x)', position: { file: '/w/A.java', lineStart: 6, colStart: 16, lineEnd: 6, colEnd: 22 } } },
+        }), currentFile, sectionState);
+
+        const name = document.querySelector('#context-vars .lj-generated-name.location-link');
+        expect(name?.getAttribute('title')).toBe(
+            'The value returned by the call to pos() at line 7. LiquidJava gives it the name #pos_result. Click to go to it.');
+        expect([name?.getAttribute('data-file'), name?.getAttribute('data-line')]).toEqual(['/w/A.java', '6']);
+    });
+
     it('honors each section collapse state independently', () => {
         document.body.innerHTML = renderContextView(context({ ghosts: [ghost('size')] }), currentFile, {
             aliases: false, ghosts: true, vars: false,

client/src/webview/views/context/context.ts

@@ -23,7 +23,7 @@ export function renderContextView(context: LJContext | undefined, currentFile: s
                 ? 'No context information available at the cursor position'
                 : `${renderContextAliases(aliases, sectionState.aliases)}
                    ${renderContextGhosts(ghosts, sectionState.ghosts)}
-                   ${renderContextVariables(allVars, sectionState.vars, errorAtCursor)}
+                   ${renderContextVariables(allVars, sectionState.vars, errorAtCursor, context?.generatedPlaces)}
             `}
         </div>
     `;

client/src/webview/views/context/variables.ts

@@ -1,10 +1,13 @@
 import { LJVariable } from "../../../types/context";
-import { RefinementMismatchError } from "../../../types/diagnostics";
+import { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression, withoutLineTag } from "../../highlighting";
 import { escapeHtml, getSimpleName } from "../../utils";
 import { renderToggleSection, renderVariableHighlightButton, renderDiagnosticRevealButton } from "../sections";
 
-export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string {
+/**
+ * @param generatedPlaces where each value the verifier introduces comes from, by name
+ */
+export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError, generatedPlaces?: TranslationTable): string {
     const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {}).map(withoutLineTag));
     return /*html*/`
         <div class="context-section">
@@ -28,7 +31,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool
                                 return /*html*/`
                                 <tr class="${isRelevant ? 'context-variable-relevant' : ''}">
                                     <td>${renderVariableHighlightButton(variable)}</td>
-                                    <td><code>${renderHighlightedInlineExpression(variable.refinement)}</code></td>
+                                    <td><code>${renderHighlightedInlineExpression(variable.refinement, generatedPlaces)}</code></td>
                                 </tr>
                             `;}).join('')}
                             ${errorAtCursor ? renderFailingRefinement(errorAtCursor) : ''}

client/src/webview/views/diagnostics/counterexample.ts

@@ -1,7 +1,7 @@
-import type { Counterexample } from "../../../types/diagnostics";
+import type { Counterexample, TranslationTable } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression } from "../../highlighting";
 
-export function renderCounterexample(counterexample: Counterexample): string {
+export function renderCounterexample(counterexample: Counterexample, translationTable?: TranslationTable): string {
     if (counterexample.assignments.length === 0) return "";
 
     return /*html*/`
@@ -10,7 +10,7 @@ export function renderCounterexample(counterexample: Counterexample): string {
                 ${counterexample.assignments.map(assignment => /*html*/`
                     <div class="counterexample-line">
                         <span class="vc-node">${renderHighlightedInlineExpression(
-                            `${assignment.variable} == ${assignment.value}`
+                            `${assignment.variable} == ${assignment.value}`, translationTable
                         )}</span>
                     </div>
                 `).join("")}

client/src/webview/views/diagnostics/errors.ts

@@ -39,14 +39,14 @@ type ErrorRendererMap = { [E in LJError as E['type']]: (error: E) => string };
 
 const errorContentRenderers: ErrorRendererMap = {
     'refinement-error': (e: RefinementError) => /*html*/ `
-        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected, e.translationTable))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
         ${e.counterexample.assignments.length > 0
-            ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample))
+            ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample, e.translationTable))
             : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/ `
-        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected, e.translationTable))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
     `,
     'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/ `