Render the verifier's line tags as subscripts and name every part of an error alike

client/src/webview/highlighting.ts

@@ -18,23 +18,33 @@ type ScopeColorRule = {
     color: string;
 };
 
+// the tag the verifier gives a variable written like others in an error: the line its value comes from, x@12,
+// 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";
+// 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");
+
 const repository = liquidJavaGrammar.repository as GrammarRepository;
 const patterns = (name: string): GrammarPattern[] => repository[name]?.patterns || [];
 
 const expressionPatterns: GrammarPattern[] = [
+    { match: LITERAL, name: "string.quoted.liquidjava.webview" },
+    { match: LINE_TAG, name: LINE_TAG_SCOPE },
     { match: "\\b(return|break|continue|if|else|switch|case|default|for|while|do|try|catch|finally|throw|throws|new)\\b", name: "keyword.control.liquidjava.webview" },
     ...patterns("keywords"),
     ...patterns("functions"),
     ...patterns("operators"),
-    { match: "\\b[a-zA-Z_][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*(?=\\s*\\()", name: "entity.name.function.liquidjava.webview" },
+    { match: "\\b[a-zA-Z_][a-zA-Z0-9_#]*(?=\\s*\\()", name: "entity.name.function.liquidjava.webview" },
     { match: "\\b[A-Z][a-zA-Z0-9_]*(?=\\s*\\()", name: "entity.name.function.constructor.liquidjava.webview" },
     ...patterns("qualified-names"),
     { match: "\\b(byte|short|long|char|void)\\b", name: "storage.type.primitive.liquidjava.webview" },
     ...patterns("types"),
     { match: "\\bnull\\b", name: "constant.language.null.liquidjava.webview" },
     ...patterns("literals"),
     { match: "[(){}.,;\\[\\]]", name: "punctuation.separator.liquidjava" },
-    { match: "#*[a-zA-Z_][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*", name: "variable.other.liquidjava" }
+    { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: "variable.other.liquidjava" }
 ];
 
 const highlightRules: HighlightRule[] = expressionPatterns
@@ -61,6 +71,57 @@ function colorForScope(scope: string): string {
         ?? "var(--vscode-editor-foreground)";
 }
 
