Autocomplete for Refinements

client/src/extension.ts

@@ -8,6 +8,7 @@ import { registerStatusBar, updateStatusBar } from "./services/status-bar";
 import { registerWebview } from "./services/webview";
 import { registerHover } from "./services/hover";
 import { registerEvents } from "./services/events";
+import { registerAutocomplete } from "./services/autocomplete";
 import { runLanguageServer, stopLanguageServer } from "./lsp/server";
 import { runClient, stopClient } from "./lsp/client";
 
@@ -21,6 +22,7 @@ export async function activate(context: vscode.ExtensionContext) {
     registerCommands(context);
     registerWebview(context);
     registerEvents(context);
+    registerAutocomplete(context);
     registerHover();
 
     extension.logger.client.info("Activating LiquidJava extension...");

client/src/lsp/client.ts

@@ -6,6 +6,8 @@ import { updateStatusBar } from '../services/status-bar';
 import { handleLJDiagnostics } from '../services/diagnostics';
 import { onActiveFileChange } from '../services/events';
 import type { LJDiagnostic } from "../types/diagnostics";
+import { ContextHistory } from '../types/context';
+import { handleContextHistory } from '../services/context';
 
 /**
  * Starts the client and connects it to the language server
@@ -42,6 +44,10 @@ export async function runClient(context: vscode.ExtensionContext, port: number)
             handleLJDiagnostics(diagnostics);
         });
 
+        extension.client.onNotification("liquidjava/context", (contextHistory: ContextHistory) => {
+            handleContextHistory(contextHistory);
+        });
+
         const editor = vscode.window.activeTextEditor;
         if (editor && editor.document.languageId === "java") {
             await onActiveFileChange(editor);

client/src/services/autocomplete.ts

@@ -0,0 +1,183 @@
+import * as vscode from "vscode";
+import { extension } from "../state";
+import type { Variable, ContextHistory, Ghost, Alias } from "../types/context";
+import { getSimpleName } from "../utils/utils";
+import { getVariablesInScope } from "./context";
+import { LIQUIDJAVA_ANNOTATION_START } from "../utils/constants";
+
+/**
+ * Registers a completion provider for LiquidJava annotations, providing context-aware suggestions based on the current context history
+ */
+export function registerAutocomplete(context: vscode.ExtensionContext) {
+    context.subscriptions.push(
+        vscode.languages.registerCompletionItemProvider("java", {
+            provideCompletionItems(document, position) {
+                if (!isInsideLiquidJavaAnnotationString(document, position) || !extension.contextHistory) return null;
+                const file = document.uri.toString().replace("file://", "");
+                const nextChar = document.getText(new vscode.Range(position, position.translate(0, 1)));
+                return getContextCompletionItems(extension.contextHistory, file, nextChar);
+            },
+        })
+    );
+}
+
+function getContextCompletionItems(context: ContextHistory, file: string, nextChar: string): vscode.CompletionItem[] {
+    const variablesInScope = getVariablesInScope(file, extension.selection);
+    const inScope = variablesInScope !== null;
+    const triggerParameterHints = nextChar !== "(";
+    const variableItems = getVariableCompletionItems([...(variablesInScope || []), ...context.globalVars]); // not including instance vars
+    const ghostItems = getGhostCompletionItems(context.ghosts, triggerParameterHints);
+    const aliasItems = getAliasCompletionItems(context.aliases, triggerParameterHints);
+    const keywordItems = getKeywordsCompletionItems(triggerParameterHints, inScope);
+    const allItems = [...variableItems, ...ghostItems, ...aliasItems, ...keywordItems];
+
+    // remove duplicates
+    const uniqueItems = new Map<string, vscode.CompletionItem>();
+    allItems.forEach(item => {
+        const label = typeof item.label === "string" ? item.label : item.label.label;
+        if (!uniqueItems.has(label)) uniqueItems.set(label, item);
+    });
+    return Array.from(uniqueItems.values());
+}
+
+function getVariableCompletionItems(variables: Variable[]): vscode.CompletionItem[] {
+    return variables.map(variable => {
+        const varSig = `${variable.type} ${variable.name}`;
+        const codeBlocks: string[] = [];
+        if (variable.mainRefinement !== "true") codeBlocks.push(`@Refinement("${variable.mainRefinement}")`);
+        codeBlocks.push(varSig);
+        return createCompletionItem({
+            name: variable.name,
+            kind: vscode.CompletionItemKind.Variable,
+            description: variable.type,
+            detail: "variable",
+            codeBlocks,
+        });
+    });
+}
+
+function getGhostCompletionItems(ghosts: Ghost[], triggerParameterHints: boolean): vscode.CompletionItem[] {
+    return ghosts.map(ghost => {
+        const parameters = ghost.parameterTypes.map(getSimpleName).join(", ");
+        const ghostSig = `${ghost.returnType} ${ghost.name}(${parameters})`;
+        const isState = /^state\d+\(_\) == \d+$/.test(ghost.refinement);
+        const description = isState ? "state" : "ghost";
+        return createCompletionItem({
+            name: ghost.name,
+            kind: vscode.CompletionItemKind.Function,
+            labelDetail: `(${parameters})`,
+            description,
+            detail: description,
+            codeBlocks: [ghostSig],
+            insertText: triggerParameterHints ? `${ghost.name}($1)` : ghost.name,
+            triggerParameterHints,
+        });
+    });
+}
+
+function getAliasCompletionItems(aliases: Alias[], triggerParameterHints: boolean): vscode.CompletionItem[] {
+    return aliases.map(alias => {
+        const parameters = alias.parameters
+            .map((parameter, index) => {
+                const type = getSimpleName(alias.types[index]);
+                return `${type} ${parameter}`;
+            }).join(", ");
+        const aliasSig = `${alias.name}(${parameters}) { ${alias.predicate} }`;
+        const description = "alias";
+        return createCompletionItem({
+            name: alias.name,
+            kind: vscode.CompletionItemKind.Function,
+            labelDetail: `(${parameters}){ ${alias.predicate} }`,
+            description,
+            detail: description,
+            codeBlocks: [aliasSig],
+            insertText: triggerParameterHints ? `${alias.name}($1)` : alias.name,
+            triggerParameterHints,
+        });
+    });
+}
+
+function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boolean): vscode.CompletionItem[] {
+    const thisItem = createCompletionItem({
+        name: "this",
+        kind: vscode.CompletionItemKind.Keyword,
+        description: "",
+        detail: "keyword",
+        documentationBlocks: ["Keyword referring to the **current instance**"],
+    });
+    const oldItem = createCompletionItem({
+        name: "old",
+        kind: vscode.CompletionItemKind.Keyword,
+        description: "",
+        detail: "keyword",
+        documentationBlocks: ["Keyword referring to the **previous state of the current instance**"],
+        insertText: triggerParameterHints ? "old($1)" : "old",
+        triggerParameterHints,
+    });
+    const items: vscode.CompletionItem[] = [thisItem, oldItem];
+    if (!inScope) {
+        const returnItem = createCompletionItem({
+            name: "return",
+            kind: vscode.CompletionItemKind.Keyword,
+            description: "",
+            detail: "keyword",
+            documentationBlocks: ["Keyword referring to the **method return value**"],
+        });
+        items.push(returnItem);
+    }
+    return items;
+}
+
+type CompletionItemOptions = {
+    name: string;
+    kind: vscode.CompletionItemKind;
+    description?: string;
+    labelDetail?: string;
+    detail: string;
+    documentationBlocks?: string[];
+    codeBlocks?: string[];
+    insertText?: string;
+    triggerParameterHints?: boolean;
+}
+
+function createCompletionItem({ name, kind, labelDetail, description, detail, documentationBlocks, codeBlocks, insertText, triggerParameterHints }: CompletionItemOptions): vscode.CompletionItem {
+    const item = new vscode.CompletionItem(name, kind);
+    item.label = { label: name, detail: labelDetail, description };
+    item.detail = detail;
+    if (insertText) item.insertText = new vscode.SnippetString(insertText);
+    if (triggerParameterHints) item.command = { command: "editor.action.triggerParameterHints", title: "Trigger Parameter Hints" };
+
+    const documentation = new vscode.MarkdownString();
+    if (documentationBlocks) documentationBlocks.forEach(block => documentation.appendMarkdown(block));
+    if (codeBlocks) codeBlocks.forEach(block => documentation.appendCodeblock(block));  
+    item.documentation = documentation;
+
+    return item;
+}
+
+function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, position: vscode.Position): boolean {
+    const textUntilCursor = document.getText(new vscode.Range(new vscode.Position(0, 0), position));
+    LIQUIDJAVA_ANNOTATION_START.lastIndex = 0;
+    let match: RegExpExecArray | null = null;
+    let lastAnnotationStart = -1;
+    while ((match = LIQUIDJAVA_ANNOTATION_START.exec(textUntilCursor)) !== null) {
+        lastAnnotationStart = match.index;
+    }
+    if (lastAnnotationStart === -1) return false;
+
+    const fromLastAnnotation = textUntilCursor.slice(lastAnnotationStart);
+    let parenthesisDepth = 0;
+    let isInsideString = false;
+    for (let i = 0; i < fromLastAnnotation.length; i++) {
+        const char = fromLastAnnotation[i];
+        const previousChar = i > 0 ? fromLastAnnotation[i - 1] : "";
+        if (char === '"' && previousChar !== "\\") {
+            isInsideString = !isInsideString;
+            continue;
+        }
+        if (isInsideString) continue;
+        if (char === "(") parenthesisDepth++;
+        if (char === ")") parenthesisDepth--;
+    }
+    return parenthesisDepth > 0;
+}

