Methods Hover

client/src/services/context.ts

@@ -5,6 +5,7 @@ import { getOriginalVariableName } from "../utils/utils";
 
 export function handleContext(context: LJContext) {
     extension.context = context;
+    extension.logger?.client.info(JSON.stringify(context.methods, null, 2))
     if (!extension.file || !extension.currentSelection) return;
 
     // update variables based on new context in current selection

client/src/services/definition.ts

@@ -0,0 +1,26 @@
+import * as vscode from 'vscode';
+
+type Definition = {
+    uri: vscode.Uri;
+}
+
+export async function getDefinitions(document: vscode.TextDocument, position: vscode.Position): Promise<Definition[]> {
+    try {
+        const definitions = await vscode.commands.executeCommand<(vscode.Location | vscode.LocationLink)[]>(
+            'vscode.executeDefinitionProvider',
+            document.uri,
+            position
+        ) || [];
+        return definitions.map(definition => definition instanceof vscode.Location
+            ? { uri: definition.uri }
+            : { uri: definition.targetUri }
+        );
+    } catch {
+        return [];
+    }
+}
+
+export function definitionMatchesClass(definition: Definition, targetClass: string): boolean {
+    const uri = definition.uri.toString();
+    return !!targetClass && (uri.includes(targetClass) || uri.includes(targetClass.replace(/\./g, '/')));
+}

client/src/services/hover.ts

@@ -1,21 +1,26 @@
 import * as vscode from 'vscode';
 import { extension } from '../state';
-import type { Range, LJVariable } from '../types/context';
+import type { LJMethod, LJVariable } from '../types/context';
 import { getSelectionContextVariables } from './context';
-import { getOriginalVariableName, normalizeFilePath, toRange } from '../utils/utils';
+import { getOriginalVariableName, normalizeFilePath } from '../utils/utils';
+import { definitionMatchesClass, getDefinitions } from './definition';
 
 /**
  * Initializes hover provider for LiquidJava diagnostics
  */
 export function registerHover() {
     vscode.languages.registerHoverProvider('java', {
-        provideHover(document, position) {
+        async provideHover(document, position) {
             const hoverContent = new vscode.MarkdownString();
             hoverContent.isTrusted = true;
 
             const variable = getHoveredVariable(document, position);
             if (variable && variable.mainRefinement && variable.mainRefinement !== 'true')
-                hoverContent.appendCodeblock(`@Refinement("${variable.mainRefinement}")`, 'java');
+                hoverContent.appendCodeblock(formatRefinement(variable.mainRefinement), 'java');
+            else {
+                const method = await getHoveredMethod(document, position);
+                if (method) hoverContent.appendCodeblock(formatMethodHover(method), 'java');
+            }
 
             const diagnostics = vscode.languages.getDiagnostics(document.uri);
             const containsDiagnostic = !!diagnostics.find(d => d.range.contains(position) && d.source === 'liquidjava');
@@ -48,3 +53,63 @@ function getHoveredVariable(document: vscode.TextDocument, position: vscode.Posi
     const { allVars } = getSelectionContextVariables(file, positionAfterVariable);
     return allVars.find(variable => getOriginalVariableName(variable.name) === hoveredWord);
 }
+
+async function getHoveredMethod(document: vscode.TextDocument, position: vscode.Position): Promise<LJMethod | null> {
+    if (!extension.context) return null;
+
+    const wordRange = document.getWordRangeAtPosition(position, /[A-Za-z_][A-Za-z0-9_]*/);
+    if (!wordRange) return null;
+
+    const hoveredWord = document.getText(wordRange);
+    const file = normalizeFilePath(document.uri.fsPath);
+    const methods = extension.context.methods.filter(method => methodNameMatches(method, hoveredWord));
+
+    const definitions = await getDefinitions(document, position);
+    const resolvedMethod = methods.find(method => definitions.some(definition => definitionMatchesClass(definition, method.targetClass)));
+    if (resolvedMethod) return resolvedMethod;
+
+    const receiver = document.lineAt(wordRange.start.line).text
+        .slice(0, wordRange.start.character)
+        .match(/([A-Za-z_][A-Za-z0-9_]*)\s*\.\s*$/)?.[1];
+    if (!receiver) return null;
+    const receiverVariable = [...(extension.context?.globalVars || []), ...(extension.context?.localVars || [])]
+        .find(variable =>
+            getOriginalVariableName(variable.name) === receiver &&
+            (!variable.position || variable.position.file === file && isBefore(variable.position, wordRange.start))
+        );
+    if (!receiverVariable) return null;
+
+    return methods.find(method => typeMatchesTargetClass(receiverVariable.type, method.targetClass)) || null;
+}
+
+function methodNameMatches(method: LJMethod, hoveredWord: string): boolean {
+    return method.name === hoveredWord || method.name.endsWith(`.${hoveredWord}`);
+}
+
+function typeMatchesTargetClass(type: string, targetClass: string): boolean {
+    return type === targetClass || targetClass.endsWith(`.${type}`) || type.endsWith(`.${targetClass}`);
+}
+
+function isBefore(range: { lineStart: number; colStart: number }, position: vscode.Position): boolean {
+    return range.lineStart < position.line || range.lineStart === position.line && range.colStart < position.character;
+}
+
+function formatRefinement(refinement: string): string {
+    return `@Refinement("${refinement}")`;
+}
+
+function formatStateRefinement(from: string | null, to: string | null): string {
+    return `@StateRefinement(${[from && `from="${from}"`, to && `to="${to}"`].filter(Boolean).join(', ')})`;
+}
+
+function formatMethodHover(method: LJMethod): string {
+    return [
+        method.returnRefinement && method.returnRefinement !== 'true' && formatRefinement(method.returnRefinement),
+        ...method.parameters
+            .filter(p => p.mainRefinement && p.mainRefinement !== 'true')
+            .map(p => `${formatRefinement(p.mainRefinement)} ${p.type} ${p.name}`),
+        ...method.stateRefinements
+            .filter(s => s.from || s.to)
+            .map(s => formatStateRefinement(s.from, s.to))
+    ].filter(Boolean).join('\n');
+}

client/src/types/context.ts

@@ -29,11 +29,25 @@ export type LJAlias = {
   predicate: string;
 }
 
+export type LJMethodStateRefinement = {
+  from: string | null;
+  to: string | null;
+}
+
+export type LJMethod = {
+  name: string;
+  targetClass: string;
+  returnRefinement: string;
+  parameters: LJVariable[];
+  stateRefinements: LJMethodStateRefinement[];
+}
+
 export type LJContext = {
   localVars: LJVariable[];
   globalVars: LJVariable[];
   ghosts: LJGhost[];
   aliases: LJAlias[];
+  methods: LJMethod[];
   visibleVars: LJVariable[]; // variables visible in the current selection
   allVars: LJVariable[]; // instance vars + global vars + vars in scope
   fileScopes: Record<string, Range[]>; // file -> scopes
@@ -44,4 +58,4 @@ export type Range = {
   colStart: number;
   lineEnd: number;
   colEnd: number;
-}
+}

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

@@ -14,6 +14,7 @@ public record ContextHistoryDTO(
     List<VariableDTO> globalVars,
     List<GhostDTO> ghosts,
     List<AliasDTO> aliases,
+    List<MethodDTO> methods,
     Map<String, List<SourcePositionDTO>> fileScopes
 ) {
     public static String stringifyType(CtTypeReference<?> typeReference) {

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

@@ -0,0 +1,43 @@
+package dtos.context;
+
+import java.util.List;
+import java.util.stream.Collectors;
+
+import liquidjava.processor.context.ObjectState;
+import liquidjava.processor.context.RefinedFunction;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
+
+/**
+ * DTO for serializing RefinedFunction instances to JSON.
+ */
+public record MethodDTO(
+    String name,
+    String targetClass,
+    String returnRefinement,
+    List<VariableDTO> parameters,
+    List<StateRefinementDTO> stateRefinements
+) {
+    public static MethodDTO from(RefinedFunction refinedFunction) {
+        return new MethodDTO(
+            refinedFunction.getName(),
+            refinedFunction.getTargetClass(),
+            format(refinedFunction.getRefReturn()),
+            refinedFunction.getArguments().stream().map(VariableDTO::from).filter(v -> v != null).collect(Collectors.toList()),
+            refinedFunction.getAllStates().stream().map(StateRefinementDTO::from).collect(Collectors.toList())
+        );
+    }
+
+    public record StateRefinementDTO(String from, String to) {
+        public static StateRefinementDTO from(ObjectState state) {
+            return new StateRefinementDTO(
+                state.hasFrom() ? format(state.getFrom()) : null,
+                state.hasTo() ? format(state.getTo()) : null
+            );
+        }
+    }
+
+    private static String format(Predicate predicate) {
+        return predicate == null ? "" : ExpressionFormatter.format(predicate);
+    }
+}

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

@@ -9,8 +9,12 @@ public record SourcePositionDTO(String file, int lineStart, int colStart, int li
 
     public static SourcePositionDTO from(SourcePosition pos) {
         if (pos == null) return null;
-        String file = pos.getFile() != null ? pos.getFile().getAbsolutePath() : null;
-        return new SourcePositionDTO(file, pos.getLine() - 1, pos.getColumn() - 1, pos.getEndLine() - 1, pos.getEndColumn());
+        try {
+            String file = pos.getFile() != null ? pos.getFile().getAbsolutePath() : null;
+            return new SourcePositionDTO(file, pos.getLine() - 1, pos.getColumn() - 1, pos.getEndLine() - 1, pos.getEndColumn());
+        } catch (UnsupportedOperationException e) {
+            return null;
+        }
     }
 
     public static SourcePositionDTO from(String pos) {

server/src/main/java/utils/ContextHistoryConverter.java

@@ -8,6 +8,7 @@
 
 import dtos.context.AliasDTO;
 import dtos.context.ContextHistoryDTO;
+import dtos.context.MethodDTO;
 import dtos.context.GhostDTO;
 import dtos.context.VariableDTO;
 import dtos.diagnostics.SourcePositionDTO;
@@ -29,6 +30,7 @@ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) {
             contextHistory.getGlobalVars().stream().map(VariableDTO::from).filter(v -> v != null).collect(Collectors.toList()),
             contextHistory.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()),
             contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()),
+            contextHistory.getMethods().stream().map(MethodDTO::from).filter(f -> f != null).collect(Collectors.toList()),
             parseFileScopes(contextHistory.getFileScopes())
         );
     }