+// the variable that ends at an index: a name such as this.items, or a call such as failures.size()
+function variableBefore(text: string, end: number): string {
+    let start = end;
+    for (let depth = 0; start > 0; start--) {
+        const c = text[start - 1];
+        if (c === ")") depth++;
+        else if (c === "(") {
+            if (depth === 0) break;
+            depth--;
+        }
+        else if (depth === 0 && !/[\w#.]/.test(c)) break;
+    }
+    return text.slice(start, end);
+}
+
+// a line tag as a subscript, l12, that says which value of the variable it stands for
+function renderLineTag(tag: string, variable: string): string {
+    const [, line, number] = /^(?:@(\d+))?(?:#(\d+))?$/.exec(tag) ?? [];
+    const name = variable || "the variable";
+    const value = !number ? `${name} at line ${line}`
+        : line ? `the ${ordinal(Number(number))} value ${name} gets at line ${line}`
+        : `the ${ordinal(Number(number))} value of ${name} (line unknown)`;
+    const text = (line ? `l${line}` : "") + (number ? `#${number}` : "");
+    return `<sub class="lj-line-tag" title="${escapeHtml(value)}">${escapeHtml(text)}</sub>`;
+}
+
+// 1st, 2nd, 3rd, 4th, ..., 11th, 12th, 13th, ..., 21st
+function ordinal(n: number): string {
+    const suffix = n % 100 >= 11 && n % 100 <= 13 ? "th" : ["th", "st", "nd", "rd"][n % 10] ?? "th";
+    return `${n}${suffix}`;
+}
+
+/**
+ * Renders text with the line tags of its variables as subscripts, x@12 as x with l12 below
+ */
+export function renderLineTags(text: string): string {
+    let html = "";
+    let index = 0;
+    for (const match of text.matchAll(LINE_TAGS_OUTSIDE_LITERALS)) {
+        if (/^["']/.test(match[0])) continue;
+        html += escapeHtml(text.slice(index, match.index)) + renderLineTag(match[0], variableBefore(text, match.index));
+        index = match.index + match[0].length;
+    }
+    return html + escapeHtml(text.slice(index));
+}
+
+/** 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 {
     let html = "";
     let index = 0;
@@ -79,7 +140,9 @@ function renderHighlightedContent(expression: string): string {
         const match = matchingRule.regex.exec(expression);
         const content = match?.[0] || expression[index] || "";
 
-        html += `<span style="color:${colorForScope(matchingRule.scope)}">${escapeHtml(content)}</span>`;
+        html += matchingRule.scope === LINE_TAG_SCOPE
+            ? renderLineTag(content, variableBefore(expression, index))
+            : `<span style="color:${colorForScope(matchingRule.scope)}">${escapeHtml(content)}</span>`;
         index += content.length;
     }
     return html;

client/src/webview/message-text.ts

@@ -1,4 +1,5 @@
 import type { LJSourceReference } from "../types/diagnostics";
+import { renderLineTags } from "./highlighting";
 import { escapeHtml } from "./utils";
 
 // a run of backticks, the code, and a run of the same length, as the verifier marks code in its messages
@@ -24,7 +25,7 @@ export function renderMessageText(message: string, references: LJSourceReference
         CODE_SPAN.lastIndex = index;
         const span = message[index] === "`" ? CODE_SPAN.exec(message) : null;
         if (span) {
-            html += `<code class="lj-code">${escapeHtml(unpad(span[2]))}</code>`;
+            html += `<code class="lj-code">${renderLineTags(unpad(span[2]))}</code>`;
             index += span[0].length;
             continue;
         }

client/src/webview/styles.ts

@@ -394,6 +394,12 @@ export function getStyles(): string {
             text-indent: -2ch;
             color: var(--vscode-descriptionForeground);
         }
+        /* the line a variable's value comes from, when the error has several values of it */
+        .lj-line-tag {
+            font-size: 0.75em;
+            color: var(--vscode-descriptionForeground);
+            cursor: help;
+        }
         .lj-expression,
         .lj-expression-code {
             font-family: var(--vscode-editor-font-family);

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

@@ -44,8 +44,8 @@ describe('context view', () => {
         expect(text('#context-ghosts tr:first-child td:last-child')).toBe('ghost');
         expect(text('#context-ghosts tr:last-child td:first-child')).toBe('phase(Example) == open');
         expect(text('#context-ghosts tr:last-child td:last-child')).toBe('state');
-        expect(text('#context-vars tbody td:first-child')).toBe('count@3');
-        expect(text('#context-vars tbody td:last-child')).toBe('count@3 > 0');
+        expect(text('#context-vars tbody td:first-child')).toBe('countl3');
+        expect(text('#context-vars tbody td:last-child')).toBe('countl3 > 0');
         expect(Array.from(document.querySelectorAll('.context-toggle-btn'), node => node.getAttribute('aria-expanded'))).toEqual(['true', 'true', 'true']);
         expect(document.querySelectorAll('.context-section-content.collapsed')).toHaveLength(0);
     });

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

@@ -1,11 +1,11 @@
 import { LJVariable } from "../../../types/context";
 import { RefinementMismatchError } from "../../../types/diagnostics";
-import { renderHighlightedInlineExpression } from "../../highlighting";
+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 {
-    const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {}));
+    const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {}).map(withoutLineTag));
     return /*html*/`
         <div class="context-section">
             ${renderToggleSection('Variables', 'context-vars', isExpanded)}

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

@@ -92,15 +92,16 @@ describe('diagnostics view', () => {
         const position = { file: '/workspace/Reader.java', lineStart: 133, colStart: 8, lineEnd: 133, colEnd: 8 };
         document.body.innerHTML = renderDiagnosticsView([{
             ...error(), messageNotes: [note], references: [{ message: note, text: 'line 134', start: 8, position }],
-            hints: [{ kind: 'general', message: "Call `` b.f('`') `` first" }],
+            hints: [{ kind: 'general', message: "Call `` b.f('`') `` first" }, { kind: 'general', message: 'Set `s@9 = "x@1"`' }],
         }], false, currentFile);
 
         const link = document.querySelector('.message-note a.location-link');
         expect(link?.textContent).toBe('line 134');
         expect([link?.getAttribute('data-file'), link?.getAttribute('data-line')]).toEqual(['/workspace/Reader.java', '133']);
         expect(text('.message-note')).toBe('Origin: line 134, new BufferedInputStream(stream) makes markState(b) == unmarked');
         expect(Array.from(document.querySelectorAll('.lj-code')).map(code => code.textContent))
-            .toEqual(['new BufferedInputStream(stream)', 'markState(b) == unmarked', "b.f('`')"]);
+            .toEqual(['new BufferedInputStream(stream)', 'markState(b) == unmarked', "b.f('`')", 'sl9 = "x@1"']);
+        expect(document.querySelector('.lj-code sub.lj-line-tag')?.getAttribute('title')).toBe('s at line 9');
     });
 
     it('shows every declaration of a refinement with their notes under them', () => {

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

@@ -50,6 +50,25 @@ describe('verification implications', () => {
         expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.textContent))
             .toEqual(['x > 0 &&']);
     });