client/src/services/context.ts

@@ -0,0 +1,62 @@
+import { extension } from "../state";
+import { ContextHistory, Selection, Variable } from "../types/context";
+
+export function handleContextHistory(contextHistory: ContextHistory) {
+    extension.contextHistory = contextHistory;
+}
+
+// Gets the variables in scope for a given file and position
+// Returns null if position not in any scope
+export function getVariablesInScope(file: string, selection: Selection): Variable[] | null {
+    if (!extension.contextHistory || !selection || !file) return null;
+
+    // get variables in file
+    const fileVars = extension.contextHistory.vars[file];
+    if (!fileVars) return null;
+
+    // get variables in the current scope based on the selection
+    let mostSpecificScope: string | null = null;
+    let minScopeSize = Infinity;
+
+    // find the most specific scope that contains the selection
+    for (const scope of Object.keys(fileVars)) {
+        const scopeSelection = parseScopeString(scope);
+        if (isSelectionWithinScope(selection, scopeSelection)) {
+            const scopeSize = (scopeSelection.endLine - scopeSelection.startLine) * 10000 + (scopeSelection.endColumn - scopeSelection.startColumn);
+            if (scopeSize < minScopeSize) {
+                mostSpecificScope = scope;
+                minScopeSize = scopeSize;
+            }
+        }
+    }
+    if (mostSpecificScope === null)
+        return null;
+
+    // filter variables to only include those that are reachable based on their position
+    const variablesInScope = fileVars[mostSpecificScope];
+    const reachableVariables = getReachableVariables(variablesInScope, selection);
+    return reachableVariables.filter(v => !v.name.startsWith("this#"));
+}
+
+function parseScopeString(scope: string): Selection {
+    const [start, end] = scope.split("-");
+    const [startLine, startColumn] = start.split(":").map(Number);
+    const [endLine, endColumn] = end.split(":").map(Number);
+    return { startLine, startColumn, endLine, endColumn };
+}
+
+function isSelectionWithinScope(selection: Selection, scope: Selection): boolean {
+    const startsWithin = selection.startLine > scope.startLine || 
+        (selection.startLine === scope.startLine && selection.startColumn >= scope.startColumn);
+    const endsWithin = selection.endLine < scope.endLine || 
+        (selection.endLine === scope.endLine && selection.endColumn <= scope.endColumn);
+    return startsWithin && endsWithin;
+}
+
+function getReachableVariables(variables: Variable[], selection: Selection): Variable[] {
+    return variables.filter((variable) => {
+        const placement = variable.placementInCode?.position;
+        if (!placement) return true;
+        return placement.line < selection.startLine || (placement.line === selection.startLine && placement.column <= selection.startColumn);
+    });
+}

