From 3d358aed459809e7d714943abcbd6412cabad620 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 14:41:34 +0000 Subject: [PATCH 01/15] Add Autocomplete --- client/src/services/autocomplete.ts | 132 ++++++------------ client/src/services/context.ts | 15 +- client/src/services/events.ts | 6 +- client/src/utils/constants.ts | 4 +- .../java/utils/ContextHistoryConverter.java | 2 +- 5 files changed, 56 insertions(+), 103 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 15c5e56..93eb180 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -1,9 +1,11 @@ import * as vscode from "vscode"; import { extension } from "../state"; import type { Variable, ContextHistory, Ghost, Alias } from "../types/context"; +import { LIQUIDJAVA_ANNOTATIONS } from "../utils/constants"; import { getSimpleName } from "../utils/utils"; import { getVariablesInScope } from "./context"; -import { LIQUIDJAVA_ANNOTATION_START } from "../utils/constants"; + +const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g"); /** * Registers a completion provider for LiquidJava annotations, providing context-aware suggestions based on the current context history @@ -14,28 +16,31 @@ export function registerAutocomplete(context: vscode.ExtensionContext) { 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); + return getContextCompletionItems(extension.contextHistory, file); }, }) ); } -function getContextCompletionItems(context: ContextHistory, file: string, nextChar: string): vscode.CompletionItem[] { +function getContextCompletionItems(context: ContextHistory, file: string): vscode.CompletionItem[] { + const variables: Variable[] = []; 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]; + variables.push(...variablesInScope); + variables.push(...context.instanceVars); + variables.push(...context.globalVars); + + const variableItems = getVariableCompletionItems(variablesInScope); + const ghostItems = getGhostCompletionItems(context.ghosts); + const aliasItems = getAliasCompletionItems(context.aliases); + const allItems = [...variableItems, ...ghostItems, ...aliasItems]; // 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); + if (!uniqueItems.has(label)) { + uniqueItems.set(label, item); + } }); return Array.from(uniqueItems.values()); } @@ -43,104 +48,73 @@ function getContextCompletionItems(context: ContextHistory, file: string, nextCh 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); + const documentationBlocks: string[] = []; + if (variable.mainRefinement !== "true") documentationBlocks.push(`@Refinement("${variable.mainRefinement}")`); + documentationBlocks.push(varSig); + return createCompletionItem({ name: variable.name, kind: vscode.CompletionItemKind.Variable, description: variable.type, detail: "variable", - codeBlocks, + documentationBlocks, }); }); } -function getGhostCompletionItems(ghosts: Ghost[], triggerParameterHints: boolean): vscode.CompletionItem[] { +function getGhostCompletionItems(ghosts: Ghost[]): 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"; + const parametersStr = `(${parameters})`; + const ghostSig = `${ghost.returnType} ${ghost.name}${parametersStr}`; return createCompletionItem({ name: ghost.name, kind: vscode.CompletionItemKind.Function, - labelDetail: `(${parameters})`, - description, - detail: description, - codeBlocks: [ghostSig], - insertText: triggerParameterHints ? `${ghost.name}($1)` : ghost.name, - triggerParameterHints, + labelDetail: parametersStr, + description: ghost.returnType, + detail: "ghost", + documentationBlocks: [ghostSig], + insertText: `${ghost.name}($1)`, + triggerParameterHints: true, }); }); } -function getAliasCompletionItems(aliases: Alias[], triggerParameterHints: boolean): vscode.CompletionItem[] { +function getAliasCompletionItems(aliases: Alias[]): 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"; + const parametersStr = `(${parameters})`; + const aliasSig = `${alias.name}${parametersStr} { ${alias.predicate} }`; + 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, + labelDetail: parametersStr, + description: alias.predicate, + detail: "alias", + documentationBlocks: [aliasSig], + insertText: `${alias.name}($1)`, + triggerParameterHints: true, }); }); } -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[]; + documentationBlocks: string[]; insertText?: string; triggerParameterHints?: boolean; } -function createCompletionItem({ name, kind, labelDetail, description, detail, documentationBlocks, codeBlocks, insertText, triggerParameterHints }: CompletionItemOptions): vscode.CompletionItem { +function createCompletionItem({ name, kind, labelDetail, description, detail, documentationBlocks, insertText, triggerParameterHints }: CompletionItemOptions): vscode.CompletionItem { const item = new vscode.CompletionItem(name, kind); item.label = { label: name, detail: labelDetail, description }; item.detail = detail; @@ -148,10 +122,8 @@ function createCompletionItem({ name, kind, labelDetail, description, detail, do 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)); + documentationBlocks.forEach(block => documentation.appendCodeblock(block)); item.documentation = documentation; - return item; } @@ -164,20 +136,6 @@ function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, posit 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; + return !fromLastAnnotation.includes(")"); } \ No newline at end of file diff --git a/client/src/services/context.ts b/client/src/services/context.ts index dcd53c7..2930ba2 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -5,14 +5,12 @@ 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; +export function getVariablesInScope(file: string, selection: Selection): Variable[] { + if (!extension.contextHistory || !selection || !file) return []; // get variables in file const fileVars = extension.contextHistory.vars[file]; - if (!fileVars) return null; + if (!fileVars) return []; // get variables in the current scope based on the selection let mostSpecificScope: string | null = null; @@ -29,13 +27,10 @@ export function getVariablesInScope(file: string, selection: Selection): Variabl } } } - if (mostSpecificScope === null) - return null; + const variablesInScope = mostSpecificScope ? fileVars[mostSpecificScope] : []; // 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#")); + return getReachableVariables(variablesInScope, selection); } function parseScopeString(scope: string): Selection { diff --git a/client/src/services/events.ts b/client/src/services/events.ts index bc8501b..c9c59e6 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -2,10 +2,10 @@ 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 }; +const SELECTION_DEBOUNCE_TIME = 250; // ms /** * Initializes file system event listeners @@ -56,5 +56,7 @@ export async function onSelectionChange(event: vscode.TextEditorSelectionChangeE }; // debounce selection changes if (selectionTimeout) clearTimeout(selectionTimeout); - selectionTimeout = setTimeout(() => extension.selection = currentSelection, SELECTION_DEBOUNCE_MS); + selectionTimeout = setTimeout(() => { + extension.selection = currentSelection; + }, SELECTION_DEBOUNCE_TIME); } \ No newline at end of file diff --git a/client/src/utils/constants.ts b/client/src/utils/constants.ts index 7123aef..b7fb09c 100644 --- a/client/src/utils/constants.ts +++ b/client/src/utils/constants.ts @@ -2,7 +2,6 @@ export const SERVER_JAR = "language-server-liquidjava.jar"; export const JAVA_BINARY = "java"; export const DEBUG_MODE = false; export const DEBUG_PORT = 50000; -export const SELECTION_DEBOUNCE_MS = 250; export const LIQUIDJAVA_SCOPES = [ "source.liquidjava keyword.other.liquidjava", "source.liquidjava entity.name.function.liquidjava", @@ -26,5 +25,4 @@ export const LIQUIDJAVA_ANNOTATIONS = [ "Ghost", "StateRefinement", "ExternalRefinementsFor", -] -export const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g"); \ No newline at end of file +] \ No newline at end of file diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index 3e98dda..1f0bf5d 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/server/src/main/java/utils/ContextHistoryConverter.java @@ -25,7 +25,7 @@ public class ContextHistoryConverter { */ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) { return new ContextHistoryDTO( - toVariablesMap(contextHistory.getFileScopeVars()), + toVariablesMap(contextHistory.getVars()), 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()), From 31cb7b73b86432fba9bd7b8957531a0d4ea5800e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 15:39:00 +0000 Subject: [PATCH 02/15] Add Keywords --- client/src/services/autocomplete.ts | 67 ++++++++++++++++++++++++----- 1 file changed, 56 insertions(+), 11 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 93eb180..55b751f 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -32,7 +32,8 @@ function getContextCompletionItems(context: ContextHistory, file: string): vscod const variableItems = getVariableCompletionItems(variablesInScope); const ghostItems = getGhostCompletionItems(context.ghosts); const aliasItems = getAliasCompletionItems(context.aliases); - const allItems = [...variableItems, ...ghostItems, ...aliasItems]; + const keywordItems = getKeywordsCompletionItems(); + const allItems = [...variableItems, ...ghostItems, ...aliasItems, ...keywordItems]; // remove duplicates const uniqueItems = new Map(); @@ -48,16 +49,16 @@ function getContextCompletionItems(context: ContextHistory, file: string): vscod function getVariableCompletionItems(variables: Variable[]): vscode.CompletionItem[] { return variables.map(variable => { const varSig = `${variable.type} ${variable.name}`; - const documentationBlocks: string[] = []; - if (variable.mainRefinement !== "true") documentationBlocks.push(`@Refinement("${variable.mainRefinement}")`); - documentationBlocks.push(varSig); + 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", - documentationBlocks, + codeBlocks, }); }); } @@ -73,7 +74,7 @@ function getGhostCompletionItems(ghosts: Ghost[]): vscode.CompletionItem[] { labelDetail: parametersStr, description: ghost.returnType, detail: "ghost", - documentationBlocks: [ghostSig], + codeBlocks: [ghostSig], insertText: `${ghost.name}($1)`, triggerParameterHints: true, }); @@ -96,25 +97,52 @@ function getAliasCompletionItems(aliases: Alias[]): vscode.CompletionItem[] { labelDetail: parametersStr, description: alias.predicate, detail: "alias", - documentationBlocks: [aliasSig], + codeBlocks: [aliasSig], insertText: `${alias.name}($1)`, triggerParameterHints: true, }); }); } +function getKeywordsCompletionItems(): 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**"], + triggerParameterHints: true, + }); + const resultItem = createCompletionItem({ + name: "return", + kind: vscode.CompletionItemKind.Keyword, + description: "", + detail: "keyword", + documentationBlocks: ["Keyword referring to the **method return value**"], + }); + return [thisItem, oldItem, resultItem]; +} + type CompletionItemOptions = { name: string; kind: vscode.CompletionItemKind; description?: string; labelDetail?: string; detail: string; - documentationBlocks: string[]; + documentationBlocks?: string[]; + codeBlocks?: string[]; insertText?: string; triggerParameterHints?: boolean; } -function createCompletionItem({ name, kind, labelDetail, description, detail, documentationBlocks, insertText, triggerParameterHints }: CompletionItemOptions): vscode.CompletionItem { +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; @@ -122,8 +150,10 @@ function createCompletionItem({ name, kind, labelDetail, description, detail, do if (triggerParameterHints) item.command = { command: "editor.action.triggerParameterHints", title: "Trigger Parameter Hints" }; const documentation = new vscode.MarkdownString(); - documentationBlocks.forEach(block => documentation.appendCodeblock(block)); + if (documentationBlocks) documentationBlocks.forEach(block => documentation.appendMarkdown(block)); + if (codeBlocks) codeBlocks.forEach(block => documentation.appendCodeblock(block)); item.documentation = documentation; + return item; } @@ -137,5 +167,20 @@ function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, posit } if (lastAnnotationStart === -1) return false; const fromLastAnnotation = textUntilCursor.slice(lastAnnotationStart); - return !fromLastAnnotation.includes(")"); + + 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; } \ No newline at end of file From ae33d56d36f5e8f3201ed145eef58120bea8fcac Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 15:58:46 +0000 Subject: [PATCH 03/15] Minor Fix --- client/src/services/autocomplete.ts | 1 + 1 file changed, 1 insertion(+) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 55b751f..1bf5fa2 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -118,6 +118,7 @@ function getKeywordsCompletionItems(): vscode.CompletionItem[] { description: "", detail: "keyword", documentationBlocks: ["Keyword referring to the **previous state of the current instance**"], + insertText: "old($1)", triggerParameterHints: true, }); const resultItem = createCompletionItem({ From 40d5a7a24834a5899ee7d2262391f5db6526335f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 23:03:13 +0000 Subject: [PATCH 04/15] Parameter Hints Based on Next Char --- client/src/services/autocomplete.ts | 41 +++++++++++++---------------- 1 file changed, 18 insertions(+), 23 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 1bf5fa2..24f61e6 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -16,32 +16,27 @@ export function registerAutocomplete(context: vscode.ExtensionContext) { provideCompletionItems(document, position) { if (!isInsideLiquidJavaAnnotationString(document, position) || !extension.contextHistory) return null; const file = document.uri.toString().replace("file://", ""); - return getContextCompletionItems(extension.contextHistory, 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): vscode.CompletionItem[] { - const variables: Variable[] = []; +function getContextCompletionItems(context: ContextHistory, file: string, nextChar: string): vscode.CompletionItem[] { const variablesInScope = getVariablesInScope(file, extension.selection); - variables.push(...variablesInScope); - variables.push(...context.instanceVars); - variables.push(...context.globalVars); - - const variableItems = getVariableCompletionItems(variablesInScope); - const ghostItems = getGhostCompletionItems(context.ghosts); - const aliasItems = getAliasCompletionItems(context.aliases); - const keywordItems = getKeywordsCompletionItems(); + const triggerParameterHints = nextChar !== "("; + const variableItems = getVariableCompletionItems([...variablesInScope, ...context.instanceVars, ...context.globalVars]); + const ghostItems = getGhostCompletionItems(context.ghosts, triggerParameterHints); + const aliasItems = getAliasCompletionItems(context.aliases, triggerParameterHints); + const keywordItems = getKeywordsCompletionItems(triggerParameterHints); 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); - } + if (!uniqueItems.has(label)) uniqueItems.set(label, item); }); return Array.from(uniqueItems.values()); } @@ -63,7 +58,7 @@ function getVariableCompletionItems(variables: Variable[]): vscode.CompletionIte }); } -function getGhostCompletionItems(ghosts: Ghost[]): vscode.CompletionItem[] { +function getGhostCompletionItems(ghosts: Ghost[], triggerParameterHints: boolean): vscode.CompletionItem[] { return ghosts.map(ghost => { const parameters = ghost.parameterTypes.map(getSimpleName).join(", "); const parametersStr = `(${parameters})`; @@ -75,13 +70,13 @@ function getGhostCompletionItems(ghosts: Ghost[]): vscode.CompletionItem[] { description: ghost.returnType, detail: "ghost", codeBlocks: [ghostSig], - insertText: `${ghost.name}($1)`, - triggerParameterHints: true, + insertText: triggerParameterHints ? `${ghost.name}($1)` : ghost.name, + triggerParameterHints, }); }); } -function getAliasCompletionItems(aliases: Alias[]): vscode.CompletionItem[] { +function getAliasCompletionItems(aliases: Alias[], triggerParameterHints: boolean): vscode.CompletionItem[] { return aliases.map(alias => { const parameters = alias.parameters .map((parameter, index) => { @@ -98,13 +93,13 @@ function getAliasCompletionItems(aliases: Alias[]): vscode.CompletionItem[] { description: alias.predicate, detail: "alias", codeBlocks: [aliasSig], - insertText: `${alias.name}($1)`, - triggerParameterHints: true, + insertText: triggerParameterHints ? `${alias.name}($1)` : alias.name, + triggerParameterHints, }); }); } -function getKeywordsCompletionItems(): vscode.CompletionItem[] { +function getKeywordsCompletionItems(triggerParameterHints: boolean): vscode.CompletionItem[] { const thisItem = createCompletionItem({ name: "this", kind: vscode.CompletionItemKind.Keyword, @@ -118,8 +113,8 @@ function getKeywordsCompletionItems(): vscode.CompletionItem[] { description: "", detail: "keyword", documentationBlocks: ["Keyword referring to the **previous state of the current instance**"], - insertText: "old($1)", - triggerParameterHints: true, + insertText: triggerParameterHints ? "old($1)" : "old", + triggerParameterHints, }); const resultItem = createCompletionItem({ name: "return", From 716ed25349245dc03930180e49f3a4336a56e254 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 23:07:08 +0000 Subject: [PATCH 05/15] Don't Show Suggestions with `this#` --- client/src/services/autocomplete.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 24f61e6..b698734 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -36,7 +36,7 @@ function getContextCompletionItems(context: ContextHistory, file: string, nextCh 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); + if (!uniqueItems.has(label) && !label.startsWith("this#")) uniqueItems.set(label, item); }); return Array.from(uniqueItems.values()); } From 4b823044f8dac5ed75867417162f4f60b6508f1d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 23:10:51 +0000 Subject: [PATCH 06/15] Move Constants --- client/src/services/autocomplete.ts | 7 ++----- client/src/services/events.ts | 6 ++---- client/src/utils/constants.ts | 4 +++- 3 files changed, 7 insertions(+), 10 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index b698734..eded5ad 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -1,11 +1,9 @@ import * as vscode from "vscode"; import { extension } from "../state"; import type { Variable, ContextHistory, Ghost, Alias } from "../types/context"; -import { LIQUIDJAVA_ANNOTATIONS } from "../utils/constants"; import { getSimpleName } from "../utils/utils"; import { getVariablesInScope } from "./context"; - -const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g"); +import { LIQUIDJAVA_ANNOTATION_START } from "../utils/constants"; /** * Registers a completion provider for LiquidJava annotations, providing context-aware suggestions based on the current context history @@ -162,14 +160,13 @@ function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, posit 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; diff --git a/client/src/services/events.ts b/client/src/services/events.ts index c9c59e6..bc8501b 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -2,10 +2,10 @@ 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 }; -const SELECTION_DEBOUNCE_TIME = 250; // ms /** * Initializes file system event listeners @@ -56,7 +56,5 @@ export async function onSelectionChange(event: vscode.TextEditorSelectionChangeE }; // debounce selection changes if (selectionTimeout) clearTimeout(selectionTimeout); - selectionTimeout = setTimeout(() => { - extension.selection = currentSelection; - }, SELECTION_DEBOUNCE_TIME); + selectionTimeout = setTimeout(() => extension.selection = currentSelection, SELECTION_DEBOUNCE_MS); } \ No newline at end of file diff --git a/client/src/utils/constants.ts b/client/src/utils/constants.ts index b7fb09c..7123aef 100644 --- a/client/src/utils/constants.ts +++ b/client/src/utils/constants.ts @@ -2,6 +2,7 @@ export const SERVER_JAR = "language-server-liquidjava.jar"; export const JAVA_BINARY = "java"; export const DEBUG_MODE = false; export const DEBUG_PORT = 50000; +export const SELECTION_DEBOUNCE_MS = 250; export const LIQUIDJAVA_SCOPES = [ "source.liquidjava keyword.other.liquidjava", "source.liquidjava entity.name.function.liquidjava", @@ -25,4 +26,5 @@ export const LIQUIDJAVA_ANNOTATIONS = [ "Ghost", "StateRefinement", "ExternalRefinementsFor", -] \ No newline at end of file +] +export const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g"); \ No newline at end of file From eb030810fe3b036986dbef2562ba52f862e4a61a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 23:16:02 +0000 Subject: [PATCH 07/15] Add `this` Keyword in Syntax Highlighting --- client/src/services/autocomplete.ts | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index eded5ad..70d4857 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -114,14 +114,14 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean): vscode.Comp insertText: triggerParameterHints ? "old($1)" : "old", triggerParameterHints, }); - const resultItem = createCompletionItem({ + const returnItem = createCompletionItem({ name: "return", kind: vscode.CompletionItemKind.Keyword, description: "", detail: "keyword", documentationBlocks: ["Keyword referring to the **method return value**"], }); - return [thisItem, oldItem, resultItem]; + return [thisItem, oldItem, returnItem]; } type CompletionItemOptions = { @@ -160,7 +160,7 @@ function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, posit lastAnnotationStart = match.index; } if (lastAnnotationStart === -1) return false; - + const fromLastAnnotation = textUntilCursor.slice(lastAnnotationStart); let parenthesisDepth = 0; let isInsideString = false; From d05b751177f02da51d98fe1c6a5937f3b0a800d5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 20 Feb 2026 15:27:53 +0000 Subject: [PATCH 08/15] Improvements --- client/src/services/autocomplete.ts | 27 +++++++++++++-------------- client/src/services/context.ts | 3 ++- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 70d4857..939f2e7 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -24,7 +24,7 @@ export function registerAutocomplete(context: vscode.ExtensionContext) { function getContextCompletionItems(context: ContextHistory, file: string, nextChar: string): vscode.CompletionItem[] { const variablesInScope = getVariablesInScope(file, extension.selection); const triggerParameterHints = nextChar !== "("; - const variableItems = getVariableCompletionItems([...variablesInScope, ...context.instanceVars, ...context.globalVars]); + 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); @@ -34,7 +34,7 @@ function getContextCompletionItems(context: ContextHistory, file: string, nextCh const uniqueItems = new Map(); allItems.forEach(item => { const label = typeof item.label === "string" ? item.label : item.label.label; - if (!uniqueItems.has(label) && !label.startsWith("this#")) uniqueItems.set(label, item); + if (!uniqueItems.has(label)) uniqueItems.set(label, item); }); return Array.from(uniqueItems.values()); } @@ -45,7 +45,6 @@ function getVariableCompletionItems(variables: Variable[]): vscode.CompletionIte const codeBlocks: string[] = []; if (variable.mainRefinement !== "true") codeBlocks.push(`@Refinement("${variable.mainRefinement}")`); codeBlocks.push(varSig); - return createCompletionItem({ name: variable.name, kind: vscode.CompletionItemKind.Variable, @@ -59,14 +58,15 @@ function getVariableCompletionItems(variables: Variable[]): vscode.CompletionIte function getGhostCompletionItems(ghosts: Ghost[], triggerParameterHints: boolean): vscode.CompletionItem[] { return ghosts.map(ghost => { const parameters = ghost.parameterTypes.map(getSimpleName).join(", "); - const parametersStr = `(${parameters})`; - const ghostSig = `${ghost.returnType} ${ghost.name}${parametersStr}`; + 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: parametersStr, - description: ghost.returnType, - detail: "ghost", + labelDetail: `(${parameters})`, + description, + detail: description, codeBlocks: [ghostSig], insertText: triggerParameterHints ? `${ghost.name}($1)` : ghost.name, triggerParameterHints, @@ -81,15 +81,14 @@ function getAliasCompletionItems(aliases: Alias[], triggerParameterHints: boolea const type = getSimpleName(alias.types[index]); return `${type} ${parameter}`; }).join(", "); - const parametersStr = `(${parameters})`; - const aliasSig = `${alias.name}${parametersStr} { ${alias.predicate} }`; - + const aliasSig = `${alias.name}(${parameters}) { ${alias.predicate} }`; + const description = "alias"; return createCompletionItem({ name: alias.name, kind: vscode.CompletionItemKind.Function, - labelDetail: parametersStr, - description: alias.predicate, - detail: "alias", + labelDetail: `(${parameters}){ ${alias.predicate} }`, + description, + detail: description, codeBlocks: [aliasSig], insertText: triggerParameterHints ? `${alias.name}($1)` : alias.name, triggerParameterHints, diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 2930ba2..70856d5 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -30,7 +30,8 @@ export function getVariablesInScope(file: string, selection: Selection): Variabl const variablesInScope = mostSpecificScope ? fileVars[mostSpecificScope] : []; // filter variables to only include those that are reachable based on their position - return getReachableVariables(variablesInScope, selection); + const reachableVariables = getReachableVariables(variablesInScope, selection); + return reachableVariables.filter(v => !v.name.startsWith("this#")) } function parseScopeString(scope: string): Selection { From 5fd0fff2b3dc94691a590c84fd487e6a726a49e0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 20 Feb 2026 15:53:30 +0000 Subject: [PATCH 09/15] Only Suggest `return` When Not In Method Scope This is still not perfect because it suggests `return` when we are refining a class field. --- client/src/services/autocomplete.ts | 27 ++++++++++++++++----------- client/src/services/context.ts | 14 +++++++++----- 2 files changed, 25 insertions(+), 16 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 939f2e7..15c5e56 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -23,11 +23,12 @@ export function registerAutocomplete(context: vscode.ExtensionContext) { 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 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); + const keywordItems = getKeywordsCompletionItems(triggerParameterHints, inScope); const allItems = [...variableItems, ...ghostItems, ...aliasItems, ...keywordItems]; // remove duplicates @@ -96,7 +97,7 @@ function getAliasCompletionItems(aliases: Alias[], triggerParameterHints: boolea }); } -function getKeywordsCompletionItems(triggerParameterHints: boolean): vscode.CompletionItem[] { +function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boolean): vscode.CompletionItem[] { const thisItem = createCompletionItem({ name: "this", kind: vscode.CompletionItemKind.Keyword, @@ -113,14 +114,18 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean): vscode.Comp insertText: triggerParameterHints ? "old($1)" : "old", triggerParameterHints, }); - const returnItem = createCompletionItem({ - name: "return", - kind: vscode.CompletionItemKind.Keyword, - description: "", - detail: "keyword", - documentationBlocks: ["Keyword referring to the **method return value**"], - }); - return [thisItem, oldItem, returnItem]; + 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 = { diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 70856d5..dcd53c7 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -5,12 +5,14 @@ export function handleContextHistory(contextHistory: ContextHistory) { extension.contextHistory = contextHistory; } -export function getVariablesInScope(file: string, selection: Selection): Variable[] { - if (!extension.contextHistory || !selection || !file) return []; +// 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 []; + if (!fileVars) return null; // get variables in the current scope based on the selection let mostSpecificScope: string | null = null; @@ -27,11 +29,13 @@ export function getVariablesInScope(file: string, selection: Selection): Variabl } } } - const variablesInScope = mostSpecificScope ? fileVars[mostSpecificScope] : []; + 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#")) + return reachableVariables.filter(v => !v.name.startsWith("this#")); } function parseScopeString(scope: string): Selection { From 65133585bf4e05eca6e027a6c7dc28d669c5a130 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 20 Feb 2026 19:09:39 +0000 Subject: [PATCH 10/15] Only Suggest Ghosts in File --- client/src/services/autocomplete.ts | 4 +++- client/src/types/context.ts | 2 +- .../main/java/dtos/context/ContextHistoryDTO.java | 2 +- server/src/main/java/dtos/context/VariableDTO.java | 1 - .../src/main/java/utils/ContextHistoryConverter.java | 12 +++++++++++- 5 files changed, 16 insertions(+), 5 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 15c5e56..fb47599 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -26,7 +26,9 @@ function getContextCompletionItems(context: ContextHistory, file: string, nextCh const inScope = variablesInScope !== null; const triggerParameterHints = nextChar !== "("; const variableItems = getVariableCompletionItems([...(variablesInScope || []), ...context.globalVars]); // not including instance vars - const ghostItems = getGhostCompletionItems(context.ghosts, triggerParameterHints); + + const ghostsInFile = context.ghosts[file] || []; + const ghostItems = getGhostCompletionItems(ghostsInFile, triggerParameterHints); const aliasItems = getAliasCompletionItems(context.aliases, triggerParameterHints); const keywordItems = getKeywordsCompletionItems(triggerParameterHints, inScope); const allItems = [...variableItems, ...ghostItems, ...aliasItems, ...keywordItems]; diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 8efebe8..613a7bb 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -27,9 +27,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/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..9f6eff3 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/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. diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index 1f0bf5d..c5e2fe6 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.getVars()), 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 + )); + } } From 8c4a8c0f641ffcbf189c8458716cb66a97a5991b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 22 Feb 2026 18:44:28 +0000 Subject: [PATCH 11/15] Annotation-Specific Suggestions --- client/src/services/autocomplete.ts | 105 ++++++++++++++++++++-------- client/src/utils/constants.ts | 3 +- 2 files changed, 78 insertions(+), 30 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index fb47599..5ef5ece 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" | "imports"; /** * Registers a completion provider for LiquidJava annotations, providing context-aware suggestions based on the current context history @@ -12,30 +25,41 @@ 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 annotation = getActiveLiquidJavaAnnotation(document, position); + if (!annotation || !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); + return getContextCompletionItems(extension.contextHistory, file, annotation, nextChar); }, }) ); } -function getContextCompletionItems(context: ContextHistory, file: string, nextChar: string): vscode.CompletionItem[] { +function getContextCompletionItems(context: ContextHistory, file: string, annotation: LJAnnotation, nextChar: string): vscode.CompletionItem[] { + const triggerParameterHints = nextChar !== "("; const variablesInScope = getVariablesInScope(file, extension.selection); const inScope = variablesInScope !== null; - const triggerParameterHints = nextChar !== "("; - const variableItems = getVariableCompletionItems([...(variablesInScope || []), ...context.globalVars]); // not including instance vars - - const ghostsInFile = context.ghosts[file] || []; - const ghostItems = getGhostCompletionItems(ghostsInFile, triggerParameterHints); - const aliasItems = getAliasCompletionItems(context.aliases, triggerParameterHints); - const keywordItems = getKeywordsCompletionItems(triggerParameterHints, inScope); - const allItems = [...variableItems, ...ghostItems, ...aliasItems, ...keywordItems]; - - // remove duplicates + 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(), + imports: () => [], // TODO: implement imports completion + } + const itemsMap: Record = { + Refinement: ["vars", "ghosts", "aliases", "keywords"], + StateRefinement: ["vars", "ghosts", "aliases", "keywords"], + Ghost: ["types"], + RefinementAlias: ["types"], + RefinementPredicate: ["types", "decls"], + StateSet: [], + ExternalRefinementsFor: ["imports"] + } + const items: vscode.CompletionItem[] = itemsMap[annotation].map(key => itemsHandlers[key]()).flat(); const uniqueItems = new Map(); - allItems.forEach(item => { + items.forEach(item => { const label = typeof item.label === "string" ? item.label : item.label.label; if (!uniqueItems.has(label)) uniqueItems.set(label, item); }); @@ -116,7 +140,20 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boo insertText: triggerParameterHints ? "old($1)" : "old", triggerParameterHints, }); - const items: vscode.CompletionItem[] = [thisItem, oldItem]; + const trueItem = createCompletionItem({ + name: "true", + kind: vscode.CompletionItemKind.Keyword, + description: "", + detail: "keyword", + }); + + 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", @@ -130,16 +167,24 @@ 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 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 { @@ -157,15 +202,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; @@ -181,5 +228,5 @@ function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, posit if (char === "(") parenthesisDepth++; if (char === ")") parenthesisDepth--; } - return parenthesisDepth > 0; + return parenthesisDepth > 0 ? lastAnnotationName : null; } \ No newline at end of file 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 From 378d619b41d5024cc878603d22b5d7bf9b66c001 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 22 Feb 2026 20:47:35 +0000 Subject: [PATCH 12/15] Renaming --- client/src/services/autocomplete.ts | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 5ef5ece..ae66a0b 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -16,7 +16,7 @@ type CompletionItemOptions = { insertText?: string; triggerParameterHints?: boolean; } -type CompletionItemKind = "vars" | "ghosts" | "aliases" | "keywords" | "types" | "decls" | "imports"; +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 @@ -46,7 +46,7 @@ function getContextCompletionItems(context: ContextHistory, file: string, annota keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope), types: () => getTypesCompletionItems(), decls: () => getDeclsCompletionItems(), - imports: () => [], // TODO: implement imports completion + packages: () => [], // TODO: implement packages completion } const itemsMap: Record = { Refinement: ["vars", "ghosts", "aliases", "keywords"], @@ -55,7 +55,7 @@ function getContextCompletionItems(context: ContextHistory, file: string, annota RefinementAlias: ["types"], RefinementPredicate: ["types", "decls"], StateSet: [], - ExternalRefinementsFor: ["imports"] + ExternalRefinementsFor: ["packages"] } const items: vscode.CompletionItem[] = itemsMap[annotation].map(key => itemsHandlers[key]()).flat(); const uniqueItems = new Map(); From dd36b62c0a0236bdebda3982b317a5f7c206c903 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 23 Feb 2026 14:12:07 +0000 Subject: [PATCH 13/15] Update Version --- server/src/main/java/utils/ContextHistoryConverter.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index c5e2fe6..cfc19e2 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/server/src/main/java/utils/ContextHistoryConverter.java @@ -26,7 +26,7 @@ public class ContextHistoryConverter { */ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) { return new ContextHistoryDTO( - toVariablesMap(contextHistory.getVars()), + toVariablesMap(contextHistory.getFileScopeVars()), contextHistory.getInstanceVars().stream().map(VariableDTO::from).collect(Collectors.toList()), contextHistory.getGlobalVars().stream().map(VariableDTO::from).collect(Collectors.toList()), toGhostsMap(contextHistory.getGhosts()), From 71be3c44b8b6b4cea84dd1365e8e179fe53a4298 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 23 Feb 2026 15:04:43 +0000 Subject: [PATCH 14/15] Add Trigger Characters Dot and quote trigger characters (dot only triggers for `this` and `old(this)`). --- client/src/services/autocomplete.ts | 64 +++++++++++++++++++---------- 1 file changed, 43 insertions(+), 21 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index ae66a0b..1b3d0d1 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -24,19 +24,34 @@ type CompletionItemKind = "vars" | "ghosts" | "aliases" | "keywords" | "types" | export function registerAutocomplete(context: vscode.ExtensionContext) { context.subscriptions.push( vscode.languages.registerCompletionItemProvider("java", { - provideCompletionItems(document, position) { + 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, annotation, 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, annotation: LJAnnotation, 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 itemsHandlers: Record vscode.CompletionItem[]> = { @@ -46,7 +61,7 @@ function getContextCompletionItems(context: ContextHistory, file: string, annota keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope), types: () => getTypesCompletionItems(), decls: () => getDeclsCompletionItems(), - packages: () => [], // TODO: implement packages completion + packages: () => [], // TODO } const itemsMap: Record = { Refinement: ["vars", "ghosts", "aliases", "keywords"], @@ -57,13 +72,7 @@ function getContextCompletionItems(context: ContextHistory, file: string, annota StateSet: [], ExternalRefinementsFor: ["packages"] } - const items: vscode.CompletionItem[] = itemsMap[annotation].map(key => itemsHandlers[key]()).flat(); - 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()); + return itemsMap[annotation].map(key => itemsHandlers[key]()).flat(); } function getVariableCompletionItems(variables: Variable[]): vscode.CompletionItem[] { @@ -131,15 +140,7 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boo 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 oldItem = getOldKeywordCompletionItem(triggerParameterHints); const trueItem = createCompletionItem({ name: "true", kind: vscode.CompletionItemKind.Keyword, @@ -167,6 +168,18 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boo return items; } +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({ @@ -229,4 +242,13 @@ function getActiveLiquidJavaAnnotation(document: vscode.TextDocument, position: if (char === ")") parenthesisDepth--; } 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 From 47331a53a4bb5abdc9e42bf62acb44ba2babd970 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 24 Feb 2026 13:28:15 +0000 Subject: [PATCH 15/15] Suggest Parameters in Method and Parameter Refinements --- client/src/services/context.ts | 2 +- client/src/types/context.ts | 1 + server/src/main/java/dtos/context/VariableDTO.java | 6 ++++-- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index dcd53c7..2476957 100644 --- a/client/src/services/context.ts +++ b/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); }); } \ No newline at end of file diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 613a7bb..ab3db6d 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -8,6 +8,7 @@ export type Variable = { refinement: string; mainRefinement: string; placementInCode: PlacementInCode | null; + isParameter: boolean; } export type Ghost = { diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index 9f6eff3..bb34f5b 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -11,7 +11,8 @@ public record VariableDTO( String type, String refinement, String mainRefinement, - PlacementInCodeDTO placementInCode + PlacementInCodeDTO placementInCode, + boolean isParameter ) { public static VariableDTO from(RefinedVariable refinedVariable) { return new VariableDTO( @@ -19,7 +20,8 @@ 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() ); } } \ No newline at end of file