diff --git a/client/src/extension.ts b/client/src/extension.ts index cf230fa..adf7f12 100644 --- a/client/src/extension.ts +++ b/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); } diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 15c5e56..1b3d0d1 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -3,7 +3,20 @@ 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 @@ -11,33 +24,55 @@ import { LIQUIDJAVA_ANNOTATION_START } from "../utils/constants"; 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(); + 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(); - 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 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 = { + 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; } \ No newline at end of file diff --git a/client/src/services/context.ts b/client/src/services/context.ts index dcd53c7..e481f42 100644 --- a/client/src/services/context.ts +++ b/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; }); } \ No newline at end of file diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 8efebe8..145a070 100644 --- a/client/src/types/context.ts +++ b/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>; // file -> (scope -> variables in scope) + ghosts: Record; // file -> ghosts in file instanceVars: Variable[]; globalVars: Variable[]; - ghosts: Ghost[]; aliases: Alias[]; } diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 9e2bdf5..6c84af1 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -9,7 +9,7 @@ export type ErrorPosition = { colEnd: number; } -export type Position = { +export type SourcePosition = { file: string; line: number; column: number; @@ -17,7 +17,7 @@ export type Position = { export type PlacementInCode = { text: string; - position: Position; + position: SourcePosition; } export type TranslationTable = Record; diff --git a/client/src/utils/constants.ts b/client/src/utils/constants.ts index 7123aef..60a53b0 100644 --- a/client/src/utils/constants.ts +++ b/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"); \ No newline at end of file +export const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g"); +export type LJAnnotation = "Refinement" | "RefinementAlias" | "RefinementPredicate" | "StateSet" | "Ghost" | "StateRefinement" | "ExternalRefinementsFor"; \ No newline at end of file diff --git a/server/pom.xml b/server/pom.xml index ce5155b..0886577 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -169,13 +169,6 @@ - io.github.liquid-java liquidjava-verifier diff --git a/server/src/main/java/dtos/context/ContextHistoryDTO.java b/server/src/main/java/dtos/context/ContextHistoryDTO.java index aa279e2..2f3f86d 100644 --- a/server/src/main/java/dtos/context/ContextHistoryDTO.java +++ b/server/src/main/java/dtos/context/ContextHistoryDTO.java @@ -12,7 +12,7 @@ public record ContextHistoryDTO( Map>> vars, List instanceVars, List globalVars, - List ghosts, + Map> ghosts, List aliases ) { public static String stringifyType(CtTypeReference typeReference) { diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index d33664c..f89148e 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/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,7 +12,9 @@ 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( @@ -20,7 +22,9 @@ public static VariableDTO from(RefinedVariable refinedVariable) { ContextHistoryDTO.stringifyType(refinedVariable.getType()), refinedVariable.getRefinement().toString(), refinedVariable.getMainRefinement().toString(), - PlacementInCodeDTO.from(refinedVariable.getPlacementInCode()) + PlacementInCodeDTO.from(refinedVariable.getPlacementInCode()), + refinedVariable.isParameter(), + SourcePositionDTO.from(refinedVariable.getAnnPosition()) ); } } \ No newline at end of file diff --git a/server/src/main/java/dtos/diagnostics/PlacementInCodeDTO.java b/server/src/main/java/dtos/diagnostics/PlacementInCodeDTO.java index 3ab1833..f782c8f 100644 --- a/server/src/main/java/dtos/diagnostics/PlacementInCodeDTO.java +++ b/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())); } } diff --git a/server/src/main/java/dtos/diagnostics/PositionDTO.java b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java similarity index 50% rename from server/src/main/java/dtos/diagnostics/PositionDTO.java rename to server/src/main/java/dtos/diagnostics/SourcePositionDTO.java index 06224e5..1e6f6f3 100644 --- a/server/src/main/java/dtos/diagnostics/PositionDTO.java +++ b/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); } } diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index 3e98dda..cfc19e2 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/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>> toVariablesMap(Map> toGhostsMap(Map> 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 + )); + } }