Skip to content

Commit

Permalink
feat: Support named arguments
Browse files Browse the repository at this point in the history
  • Loading branch information
@famoser
famoser committed Feb 11, 2024
1 parent f5b0554 commit 2c7fb59
Show file tree
Hide file tree
Showing 4 changed files with 76 additions and 24 deletions.
0 ...parseTree/get_terminal_before_position.ts → ...r/src/parseTree/get_signature_position.ts
View file
File renamed without changes.
24 changes: 17 additions & 7 deletions server/src/signature_help.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ import {
uinteger
} from "vscode-languageserver";
import {DocumentManagerInterface} from "./document_manager";
import {getDefinitionSymbolFromPosition} from "./go_to_definition";
import {getSignaturePosition} from "./parseTree/get_terminal_before_position";
import {DefinitionSymbol, getDefinitionSymbolFromPosition} from "./go_to_definition";
import {getSignaturePosition} from "./parseTree/get_signature_position";

export const getSignatureHelp = async (identifier: TextDocumentIdentifier, position: Position, documentManager: DocumentManagerInterface): Promise<SignatureHelp | undefined> => {
const parseResult = await documentManager.getParseResult(identifier);
Expand All @@ -26,25 +26,35 @@ export const getSignatureHelp = async (identifier: TextDocumentIdentifier, posit
return undefined;
}

const parameterLabels = (definitionSymbol.symbol.parameters ?? []).map(parameter => parameter?.text ?? "");
const {parameters, signatureLabel} = createOffsetLabels(parameterLabels, definitionSymbol.symbol.node.text);
const {parameters, signatureLabel} = createOffsetLabels(definitionSymbol);

const signature: SignatureInformation = {label: signatureLabel, parameters};
return {signatures: [signature], activeSignature: 0, activeParameter: signaturePosition.parameterPosition};
};

