feat: Support different active parameter

server/src/parseTree/get_terminal_before_position.ts

@@ -1,18 +1,41 @@
-import {ParseTree, TerminalNode} from "antlr4ts/tree";
-import {Position} from "vscode-languageserver";
+import {Position, uinteger} from "vscode-languageserver";
 import {TokenStream} from "antlr4ts/TokenStream";
 import {Token} from "antlr4ts";
+import {ProverifLexer} from "../parser-proverif/ProverifLexer";
 
-export const getPositionOfTokenBefore = (tokens: TokenStream, position: Position): Position | undefined => {
+export const getPositionOfTokenBeforeLastLParen = (tokens: TokenStream, position: Position): Position | undefined => {
     let lastToken: Token|undefined = undefined;
+    let nextLastToken: Token|undefined = undefined;
     for (let i = 0; i < tokens.size; i++) {
         const token = tokens.get(i); // lookup seems to be O(1)
         if (token.line >= position.line + 1 && token.charPositionInLine >= position.character) {
             break;
         }
 
-        lastToken = token;
+        if (token.type === ProverifLexer.LPAREN) {
+            lastToken = nextLastToken;
+        } else {
+            nextLastToken = token;
+        }
     }
 
     return lastToken ? Position.create(lastToken.line-1, lastToken.charPositionInLine) : undefined;
+};
+
+export const countCommasAfterLParenButBeforeToken = (tokens: TokenStream, position: Position): uinteger | undefined => {
+    let commaCount: uinteger = 0;
+    for (let i = 0; i < tokens.size; i++) {
+        const token = tokens.get(i); // lookup seems to be O(1)
+        if (token.line >= position.line + 1 && token.charPositionInLine >= position.character) {
+            break;
+        }
+
+        if (token.type === ProverifLexer.COMMA) {
+            commaCount++;
+        } else if (token.type === ProverifLexer.LPAREN) {
+            commaCount = 0;
+        }
+    }
+
+    return commaCount;
 };

server/src/server.ts

@@ -15,7 +15,7 @@ import {rename} from "./rename";
 import {getReferences} from "./references";
 import {getSemanticTokens} from './semantic_token_provider';
 import {getDocumentLinks} from "./document_links";
-import {getSignatureHelp} from "./signature_help";
+import {getActiveParameter, getSignatureHelp} from "./signature_help";
 
 const connection = createConnection(ProposedFeatures.all);
 const documents: TextDocuments<TextDocument> = new TextDocuments(TextDocument);
@@ -96,7 +96,13 @@ connection.onDocumentLinks(async params => {
 });
 
 connection.onSignatureHelp(async params => {
-    console.log("calling", params);
+    if (params.context?.isRetrigger && params.context.activeSignatureHelp) {
+        const activeParameter = await getActiveParameter(params.textDocument, params.position, documentManager) ?? 0;
+        return { ...params.context.activeSignatureHelp, activeParameter };
+    }
+
+    // TODO: Deal with case when signature is opened using ctrl shift space, notably not at first parameter position
+    // TODO: Ensure signature help is closed again when outside method scope (check for RParen?)
     const signatureHelp = await getSignatureHelp(params.textDocument, params.position, documentManager);
     if (!signatureHelp) {
         console.log("not found");

server/src/signature_help.ts

@@ -3,19 +3,23 @@ import {
     Position,
     SignatureHelp,
     SignatureInformation,
-    TextDocumentIdentifier
+    TextDocumentIdentifier,
+    uinteger
 } from "vscode-languageserver";
 import {DocumentManagerInterface} from "./document_manager";
 import {getDefinitionSymbolFromPosition} from "./go_to_definition";
-import {getPositionOfTokenBefore} from "./parseTree/get_terminal_before_position";
+import {
+    countCommasAfterLParenButBeforeToken,
+    getPositionOfTokenBeforeLastLParen
+} from "./parseTree/get_terminal_before_position";
 
 export const getSignatureHelp = async (identifier: TextDocumentIdentifier, position: Position, documentManager: DocumentManagerInterface): Promise<SignatureHelp | undefined> => {
     const parseResult = await documentManager.getParseResult(identifier);
     if (!parseResult) {
         return undefined;
     }
 
-    const positionOfTokenBefore = getPositionOfTokenBefore(parseResult.parser.inputStream, position);
+    const positionOfTokenBefore = getPositionOfTokenBeforeLastLParen(parseResult.parser.inputStream, position);
     if (!positionOfTokenBefore) {
         return undefined;
     }
@@ -25,7 +29,32 @@ export const getSignatureHelp = async (identifier: TextDocumentIdentifier, posit
         return undefined;
     }
 
-    const parameters: ParameterInformation[] =  (definitionSymbol.symbol.parameters ?? []).map(parameter => ({ label: parameter?.text ?? "" }));
-    const signature: SignatureInformation = { label: definitionSymbol.symbol.node.text, parameters, activeParameter: 0 };
+    const parameterLabels =  (definitionSymbol.symbol.parameters ?? []).map(parameter => parameter?.text ?? "");
+    let signatureLabel = definitionSymbol.symbol.node.text + "(";
+
+    const parameters: ParameterInformation[] = [];
+    let currentOffset = signatureLabel.length;
+    for (let i = 0; i < parameterLabels.length; i++) {
+        const parameterLabel = parameterLabels[i];
+        parameters.push({ label: [currentOffset, currentOffset + parameterLabel.length]});
+        currentOffset += parameterLabel.length + 1;
+    }
+    signatureLabel += parameterLabels.join(",") + ")";
+
+    const signature: SignatureInformation = { label: signatureLabel, parameters };
     return { signatures: [signature], activeSignature: 0, activeParameter: 0 };
-};
+};
+
+export const getActiveParameter = async (identifier: TextDocumentIdentifier, position: Position, documentManager: DocumentManagerInterface): Promise<uinteger | undefined> => {
+    const parseResult = await documentManager.getParseResult(identifier);
+    if (!parseResult) {
+        return undefined;
+    }
+
+    const positionOfTokenBefore = countCommasAfterLParenButBeforeToken(parseResult.parser.inputStream, position);
+    if (!positionOfTokenBefore) {
+        return undefined;
+    }
+
+    return positionOfTokenBefore;
+};

server/src/tasks/create_symbol_table.ts

@@ -1,17 +1,20 @@
 import {AbstractParseTreeVisitor, ParseTree} from "antlr4ts/tree";
 import {ProverifParserVisitor} from "../parser-proverif/ProverifParserVisitor";
-import {Extended_equationContext, LibContext, TprocessContext} from "../parser-proverif/ProverifParser";
+import {LibContext, TprocessContext} from "../parser-proverif/ProverifParser";
 import {TerminalNode} from "antlr4ts/tree/TerminalNode";
 import {
-    collecMayfailvartypeseq, collectBasicpattern,
+    collecMayfailvartypeseq,
+    collectBasicpattern,
     collectEqlist,
     collectNeidentseq,
     collectNemayfailvartypeseq,
     collectNevartype,
     collectTPattern,
     collectTPatternSeq,
     collectTreduc,
-    collectTypeidseq, getType, TypedTerminal
+    collectTypeidseq,
+    getType,
+    TypedTerminal
 } from "./ident_collectors";
 
 

server/src/tasks/ident_collectors.ts

@@ -2,17 +2,19 @@ import {
     BasicpatternContext,
     EqlistContext,
     Extended_equationContext,
-    ForallvartypeContext, MayfailvartypeContext,
+    ForallvartypeContext,
+    MayfailvartypeContext,
     MayfailvartypeseqContext,
     NeidentseqContext,
     NemayfailvartypeseqContext,
     NepatternseqContext,
     NetypeidseqContext,
     NevartypeContext,
-    OnevartypeContext, TermContext,
+    OnevartypeContext,
     TpatternContext,
     TpatternseqContext,
-    TreducContext, TypeidContext,
+    TreducContext,
+    TypeidContext,
     TypeidseqContext
 } from "../parser-proverif/ProverifParser";
 import {TerminalNode} from "antlr4ts/tree/TerminalNode";

server/tests/signature_help.test.ts

@@ -1,12 +1,13 @@
-import {assert, expect} from "chai";
+import {assert, expect, should} from "chai";
 
 import {Location, Position, Range} from "vscode-languageserver";
 import {MockDocumentManager} from "./mocks/mock_document_manager";
 import {getReferences} from "../src/references";
 import {getSignatureHelp} from "../src/signature_help";
+import {number} from "vscode-languageserver/lib/common/utils/is";
 
 describe('references', function () {
-    const assertSignatureDefinitionFound = async (code: string, signatureInvoked: Position, parameters: string[], activeParameter: number) => {
+    const assertSignatureDefinitionFound = async (code: string, signatureInvoked: Position, definitionLabel: string, parameters: string[], activeParameter: number) => {
         const uri = 'main.pv';
 
         const documentManager = new MockDocumentManager();
@@ -21,16 +22,37 @@ describe('references', function () {
         expect(signatureHelp.signatures.length).to.equal(1)
         const signature = signatureHelp.signatures[0]
 
+        expect(signature.label).to.contain(definitionLabel)
+        expect(signature.label).to.contain(parameters.join(","));
         expect(signature.parameters.length).to.equal(parameters.length);
-        expect(signature.parameters.map(parameter => parameter.label)).deep.equal(parameters);
 
-        expect(signature.activeParameter).to.equal(activeParameter);
+        if (signature.parameters.length > 0) {
+            const start = signature.parameters[0].label[0]
+            expect(start).to.equal(definitionLabel.length + 1)
+
+            let currentIndex = Number(start)
+            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
+            })
+        }
+
+        expect(signatureHelp.activeParameter).to.equal(activeParameter);
+        should().equal(signature.activeParameter, undefined)
     };
 
     it("finds table signature definition", async () => {
         const code = `table Ids(nat).\nprocess \nget Ids(`;
         const signatureInvoked = {line: 2, character: 8};
 
-        await assertSignatureDefinitionFound(code, signatureInvoked, ['nat'], 0);
+        await assertSignatureDefinitionFound(code, signatureInvoked, 'Ids', ['nat'], 0);
+    });
+
+    it("finds let signature definition", async () => {
+        const code = `let P(arg: nat) = 0.\nprocess \nP(`;
+        const signatureInvoked = {line: 2, character: 2};
+
+        await assertSignatureDefinitionFound(code, signatureInvoked, 'P', ['nat'], 0);
     });
 });