client/src/services/events.ts

@@ -1,6 +1,11 @@
 import * as vscode from 'vscode';
 import { extension } from '../state';
 import { updateStateMachine } from './state-machine';
+import { Selection } from '../types/context';
+import { SELECTION_DEBOUNCE_MS } from '../utils/constants';
+
+let selectionTimeout: NodeJS.Timeout | null = null;
+let currentSelection: Selection = { startLine: 0, startColumn: 0, endLine: 0, endColumn: 0 };
 
 /**
  * Initializes file system event listeners
@@ -12,11 +17,15 @@ export function registerEvents(context: vscode.ExtensionContext) {
         vscode.window.onDidChangeActiveTextEditor(async editor => {
             if (!editor || editor.document.languageId !== "java") return;
             await onActiveFileChange(editor);
-
         }),
         vscode.workspace.onDidSaveTextDocument(async document => {
             if (document.uri.scheme !== 'file' || document.languageId !== "java") return;
             await updateStateMachine(document)
+        }),
+        vscode.window.onDidChangeTextEditorSelection(event => {
+            if (event.textEditor.document.uri.scheme !== 'file' || event.textEditor.document.languageId !== "java") return;
+            if (event.selections.length === 0) return;
+            onSelectionChange(event);
         })
     );
 }
@@ -29,4 +38,23 @@ export async function onActiveFileChange(editor: vscode.TextEditor) {
     extension.file = editor.document.uri.fsPath;
     extension.webview?.sendMessage({ type: "file", file: extension.file });
     await updateStateMachine(editor.document);
+}
+
+/**
+ * Handles selection change events
+ * @param event The selection change event
+ */
+export async function onSelectionChange(event: vscode.TextEditorSelectionChangeEvent) {        
+    // update current selection
+    const selectionStart = event.selections[0].start;
+    const selectionEnd = event.selections[0].end;
+    currentSelection = {
+        startLine: selectionStart.line,
+        startColumn: selectionStart.character,
+        endLine: selectionEnd.line,
+        endColumn: selectionEnd.character
+    };
+    // debounce selection changes
+    if (selectionTimeout) clearTimeout(selectionTimeout);
+    selectionTimeout = setTimeout(() => extension.selection = currentSelection, SELECTION_DEBOUNCE_MS);
 }