const createOffsetLabels = (parameterLabels: string[], signatureText: string) => {
const createOffsetLabels = (definitionSymbol: DefinitionSymbol) => {
const parameterLabels = (definitionSymbol.symbol.parameters ?? []).map(parameter => {
if (!parameter) {
return ""

Check failure on line 38 in server/src/signature_help.ts

View workflow job for this annotation

GitHub Actions / Node 

Missing semicolon
}

const typeSuffix = parameter.type ? ": " + parameter.type.text : "";
return parameter.node.text + typeSuffix

Check failure on line 42 in server/src/signature_help.ts

View workflow job for this annotation

GitHub Actions / Node 

Missing semicolon
});


const parameters: ParameterInformation[] = [];
const signatureText = definitionSymbol.symbol.node.text;
let currentOffset = signatureText.length + 1;
for (let i = 0; i < parameterLabels.length; i++) {
const parameterLabel = parameterLabels[i];
parameters.push({label: [currentOffset, currentOffset + parameterLabel.length]});
currentOffset += parameterLabel.length + 1;
currentOffset += parameterLabel.length + 2;
}

return {
parameters,
signatureLabel: `${signatureText}(${parameterLabels.join(",")})`
signatureLabel: `${signatureText}(${parameterLabels.join(", ")})`
};
};

Expand Down
66 changes: 54 additions & 12 deletions server/src/tasks/create_symbol_table.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,14 +74,14 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i
this.registerTerminal(ctx.IDENT(), DeclarationType.Type);
} else if (ctx.FUN()) {
const parameters = collectTypeidseq(ctx.typeidseq());
this.registerTerminal(ctx.IDENT(), DeclarationType.Fun, getType(ctx.typeid()), parameters);
this.registerTerminalWithParameters(ctx.IDENT(), DeclarationType.Fun, parameters, getType(ctx.typeid()));
} else if (ctx.EVENT() || ctx.PREDICATE() || ctx.TABLE() || ctx.DEFINE()) {
const declarationType =
ctx.EVENT() ? DeclarationType.Event :
(ctx.PREDICATE() ? DeclarationType.Predicate :
(ctx.TABLE() ? DeclarationType.Table : DeclarationType.Define));
const parameters = collectTypeidseq(ctx.typeidseq());
this.registerTerminal(ctx.IDENT(), declarationType, undefined, parameters);
this.registerTerminalWithParameters(ctx.IDENT(), declarationType, parameters);

if (ctx.DEFINE()) {
this.withContext(ctx, () => {
Expand All @@ -93,12 +93,12 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i
} else if (ctx.EXPAND()) {
const parameters = collectTypeidseq(ctx.typeidseq());
parameters.forEach(identifier => {
this.registerTerminal(identifier, DeclarationType.DefineParameter);
this.registerTerminal(identifier, DeclarationType.ExpandParameter);
});
} else if (ctx.LET() || ctx.LETFUN()) {
const declarationType = ctx.LET() ? DeclarationType.Let : DeclarationType.LetFun;
const parameters = collecMayfailvartypeseq(ctx.mayfailvartypeseq());
this.registerTerminal(ctx.IDENT(), declarationType, undefined, parameters.map(typedTerminal => typedTerminal.type));
this.registerTerminalWithNamedParameters(ctx.IDENT(), declarationType, parameters);
this.withContext(ctx, () => {
parameters.forEach(typedTerminal => {
this.registerTypedTerminal(typedTerminal, DeclarationType.Parameter);
Expand Down Expand Up @@ -135,7 +135,6 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i

public visitTprocess = (ctx: TprocessContext) => {
return this.withContext(ctx, () => {
const tpattern = ctx.tpattern();
if (ctx.LET() || ctx.IN()) {
collectTPattern(ctx.tpattern()).forEach(typedTerminal => {
this.registerTypedTerminal(typedTerminal, DeclarationType.Parameter);
Expand All @@ -162,20 +161,58 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i
});
};

private registerTerminal(identifier: TerminalNode | undefined, declaration: DeclarationType, type?: ParseTree, parameters?: (ParseTree | undefined)[]) {
private registerTerminal(identifier: TerminalNode | undefined, declaration: DeclarationType, type?: ParseTree) {
if (!identifier) {
return;
}

this.symbolTable.addSymbol(identifier, declaration, type, parameters, this.context);
this.symbolTable.addSymbol({
node: identifier,
declaration,
type,
context: this.context
});
}

private registerTypedTerminal(identifier: TypedTerminal | undefined, declaration: DeclarationType) {
if (!identifier) {
return;
}

this.symbolTable.addSymbol({
node: identifier.terminal,
declaration,
type: identifier.type,
context: this.context
});
}

private registerTypedTerminal(identifier: TypedTerminal | undefined, declaration: DeclarationType, parameters?: (ParseTree | undefined)[]) {
private registerTerminalWithParameters(identifier: TerminalNode | undefined, declaration: DeclarationType, parameters: (ParseTree | undefined)[], type?: ParseTree) {
if (!identifier) {
return;
}

this.symbolTable.addSymbol(identifier.terminal, declaration, identifier.type, parameters, this.context);
this.symbolTable.addSymbol({
node: identifier,
declaration,
type,
parameters: parameters.map(parameter => parameter ? ({node: parameter}) : undefined),
context: this.context
});
}

private registerTerminalWithNamedParameters(identifier: TerminalNode | undefined, declaration: DeclarationType, parameters: (TypedTerminal|undefined)[], type?: ParseTree) {
if (!identifier) {
return;
}

this.symbolTable.addSymbol({
node: identifier,
declaration,
type,
parameters: parameters.map(parameter => parameter ? ({node: parameter.terminal, type: parameter.type}) : undefined),
context: this.context
});
}

private withContext<T>(context: undefined | ParseTree, action: () => T): T {
Expand All @@ -189,19 +226,24 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i
}
}

export type ProverifSymbolParameter = {
node: ParseTree
type?: ParseTree
}

export type ProverifSymbol = {
node: TerminalNode
declaration: DeclarationType
type?: ParseTree
parameters?: (ParseTree | undefined)[]
parameters?: (ProverifSymbolParameter | undefined)[]
context?: ParseTree
}

export class ProverifSymbolTable {
private symbols: ProverifSymbol[] = [];

public addSymbol(node: TerminalNode, declaration: DeclarationType, type?: ParseTree, parameters?: (ParseTree | undefined)[], context?: ParseTree) {
this.symbols.push({node, declaration, type, parameters, context});
public addSymbol(symbol: ProverifSymbol) {
this.symbols.push(symbol);
}

public findClosestSymbol(node: ParseTree): ProverifSymbol | undefined {
Expand Down
10 changes: 5 additions & 5 deletions server/tests/signature_help.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ describe('signature help', function () {
const signature = signatureHelp.signatures[0]

expect(signature.label).to.contain(definitionLabel)
expect(signature.label).to.contain(parameters.join(","));
expect(signature.label).to.contain(parameters.join(", "));
expect(signature.parameters.length).to.equal(parameters.length);

if (signature.parameters.length > 0) {
Expand All @@ -34,7 +34,7 @@ describe('signature help', function () {
signature.parameters.forEach((parameter, index) => {
expect(parameter.label[0]).to.equal(currentIndex)
expect(parameter.label[1]).to.equal(Number(currentIndex) + parameters[index].length)
currentIndex += parameters[index].length + 1
currentIndex += parameters[index].length + 2
})
}

Expand All @@ -53,13 +53,13 @@ describe('signature help', function () {
const code = `let P(arg: nat) = 0.\nprocess \nP(`;
const signatureInvoked = {line: 2, character: 2};

await assertSignatureDefinitionFound(code, signatureInvoked, 'P', ['nat'], 0);
await assertSignatureDefinitionFound(code, signatureInvoked, 'P', ['arg: nat'], 0);
});

it("finds second argument position", async () => {
const code = `let P(arg: nat, arg2: nat) = 0.\nprocess \nP(0,`;
const code = `let P(arg: nat, arg2:nat) = 0.\nprocess \nP(0,`;
const signatureInvoked = {line: 2, character: 4};

await assertSignatureDefinitionFound(code, signatureInvoked, 'P', ['nat', 'nat'], 1);
await assertSignatureDefinitionFound(code, signatureInvoked, 'P', ['arg: nat', 'arg2: nat'], 1);
});
});

0 comments on commit 2c7fb59

Please sign in to comment.