Show the Context tab's refinements as the error messages show them

client/src/types/context.ts

@@ -4,6 +4,7 @@ import { SourcePosition } from "./diagnostics";
 
 export type LJVariable = {
   name: string;
+  displayName: string; // as error messages name it, such as x@12 for the value x takes at line 12
   internalName: string;
   type: string;
   refinement: string;
@@ -19,6 +20,7 @@ export type LJGhost = {
   parameterTypes: string[];
   refinement: string;
   isState: boolean;
+  stateSet: string | null; // the name of the state's set, when it is not a generated one
   file: string;
 }
 

client/src/webview/script.spec.ts

@@ -30,6 +30,7 @@ function diagnostic(file: string, title: string, category: 'error' | 'warning' =
 function context(file = currentFile): LJContext {
     const variable: LJVariable = {
         name: 'count',
+        displayName: 'count',
         internalName: 'count_1',
         type: 'int',
         refinement: 'count > 0',

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

@@ -5,10 +5,10 @@ import { renderContextView } from './context';
 const currentFile = 'file:///workspace/Current.java';
 const sectionState = { aliases: true, ghosts: true, vars: true };
 
-function ghost(name: string, file = currentFile, isState = false): LJGhost {
+function ghost(name: string, file = currentFile, stateSet: string | null = null): LJGhost {
     return {
-        name, qualifiedName: `Example.${name}`, returnType: isState ? 'boolean' : 'int',
-        parameterTypes: ['Example'], refinement: '', isState, file,
+        name, qualifiedName: `Example.${name}`, returnType: stateSet ? 'boolean' : 'int',
+        parameterTypes: ['Example'], refinement: '', isState: stateSet !== null, stateSet, file,
     };
 }
 
@@ -29,9 +29,9 @@ describe('context view', () => {
     it('renders aliases, current-file ghosts and states, and variables', () => {
         document.body.innerHTML = renderContextView(context({
             aliases: [{ name: 'Positive', parameters: ['x'], types: ['int'], predicate: 'x > 0' }],
-            ghosts: [ghost('size'), ghost('open', currentFile, true), ghost('other', 'file:///workspace/Other.java')],
+            ghosts: [ghost('size'), ghost('open', currentFile, 'phase'), ghost('other', 'file:///workspace/Other.java')],
             allVars: [{
-                name: 'count', internalName: 'count#1', type: 'int', refinement: 'count > 0',
+                name: 'count', displayName: 'count@3', internalName: '#count_1', type: 'int', refinement: 'count@3 > 0',
                 mainRefinement: 'count > 0', position: null, annotationPosition: null,
             }],
         }), currentFile, sectionState);
@@ -42,9 +42,10 @@ describe('context view', () => {
         expect(document.querySelectorAll('#context-ghosts tr')).toHaveLength(2);
         expect(text('#context-ghosts tr:first-child td:first-child')).toBe('int size(Example)');
         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');
-        expect(text('#context-vars tbody td:last-child')).toBe('count > 0');
+        expect(text('#context-vars tbody td:first-child')).toBe('count@3');
+        expect(text('#context-vars tbody td:last-child')).toBe('count@3 > 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/ghosts.ts

@@ -25,6 +25,9 @@ export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): str
     `;
 }
 
+// a state of a named set is written as a value of its set, as error messages write it
 function renderGhost(ghost: LJGhost): string {
-    return `${ghost.returnType} ${ghost.name}(${ghost.parameterTypes.map(getSimpleName).join(', ')})`;
+    const parameters = ghost.parameterTypes.map(getSimpleName).join(', ');
+    if (ghost.stateSet) return `${ghost.stateSet}(${parameters}) == ${ghost.name}`;
+    return `${ghost.returnType} ${ghost.name}(${parameters})`;
 }

client/src/webview/views/sections.ts

@@ -1,5 +1,5 @@
 import type { LJDiagnostic, LJHint, SourcePosition } from "../../types/diagnostics";
-import { escapeHtml, getFileName, getSimpleName } from "../utils";
+import { escapeHtml, getFileName } from "../utils";
 import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting";
 import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal";
 import { renderCodicon, renderCodiconButton } from "../icons";
@@ -98,7 +98,7 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => {
 };
 
 export function renderVariableHighlightButton(variable: LJVariable): string {
-    const displayName = getSimpleName(variable.name);
+    const displayName = variable.displayName;
     const position = variable.position;
     if (!position || !position.file) return `<code>${displayName}</code>`;
     return renderSourceHighlightButton(

server/src/main/java/dtos/context/ContextDisplay.java

@@ -0,0 +1,137 @@
+package dtos.context;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Objects;
+import java.util.Optional;
+import java.util.Set;
+import java.util.stream.Stream;
+
+import liquidjava.processor.context.ContextHistory;
+import liquidjava.processor.context.GhostFunction;
+import liquidjava.processor.context.GhostState;
+import liquidjava.processor.context.RefinedVariable;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.StateValues;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
+import liquidjava.utils.GeneratedNames;
+
+/**
+ * Shows the variables of a context as the verifier's error messages do: the states of a named set as values of the
+ * set, {@code display(host) == notDisplayable}, and variables written alike told apart by the line of their value,
+ * {@code host@23}. The values the verifier introduces are not variables of the program: one that stands for a single
+ * expression is replaced by it, and a fact about one that is not constrained at all is left out
+ */
+public final class ContextDisplay {
+    private final DisplayNames names;
+    private final List<GhostState> states;
+    private final List<GhostFunction> stateSets;
+    private final Map<String, Expression> generatedValues;
+    private final Set<String> unconstrained;
+
+    private ContextDisplay(DisplayNames names, List<GhostState> states, Map<String, Expression> generatedValues,
+            Set<String> unconstrained) {
+        this.names = names;
+        this.states = states;
+        // the verifier also passes its other ghost functions, which the context history does not keep
+        this.stateSets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct().toList();
+        this.generatedValues = generatedValues;
+        this.unconstrained = unconstrained;
+    }
+
+    public static ContextDisplay of(ContextHistory history) {
+        List<RefinedVariable> variables = Stream.concat(history.getLocalVars().stream(),
+                history.getGlobalVars().stream()).toList();
+        // the variables of the context first, then the others its refinements mention
+        List<String> shown = new ArrayList<>();
+        List<String> others = new ArrayList<>();
+        Map<String, List<Expression>> generatedFacts = new HashMap<>();
+        for (RefinedVariable variable : variables) {
+            Expression refinement = variable.getRefinement().getExpression();
+            refinement.getVariableNames(others);
+            if (!GeneratedNames.isGenerated(variable.getName()))
+                shown.add(variable.getName());
+            else {
+                others.add(variable.getName());
+                generatedFacts.computeIfAbsent(variable.getName(), name -> new ArrayList<>()).add(refinement);
+            }
+        }
+        Map<String, Expression> values = new HashMap<>();
+        Set<String> unconstrained = new HashSet<>();
+        generatedFacts.forEach((name, facts) -> {
+            if (facts.stream().allMatch(Expression::isBooleanTrue))
+                unconstrained.add(name);
+            else
+                valueOf(name, facts).ifPresent(value -> values.put(name, value));
+        });
+        return new ContextDisplay(DisplayNames.of(shown, others, history::lineOf), new ArrayList<>(history.getGhosts()),
+                values, unconstrained);
+    }
+
+    public String name(String variable) {
+        return names.get(variable);
+    }
+
+    public String format(Predicate refinement) {
+        Expression expression = withoutUnconstrained(inlineGenerated(refinement.getExpression()));
+        return ExpressionFormatter.format(StateValues.toSetForm(expression, states, stateSets), names);
+    }
+
+    /** The expression a generated value stands for, when every fact about it is {@code name == expression} */
+    private static Optional<Expression> valueOf(String name, List<Expression> facts) {
+        Set<Expression> values = new HashSet<>();
+        for (Expression fact : facts) {
+            Optional<Expression> value = equatedTo(name, fact);
+            if (value.isEmpty())
+                return Optional.empty();
+            values.add(value.get());
+        }
+        return values.size() == 1 ? values.stream().findFirst() : Optional.empty();
+    }
+
+    private static Optional<Expression> equatedTo(String name, Expression fact) {
+        if (!(fact instanceof BinaryExpression equality && equality.getOperator().equals("==")))
+            return Optional.empty();
+        Var variable = new Var(name);
+        Expression other = variable.equals(equality.getFirstOperand()) ? equality.getSecondOperand()
+                : variable.equals(equality.getSecondOperand()) ? equality.getFirstOperand() : null;
+        return other == null || mentions(other, name) ? Optional.empty() : Optional.of(other);
+    }
+
+    // a value can stand for an expression over other generated values, so it is replaced until none is left
+    private Expression inlineGenerated(Expression expression) {
+        for (int i = 0; i <= generatedValues.size(); i++) {
+            Optional<String> generated = variablesOf(expression).stream().filter(generatedValues::containsKey)
+                    .findFirst();
+            if (generated.isEmpty())
+                break;
+            expression = expression.substitute(new Var(generated.get()), generatedValues.get(generated.get()));
+        }
+        return expression;
+    }
+
+    private Expression withoutUnconstrained(Expression expression) {
+        return expression.getConjuncts().stream()
+                .filter(conjunct -> variablesOf(conjunct).stream().noneMatch(unconstrained::contains))
+                .reduce((left, right) -> new BinaryExpression(left, "&&", right))
+                .orElse(new LiteralBoolean(true));
+    }
+
+    private static boolean mentions(Expression expression, String name) {
+        return variablesOf(expression).contains(name);
+    }
+
+    private static List<String> variablesOf(Expression expression) {
+        List<String> variables = new ArrayList<>();
+        expression.getVariableNames(variables);
+        return variables;
+    }
+}

server/src/main/java/dtos/context/GhostDTO.java

@@ -1,10 +1,11 @@
 package dtos.context;
 
 import java.util.List;
-import java.util.regex.Pattern;
 import java.util.stream.Collectors;
 
+import liquidjava.processor.context.GhostFunction;
 import liquidjava.processor.context.GhostState;
+import liquidjava.utils.constants.Formats;
 
 /**
  * DTO for serializing GhostState instances to JSON.
@@ -16,21 +17,22 @@ public record GhostDTO(
     List<String> parameterTypes,
     String refinement,
     boolean isState,
+    String stateSet,
     String file
 ) {
-    private static final Pattern STATE_REFINEMENT_PATTERN = Pattern.compile("^state\\d+\\(_\\) == \\d+$");
-
     public static GhostDTO from(GhostState ghostState) {
-        String refinement = ghostState.getRefinement() != null ? ghostState.getRefinement().toString() : null;
-        boolean isState = refinement != null && STATE_REFINEMENT_PATTERN.matcher(refinement).matches();
+        GhostFunction set = ghostState.getParent();
+        // a state of a set with a generated name, such as state1, is written as the state alone
+        boolean isNamedSet = set != null && !set.getName().matches(Formats.STATE_SET_NAMES);
 
         return new GhostDTO(
             ghostState.getName(),
             ghostState.getQualifiedName(),
             ContextHistoryDTO.stringifyType(ghostState.getReturnType()),
             ghostState.getParametersTypes().stream().map(ContextHistoryDTO::stringifyType).collect(Collectors.toList()),
-            refinement,
-            isState,
+            ghostState.getRefinement() != null ? ghostState.getRefinement().toString() : null,
+            set != null,
+            isNamedSet ? set.getName() : null,
             ghostState.getFile()
         );
     }

server/src/main/java/dtos/context/VariableDTO.java

@@ -1,8 +1,12 @@
 package dtos.context;
 
+import java.util.function.Function;
+import java.util.function.UnaryOperator;
+
 import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.processor.context.PlacementInCode;
 import liquidjava.processor.context.RefinedVariable;
+import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 
@@ -11,21 +15,35 @@
  */
 public record VariableDTO(
     String name,
+    String displayName,
     String internalName,
     String type,
     String refinement,
     String mainRefinement,
     SourcePositionDTO position,
     SourcePositionDTO annotationPosition
 ) {
+    /** A variable on its own, such as a method parameter */
     public static VariableDTO from(RefinedVariable refinedVariable) {
+        return from(refinedVariable, VariableFormatter::format, ExpressionFormatter::format);
+    }
+
+    /** A variable of a context, shown as the context shows it */
+    public static VariableDTO from(RefinedVariable refinedVariable, ContextDisplay display) {
+        return from(refinedVariable, display::name, display::format);
+    }
+
+    private static VariableDTO from(RefinedVariable refinedVariable, UnaryOperator<String> displayName,
+            Function<Predicate, String> format) {
         PlacementInCode placement = refinedVariable.getPlacementInCode();
         if (placement == null) return null;
         return new VariableDTO(
             VariableFormatter.format(refinedVariable.getName()),
+            displayName.apply(refinedVariable.getName()),
             refinedVariable.getName(),
             ContextHistoryDTO.stringifyType(refinedVariable.getType()),
-            ExpressionFormatter.format(refinedVariable.getRefinement()),
+            format.apply(refinedVariable.getRefinement()),
+            // the annotation as it is written in code, for hovers and completions
             ExpressionFormatter.format(refinedVariable.getMainRefinement()),
             SourcePositionDTO.from(placement.getPosition()),
             SourcePositionDTO.from(placement.getAnnotationPosition())