Skip to content

Commit e4bfc98

Browse files
rcosta358rcosta358
committed
Autocomplete for Refinements (#58)
1 parent 81fcfaf commit e4bfc98

10 files changed

Lines changed: 63 additions & 146 deletions

File tree

‎client/src/extension.ts‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,15 @@ import { runClient, stopClient } from "./lsp/client";
1818
*/
1919
export async function activate(context: vscode.ExtensionContext) {
2020
registerLogger(context);
21-
extension.logger.client.info("Activating LiquidJava extension...");
22-
2321
registerStatusBar(context);
2422
registerCommands(context);
25-
registerEvents(context);
2623
registerWebview(context);
24+
registerEvents(context);
2725
registerAutocomplete(context);
2826
registerHover();
27+
28+
extension.logger.client.info("Activating LiquidJava extension...");
29+
2930
await applyItalicOverlay();
3031
await startExtension(context);
3132
}

‎client/src/services/autocomplete.ts‎

Lines changed: 39 additions & 110 deletions
Original file line numberDiff line numberDiff line change
@@ -3,76 +3,41 @@ import { extension } from "../state";
33
import type { Variable, ContextHistory, Ghost, Alias } from "../types/context";
44
import { getSimpleName } from "../utils/utils";
55
import { getVariablesInScope } from "./context";
6-
import { LIQUIDJAVA_ANNOTATION_START, LJAnnotation } from "../utils/constants";
7-
8-
type CompletionItemOptions = {
9-
name: string;
10-
kind: vscode.CompletionItemKind;
11-
description?: string;
12-
labelDetail?: string;
13-
detail: string;
14-
documentationBlocks?: string[];
15-
codeBlocks?: string[];
16-
insertText?: string;
17-
triggerParameterHints?: boolean;
18-
}
19-
type CompletionItemKind = "vars" | "ghosts" | "aliases" | "keywords" | "types" | "decls" | "packages";
6+
import { LIQUIDJAVA_ANNOTATION_START } from "../utils/constants";
207

218
/**
229
* Registers a completion provider for LiquidJava annotations, providing context-aware suggestions based on the current context history
2310
*/
2411
export function registerAutocomplete(context: vscode.ExtensionContext) {
2512
context.subscriptions.push(
2613
vscode.languages.registerCompletionItemProvider("java", {
27-
provideCompletionItems(document, position, _token, completionContext) {
28-
const annotation = getActiveLiquidJavaAnnotation(document, position);
29-
if (!annotation || !extension.contextHistory) return null;
30-
31-
const isDotTrigger = completionContext.triggerKind === vscode.CompletionTriggerKind.TriggerCharacter && completionContext.triggerCharacter === ".";
32-
const receiver = isDotTrigger ? getReceiverBeforeDot(document, position) : null;
14+
provideCompletionItems(document, position) {
15+
if (!isInsideLiquidJavaAnnotationString(document, position) || !extension.contextHistory) return null;
3316
const file = document.uri.toString().replace("file://", "");
3417
const nextChar = document.getText(new vscode.Range(position, position.translate(0, 1)));
35-
const items = getContextCompletionItems(extension.contextHistory, file, annotation, nextChar, isDotTrigger, receiver);
36-
const uniqueItems = new Map<string, vscode.CompletionItem>();
37-
items.forEach(item => {
38-
const label = typeof item.label === "string" ? item.label : item.label.label;
39-
if (!uniqueItems.has(label)) uniqueItems.set(label, item);
40-
});
41-
return Array.from(uniqueItems.values());
18+
return getContextCompletionItems(extension.contextHistory, file, nextChar);
4219
},
43-
}, '.', '"')
20+
})
4421
);
4522
}
4623

