Autocomplete Improvements

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,7 @@ 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;
+        if (!placement || 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)
         return placement.line < selection.startLine || (placement.line === selection.startLine && placement.column <= selection.startColumn);
     });
 }

client/src/types/context.ts

@@ -8,6 +8,7 @@ export type Variable = {
   refinement: string;
   mainRefinement: string;
   placementInCode: PlacementInCode | null;
+  isParameter: boolean;
 }
 
 export type Ghost = {
@@ -27,9 +28,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/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/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

@@ -2,7 +2,6 @@
 
 import dtos.diagnostics.PlacementInCodeDTO;
 import liquidjava.processor.context.RefinedVariable;
-import spoon.reflect.reference.CtTypeReference;
 
 /**
  * DTO for serializing RefinedVariable instances to JSON.
@@ -12,15 +11,17 @@ public record VariableDTO(
     String type,
     String refinement,
     String mainRefinement,
-    PlacementInCodeDTO placementInCode
+    PlacementInCodeDTO placementInCode,
+    boolean isParameter
 ) {
     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()
         );
     }
 }

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

@@ -11,6 +11,7 @@
 import dtos.context.GhostDTO;
 import dtos.context.VariableDTO;
 import liquidjava.processor.context.ContextHistory;
+import liquidjava.processor.context.GhostState;
 import liquidjava.processor.context.RefinedVariable;
 
 /**
@@ -28,7 +29,7 @@ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) {
             toVariablesMap(contextHistory.getFileScopeVars()),
             contextHistory.getInstanceVars().stream().map(VariableDTO::from).collect(Collectors.toList()),
             contextHistory.getGlobalVars().stream().map(VariableDTO::from).collect(Collectors.toList()),
-            contextHistory.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()),
+            toGhostsMap(contextHistory.getGhosts()),
             contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList())
         );
     }
@@ -46,4 +47,13 @@ private static Map<String, Map<String, List<VariableDTO>>> toVariablesMap(Map<St
             HashMap::new
         ));
     }
+
+    private static Map<String, List<GhostDTO>> toGhostsMap(Map<String, Set<GhostState>> ghosts) {
+        return ghosts.entrySet().stream().collect(Collectors.toMap(
+            Map.Entry::getKey,
+            entry -> entry.getValue().stream().map(GhostDTO::from).collect(Collectors.toList()),
+            (left, right) -> left,
+            HashMap::new
+        ));
+    }
 }