Autocomplete Improvements

client/src/extension.ts

@@ -18,15 +18,14 @@ import { runClient, stopClient } from "./lsp/client";
  */
 export async function activate(context: vscode.ExtensionContext) {
     registerLogger(context);
+    extension.logger.client.info("Activating LiquidJava extension...");
+
     registerStatusBar(context);
     registerCommands(context);
-    registerWebview(context);
     registerEvents(context);
+    registerWebview(context);
     registerAutocomplete(context);
     registerHover();
-
-    extension.logger.client.info("Activating LiquidJava extension...");
-
     await applyItalicOverlay();
     await startExtension(context);
 }

client/src/services/autocomplete.ts

@@ -3,41 +3,76 @@ 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";
+import { LIQUIDJAVA_ANNOTATION_START, LJAnnotation } from "../utils/constants";
+
+type CompletionItemOptions = {
+    name: string;
+    kind: vscode.CompletionItemKind;
+    description?: string;
+    labelDetail?: string;
+    detail: string;
+    documentationBlocks?: string[];
+    codeBlocks?: string[];
+    insertText?: string;
+    triggerParameterHints?: boolean;
+}
+type CompletionItemKind = "vars" | "ghosts" | "aliases" | "keywords" | "types" | "decls" | "packages";
 
 /**
  * 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;
+            provideCompletionItems(document, position, _token, completionContext) {
+                const annotation = getActiveLiquidJavaAnnotation(document, position);
+                if (!annotation || !extension.contextHistory) return null;
+
+                const isDotTrigger =  completionContext.triggerKind === vscode.CompletionTriggerKind.TriggerCharacter && completionContext.triggerCharacter === ".";
+                const receiver = isDotTrigger ? getReceiverBeforeDot(document, position) : 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);
+                const items = getContextCompletionItems(extension.contextHistory, file, annotation, nextChar, isDotTrigger, receiver);
+                const uniqueItems = new Map<string, vscode.CompletionItem>();
+                items.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 getContextCompletionItems(context: ContextHistory, file: string, nextChar: string): vscode.CompletionItem[] {
+function getContextCompletionItems(context: ContextHistory, file: string, annotation: LJAnnotation, nextChar: string, isDotTrigger: boolean, receiver: string | null): vscode.CompletionItem[] {
+    const triggerParameterHints = nextChar !== "(";
+    if (isDotTrigger) {
+        if (receiver === "this" || receiver === "old(this)") {
+            return getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints);
+        }
+        return [];
+    } 
     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());
+    const itemsHandlers: Record<CompletionItemKind, () => vscode.CompletionItem[]> = {
+        vars: () => getVariableCompletionItems(variablesInScope || []),
+        ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints),
+        aliases: () => getAliasCompletionItems(context.aliases, triggerParameterHints),
+        keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope),
+        types: () => getTypesCompletionItems(),
+        decls: () => getDeclsCompletionItems(),
+        packages: () => [], // TODO
+    }
+    const itemsMap: Record<LJAnnotation, CompletionItemKind[]> = {
+        Refinement: ["vars", "ghosts", "aliases", "keywords"],
+        StateRefinement: ["vars", "ghosts", "aliases", "keywords"],
+        Ghost: ["types"],
+        RefinementAlias: ["types"],
+        RefinementPredicate: ["types", "decls"],
+        StateSet: [],
+        ExternalRefinementsFor: ["packages"]
+    }
+    return itemsMap[annotation].map(key => itemsHandlers[key]()).flat();
 }
 
 function getVariableCompletionItems(variables: Variable[]): vscode.CompletionItem[] {
@@ -105,16 +140,21 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boo
         detail: "keyword",
         documentationBlocks: ["Keyword referring to the **current instance**"],
     });
-    const oldItem = createCompletionItem({
-        name: "old",
+    const oldItem = getOldKeywordCompletionItem(triggerParameterHints);
+    const trueItem = createCompletionItem({
+        name: "true",
         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];
+
+    const falseItem = createCompletionItem({
+        name: "false",
+        kind: vscode.CompletionItemKind.Keyword,
+        description: "",
+        detail: "keyword",
+    });
+    const items: vscode.CompletionItem[] = [thisItem, oldItem, trueItem, falseItem];
     if (!inScope) {
         const returnItem = createCompletionItem({
             name: "return",
@@ -128,16 +168,36 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boo
     return items;
 }
 
-type CompletionItemOptions = {
-    name: string;
-    kind: vscode.CompletionItemKind;
-    description?: string;
-    labelDetail?: string;
-    detail: string;
-    documentationBlocks?: string[];
-    codeBlocks?: string[];
-    insertText?: string;
-    triggerParameterHints?: boolean;
+function getOldKeywordCompletionItem(triggerParameterHints: boolean): vscode.CompletionItem {
+    return 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,
+    });
+}
+
+function getTypesCompletionItems(): vscode.CompletionItem[] {
+    const types = ["int", "double", "float", "boolean"];
+    return types.map(type => createCompletionItem({
+        name: type,
+        kind: vscode.CompletionItemKind.Keyword,
+        description: "",
+        detail: "keyword",
+    }));
+}
+
+function getDeclsCompletionItems(): vscode.CompletionItem[] {
+    const decls = ["ghost", "type"]
+    return decls.map(decl => createCompletionItem({
+        name: decl,
+        kind: vscode.CompletionItemKind.Keyword,
+        description: "",
+        detail: "keyword",
+    }));
 }
 
 function createCompletionItem({ name, kind, labelDetail, description, detail, documentationBlocks, codeBlocks, insertText, triggerParameterHints }: CompletionItemOptions): vscode.CompletionItem {
@@ -155,15 +215,17 @@ function createCompletionItem({ name, kind, labelDetail, description, detail, do
     return item;
 }
 
-function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, position: vscode.Position): boolean {
+function getActiveLiquidJavaAnnotation(document: vscode.TextDocument, position: vscode.Position): LJAnnotation | null {
     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;
+    let lastAnnotationName: LJAnnotation | null = null;
     while ((match = LIQUIDJAVA_ANNOTATION_START.exec(textUntilCursor)) !== null) {
         lastAnnotationStart = match.index;
+        lastAnnotationName = match[2] as LJAnnotation || null;
     }
-    if (lastAnnotationStart === -1) return false;
+    if (lastAnnotationStart === -1 || !lastAnnotationName) return null;
 
     const fromLastAnnotation = textUntilCursor.slice(lastAnnotationStart);
     let parenthesisDepth = 0;
@@ -179,5 +241,14 @@ function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, posit
         if (char === "(") parenthesisDepth++;
         if (char === ")") parenthesisDepth--;
     }
-    return parenthesisDepth > 0;
+    return parenthesisDepth > 0 ? lastAnnotationName : null;
+}
+
+function getReceiverBeforeDot(document: vscode.TextDocument, position: vscode.Position): string | null {
+    const prefix = document.lineAt(position.line).text.slice(0, position.character);
+    const match = prefix.match(/((?:old\s*\(\s*this\s*\))|(?:[A-Za-z_]\w*))\.\w*$/);
+    if (!match) return null;
+    const receiver = match[1].trim();
+    if (/^old\s*\(\s*this\s*\)$/.test(receiver)) return "old(this)";
+    return receiver;
 }

client/src/services/context.ts

@@ -56,7 +56,10 @@ function isSelectionWithinScope(selection: Selection, scope: Selection): boolean
 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);
+        const startPosition = variable.annPosition || placement;
+        if (!startPosition || variable.isParameter) return true; // if is parameter we need to access it even if it's declared after the selection (for method and parameter refinements)
+
+        // variable was declared before the cursor line or its in the same line but before the cursor column
+        return startPosition.line < selection.startLine || startPosition.line === selection.startLine && startPosition.column <= selection.startColumn;
     });
 }

client/src/types/context.ts

@@ -1,4 +1,4 @@
-import { PlacementInCode } from "./diagnostics";
+import { PlacementInCode, SourcePosition } from "./diagnostics";
 
 // Type definitions used for LiquidJava context information
 
@@ -8,6 +8,8 @@ export type Variable = {
   refinement: string;
   mainRefinement: string;
   placementInCode: PlacementInCode | null;
+  isParameter: boolean;
+  annPosition: SourcePosition | null;
 }
 
 export type Ghost = {
@@ -27,9 +29,9 @@ export type Alias = {
 
 export type ContextHistory = {
   vars: Record<string, Record<string, Variable[]>>; // file -> (scope -> variables in scope)
+  ghosts: Record<string, Ghost[]>; // file -> ghosts in file
   instanceVars: Variable[];
   globalVars: Variable[];
-  ghosts: Ghost[];
   aliases: Alias[];
 }
 

client/src/types/diagnostics.ts

@@ -9,15 +9,15 @@ export type ErrorPosition = {
     colEnd: number;
 }
 
-export type Position = {
+export type SourcePosition = {
     file: string;
     line: number;
     column: number;
 }
 
 export type PlacementInCode = {
     text: string;
-    position: Position;
+    position: SourcePosition;
 }
 
 export type TranslationTable = Record<string, PlacementInCode>;

client/src/utils/constants.ts

@@ -27,4 +27,5 @@ export const LIQUIDJAVA_ANNOTATIONS = [
     "StateRefinement",
     "ExternalRefinementsFor",
 ]
-export const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g");
+export const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g");
+export type LJAnnotation = "Refinement" | "RefinementAlias" | "RefinementPredicate" | "StateSet" | "Ghost" | "StateRefinement" | "ExternalRefinementsFor";

server/pom.xml

@@ -169,13 +169,6 @@
 	</dependencyManagement>
 
 	<dependencies>
-		<!-- <dependency>
-			<groupId>liquidjava</groupId>
-			<artifactId>verifier</artifactId>
-			<version>0.0.13</version>
-			<scope>system</scope>
-			<systemPath>${project.basedir}/libs/liquidjava-verifier.jar</systemPath>
-		</dependency> -->
 		<dependency>
 			<groupId>io.github.liquid-java</groupId>
 			<artifactId>liquidjava-verifier</artifactId>

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

@@ -12,7 +12,7 @@ public record ContextHistoryDTO(
     Map<String, Map<String, List<VariableDTO>>> vars,
     List<VariableDTO> instanceVars,
     List<VariableDTO> globalVars,
-    List<GhostDTO> ghosts,
+    Map<String, List<GhostDTO>> ghosts,
     List<AliasDTO> aliases
 ) {
     public static String stringifyType(CtTypeReference<?> typeReference) {

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

@@ -1,8 +1,8 @@
 package dtos.context;
 
 import dtos.diagnostics.PlacementInCodeDTO;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.processor.context.RefinedVariable;
-import spoon.reflect.reference.CtTypeReference;
 
 /**
  * DTO for serializing RefinedVariable instances to JSON.
@@ -12,15 +12,19 @@ public record VariableDTO(
     String type,
     String refinement,
     String mainRefinement,
-    PlacementInCodeDTO placementInCode
+    PlacementInCodeDTO placementInCode,
+    boolean isParameter,
+    SourcePositionDTO annPosition
 ) {
     public static VariableDTO from(RefinedVariable refinedVariable) {
         return new VariableDTO(
             refinedVariable.getName(),
             ContextHistoryDTO.stringifyType(refinedVariable.getType()),
             refinedVariable.getRefinement().toString(),
             refinedVariable.getMainRefinement().toString(),
-            PlacementInCodeDTO.from(refinedVariable.getPlacementInCode())
+            PlacementInCodeDTO.from(refinedVariable.getPlacementInCode()),
+            refinedVariable.isParameter(),
+            SourcePositionDTO.from(refinedVariable.getAnnPosition())
         );
     }
 }

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

@@ -5,11 +5,11 @@
 /**
  * DTO for serializing PlacementInCode instances to JSON
  */
-public record PlacementInCodeDTO(String text, PositionDTO position) {
+public record PlacementInCodeDTO(String text, SourcePositionDTO position) {
 
     public static PlacementInCodeDTO from(PlacementInCode placement) {
         if (placement == null)
             return null;
-        return new PlacementInCodeDTO(placement.getText(), PositionDTO.from(placement.getPosition()));
+        return new PlacementInCodeDTO(placement.getText(), SourcePositionDTO.from(placement.getPosition()));
     }
 }

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

@@ -5,10 +5,10 @@
 /**
  * DTO for serializing Spoon SourcePosition to JSON
  */
-public record PositionDTO(String file, int line, int column) {
+public record SourcePositionDTO(String file, int line, int column) {
 
-    public static PositionDTO from(SourcePosition position) {
+    public static SourcePositionDTO from(SourcePosition position) {
         String file = position.getFile() != null ? position.getFile().getAbsolutePath() : "";
-        return new PositionDTO(file, position.getLine(), position.getColumn());
+        return new SourcePositionDTO(file, position.getLine() - 1, position.getColumn() - 1);
     }
 }