47-
function getContextCompletionItems(context: ContextHistory, file: string, annotation: LJAnnotation, nextChar: string, isDotTrigger: boolean, receiver: string | null): vscode.CompletionItem[] {
48-
const triggerParameterHints = nextChar !== "(";
49-
if (isDotTrigger) {
50-
if (receiver === "this" || receiver === "old(this)") {
51-
return getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints);
52-
}
53-
return [];
54-
}
24+
function getContextCompletionItems(context: ContextHistory, file: string, nextChar: string): vscode.CompletionItem[] {
5525
const variablesInScope = getVariablesInScope(file, extension.selection);
5626
const inScope = variablesInScope !== null;
57-
const itemsHandlers: Record<CompletionItemKind, () => vscode.CompletionItem[]> = {
58-
vars: () => getVariableCompletionItems(variablesInScope || []),
59-
ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints),
60-
aliases: () => getAliasCompletionItems(context.aliases, triggerParameterHints),
61-
keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope),
62-
types: () => getTypesCompletionItems(),
63-
decls: () => getDeclsCompletionItems(),
64-
packages: () => [], // TODO
65-
}
66-
const itemsMap: Record<LJAnnotation, CompletionItemKind[]> = {
67-
Refinement: ["vars", "ghosts", "aliases", "keywords"],
68-
StateRefinement: ["vars", "ghosts", "aliases", "keywords"],
69-
Ghost: ["types"],
70-
RefinementAlias: ["types"],
71-
RefinementPredicate: ["types", "decls"],
72-
StateSet: [],
73-
ExternalRefinementsFor: ["packages"]
74-
}
75-
return itemsMap[annotation].map(key => itemsHandlers[key]()).flat();
27+
const triggerParameterHints = nextChar !== "(";
28+
const variableItems = getVariableCompletionItems([...(variablesInScope || []), ...context.globalVars]); // not including instance vars
29+
const ghostItems = getGhostCompletionItems(context.ghosts, triggerParameterHints);
30+
const aliasItems = getAliasCompletionItems(context.aliases, triggerParameterHints);
31+
const keywordItems = getKeywordsCompletionItems(triggerParameterHints, inScope);
32+
const allItems = [...variableItems, ...ghostItems, ...aliasItems, ...keywordItems];
33+
34+
// remove duplicates
35+
const uniqueItems = new Map<string, vscode.CompletionItem>();
36+
allItems.forEach(item => {
37+
const label = typeof item.label === "string" ? item.label : item.label.label;
38+
if (!uniqueItems.has(label)) uniqueItems.set(label, item);
39+
});
40+
return Array.from(uniqueItems.values());
7641
}
7742