+    it('writes a line tag under its variable, saying which value it stands for, and changes it with its variable', () => {
+        document.body.innerHTML = renderImplication({
+            name: 'x@12', type: 'int', predicate: 'x@12 > failures.size()@84 && y#2 > z@25#2 && s == "x@1"', next: conclusion,
+        });
+
+        const tags = Array.from(document.querySelectorAll('sub.lj-line-tag'));
+        expect(tags.map(tag => [tag.textContent, tag.getAttribute('title')])).toEqual([
+            ['l12', 'x at line 12'], ['l12', 'x at line 12'],
+            ['l84', 'failures.size() at line 84'], ['#2', 'the 2nd value of y (line unknown)'],
+            ['l25#2', 'the 2nd value z gets at line 25'],
+        ]);
+
+        document.body.innerHTML = renderImplicationChange(
+            { ...conclusion, predicate: 'x@12 > 0 && s == "x@1"' }, { ...conclusion, predicate: 'x@13 > 0 && s == "x@1"' },
+        );
+        expect(document.querySelectorAll('sub')).toHaveLength(1);
+        expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.innerHTML))
+            .toEqual([expect.stringMatching(/^<span [^>]*>x<\/span><sub [^>]*>l13<\/sub>$/)]);
+    });
     it.each([
         ['initial rendering', () => renderImplication({ ...implication, next: null })],
         ['simplification change', () => renderImplicationChange(implication, { ...implication, next: null })],

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

@@ -1,14 +1,17 @@
 import type { VCImplication } from "../../../types/vc-implications";
 import type { TranslationTable } from "../../../types/diagnostics";
-import { getExpressionLines, renderExpressionLines, renderHighlightedInlineExpression } from "../../highlighting";
+import {
+    getExpressionLines, LINE_TAG, LITERAL, renderExpressionLines, renderHighlightedInlineExpression, renderLineTags,
+} from "../../highlighting";
 import { escapeHtml } from "../../utils";
 import { renderSourceHighlightButton } from "../sections";
 
 type ChangeKind = "unchanged" | "removed" | "added";
 type DiffOperation<T> = { kind: ChangeKind; value: T };
 
 const MIN_LINE_SIMILARITY = 0.3;
-const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu;
+const TOKEN_PATTERN = new RegExp(
+    `\\s+|${LITERAL}|-->|&&|\\|\\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#]*(?:${LINE_TAG})?|${LINE_TAG}|\\d+(?:\\.\\d+)?|[^\\s]`, "gu");
 const WHITESPACE_PATTERN = /^\s+$/u;
 const VC_LINE_SEPARATOR = "\t";
 
@@ -39,10 +42,10 @@ function getImplicationLines(node: VCImplication): string[] {
 function renderBinder(binder: string, type: string, translationTable?: TranslationTable): string {
     const placement = translationTable?.[binder.slice(1)];
     if (!placement?.position?.file) {
-        return `<span class="vc-node vc-binder" title="${escapeHtml(type)}">${escapeHtml(binder)}</span>`;
+        return `<span class="vc-node vc-binder" title="${escapeHtml(type)}">${renderLineTags(binder)}</span>`;
     }
     return renderSourceHighlightButton(
-        escapeHtml(binder),
+        renderLineTags(binder),
         type ? `Go to source (${type})` : "Go to source",
         placement.position,
         "vc-node vc-binder clickable",

client/src/webview/views/sections.ts

@@ -113,11 +113,11 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => {
 };
 
 export function renderVariableHighlightButton(variable: LJVariable): string {
-    const displayName = variable.displayName;
+    const name = `<code>${renderHighlightedInlineExpression(variable.displayName)}</code>`;
     const position = variable.position;
-    if (!position || !position.file) return `<code>${displayName}</code>`;
+    if (!position || !position.file) return name;
     return renderSourceHighlightButton(
-        `<code>${renderHighlightedInlineExpression(displayName)}</code>`,
+        name,
         variable.type ? `Go to source (${variable.type})` : "Go to source",
         position,
         "clickable",

server/src/main/java/dtos/diagnostics/CounterexampleDTO.java

@@ -2,21 +2,21 @@
 
 import java.util.List;
 
-import liquidjava.rj_language.ast.formatter.VariableFormatter;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
 import liquidjava.smt.Counterexample;
 
 /**
  * DTO for serializing counterexample assignments.
  */
 public record CounterexampleDTO(List<AssignmentDTO> assignments) {
 
-    public static CounterexampleDTO from(Counterexample counterexample) {
+    public static CounterexampleDTO from(Counterexample counterexample, DisplayNames names) {
         if (counterexample == null)
             return null;
 
         List<AssignmentDTO> assignments = counterexample.assignments().stream()
                 .map(assignment -> new AssignmentDTO(
-                        VariableFormatter.format(assignment.first()),
+                        names.get(assignment.first()),
                         assignment.second()))
                 .toList();
         return new CounterexampleDTO(assignments);

server/src/main/java/dtos/diagnostics/TranslationTableDTO.java

@@ -3,6 +3,7 @@
 import java.util.HashMap;
 
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 
 /**
@@ -11,11 +12,14 @@
  */
 public class TranslationTableDTO extends HashMap<String, PlacementInCodeDTO> {
 
-    public static TranslationTableDTO from(TranslationTable translationTable) {
+    /**
+     * @param names the names the error gives its variables, or null to write them as in code
+     */
+    public static TranslationTableDTO from(TranslationTable translationTable, DisplayNames names) {
         TranslationTableDTO dto = new TranslationTableDTO();
         if (translationTable != null) {
             translationTable.forEach((key, value) -> {
-                dto.put(VariableFormatter.format(key), PlacementInCodeDTO.from(value));
+                dto.put(names == null ? VariableFormatter.format(key) : names.get(key), PlacementInCodeDTO.from(value));
             });
         }
         return dto;

server/src/main/java/dtos/diagnostics/VCImplicationDTO.java

@@ -1,28 +1,29 @@
 package dtos.diagnostics;
 
 import liquidjava.processor.VCImplication;
-import liquidjava.rj_language.ast.formatter.VariableFormatter;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import liquidjava.utils.Utils;
 
 /**
  * DTO for serializing a complete VC implication chain.
  */
 public record VCImplicationDTO(String name, String type, String predicate, VCImplicationDTO next) {
 
-    public static VCImplicationDTO from(VCImplication implication) {
+    public static VCImplicationDTO from(VCImplication implication, DisplayNames names) {
         if (implication == null)
             return null;
 
         String name = null;
         String type = null;
         if (implication.hasBinder()) {
-            name = VariableFormatter.format(implication.getName());
+            name = names.get(implication.getName());
             type = Utils.getSimpleName(implication.getType().getQualifiedName());
         }
         return new VCImplicationDTO(
                 name,
                 type,
-                implication.getRefinement().getExpression().toDisplayString(),
-                from(implication.getNext()));
+                ExpressionFormatter.format(implication.getRefinement().getExpression(), names),
+                from(implication.getNext(), names));
     }
 }

server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java

@@ -1,19 +1,20 @@
 package dtos.diagnostics;
 
+import liquidjava.rj_language.ast.formatter.DisplayNames;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 
 /**
  * DTO for serializing a simplified VC and its complete predecessor states.
  */
 public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin, String simplification) {
 
-    public static VCSimplificationResultDTO from(VCSimplificationResult result) {
+    public static VCSimplificationResultDTO from(VCSimplificationResult result, DisplayNames names) {
         if (result == null)
             return null;
 
         return new VCSimplificationResultDTO(
-                VCImplicationDTO.from(result.getImplication()),
-                from(result.getOrigin()),
+                VCImplicationDTO.from(result.getImplication(), names),
+                from(result.getOrigin(), names),
                 result.getSimplification()
         );
     }

server/src/main/java/dtos/errors/LJErrorDTO.java

@@ -17,12 +17,12 @@ public class LJErrorDTO extends LJDiagnosticDTO {
 
     public LJErrorDTO(String type, LJError error) {
         super("error", type, error);
-        this.translationTable = TranslationTableDTO.from(error.getTranslationTable());
+        this.translationTable = TranslationTableDTO.from(error.getTranslationTable(), error.getDisplayNames());
     }
 
     protected LJErrorDTO(String category, String type, LJError error) {
         super(category, type, error);
-        this.translationTable = TranslationTableDTO.from(error.getTranslationTable());
+        this.translationTable = TranslationTableDTO.from(error.getTranslationTable(), error.getDisplayNames());
     }
 
     public LJErrorDTO(String category, String type, String title, String message, List<HintDTO> hints, String file,

server/src/main/java/dtos/errors/RefinementErrorDTO.java

@@ -25,10 +25,10 @@ public class RefinementErrorDTO extends LJErrorDTO {
 
     public RefinementErrorDTO(RefinementError error) {
         super("refinement-error", error);
-        this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected());
-        this.found = VCSimplificationResultDTO.from(error.getFound());
+        this.expected = error.getExpected() == null ? null : ExpressionFormatter.format(error.getExpected().getExpression(), error.getDisplayNames());
+        this.found = VCSimplificationResultDTO.from(error.getFound(), error.getDisplayNames());
         this.customMessage = error.getCustomMessage();
-        this.counterexample = CounterexampleDTO.from(error.getCounterexample());
+        this.counterexample = CounterexampleDTO.from(error.getCounterexample(), error.getDisplayNames());
         this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
         this.declarationPositions = error.getDeclarationPositions().stream().map(SourcePositionDTO::from).toList();
         this.declarationNotes = error.getDeclarationNotes();