client/src/state.ts

@@ -6,6 +6,7 @@ import { LiquidJavaLogger } from "./services/logger";
 import { LiquidJavaWebviewProvider } from "./webview/provider";
 import type { LJDiagnostic } from "./types/diagnostics";
 import type { StateMachine } from "./types/fsm";
+import { ContextHistory, Selection } from "./types/context";
 
 export class ExtensionState {
     // server/client state
@@ -22,6 +23,8 @@ export class ExtensionState {
     file?: string;
     diagnostics?: LJDiagnostic[];
     stateMachine?: StateMachine;
+    contextHistory?: ContextHistory;
+    selection?: Selection;
 }
 
 export const extension = new ExtensionState();

client/src/types/context.ts

@@ -0,0 +1,41 @@
+import { PlacementInCode } from "./diagnostics";
+
+// Type definitions used for LiquidJava context information
+
+export type Variable = {
+  name: string;
+  type: string;
+  refinement: string;
+  mainRefinement: string;
+  placementInCode: PlacementInCode | null;
+}
+
+export type Ghost = {
+  name: string;
+  qualifiedName: string;
+  returnType: string;
+  parameterTypes: string[];
+  refinement: string;
+}
+
+export type Alias = {
+  name: string;
+  parameters: string[];
+  types: string[];
+  predicate: string;
+}
+
+export type ContextHistory = {
+  vars: Record<string, Record<string, Variable[]>>; // file -> (scope -> variables in scope)
+  instanceVars: Variable[];
+  globalVars: Variable[];
+  ghosts: Ghost[];
+  aliases: Alias[];
+}
+
+export type Selection = {
+  startLine: number;
+  startColumn: number;
+  endLine: number;
+  endColumn: number;
+}