7843
function getVariableCompletionItems(variables: Variable[]): vscode.CompletionItem[] {
@@ -140,21 +105,16 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boo
140105
detail: "keyword",
141106
documentationBlocks: ["Keyword referring to the **current instance**"],
142107
});
143-
const oldItem = getOldKeywordCompletionItem(triggerParameterHints);
144-
const trueItem = createCompletionItem({
145-
name: "true",
146-
kind: vscode.CompletionItemKind.Keyword,
147-
description: "",
148-
detail: "keyword",
149-
});
150-
151-
const falseItem = createCompletionItem({
152-
name: "false",
108+
const oldItem = createCompletionItem({
109+
name: "old",
153110
kind: vscode.CompletionItemKind.Keyword,
154111
description: "",
155112
detail: "keyword",
113+
documentationBlocks: ["Keyword referring to the **previous state of the current instance**"],
114+
insertText: triggerParameterHints ? "old($1)" : "old",
115+
triggerParameterHints,
156116
});
157-
const items: vscode.CompletionItem[] = [thisItem, oldItem, trueItem, falseItem];
117+
const items: vscode.CompletionItem[] = [thisItem, oldItem];
158118
if (!inScope) {
159119
const returnItem = createCompletionItem({
160120
name: "return",
@@ -168,36 +128,16 @@ function getKeywordsCompletionItems(triggerParameterHints: boolean, inScope: boo
168128
return items;
169129
}
170130

171-
function getOldKeywordCompletionItem(triggerParameterHints: boolean): vscode.CompletionItem {
172-
return createCompletionItem({
173-
name: "old",
174-
kind: vscode.CompletionItemKind.Keyword,
175-
description: "",
176-
detail: "keyword",
177-
documentationBlocks: ["Keyword referring to the **previous state of the current instance**"],
178-
insertText: triggerParameterHints ? "old($1)" : "old",
179-
triggerParameterHints,
180-
});
181-
}
182-
183-
function getTypesCompletionItems(): vscode.CompletionItem[] {
184-
const types = ["int", "double", "float", "boolean"];
185-
return types.map(type => createCompletionItem({
186-
name: type,
187-
kind: vscode.CompletionItemKind.Keyword,
188-
description: "",
189-
detail: "keyword",
190-
}));
191-
}
192-
193-
function getDeclsCompletionItems(): vscode.CompletionItem[] {
194-
const decls = ["ghost", "type"]
195-
return decls.map(decl => createCompletionItem({
196-
name: decl,
197-
kind: vscode.CompletionItemKind.Keyword,
198-
description: "",
199-
detail: "keyword",
200-
}));
131+
type CompletionItemOptions = {
132+
name: string;
133+
kind: vscode.CompletionItemKind;
134+
description?: string;
135+
labelDetail?: string;
136+
detail: string;
137+
documentationBlocks?: string[];
138+
codeBlocks?: string[];
139+
insertText?: string;
140+
triggerParameterHints?: boolean;
201141
}
202142

203143
function createCompletionItem({ name, kind, labelDetail, description, detail, documentationBlocks, codeBlocks, insertText, triggerParameterHints }: CompletionItemOptions): vscode.CompletionItem {
@@ -215,17 +155,15 @@ function createCompletionItem({ name, kind, labelDetail, description, detail, do
215155
return item;
216156
}
217157

218-
function getActiveLiquidJavaAnnotation(document: vscode.TextDocument, position: vscode.Position): LJAnnotation | null {
158+
function isInsideLiquidJavaAnnotationString(document: vscode.TextDocument, position: vscode.Position): boolean {
219159
const textUntilCursor = document.getText(new vscode.Range(new vscode.Position(0, 0), position));
220160
LIQUIDJAVA_ANNOTATION_START.lastIndex = 0;
221161
let match: RegExpExecArray | null = null;
222162
let lastAnnotationStart = -1;
223-
let lastAnnotationName: LJAnnotation | null = null;
224163
while ((match = LIQUIDJAVA_ANNOTATION_START.exec(textUntilCursor)) !== null) {
225164
lastAnnotationStart = match.index;
226-
lastAnnotationName = match[2] as LJAnnotation || null;
227165
}
228-
if (lastAnnotationStart === -1 || !lastAnnotationName) return null;
166+
if (lastAnnotationStart === -1) return false;
229167

230168
const fromLastAnnotation = textUntilCursor.slice(lastAnnotationStart);
231169
let parenthesisDepth = 0;
@@ -241,14 +179,5 @@ function getActiveLiquidJavaAnnotation(document: vscode.TextDocument, position:
241179
if (char === "(") parenthesisDepth++;
242180
if (char === ")") parenthesisDepth--;
243181
}
244-
return parenthesisDepth > 0 ? lastAnnotationName : null;
245-
}
246-
247-
function getReceiverBeforeDot(document: vscode.TextDocument, position: vscode.Position): string | null {
248-
const prefix = document.lineAt(position.line).text.slice(0, position.character);
249-
const match = prefix.match(/((?:old\s*\(\s*this\s*\))|(?:[A-Za-z_]\w*))\.\w*$/);
250-
if (!match) return null;
251-
const receiver = match[1].trim();
252-
if (/^old\s*\(\s*this\s*\)$/.test(receiver)) return "old(this)";
253-
return receiver;
182+
return parenthesisDepth > 0;
254183
}

‎client/src/services/context.ts‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -56,10 +56,7 @@ function isSelectionWithinScope(selection: Selection, scope: Selection): boolean
5656
function getReachableVariables(variables: Variable[], selection: Selection): Variable[] {
5757
return variables.filter((variable) => {
5858
const placement = variable.placementInCode?.position;
59-
const startPosition = variable.annPosition || placement;
60-
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)
61-
62-
// variable was declared before the cursor line or its in the same line but before the cursor column
63-
return startPosition.line < selection.startLine || startPosition.line === selection.startLine && startPosition.column <= selection.startColumn;
59+
if (!placement) return true;
60+
return placement.line < selection.startLine || (placement.line === selection.startLine && placement.column <= selection.startColumn);
6461
});
6562
}

‎client/src/types/context.ts‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import { PlacementInCode, SourcePosition } from "./diagnostics";
1+
import { PlacementInCode } from "./diagnostics";
22

33
// Type definitions used for LiquidJava context information
44

@@ -8,8 +8,6 @@ export type Variable = {
88
refinement: string;
99
mainRefinement: string;
1010
placementInCode: PlacementInCode | null;
11-
isParameter: boolean;
12-
annPosition: SourcePosition | null;
1311
}
1412

1513
export type Ghost = {
@@ -29,9 +27,9 @@ export type Alias = {
2927

3028
export type ContextHistory = {
3129
vars: Record<string, Record<string, Variable[]>>; // file -> (scope -> variables in scope)
32-
ghosts: Record<string, Ghost[]>; // file -> ghosts in file
3330
instanceVars: Variable[];
3431
globalVars: Variable[];
32+
ghosts: Ghost[];
3533
aliases: Alias[];
3634
}
3735

‎client/src/utils/constants.ts‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,5 +27,4 @@ export const LIQUIDJAVA_ANNOTATIONS = [
2727
"StateRefinement",
2828
"ExternalRefinementsFor",
2929
]
30-
export const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g");
31-
export type LJAnnotation = "Refinement" | "RefinementAlias" | "RefinementPredicate" | "StateSet" | "Ghost" | "StateRefinement" | "ExternalRefinementsFor";
30+
export const LIQUIDJAVA_ANNOTATION_START = new RegExp(`@(liquidjava\\.specification\\.)?(${LIQUIDJAVA_ANNOTATIONS.join("|")})\\s*\\(`, "g");

‎server/pom.xml‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,10 +169,17 @@
169169
</dependencyManagement>
170170

171171
<dependencies>
172+
<!-- <dependency>
173+
<groupId>liquidjava</groupId>
174+
<artifactId>verifier</artifactId>
175+
<version>0.0.13</version>
176+
<scope>system</scope>
177+
<systemPath>${project.basedir}/libs/liquidjava-verifier.jar</systemPath>
178+
</dependency> -->
172179
<dependency>
173180
<groupId>io.github.liquid-java</groupId>
174181
<artifactId>liquidjava-verifier</artifactId>
175-
<version>0.0.15</version>
182+
<version>0.0.14</version>
176183
</dependency>
177184
<dependency>
178185
<groupId>tools.aqua</groupId>

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ public record ContextHistoryDTO(
1212
Map<String, Map<String, List<VariableDTO>>> vars,
1313
List<VariableDTO> instanceVars,
1414
List<VariableDTO> globalVars,
15-
Map<String, List<GhostDTO>> ghosts,
15+
List<GhostDTO> ghosts,
1616
List<AliasDTO> aliases
1717
) {
1818
public static String stringifyType(CtTypeReference<?> typeReference) {

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

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
package dtos.context;
22

33
import dtos.diagnostics.PlacementInCodeDTO;
4-
import dtos.diagnostics.SourcePositionDTO;
54
import liquidjava.processor.context.RefinedVariable;
5+
import spoon.reflect.reference.CtTypeReference;
66

77
/**
88
* DTO for serializing RefinedVariable instances to JSON.
@@ -12,19 +12,15 @@ public record VariableDTO(
1212
String type,
1313
String refinement,
1414
String mainRefinement,
15-
PlacementInCodeDTO placementInCode,
16-
boolean isParameter,
17-
SourcePositionDTO annPosition
15+
PlacementInCodeDTO placementInCode
1816
) {
1917
public static VariableDTO from(RefinedVariable refinedVariable) {
2018
return new VariableDTO(
2119
refinedVariable.getName(),
2220
ContextHistoryDTO.stringifyType(refinedVariable.getType()),
2321
refinedVariable.getRefinement().toString(),
2422
refinedVariable.getMainRefinement().toString(),
25-
PlacementInCodeDTO.from(refinedVariable.getPlacementInCode()),
26-
refinedVariable.isParameter(),
27-
SourcePositionDTO.from(refinedVariable.getAnnPosition())
23+
PlacementInCodeDTO.from(refinedVariable.getPlacementInCode())
2824
);
2925
}
3026
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,11 @@
55
/**
66
* DTO for serializing PlacementInCode instances to JSON
77
*/
8-
public record PlacementInCodeDTO(String text, SourcePositionDTO position) {
8+
public record PlacementInCodeDTO(String text, PositionDTO position) {
99

1010
public static PlacementInCodeDTO from(PlacementInCode placement) {
1111
if (placement == null)
1212
return null;
13-
return new PlacementInCodeDTO(placement.getText(), SourcePositionDTO.from(placement.getPosition()));
13+
return new PlacementInCodeDTO(placement.getText(), PositionDTO.from(placement.getPosition()));
1414
}
1515
}

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

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111
import dtos.context.GhostDTO;
1212
import dtos.context.VariableDTO;
1313
import liquidjava.processor.context.ContextHistory;
14-
import liquidjava.processor.context.GhostState;
1514
import liquidjava.processor.context.RefinedVariable;
1615

1716
/**
@@ -29,7 +28,7 @@ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) {
2928
toVariablesMap(contextHistory.getFileScopeVars()),
3029
contextHistory.getInstanceVars().stream().map(VariableDTO::from).collect(Collectors.toList()),
3130
contextHistory.getGlobalVars().stream().map(VariableDTO::from).collect(Collectors.toList()),
32-
toGhostsMap(contextHistory.getGhosts()),
31+
contextHistory.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()),
3332
contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList())
3433
);
3534
}
@@ -47,13 +46,4 @@ private static Map<String, Map<String, List<VariableDTO>>> toVariablesMap(Map<St
4746
HashMap::new
4847
));
4948
}
50-
51-
private static Map<String, List<GhostDTO>> toGhostsMap(Map<String, Set<GhostState>> ghosts) {
52-
return ghosts.entrySet().stream().collect(Collectors.toMap(
53-
Map.Entry::getKey,
54-
entry -> entry.getValue().stream().map(GhostDTO::from).collect(Collectors.toList()),
55-
(left, right) -> left,
56-
HashMap::new
57-
));
58-
}
5949
}

0 commit comments

Comments
 (0)