feat: Add semantic token provider

server/src/parseTree/collect_matching_terminals.ts → server/src/parseTree/collect_terminals.ts

@@ -1,5 +1,6 @@
 import {ParseTree, TerminalNode} from "antlr4ts/tree";
 import {ParserRuleContext} from "antlr4ts";
+import {ProverifParser} from "../parser-proverif/ProverifParser";
 
 export const collectMatchingTerminals = (parseTree: ParseTree, text: string): TerminalNode[] => {
     if (parseTree instanceof TerminalNode) {
@@ -20,3 +21,23 @@ export const collectMatchingTerminals = (parseTree: ParseTree, text: string): Te
 
     return matchingTerminals;
 };
+
+export const collectIdentTerminals = (parseTree: ParseTree): TerminalNode[] => {
+    if (parseTree instanceof TerminalNode) {
+        const token = parseTree.symbol;
+        if (token.type === ProverifParser.IDENT) {
+            return [parseTree];
+        }
+    }
+
+    const matchingTerminals: TerminalNode[] = [];
+    if (parseTree instanceof ParserRuleContext) {
+        // check if children match
+        for (let i = 0; i < parseTree.childCount; i++) {
+            const matchingTerminalsChild = collectIdentTerminals(parseTree.getChild(i));
+            matchingTerminals.push(...matchingTerminalsChild);
+        }
+    }
+
+    return matchingTerminals;
+};

server/src/references.ts

@@ -6,7 +6,7 @@ import {
     getDefinitionSymbolFromMatch,
     getDefinitionSymbolFromPosition
 } from "./go_to_definition";
-import {collectMatchingTerminals} from "./parseTree/collect_matching_terminals";
+import {collectMatchingTerminals} from "./parseTree/collect_terminals";
 import {ParseTree} from "antlr4ts/tree";
 import {getRange} from "./parseTree/get_range";
 import {nonNullable} from "./utils/array";

server/src/semantic_token_provider.ts

@@ -1,14 +1,43 @@
-import {SemanticTokensBuilder} from 'vscode-languageserver';
-import {ParseResult} from './document_manager';
+import {integer, SemanticTokensBuilder} from 'vscode-languageserver';
+import {DocumentManagerInterface, ParseResult} from './document_manager';
+import {collectIdentTerminals, collectMatchingTerminals} from "./parseTree/collect_terminals";
+import {definitionSymbolsEqual, getDefinitionSymbolFromMatch} from "./go_to_definition";
+import {nonNullable} from "./utils/array";
+import {notNull} from "antlr4ts/misc";
+import {DeclarationType} from "./tasks/create_symbol_table";
 
 export const tokenModifier = ['declaration', 'deprecated'];
 export const tokenTypes = ['function', 'variable', 'parameter', 'event'];
 
-export const getSemanticTokens = (parseResult: ParseResult) => {
-	// solely for demonstration purposes
-    const tokensBuilder = new SemanticTokensBuilder();
-	tokensBuilder.push(9, 8, 1, tokenTypes.indexOf('variable'), [tokenModifier.indexOf('deprecated')] as any);
-	tokensBuilder.push(10, 8, 1, tokenTypes.indexOf('variable'), [] as any);
-	tokensBuilder.push(10, 11, 1, tokenTypes.indexOf('variable'), tokenModifier.indexOf('deprecated'));
+export const getSemanticTokens = async (parseResult: ParseResult, documentManager: DocumentManagerInterface) => {
+    // collect references
+    const candidateTerminals = collectIdentTerminals(parseResult.parserTree);
+    const terminalDefinitions = candidateTerminals
+        .map(async terminal => getDefinitionSymbolFromMatch(parseResult, terminal, documentManager));
+
+	const tokensBuilder = new SemanticTokensBuilder();
+    (await Promise.all(terminalDefinitions))
+		.filter(nonNullable)
+        .forEach(terminalDefinition => {
+			const tokenType = getTokenType(terminalDefinition.symbol.declaration)
+			if (tokenType) {
+				const line = terminalDefinition.origin.match.symbol.line - 1;
+				const char = terminalDefinition.origin.match.symbol.charPositionInLine;
+				const length = terminalDefinition.origin.match.symbol.stopIndex - terminalDefinition.origin.match.symbol.startIndex + 1;
+				tokensBuilder.push(line, char, length, tokenType, [] as any)
+			}
+        });
+
     return tokensBuilder.build();
-};
+};
+
+const getTokenType = (declarationType: DeclarationType): number|undefined => {
+	switch (declarationType) {
+		case DeclarationType.Channel:
+		case DeclarationType.Free:
+		case DeclarationType.Const:
+			return tokenTypes.indexOf('variable')
+	}
+
+	return undefined
+}

server/src/server.ts

@@ -13,7 +13,7 @@ import {DocumentManager, DocumentManagerInterface,} from "./document_manager";
 import {getDefinitionLink} from "./go_to_definition";
 import {rename} from "./rename";
 import {getReferences} from "./references";
-import {getSemanticTokens} from './semantic_token_provider';
+import {getSemanticTokens, tokenModifier, tokenTypes} from './semantic_token_provider';
 import {getDocumentLinks} from "./document_links";
 import {getSignatureHelp} from "./signature_help";
 import {getHover} from "./hover";
@@ -45,15 +45,13 @@ connection.onInitialize((params: InitializeParams) => {
             referencesProvider: true,
             renameProvider: true,
             signatureHelpProvider: { triggerCharacters: ['('], retriggerCharacters: [',', ', '] },
-            hoverProvider: true
-            /**
+            hoverProvider: true,
             semanticTokensProvider: {
                 documentSelector: null, // use client-side definition
                 legend: {tokenModifiers: tokenModifier, tokenTypes: tokenTypes},
                 full: true,
                 range: false
             },
-             **/
         },
     };
 
@@ -122,12 +120,14 @@ connection.languages.semanticTokens.on(async params => {
         return new ResponseError(2, 'Parsing failed', undefined);
     }
 
-    const semanticTokens = getSemanticTokens(parseResult);
+    const semanticTokens = await getSemanticTokens(parseResult, documentManager);
     if (!semanticTokens) {
         connection.console.error("Retrieving semantic tokens failed.");
         return new ResponseError(3, 'Semantic tokens extraction failed', undefined);
     }
 
+    console.log(semanticTokens)
+
     return semanticTokens;
 });