From 2c7fb598496b954994c00029c446aaca1a99cd5e Mon Sep 17 00:00:00 2001 From: Florian Moser Date: Sun, 11 Feb 2024 09:22:48 +0100 Subject: [PATCH] feat: Support named arguments --- ..._position.ts => get_signature_position.ts} | 0 server/src/signature_help.ts | 24 +++++-- server/src/tasks/create_symbol_table.ts | 66 +++++++++++++++---- server/tests/signature_help.test.ts | 10 +-- 4 files changed, 76 insertions(+), 24 deletions(-) rename server/src/parseTree/{get_terminal_before_position.ts => get_signature_position.ts} (100%) diff --git a/server/src/parseTree/get_terminal_before_position.ts b/server/src/parseTree/get_signature_position.ts similarity index 100% rename from server/src/parseTree/get_terminal_before_position.ts rename to server/src/parseTree/get_signature_position.ts diff --git a/server/src/signature_help.ts b/server/src/signature_help.ts index f36ea69..94d8902 100644 --- a/server/src/signature_help.ts +++ b/server/src/signature_help.ts @@ -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 => { const parseResult = await documentManager.getParseResult(identifier); @@ -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 "" + } + + const typeSuffix = parameter.type ? ": " + parameter.type.text : ""; + return parameter.node.text + typeSuffix + }); + + 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(", ")})` }; }; diff --git a/server/src/tasks/create_symbol_table.ts b/server/src/tasks/create_symbol_table.ts index c2b8069..78b297b 100644 --- a/server/src/tasks/create_symbol_table.ts +++ b/server/src/tasks/create_symbol_table.ts @@ -74,14 +74,14 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor 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, () => { @@ -93,12 +93,12 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor 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); @@ -135,7 +135,6 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor 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); @@ -162,20 +161,58 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor 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(context: undefined | ParseTree, action: () => T): T { @@ -189,19 +226,24 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor 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 { diff --git a/server/tests/signature_help.test.ts b/server/tests/signature_help.test.ts index f96ddb0..3757e5f 100644 --- a/server/tests/signature_help.test.ts +++ b/server/tests/signature_help.test.ts @@ -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) { @@ -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 }) } @@ -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); }); }); \ No newline at end of file