From 786b040753d6b2ea84bb4b80234928d8a8e98c58 Mon Sep 17 00:00:00 2001 From: Florian Moser Date: Mon, 25 Mar 2024 07:42:06 +0100 Subject: [PATCH] refactor: Avoid recursing twice --- server/src/go_to_definition.ts | 39 ++++++++++++++++++------- server/src/tasks/create_symbol_table.ts | 14 ++++----- 2 files changed, 35 insertions(+), 18 deletions(-) diff --git a/server/src/go_to_definition.ts b/server/src/go_to_definition.ts index f021d3e..28eed05 100644 --- a/server/src/go_to_definition.ts +++ b/server/src/go_to_definition.ts @@ -4,8 +4,9 @@ import {getMatchingParseTree} from "./parseTree/get_matching_parse_tree"; import {getRange} from "./parseTree/get_range"; import {DefinitionLink} from "vscode-languageserver-protocol"; import {ParseTree} from "antlr4ts/tree"; -import {ProverifSymbol} from "./tasks/create_symbol_table"; +import {DeclarationType, ProverifSymbol} from "./tasks/create_symbol_table"; import {TerminalNode} from "antlr4ts/tree/TerminalNode"; +import {LibraryDependencyToken} from "./tasks/parse_library_dependencies"; type Origin = { uri: TextDocumentIdentifier, match: TerminalNode }; export type DefinitionSymbol = { uri: TextDocumentIdentifier, symbol: ProverifSymbol, origin: Origin } @@ -26,22 +27,27 @@ export const getDefinitionSymbolFromPosition = async (identifier: TextDocumentId export const getDefinitionSymbolFromMatch = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface): Promise => { - const definition = getDefinitionSymbolFromMatchMacroAware(parseResult, matchingParseTree, documentManager, false); - if (definition) { - return definition; - } - - return getDefinitionSymbolFromMatchMacroAware(parseResult, matchingParseTree, documentManager, true); + return getDefinitionSymbolFromMatchMacroAware(parseResult, matchingParseTree, documentManager); }; -export const getDefinitionSymbolFromMatchMacroAware = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface, considerMacros: boolean): Promise => { +const getDefinitionSymbolFromMatchMacroAware = async (parseResult: ParseResult, matchingParseTree: TerminalNode, documentManager: DocumentManagerInterface): Promise => { const origin = {uri: parseResult.identifier, match: matchingParseTree}; - const closestSymbol = parseResult.symbolTable.findClosestSymbol(matchingParseTree.text, matchingParseTree, considerMacros); + const closestSymbol = parseResult.symbolTable.findClosestSymbol(matchingParseTree.text, matchingParseTree); if (closestSymbol) { + if (closestSymbol.declaration === DeclarationType.ExpandParameter) { + // TODO: break the cycle + const originSymbol = await getDefinitionSymbolFromMatch(parseResult, closestSymbol.node, documentManager); + if (originSymbol) { + return originSymbol; + } + } + return {uri: parseResult.identifier, symbol: closestSymbol, origin}; } + let currentClosestSymbol: ProverifSymbol|undefined; + let currentClosestSymbolDependency: LibraryDependencyToken|undefined; for (let i = 0; i < parseResult.dependencyTokens.length; i++) { const dependency = parseResult.dependencyTokens[i]; if (!dependency.exists) { @@ -53,12 +59,23 @@ export const getDefinitionSymbolFromMatchMacroAware = async (parseResult: ParseR continue; } - const closestSymbol = dependencyParseResult.symbolTable.findClosestSymbol(matchingParseTree.text, undefined, considerMacros); + const closestSymbol = dependencyParseResult.symbolTable.findClosestSymbol(matchingParseTree.text, undefined); if (!closestSymbol) { continue; } - return {uri: dependency, symbol: closestSymbol, origin}; + currentClosestSymbol = closestSymbol; + currentClosestSymbolDependency = dependency; + if (closestSymbol.declaration === DeclarationType.ExpandParameter) { + // TODO: check in library first for previous declaration, before going to another library + continue; + } + + break; + } + + if (currentClosestSymbol && currentClosestSymbolDependency) { + return {uri: currentClosestSymbolDependency, symbol: currentClosestSymbol, origin} } return undefined; diff --git a/server/src/tasks/create_symbol_table.ts b/server/src/tasks/create_symbol_table.ts index 63db823..cde1861 100644 --- a/server/src/tasks/create_symbol_table.ts +++ b/server/src/tasks/create_symbol_table.ts @@ -409,28 +409,28 @@ export class ProverifSymbolTable { this.publicContext = publicContext; } - public findClosestSymbol(text: string, context: ParseTree|undefined, considerMacros: boolean): ProverifSymbol | undefined { - return this.findClosestSymbolInternal(text, context ?? this.publicContext, considerMacros); + public findClosestSymbol(text: string, context: ParseTree|undefined): ProverifSymbol | undefined { + return this.findClosestSymbolInternal(text, context ?? this.publicContext); } public getSymbols(): ProverifSymbol[] { return this.symbols; } - private findClosestSymbolInternal(name: string, context: ParseTree|undefined, considerMacros: boolean): ProverifSymbol | undefined { + private findClosestSymbolInternal(name: string, context: ParseTree|undefined): ProverifSymbol | undefined { if (!context) { return undefined; } const symbolsOfContext = this.symbols.filter(symbol => symbol.context === context); const matchingSymbol = symbolsOfContext.find(symbol => symbol.node.text === name); - if (matchingSymbol && (considerMacros || matchingSymbol.declaration !== DeclarationType.ExpandParameter)) { + if (matchingSymbol) { return matchingSymbol; } // if in tprocess, check whether defined in library if (context instanceof TprocessContext && context.parent instanceof AllContext) { - return this.findClosestSymbolInternal(name, this.publicContext, considerMacros); + return this.findClosestSymbolInternal(name, this.publicContext); } // if in OTHERWISE, then jump directly to the real parent, not the previous clauses @@ -440,10 +440,10 @@ export class ProverifSymbolTable { realParent = realParent.parent; } - return this.findClosestSymbolInternal(name, realParent, considerMacros); + return this.findClosestSymbolInternal(name, realParent); } - return this.findClosestSymbolInternal(name, context.parent, considerMacros); + return this.findClosestSymbolInternal(name, context.parent); } }