diff --git a/buildSrc/src/main/kotlin/buildlogic.java-common-conventions.gradle.kts b/buildSrc/src/main/kotlin/buildlogic.java-common-conventions.gradle.kts index 41fdeee272..7b8d343f2c 100644 --- a/buildSrc/src/main/kotlin/buildlogic.java-common-conventions.gradle.kts +++ b/buildSrc/src/main/kotlin/buildlogic.java-common-conventions.gradle.kts @@ -137,7 +137,7 @@ dokka { } // To generate documentation in HTML -val dokkaHtmlJar by tasks.registering(Jar::class) { +val dokkaHtmlJar = tasks.register("dokkaHtmlJar") { description = "A HTML Documentation JAR containing Dokka HTML" from(tasks.dokkaGeneratePublicationHtml.flatMap { it.outputDirectory }) archiveClassifier.set("html-doc") diff --git a/buildSrc/src/main/kotlin/publish-convention.gradle.kts b/buildSrc/src/main/kotlin/publish-convention.gradle.kts index 4225cb427f..6fd718e89f 100644 --- a/buildSrc/src/main/kotlin/publish-convention.gradle.kts +++ b/buildSrc/src/main/kotlin/publish-convention.gradle.kts @@ -60,11 +60,19 @@ mavenPublishing { } } developers { + developer { + id = "weigl" + email = "weigl@kit.edu" + name = "Alexander Weigl" + organization = "Karlsruhe Institute of Technology" + organizationUrl = "https://kikit.kit.edu" + roles = listOf("developer", "maintainer") + } } scm { - connection = "scm:git:git://example.com/my-library.git" - developerConnection = "scm:git:ssh://example.com/my-library.git" - url = "http://example.com/my-library/" + connection = "scm:git:git://github.com/keyproject/key-rpc.git" + developerConnection = "scm:git:ssh://github.com/keyproject/key-rpc.git" + url = "http://keyproject.github.io/key-rpc" } } } @@ -73,7 +81,7 @@ fun envOrPropertyValue(key: String): String = if (key in System.getenv()) { System.getenv(key) } else { - project.properties[key]?.toString() ?: "" + project.findProperty(key)?.toString() ?: "" } val emptyJavadocJar = tasks.findByName("plainJavadocJar")!! diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 3825ef30c7..e27e0ae139 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -11,6 +11,7 @@ therapi = "0.15.0" kotlin-gradle-plugin = "2.4.0" dokka = "2.2.0" spotless = "8.7.0" +assertj = "3.27.7" [libraries] kotlin-gradle-plugin = { module = "org.jetbrains.kotlin:kotlin-gradle-plugin", version.ref = "kotlin-gradle-plugin" } @@ -22,11 +23,17 @@ key-ui = { module = "org.key-project:key.ui", version.ref = "key" } jacoco-cobertura = { module = "name.remal.jacoco-to-cobertura:name.remal.jacoco-to-cobertura.gradle.plugin", version = "2.0.4" } lsp4j-jsonrpc = { module = "org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc", version.ref = "lsp4j" } +lsp4j-lsp = { module = "org.eclipse.lsp4j:org.eclipse.lsp4j", version.ref = "lsp4j" } lsp4j-websocket-jakarta = { module = "org.eclipse.lsp4j:org.eclipse.lsp4j.websocket.jakarta", version.ref = "lsp4j" } jetty-websocket-javax-server = { module = "org.eclipse.jetty.websocket:websocket-javax-server", version.ref = "jetty-websocket" } picocli = { module = "info.picocli:picocli", version.ref = "picocli" } guava = { module = "com.google.guava:guava", version.ref = "guava" } +auto-service = { module = "com.google.auto.service:auto-service", version = "1.1.1" } therapi-runtime-javadoc-scribe = { module = "com.github.therapi:therapi-runtime-javadoc-scribe", version.ref = "therapi" } therapi-runtime-javadoc = { module = "com.github.therapi:therapi-runtime-javadoc", version.ref = "therapi" } clickt = { module = "com.github.ajalt.clikt:clikt", version = "5.1.0" } vanniktech-maven = { module = "com.vanniktech.maven.publish:com.vanniktech.maven.publish.gradle.plugin", version = "0.37.0" } +assertj-core = { module = "org.assertj:assertj-core", version.ref = "assertj" } + +[plugins] +shadow = { id = "com.gradleup.shadow", version = "9.6.1" } diff --git a/keyext.lsp/build.gradle.kts b/keyext.lsp/build.gradle.kts new file mode 100644 index 0000000000..a0bf6b3fe5 --- /dev/null +++ b/keyext.lsp/build.gradle.kts @@ -0,0 +1,39 @@ +plugins { + id("buildlogic.java-library-conventions") + application + alias(libs.plugins.shadow) + kotlin("kapt") +} + +application { + mainClass = "org.key_project.key.lsp.Main" +} + +dependencies { + api(project(":keyext.api")) + api(libs.lsp4j.jsonrpc) + api(libs.lsp4j.lsp) + implementation(libs.lsp4j.websocket.jakarta) + implementation(libs.jetty.websocket.javax.server) + implementation(libs.picocli) + implementation(libs.guava) + implementation(libs.auto.service) + implementation(libs.clickt) + + annotationProcessor(libs.therapi.runtime.javadoc.scribe) + api(libs.therapi.runtime.javadoc) + + implementation("io.github.wadoon:kotlin-prettyprinting:1.1.0") + + testImplementation(libs.assertj.core) + testImplementation("org.mockito:mockito-core:5.23.0") + testImplementation(kotlin("test")) +} + +tasks.named("compileJava") { + options.compilerArgs.add("-parameters") // for having parameter name in reflection +} + +repositories { + mavenCentral() +} \ No newline at end of file diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/Formatter.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/Formatter.kt new file mode 100644 index 0000000000..3f51661230 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/Formatter.kt @@ -0,0 +1,390 @@ +package org.key_project.key.lsp + +import de.uka.ilkd.key.nparser.JavaKeYLexer.* +import de.uka.ilkd.key.nparser.ParsingFacade +import de.uka.ilkd.key.speclang.PositionedString +import io.github.wadoon.pp.* +import org.antlr.v4.runtime.CharStreams +import org.antlr.v4.runtime.Token +import org.key_project.util.parsing.Location +import java.nio.file.Path +import java.util.* + +internal typealias TokenIter = PushbackIterator + +class Formatter { + fun format(code: String) = + format(ParsingFacade.createLexer(CharStreams.fromString(code)).allTokens) + + fun format(code: String, location: Location) = + format(ParsingFacade.createLexer(PositionedString(code, location)).allTokens) + + fun format(path: Path) = + format(ParsingFacade.createLexer(path).allTokens) + + fun format(tokens: List, width: Int = 80, rfrac: Double = 1.0, indent: Int = 0): String { + val doc = createDoc(tokens) + return Engine.pretty(doc, width, rfrac, indent) + } + + fun createDoc(code: List): Document { + var doc: Document = empty + val iter = PushbackIterator(code) + while (iter.hasNext()) { + val token = iter.next() + doc += asDoc(token, iter) + } + return doc + } + + private fun formatUntil(iter: TokenIter, pred: (Token) -> Boolean): Document { + var doc: Document = empty + while (iter.hasNext()) { + val token = iter.next() + if (pred(token)) { + iter.back() + break + } + doc += asDoc(token, iter) + } + return doc + } + + private fun asDoc(iter: TokenIter): Document = if (iter.hasNext()) asDoc(iter.next(), iter) else empty + + private fun asDoc(token: Token, iter: TokenIter): Document = when (token.type) { + MODALITY -> empty + + TERMLABEL -> keyword(token, iter) + + MODIFIABLE -> keyword(token, iter) + + GET_VARIANT, + IS_LABELED, + SAME_OBSERVER, + DEPENDINGON, + DISJOINTMODULONULL, + GET_FREE_INVARIANT, GET_INVARIANT, HAS_INVARIANT, STORE_STMT_IN, STORE_TERM_IN, PROGRAMVARIABLES -> keyword( + token, + iter + ) + + DROP_EFFECTLESS_STORES, + ENUM_CONST, + FREELABELIN, + FIELDTYPE, + FINAL, + ELEMSORT, + HASLABEL, + HASSUBFORMULAS, + ISARRAY, + ISARRAYLENGTH, + ISCONSTANT, + ISENUMTYPE, + ISINDUCTVAR, + ISLOCALVARIABLE, + ISOBSERVER, + METADISJOINT, + ISTHISREFERENCE, + DIFFERENTFIELDS, + ISREFERENCE, + ISREFERENCEARRAY, + ISSTATICFIELD, + ISMODELFIELD, + ISINSTRICTFP, + NEW_DEPENDING_ON, + NEW_LOCAL_VARS, + NEWLABEL, + CONTAINS_ASSIGNMENT, + NOTFREEIN, + STATIC, + STATICMETHODREFERENCE, + MAXEXPANDMETHOD, + CLASSPATH, + BOOTCLASSPATH, + NODEFAULTCLASSES, + JAVASOURCE, + CHOOSECONTRACT, + CONTRACTS, + INVARIANTS, + IN_TYPE, + IS_ABSTRACT_OR_INTERFACE, + IS_FINAL, + CONTAINERTYPE, + GENERIC, + PROXY, + EXTENDS, + ONEOF, + ABSTRACT, + ALIAS -> keyword(token, iter) + + VARIABLES, SCHEMAVARIABLES, + SORTS -> sectionKw(token, iter) + + SCHEMAVAR, + + MODALOPERATOR, + + PROGRAM, + FORMULA, + TERM, + UPDATE, + VARIABLE, + SKOLEMTERM, + SKOLEMFORMULA, + VARCOND, + + APPLY_UPDATE_ON_RIGID, + + DROP_EFFECTLESS_ELEMENTARIES, + + SIMPLIFY_IF_THEN_ELSE_UPDATE, + + HASSORT, + + DIFFERENT, + + ISSUBTYPE, + + EQUAL_UNIQUE, + + NEW, + + NEW_TYPE_OF, + + HAS_ELEMENTARY_SORT, + + DOC_COMMENT -> comment(token) + + ML_COMMENT -> comment(token) + + NOT_, + + SAME, + + STRICT, + + TYPEOF, + + INSTANTIATE_GENERIC, + + FORALL, + + EXISTS, + + SUBST, + + IF, + + IFEX, + + THEN, + + ELSE, + + INCLUDE, + + INCLUDELDTS, + + PROGRAMSOURCE, + + WITHOPTIONS, + + OPTIONSDECL, + + KEYSETTINGS, + + PROFILE, + + TRUE, + + FALSE, + + SAMEUPDATELEVEL, + + IGNOREUPDATELEVEL, + + INSEQUENTSTATE, + + ANTECEDENTPOLARITY, + + SUCCEDENTPOLARITY, + + CLOSEGOAL, + + HEURISTICSDECL, + + NONINTERACTIVE, + + DISPLAYNAME, + + HELPTEXT, + + REPLACEWITH, + + ADDRULES, + + ADDPROGVARS, + + HEURISTICS, + + FIND, + + ADD, + + ASSUMES, + + TRIGGER, + + AVOID, + + TRANSFORMERS, + + UNIQUE, + + FREE, + + FUNCTIONS, PREDICATES, + DATATYPES, RULES, AXIOMS, + PROBLEM, PROOFOBLIGATION, PROOF, + PROOFSCRIPT -> sectionKw(token, iter) + + LEMMA -> hardline + keyword(token, iter) + + + SEMI -> string(token) + (if (section) { + iter.skip { it.type == WS } + if (iter.peekClosing()) empty else hardline + } else empty) + + COMMA -> commaSpace + EMPTYBRACKETS -> string(token) + PARALLEL, OR, AND, NOT, IMP, EQUALS, NOT_EQUALS, SEQARROW, + EXP, TILDE, PERCENT, STAR, MINUS, PLUS, GREATER, GREATEREQUAL, LESS, LESSEQUAL, EQV, PRIMES, + UTF_PRECEDES, UTF_IN, UTF_EMPTY, UTF_UNION, UTF_INTERSECT, UTF_SUBSET_EQ, + UTF_SUBSEQ, UTF_SETMINUS, SLASH, COLON, DOUBLECOLON, ASSIGN, AT, + DOT, DOTRANGE -> separator(token, break1, break1) + + STRING_LITERAL, CHAR_LITERAL, QUOTED_STRING_LITERAL -> string(token) + WS -> handleWhitespace(token) + + OPENTYPEPARAMS -> groupUntil(token, CLOSETYPEPARAMS, iter) + CLOSETYPEPARAMS -> string(token) + LGUILLEMETS -> groupUntil(token, RGUILLEMETS, iter) + RGUILLEMETS -> string(token) + + LPAREN -> groupUntil(token, RPAREN, iter) + RPAREN -> string(token) + + LBRACE -> groupUntil(token, RBRACE, iter, section) + + RBRACE -> string(token) + + LBRACKET -> groupUntil(token, RBRACKET, iter) + + RBRACKET -> string(token) + + SL_COMMENT, BIN_LITERAL, HEX_LITERAL, INT_LITERAL, + FLOAT_LITERAL, DOUBLE_LITERAL, REAL_LITERAL, + MATCH_IDENT, IDENT -> string(token) + + else -> string(token) + } + + private fun string(s: Token): Document = string(s.text) + + private fun separator(token: Token, before: Document = break1, after: Document = break1) = + before + string(token) + after + + private fun handleWhitespace(token: Token): Document { + val hl = token.text.count { it == '\n' } + return if (hl != 0) { + hardline + hardline + } else { + breakableSpace + } + } + + var section = false + private fun groupUntil( + token: Token, + untilType: Int, + iter: PushbackIterator, + forceLine: Boolean = false + ): Document { + if (section) { + val s = if (forceLine) { + iter.skipWS() + hardline + } else if (iter.peekWS()) { + iter.skipWS() + breakableSpace + } else { + empty + } + iter.skipWS() + + val doc = string(token) + nest(4, s + formatUntil(iter) { it.type == untilType }) + s + asDoc(iter) + section = false + return doc + } else { + return string(token) + breakableSpace + nest(4, formatUntil(iter) { it.type == untilType }) + } + } + + + private fun comment(token: Token): Document = StringTokenizer(token.text, " \t\n\r", true).asIterator().asSequence() + .map { it.toString() } + .map { if (it.isBlank()) breakableSpace else string(it) } + .reduce { acc, unit -> acc + unit } + + private fun keyword(token: Token, iter: PushbackIterator): Document = keyword(token, iter.peek()) + private fun keyword(token: Token, peek: Token): Document = string(token.text) + private fun sectionKw(token: Token, iter: PushbackIterator): Document { + section = true + iter.skipWS() + return clearline + string(token.text) + space + } +} + +private fun TokenIter.peekClosing(): Boolean = peek().type in arrayOf(RPAREN, RBRACE, RBRACE, RGUILLEMETS) +private fun TokenIter.peekWS(): Boolean = peek().type == WS +private fun TokenIter.skipWS() = skip { it.type == WS } + +private fun String.weightedCount(value: (Int) -> Int): Int = chars().map { value(it) }.sum() + +private operator fun Document.times(count: Int): Document = + if (count <= 0) { + empty + } else { + (0 until count).toList().concatMap { hardline } + } + +internal class PushbackIterator(val tokens: List) : Iterator { + var pos = 0 + + override fun next() = tokens[pos++] + fun back() = pos-- + + override fun hasNext(): Boolean = pos < tokens.size + + fun peek() = tokens[pos] + + fun seek(a: Int) { + pos += a + require(0 <= pos) + } + + fun mark(): Int = pos + fun skip(pred: (T) -> Boolean) { + while (hasNext()) { + if (pred(peek())) { + next() + } else { + break + } + } + } +} + +val clearline: Document = hardline diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/KeyLanguageServer.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/KeyLanguageServer.kt new file mode 100644 index 0000000000..956b19d8a6 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/KeyLanguageServer.kt @@ -0,0 +1,155 @@ +/* This file is part of jmltoolkit project - https://github.com/jmltoolkit + * jmltk is licensed under the Lesser GNU General Public License Version 2 and Apache License + * SPDX-License-Identifier: LGPL-3.0-or-later Apache-2.0 + */ +package org.key_project.key.lsp + +import de.uka.ilkd.key.util.KeYConstants +import org.eclipse.lsp4j.* +import org.eclipse.lsp4j.jsonrpc.messages.Either +import org.eclipse.lsp4j.services.* +import org.key_project.key.lsp.actions.LspAction +import org.key_project.key.lsp.highlighting.LEGEND +import org.key_project.key.lsp.services.KeyNotebookDocumentServices +import org.key_project.key.lsp.services.KeyTextDocumentService +import org.key_project.key.lsp.services.KeyWorkspaceService +import org.slf4j.LoggerFactory +import java.util.* +import java.util.concurrent.CompletableFuture +import java.util.concurrent.ExecutorService +import java.util.concurrent.ForkJoinPool +import java.util.concurrent.TimeUnit +import kotlin.system.exitProcess + +/** + * Language Server implementation for KeY files. + * + * Provides LSP features including: + * - Semantic highlighting + * - Document symbols + * - Code lenses + * - Hover information + * - Completion providers + * - Workspace diagnostics + * - Command execution + * + * @author Alexander Weigl + * @version 1.0 + */ +class KeyLanguageServer : + LanguageServer, + LanguageClientAware { + internal val executorService: ExecutorService = ForkJoinPool.commonPool() + internal val keyTextDocumentService by lazy { KeyTextDocumentService(this) } + internal val keyWorkspaceService by lazy { KeyWorkspaceService(this) } + internal val keyNotebookDocumentServices by lazy { KeyNotebookDocumentServices() } + + internal lateinit var client: LanguageClient + + internal lateinit var initParams: InitializeParams + + internal val capabilities: ClientCapabilities + get() = initParams.capabilities + + /** + * Loads LSP actions via ServiceLoader pattern. + * + * Extensions can register custom actions by implementing [LspAction] interface + * and adding a META-INF/services/org.key_project.key.lsp.actions.LspAction file + * with the fully qualified class name. + */ + internal val actions by lazy { + ServiceLoader.load(LspAction::class.java).toList() + } + + override fun initialize(params: InitializeParams): CompletableFuture { + initParams = params + val keyFiles = DocumentFilter("key", "file", Either.forLeft("**/*.key")) + val keyFilesJar = DocumentFilter("key", "jar:file", Either.forLeft("**/*.key")) + + val capabilities = ServerCapabilities() + capabilities.setHoverProvider(true) + capabilities.signatureHelpProvider = SignatureHelpOptions(listOf("<", "("), listOf("<", "(", ",")) + capabilities.foldingRangeProvider = Either.forRight(FoldingRangeProviderOptions("KeY")) + capabilities.diagnosticProvider = DiagnosticRegistrationOptions(false, true).also { + it.identifier = "key-lsp" + it.documentSelector = listOf(keyFiles, keyFilesJar) + } + + capabilities.setDocumentSymbolProvider(true) + capabilities.setDeclarationProvider(DeclarationRegistrationOptions("KeY")) + + capabilities.setCodeActionProvider(CodeActionOptions(listOf("key"))) + capabilities.executeCommandProvider = ExecuteCommandOptions(actions.map { it.id }) + capabilities.codeLensProvider = CodeLensOptions(true) + capabilities.selectionRangeProvider = Either.forRight(SelectionRangeRegistrationOptions("KeY")) + + capabilities.setTextDocumentSync(TextDocumentSyncKind.Full) + capabilities.completionProvider = CompletionOptions(true, listOf(",", "(", ")", "<", ">", "\\")) + + capabilities.semanticTokensProvider = SemanticTokensWithRegistrationOptions( + LEGEND, SemanticTokensServerFull(true), false, + listOf( + keyFiles, keyFilesJar + ) + ) + capabilities.semanticTokensProvider.id = "key-lsp" + capabilities.semanticTokensProvider.range = Either.forLeft(true) + + capabilities.documentOnTypeFormattingProvider = null + + capabilities.setDocumentFormattingProvider(true) + capabilities.setDocumentRangeFormattingProvider(true) + capabilities.documentLinkProvider = DocumentLinkOptions(false) + + capabilities.setWorkspaceSymbolProvider(true) + + capabilities.textDocument = TextDocumentServerCapabilities() + capabilities.textDocument.diagnostic = DiagnosticServerCapabilities().also { it.markupMessageSupport = true } + + capabilities.workspace = WorkspaceServerCapabilities() + capabilities.workspace.workspaceFolders = WorkspaceFoldersOptions().also { + it.supported = true + it.changeNotifications = Either.forRight(true) + } + + capabilities.workspace.textDocumentContent = TextDocumentContentRegistrationOptions( + listOf("jar:file") + ) + + + return CompletableFuture.completedFuture( + InitializeResult( + capabilities, + ServerInfo( + "key-lsp", + "using${KeYConstants.VERSION} (${KeYConstants.INTERNAL_VERSION})" + ) + ) + ) + } + + override fun shutdown(): CompletableFuture { + executorService.shutdown() + val c = executorService.awaitTermination(5, TimeUnit.SECONDS) + val i = executorService.shutdownNow() + return CompletableFuture.completedFuture("Finish: Waited 5 seconds. $c, ${i.size} jobs killed.") + } + + override fun exit() { + shutdown() + exitProcess(0) + } + + override fun getNotebookDocumentService(): NotebookDocumentService = keyNotebookDocumentServices + + override fun getTextDocumentService(): TextDocumentService = keyTextDocumentService + + override fun getWorkspaceService(): WorkspaceService = keyWorkspaceService + + override fun connect(client: LanguageClient) { + this.client = client + } +} + +internal val LOGGER = LoggerFactory.getLogger("key-lsp") diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/RemoteApi.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/RemoteApi.kt new file mode 100644 index 0000000000..6129c6347e --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/RemoteApi.kt @@ -0,0 +1,7 @@ +package org.key_project.key.lsp + +import org.eclipse.lsp4j.services.LanguageClient + +public interface RemoteApi : + //ClientApi, + LanguageClient \ No newline at end of file diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/actions/LspAction.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/actions/LspAction.kt new file mode 100644 index 0000000000..1f1a99ef2e --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/actions/LspAction.kt @@ -0,0 +1,10 @@ +package org.key_project.key.lsp.actions + +import org.eclipse.lsp4j.ExecuteCommandParams + +interface LspAction { + val id: String + get() = this::class.java.name + + fun execute(params: ExecuteCommandParams): Any? +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/actions/StartKey.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/actions/StartKey.kt new file mode 100644 index 0000000000..bc04d13c9d --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/actions/StartKey.kt @@ -0,0 +1,40 @@ +package org.key_project.key.lsp.actions + +import de.uka.ilkd.key.core.Main +import de.uka.ilkd.key.gui.MainWindow +import de.uka.ilkd.key.nparser.JavaKeYParser +import org.eclipse.lsp4j.CodeLens +import org.eclipse.lsp4j.Command +import org.eclipse.lsp4j.ExecuteCommandParams +import org.key_project.key.lsp.services.asUri +import org.key_project.key.lsp.services.toPath +import org.key_project.key.lsp.symbols.asRange +import java.nio.file.Paths +import javax.swing.SwingUtilities +import kotlin.io.path.absolute + + +class StartKey : LspAction { + fun createCodeLens(ctx: JavaKeYParser.ProblemContext, uri: String): CodeLens = + CodeLens(ctx.asRange, createCommand(uri), null) + + fun createCommand(uri: String) = Command( + "Start KeY", id, + listOf( + uri.toPath().toAbsolutePath().asUri + ) + ).also { + it.tooltip = "Start the KeY Theorem Prover with this problem definition" + } + + override fun execute(params: ExecuteCommandParams): Any? { + Main::class.java.getDeclaredField("workingDir").also { + it.isAccessible = true + it.set(null, Paths.get(".").absolute()) + } + val path = Paths.get(params.arguments.first().toString()) + val mainWindow = MainWindow.getInstance(true) + mainWindow.userInterface.loadProblem(path) + return null + } +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/highlighting/DocumentHighlighter.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/highlighting/DocumentHighlighter.kt new file mode 100644 index 0000000000..34d56c8281 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/highlighting/DocumentHighlighter.kt @@ -0,0 +1,84 @@ +/* This file is part of jmltoolkit project - https://github.com/jmltoolkit + * jmltk is licensed under the Lesser GNU General Public License Version 2 and Apache License + * SPDX-License-Identifier: LGPL-3.0-or-later Apache-2.0 + */ +package org.key_project.key.lsp.highlighting + +import com.github.javaparser.Token +import org.eclipse.lsp4j.* + +/** + * + * @author Alexander Weigl + * @version 1 (04.02.24) + */ +interface DocumentHighlighter { + fun analyzeToken(text: String): SemanticTokens +} + +enum class SupportedTokenTypes(val kind: String) { + COMMENT(SemanticTokenTypes.Comment), + VARIABLE(SemanticTokenTypes.Variable), + KEYWORD(SemanticTokenTypes.Keyword), + STRING(SemanticTokenTypes.String), + NUMBER(SemanticTokenTypes.Number), + OPERATOR(SemanticTokenTypes.Operator), + MODIFIER(SemanticTokenTypes.Modifier), +} + +enum class SupportedTokenModifier(val kind: String) { + DECLARATION(SemanticTokenModifiers.Declaration), + DOCUMENTATION(SemanticTokenModifiers.Documentation), + DEPRECATED(SemanticTokenModifiers.Deprecated), + STATIC(SemanticTokenModifiers.Static), +} + +private val Token.asRange: Range + get() = Range(Position(beginLine, beginColumn), Position(endLine, endColumn)) + +val tokenTypes = SupportedTokenTypes.entries.map { it.kind } +val tokenModifiers = SupportedTokenModifier.entries.map { it.kind } +val LEGEND: SemanticTokensLegend = SemanticTokensLegend(tokenTypes, tokenModifiers) + +/* + There are different ways how the position of a token can be expressed in a file. + Absolute positions or relative positions. The protocol for the token format relative uses + relative positions, because most tokens remain stable relative to each other when edits + are made in a file. This simplifies the computation of a delta if a server supports it. + So each token is represented using 5 integers. A specific token i in the file consists + of the following array indices: + + at index 5*i - deltaLine: token line number, relative to the previous token + at index 5*i+1 - deltaStart: token start character, relative to the previous token (relative to 0 or the previous + token’s start if they are on the same line) + at index 5*i+2 - length: the length of the token. + at index 5*i+3 - tokenType: will be looked up in SemanticTokensLegend.tokenTypes. We currently ask that tokenType < 65536. + at index 5*i+4 - tokenModifiers: each set bit will be looked up in SemanticTokensLegend.tokenModifiers + */ +data class SemanticTokensBuilder(val data: ArrayList = ArrayList(4096)) { + private var lastLineStart = 0 + private var lastColumnStart = 0 + fun add(tok: Token, tokenType: Int, modifiers: Int) { + // Conversion from jmltk to lsp: + // line - 1 + // column - 1 + + add(tok.beginLine - 1, tok.beginColumn - 1, tok.image.length, tokenType, modifiers) + } + + fun add(beginLine: Int, beginColumn: Int, length: Int, tokenType: Int, modifiers: Int) { + data.ensureCapacity(data.size + 5) + if (beginLine != lastLineStart) { + lastColumnStart = 0 + } + + data.add(beginLine - lastLineStart) + data.add(beginColumn - lastColumnStart) + data.add(length) + data.add(tokenType) + data.add(modifiers) + + lastLineStart = beginLine + lastColumnStart = beginColumn + } +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/highlighting/KeyDocumentHighlighter.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/highlighting/KeyDocumentHighlighter.kt new file mode 100644 index 0000000000..a7c7a6f47d --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/highlighting/KeyDocumentHighlighter.kt @@ -0,0 +1,270 @@ +/* This file is part of jmltoolkit project - https://github.com/jmltoolkit + * jmltk is licensed under the Lesser GNU General Public License Version 2 and Apache License + * SPDX-License-Identifier: LGPL-3.0-or-later Apache-2.0 + */ +package org.key_project.key.lsp.highlighting + +import de.uka.ilkd.key.nparser.JavaKeYLexer.* +import de.uka.ilkd.key.nparser.ParsingFacade +import org.antlr.v4.runtime.CharStreams +import org.antlr.v4.runtime.Token +import org.eclipse.lsp4j.SemanticTokens + +class KeyDocumentHighlighter : DocumentHighlighter { + override fun analyzeToken(text: String): SemanticTokens { + val lexer = ParsingFacade.createLexer(CharStreams.fromString(text)) + val tb = SemanticTokensBuilder() + do { + val token = lexer.nextToken() + if (token.type == EOF) { + break + } + tokenType(token)?.let { tt -> + tb.add(token.line - 1, token.charPositionInLine, token.text.length, tt, tokenModifier(token)) + } + } while (token.type != EOF) + return SemanticTokens(tb.data) + } + + private fun tokenType(token: Token): Int? = when (token.type) { + SL_COMMENT, + COMMENT_END, + DOC_COMMENT, + ML_COMMENT, + MODALITYD_LINE_COMMENT, + COMMENT -> SupportedTokenTypes.COMMENT.ordinal + + MATCH_IDENT, + IDENT + -> SupportedTokenTypes.VARIABLE.ordinal + + ERROR_UKNOWN_ESCAPE, + ERROR_CHAR, + -> null + + TRUE, + FALSE, + BIN_LITERAL, + HEX_LITERAL, + INT_LITERAL, + CHAR_LITERAL, + REAL_LITERAL, + DOUBLE_LITERAL, + FLOAT_LITERAL, + -> SupportedTokenTypes.NUMBER.ordinal + + MODALITYD_STRING, + MODALITYD_CHAR, + STRING_LITERAL, + QUOTED_STRING_LITERAL, + -> SupportedTokenTypes.STRING.ordinal + + TERMLABEL, + MODIFIABLE, + PROGRAMVARIABLES, + STORE_TERM_IN, + STORE_STMT_IN, + HAS_INVARIANT, + GET_INVARIANT, + GET_VARIANT, + IS_LABELED, + SAME_OBSERVER, + DEPENDINGON, + DISJOINTMODULONULL, + DROP_EFFECTLESS_STORES, + ENUM_CONST, + FREELABELIN, + FIELDTYPE, + FINAL, + ELEMSORT, + HASLABEL, + HASSUBFORMULAS, + ISARRAY, + ISARRAYLENGTH, + ISCONSTANT, + ISENUMTYPE, + ISINDUCTVAR, + ISLOCALVARIABLE, + ISOBSERVER, + METADISJOINT, + ISTHISREFERENCE, + DIFFERENTFIELDS, + ISREFERENCE, + ISREFERENCEARRAY, + ISSTATICFIELD, + ISMODELFIELD, + ISINSTRICTFP, + NEW_DEPENDING_ON, + NEW_LOCAL_VARS, + NEWLABEL, + CONTAINS_ASSIGNMENT, + NOTFREEIN, + STATIC, + STATICMETHODREFERENCE, + MAXEXPANDMETHOD, + CLASSPATH, + BOOTCLASSPATH, + NODEFAULTCLASSES, + JAVASOURCE, + CHOOSECONTRACT, + CONTRACTS, + INVARIANTS, + IN_TYPE, + IS_ABSTRACT_OR_INTERFACE, + IS_FINAL, + CONTAINERTYPE, + SORTS, + GENERIC, + PROXY, + EXTENDS, + ONEOF, + ABSTRACT, + ALIAS, + SCHEMAVARIABLES, + SCHEMAVAR, + MODALOPERATOR, + PROGRAM, + FORMULA, + TERM, + UPDATE, + VARIABLES, + SKOLEMTERM, + SKOLEMFORMULA, + VARCOND, + APPLY_UPDATE_ON_RIGID, + DROP_EFFECTLESS_ELEMENTARIES, + SIMPLIFY_IF_THEN_ELSE_UPDATE, + HASSORT, + DIFFERENT, + ISSUBTYPE, + EQUAL_UNIQUE, + NEW, + NEW_TYPE_OF, + HAS_ELEMENTARY_SORT, + NOT_, + SAME, + STRICT, + TYPEOF, + INSTANTIATE_GENERIC, + FORALL, + EXISTS, + SUBST, + IF, + IFEX, + THEN, + ELSE, + INCLUDE, + INCLUDELDTS, + PROGRAMSOURCE, + WITHOPTIONS, + OPTIONSDECL, + KEYSETTINGS, + PROFILE, + SAMEUPDATELEVEL, + IGNOREUPDATELEVEL, + INSEQUENTSTATE, + ANTECEDENTPOLARITY, + SUCCEDENTPOLARITY, + CLOSEGOAL, + HEURISTICSDECL, + NONINTERACTIVE, + DISPLAYNAME, + HELPTEXT, + REPLACEWITH, + ADDRULES, + ADDPROGVARS, + HEURISTICS, + FIND, + + ADD, + ASSUMES, + TRIGGER, + AVOID, + PREDICATES, + FUNCTIONS, + DATATYPES, + TRANSFORMERS, + UNIQUE, + FREE, + RULES, + AXIOMS, + PROBLEM, + PROOFOBLIGATION, + PROOF, + PROOFSCRIPT, + LEMMA, + VARIABLE, + -> SupportedTokenTypes.KEYWORD.ordinal + + MODALITYBB, + MODAILITYGENERIC3, + MODAILITYGENERIC5, + MODAILITYGENERIC6, + MODAILITYGENERIC7, + MODALITYD, + MODALITYB, + MODAILITYGENERIC1, + MODAILITYGENERIC2, + MODAILITYGENERIC4, + MODALITYD_END, + MODALITYG_END, + MODALITYB_END, + MODALITYBB_END, + UTF_PRECEDES, + UTF_IN, + UTF_EMPTY, + UTF_UNION, + UTF_INTERSECT, + UTF_SUBSET_EQ, + UTF_SUBSEQ, + UTF_SETMINUS, + SEMI, + SLASH, + COLON, + DOUBLECOLON, + ASSIGN, + DOT, + DOTRANGE, + COMMA, + LPAREN, + RPAREN, + LBRACE, + RBRACE, + LBRACKET, + RBRACKET, + EMPTYBRACKETS, + AT, + PARALLEL, + OR, + AND, + NOT, + IMP, + EQUALS, + NOT_EQUALS, + SEQARROW, + EXP, + TILDE, + PERCENT, + STAR, + MINUS, + PLUS, + GREATER, + GREATEREQUAL, + OPENTYPEPARAMS, + CLOSETYPEPARAMS, + LESS, + LESSEQUAL, + LGUILLEMETS, + RGUILLEMETS, + EQV, + PRIMES, + MODALITY, + -> SupportedTokenTypes.OPERATOR.ordinal + + else -> null + } + + private fun tokenModifier(token: Token): Int = when (token.type) { + else -> 0 + } +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/main.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/main.kt new file mode 100644 index 0000000000..5c07026e24 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/main.kt @@ -0,0 +1,130 @@ +/* This file is part of jmltoolkit project - https://github.com/jmltoolkit + * jmltk is licensed under the Lesser GNU General Public License Version 2 and Apache License + * SPDX-License-Identifier: LGPL-3.0-or-later Apache-2.0 + */ +package org.key_project.key.lsp + +import com.github.ajalt.clikt.core.CliktCommand +import com.github.ajalt.clikt.core.main +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.flag +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.int +import org.eclipse.lsp4j.jsonrpc.Launcher +import org.eclipse.lsp4j.launch.LSPLauncher +import org.eclipse.lsp4j.services.LanguageServer +import org.keyproject.key.api.KeyApiImpl +import org.keyproject.key.api.StartServer +import java.io.InputStream +import java.io.OutputStream +import java.io.PrintWriter +import java.net.InetAddress +import java.net.ServerSocket +import java.net.Socket +import java.util.concurrent.ExecutorService +import java.util.concurrent.ForkJoinPool +import java.util.concurrent.Future +import kotlin.concurrent.thread + +/** + * @author Alexander Weigl + * @version 1 (10.07.22) + */ +object Main { + @JvmStatic + fun main(args: Array) { + KeyLspCommand().main(args) + } +} + +val executorService: ExecutorService = ForkJoinPool.commonPool() + +class KeyLspCommand : CliktCommand() { + private val traceEnabled by option("--trace") + private val stdioMode by option("--stdio").flag() + private val serverMode by option("--server").int() + private val client by option("--client").int() + + override fun run() { + try { + when { + stdioMode -> launchLanguageServer(System.`in`, System.out).get() + serverMode != null -> runAsServer(serverMode!!) + client != null -> runAsClient(client!!) + else -> launchLanguageServer(System.`in`, System.out).get() + } + } catch (e: Exception) { + LOGGER.error("Error at starting LSP server", e) + } + } + + private fun launchLanguageServer(input: InputStream, output: OutputStream): Future<*> { + val languageServer = KeyLanguageServer() + val keyApiServer = KeyApiImpl() + + val launcher = createServerLauncher( + languageServer, + listOf(keyApiServer), + input, output + ) + + val client = launcher.remoteProxy + languageServer.connect(client) + //keyApiServer.setClientApi(client) + return launcher.startListening() + } + + private fun createServerLauncher( + lsp: LanguageServer, + furtherServices: List, + input: InputStream, + output: OutputStream + ): Launcher { + val l = LSPLauncher.Builder() + .setLocalServices(listOf(lsp) + furtherServices) + .setRemoteInterface(RemoteApi::class.java) + .setInput(input) + .setOutput(output) + .setExecutorService(executorService) + .validateMessages(true) + // .wrapMessages(wrapper) + .configureGson(StartServer::configureJson) + .setClassLoader(javaClass.classLoader) + + traceEnabled?.let { + LOGGER.info("Tracing enabled: $it") + if (it == "-") { + l.traceMessages(PrintWriter(System.err)) + } else { + l.traceMessages(PrintWriter(it)) + } + } + + return l.create() + } + + private fun runAsClient(port: Int) { + val socket = Socket("localhost", port) + socket.tcpNoDelay = true + socket.keepAlive = true + launchLanguageServer(socket.getInputStream(), socket.getOutputStream()).get() + } + + private fun runAsServer(port: Int) { + try { + ServerSocket(port, 1, InetAddress.getLoopbackAddress()).use { serverSocket -> + while (true) { + LOGGER.info("Listening on {}", serverSocket.localSocketAddress) + val socket = serverSocket.accept() + socket.tcpNoDelay = true + socket.keepAlive = true + thread(start = true, isDaemon = true, name = "connection-worker") { + launchLanguageServer(socket.getInputStream(), socket.getOutputStream()).get() + } + } + } + } catch (e: Exception) { + LOGGER.error("", e) + } + } +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/CodeActionVisitor.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/CodeActionVisitor.kt new file mode 100644 index 0000000000..286fc17dd6 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/CodeActionVisitor.kt @@ -0,0 +1,7 @@ +package org.key_project.key.lsp.services + +import de.uka.ilkd.key.nparser.JavaKeYParserBaseVisitor +import org.eclipse.lsp4j.Command +import org.eclipse.lsp4j.Range + +class CodeActionVisitor(val range: Range) : JavaKeYParserBaseVisitor?>() diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/CodeLensVisitor.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/CodeLensVisitor.kt new file mode 100644 index 0000000000..2bf742d1a8 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/CodeLensVisitor.kt @@ -0,0 +1,24 @@ +package org.key_project.key.lsp.services + +import de.uka.ilkd.key.nparser.JavaKeYParser +import de.uka.ilkd.key.nparser.JavaKeYParserBaseVisitor +import org.eclipse.lsp4j.CodeLens +import org.eclipse.lsp4j.CodeLensParams +import org.key_project.key.lsp.actions.StartKey + +class CodeLensVisitor(val params: CodeLensParams) : JavaKeYParserBaseVisitor?>() { + override fun aggregateResult( + aggregate: List?, + nextResult: List? + ): List? = if (aggregate == null) { + nextResult + } else if (nextResult == null) { + aggregate + } else { + aggregate + nextResult + } + + override fun visitPreferences(ctx: JavaKeYParser.PreferencesContext?): List = listOf() + + override fun visitProblem(ctx: JavaKeYParser.ProblemContext): List = listOf(StartKey().createCodeLens(ctx, params.textDocument.uri)) +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/HoverDictionary.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/HoverDictionary.kt new file mode 100644 index 0000000000..97e69904e4 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/HoverDictionary.kt @@ -0,0 +1,37 @@ +package org.key_project.key.lsp.services + +import org.eclipse.lsp4j.MarkupContent +import org.eclipse.lsp4j.MarkupKind +import java.util.concurrent.ConcurrentHashMap + +object HoverDictionary { + private val dynamic: Map String> = ConcurrentHashMap() + + private val dictionary: Map by lazy { + val map = mutableMapOf() + val lines = javaClass.getResourceAsStream("/doc.md") + ?.bufferedReader()?.readLines() + ?: error("Could not load /doc.md") + + var keys = setOf() + val builder = StringBuilder() + for (line in lines) { + if (line.startsWith("%keywords")) { + keys = line.substringAfter(' ').splitToSequence(' ').toSet() + } else { + if (line.startsWith("-----")) { + val s = builder.toString().intern() + for (key in keys) { + map[key] = s + } + builder.clear() + } else { + builder.appendLine(line) + } + } + } + ConcurrentHashMap(map) + } + + fun get(text: String) = dynamic[text]?.let { it() } ?: dictionary[text] +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyNotebookDocumentServices.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyNotebookDocumentServices.kt new file mode 100644 index 0000000000..d13f0394a5 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyNotebookDocumentServices.kt @@ -0,0 +1,14 @@ +package org.key_project.key.lsp.services + +import org.eclipse.lsp4j.DidChangeNotebookDocumentParams +import org.eclipse.lsp4j.DidCloseNotebookDocumentParams +import org.eclipse.lsp4j.DidOpenNotebookDocumentParams +import org.eclipse.lsp4j.DidSaveNotebookDocumentParams +import org.eclipse.lsp4j.services.NotebookDocumentService + +class KeyNotebookDocumentServices : NotebookDocumentService { + override fun didOpen(params: DidOpenNotebookDocumentParams) {} + override fun didChange(params: DidChangeNotebookDocumentParams) {} + override fun didSave(params: DidSaveNotebookDocumentParams) {} + override fun didClose(params: DidCloseNotebookDocumentParams) {} +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyTextDocumentService.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyTextDocumentService.kt new file mode 100644 index 0000000000..2c17d9727b --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyTextDocumentService.kt @@ -0,0 +1,529 @@ +package org.key_project.key.lsp.services + +import com.google.common.cache.CacheBuilder +import de.uka.ilkd.key.nparser.JavaKeYLexer +import de.uka.ilkd.key.nparser.JavaKeYParser +import de.uka.ilkd.key.nparser.ParsingFacade +import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter +import org.antlr.v4.runtime.CharStreams +import org.antlr.v4.runtime.ParserRuleContext +import org.antlr.v4.runtime.Token +import org.antlr.v4.runtime.misc.ParseCancellationException +import org.antlr.v4.runtime.tree.ParseTree +import org.antlr.v4.runtime.tree.TerminalNode +import org.eclipse.lsp4j.* +import org.eclipse.lsp4j.jsonrpc.messages.Either +import org.eclipse.lsp4j.services.TextDocumentService +import org.key_project.key.lsp.Formatter +import org.key_project.key.lsp.KeyLanguageServer +import org.key_project.key.lsp.LOGGER +import org.key_project.key.lsp.highlighting.KeyDocumentHighlighter +import org.key_project.key.lsp.symbols.KeyCatchSymbols +import org.key_project.key.lsp.symbols.asRange +import org.key_project.util.java.IOUtil +import java.net.URI +import java.nio.file.Path +import java.nio.file.Paths +import java.time.Duration +import java.util.* +import java.util.concurrent.CompletableFuture +import java.util.concurrent.CompletableFuture.supplyAsync +import kotlin.io.path.readText +import kotlin.math.max +import kotlin.math.min + +private fun TerminalNode.parentSequence(): Sequence = generateSequence(this as ParseTree) { it.parent } + +val org.key_project.util.parsing.Location.toRange: Range + get() = Range(Position(position.line() + 1, position.column()), Position(position.line() + 1, position.column())) + +class KeyTextDocumentService(val server: KeyLanguageServer) : TextDocumentService { + // region file management + val fileErrors = CacheBuilder.newBuilder() + .expireAfterWrite(Duration.ofMinutes(5)) + .expireAfterAccess(Duration.ofMinutes(1)) + .maximumSize(250) + .initialCapacity(25) + .build() + .asMap() + + val fileCache = CacheBuilder.newBuilder() + .expireAfterWrite(Duration.ofMinutes(5)) + .expireAfterAccess(Duration.ofMinutes(1)) + .maximumSize(250) + .initialCapacity(25) + .build() + .asMap() + + fun getSync(uri: String): JavaKeYParser.FileContext { + if (uri !in fileCache) { + load(uri) + } + return fileCache[uri] ?: throw fileErrors[uri]!! + } + + fun get(uri: String): CompletableFuture = supplyAsync { + try { + getSync(uri) + } catch (e: SyntaxErrorReporter.ParserException) { + server.client.publishDiagnostics( + PublishDiagnosticsParams(uri, e.toDiagnostics()) + ) + throw e + } catch (e: ParseCancellationException) { + server.client.publishDiagnostics( + PublishDiagnosticsParams(uri, e.toDiagnostics()) + ) + throw e + } + } + + private fun load(uri: String): JavaKeYParser.FileContext? { + val path = uri.toPath() + try { + val p = ParsingFacade.createParser(CharStreams.fromPath(path)) + val ctx = p.file() + p.errorReporter.throwException() + fileErrors.remove(uri) + fileCache[uri] = ctx + return ctx + } catch (e: SyntaxErrorReporter.ParserException) { + fileErrors[uri] = e + throw e + } + } + + private fun invalidate(uri: String) { + fileCache.remove(uri) + } + + override fun didOpen(params: DidOpenTextDocumentParams) { + // read in, in advance + getSync(params.textDocument.uri) + } + + override fun didChange(params: DidChangeTextDocumentParams) { + invalidate(params.textDocument.uri) + } + + override fun didClose(params: DidCloseTextDocumentParams) { + // Nothing to do + } + + override fun didSave(params: DidSaveTextDocumentParams) { + invalidate(params.textDocument.uri) + getSync(params.textDocument.uri) + } + +//endregion + + //region Hover + override fun hover(params: HoverParams): CompletableFuture = + get(params.textDocument.uri) + .thenApply { symbolicLocation(it, params.position) } + .thenApply { describeAsHover(it) } + .exceptionally { e -> + LOGGER.warn("Error computing hover information", e) + null + } + + private tailrec fun symbolicLocation(ctx: ParserRuleContext, position: Position): TerminalNode { + for (tree in ctx.children) { + if (position in tree) { + return tree as? TerminalNode ?: symbolicLocation(tree as ParserRuleContext, position) + } + } + throw IllegalStateException() + } + + private fun describeAsHover(it: TerminalNode) = + HoverDictionary.get(it.symbol.text)?.let { Hover(MarkupContent(MarkupKind.MARKDOWN, it)) } + + override fun signatureHelp(params: SignatureHelpParams): CompletableFuture = + get(params.textDocument.uri) + .thenApplyAsync { file -> + val v = KeyCatchSymbols() + file.accept(v) + + val tn = symbolicLocation(file, params.position) + val accessTerm = tn.parentSequence().filterIsInstance().firstOrNull() + if (accessTerm != null) { + val declaredFunctions = v.declaredFunctions.filter { it.name == accessTerm.firstName.text } + val formalSortArgs = + tn.parentSequence().filterIsInstance().firstOrNull() + val callArgs = + tn.parentSequence().filterIsInstance().firstOrNull() + + if (formalSortArgs != null) { + val signatures = declaredFunctions.map { + SignatureInformation(it.name, it.documentation, it.sortArgs) + } + val pos = + formalSortArgs.COMMA().indexOfLast { + (it.symbol.line to it.symbol.charPositionInLine) <= + (params.position.line to params.position.character) + } + val p = signatures.indexOfFirst { it.parameters.size > pos } + SignatureHelp(signatures, max(0, pos), max(0, p)) + } else if (callArgs != null) { + val signatures = declaredFunctions.map { + SignatureInformation(it.name, it.documentation, it.args) + } + val pos = + callArgs.COMMA().indexOfLast { + (it.symbol.line to it.symbol.charPositionInLine) <= + (params.position.line to params.position.character) + } + val p = signatures.indexOfFirst { it.parameters.size > pos } + SignatureHelp(signatures, max(0, pos), max(0, p)) + } else { + null + } + } else { + null + } + }.exceptionally { + LOGGER.info("", it) + null + } +//endregion + + //region Folding + private val rulesOfFoldingInterests = mutableMapOf, (ParserRuleContext) -> String?>() + fun registerFoldingContext(ctx: Class, fn: (T) -> String?) { + rulesOfFoldingInterests[ctx] = fn as (ParserRuleContext) -> String? + } + + init { + registerFoldingContext(JavaKeYParser.ProblemContext::class.java) { + "Problem" + } + registerFoldingContext(JavaKeYParser.PreferencesContext::class.java) { + "Preferences" + } + registerFoldingContext(JavaKeYParser.ProofContext::class.java) { + "Proof" + } + registerFoldingContext(JavaKeYParser.RulesOrAxiomsContext::class.java) { + "Rules (${it.taclet().size} under ${it.option_list().text})" + } + + registerFoldingContext(JavaKeYParser.Sort_declsContext::class.java) { "Sorts" } + registerFoldingContext(JavaKeYParser.Func_declsContext::class.java) { "Functions" } + registerFoldingContext(JavaKeYParser.Pred_declsContext::class.java) { "Predicates" } + registerFoldingContext(JavaKeYParser.Transform_declsContext::class.java) { "Transformers" } + registerFoldingContext(JavaKeYParser.Datatype_declsContext::class.java) { "Datatypes" } + registerFoldingContext(JavaKeYParser.Datatype_declContext::class.java) { "${it.name}" } + registerFoldingContext(JavaKeYParser.TacletContext::class.java) { "Taclet: ${it.name}" } + registerFoldingContext(JavaKeYParser.GoalspecsContext::class.java) { "Goals" } + registerFoldingContext(JavaKeYParser.GoalspecContext::class.java) { "Goal ${it.name}" } + } + + override fun foldingRange(params: FoldingRangeRequestParams): CompletableFuture> = + get(params.textDocument.uri) + .thenApplyAsync { + val result = ArrayList(128) + val queue = LinkedList() + queue += it + while (queue.isNotEmpty()) { + val n = queue.pollFirst() + if (n.start.line == n.stop.line) continue // one line ParserRuleContext, nothing to gain by folding + rulesOfFoldingInterests[n.javaClass]?.let { + it(n)?.let { text -> + val range = FoldingRange(n.start.line, n.stop.line) + range.collapsedText = text + result.add(range) + } + } + queue.addAll(n.children.filterIsInstance()) + } + result as List + } + .exceptionally { e -> + LOGGER.error("Error in finding folding ranges", e) + listOf() + } +//endregion + + //region diagnostics + override fun diagnostic(params: DocumentDiagnosticParams): CompletableFuture = + get(params.textDocument.uri) + .thenApply { + DocumentDiagnosticReport(RelatedFullDocumentDiagnosticReport()) + } + .exceptionally { e -> + var items = listOf() + if (e is SyntaxErrorReporter.ParserException) { + items = e.toDiagnostics() + } + DocumentDiagnosticReport(RelatedFullDocumentDiagnosticReport(items)) + } +//endregion + + // region documentSymbol + override fun documentSymbol(params: DocumentSymbolParams): CompletableFuture>> = + get(params.textDocument.uri) + .thenApplyAsync>> { + val v = KeyCatchSymbols() + it.accept(v)?.map { symbol -> Either.forRight(symbol) } ?: listOf() + } + .exceptionally { + LOGGER.error("Error in documentSymbol", it) + listOf() + } +//endregion + + // region Declaration + override fun declaration(params: DeclarationParams): CompletableFuture, List>> = + get(params.textDocument.uri) + .thenApplyAsync { + val tn = symbolicLocation(it, params.position) + val isSortId = tn.parentSequence().any { it is JavaKeYParser.SortIdContext } + val v = KeyCatchSymbols() + val symbols = it.accept(v)?.filter { it.name == tn.symbol.text } ?: listOf() + Either.forLeft(symbols.map { Location(params.textDocument.uri, it.selectionRange) }) + } +// endregion + + //region Actions + override fun codeAction(params: CodeActionParams): CompletableFuture>> = + get(params.textDocument.uri) + .thenApplyAsync { it.accept(CodeActionVisitor(params.range)) ?: listOf() } + .thenApply>> { it.map { it: Command -> Either.forLeft(it) } } + .exceptionally { + listOf() + } + + override fun codeLens(params: CodeLensParams): CompletableFuture> = + get(params.textDocument.uri).thenApplyAsync { it.accept(CodeLensVisitor(params)) ?: listOf() } +//endregion + + //region Selection Range + override fun selectionRange(params: SelectionRangeParams): CompletableFuture> = + get(params.textDocument.uri) + .thenApplyAsync { + params.positions.map { pos -> + try { + symbolicLocation(it, pos) + } catch (e: IllegalStateException) { + null + } + } + .map { tn -> buildChangeSelectionChain(tn) } + } + + fun buildChangeSelectionChain(x: TerminalNode?): SelectionRange = + if (x == null) { + SelectionRange() + } else { + val parents = x.parentSequence().toList().foldRight(null as SelectionRange?) { tree, acc -> + val range = (tree as ParserRuleContext).asRange + if (range == acc?.range) { + acc + } else { + SelectionRange(range, acc) + } + } + SelectionRange(x.symbol.asRange, parents) + } +//endregion + + //region Semantic Tokens + override fun semanticTokensFull(params: SemanticTokensParams): CompletableFuture = + supplyAsync { params.textDocument.uri.toPath().readText() } + .thenApplyAsync { KeyDocumentHighlighter().analyzeToken(it) } + + override fun semanticTokensRange(params: SemanticTokensRangeParams): CompletableFuture = + supplyAsync { (params.textDocument.uri).toPath().readText().substring(params.range.start, params.range.end) } + .thenApplyAsync { KeyDocumentHighlighter().analyzeToken(it) } +//endregion + + //region Completion + override fun completion(params: CompletionParams): CompletableFuture, CompletionList>> = + supplyAsync { params.textDocument.uri.toPath().readText() } + .thenApply, CompletionList>> { + var prefix = "" + val index = it.indexOf(params.position) + if (index >= 0) { + val delim = max(index, it.lastIndexOfAny(" \n\t".toCharArray(), index)) + prefix = it.substring(delim, index) + } + Either.forLeft( + getEscapeKeywords(prefix) + usedIdentifier(prefix, params.textDocument.uri) + ) + } + .exceptionally { + LOGGER.warn("Error computing completions", it) + Either.forLeft(listOf()) + } + + private fun usedIdentifier(prefix: String, uri: String): List = + ParsingFacade.createLexer(uri.toPath()).asSequence() + .filter { it.type == JavaKeYLexer.IDENT } + .map { it.text } + .filter { it.startsWith(prefix) } + .toSortedSet() + .map { CompletionItem(it).also { it.kind = CompletionItemKind.Variable } } + .toList() + + private fun getEscapeKeywords(prefix: String): List = + (0..JavaKeYLexer.VOCABULARY.maxTokenType).asSequence() + .mapNotNull { JavaKeYLexer.VOCABULARY.getLiteralName(it) } + .filter { it.startsWith(prefix) } + .map { it.trim('\'') } + .toSortedSet() + .map { CompletionItem(it).also { it.kind = CompletionItemKind.Keyword } } + //endregion + + //region Format + override fun formatting(params: DocumentFormattingParams): CompletableFuture> { + val path = params.textDocument.uri.toPath() + return supplyAsync { Formatter().format(path) } + .thenApplyAsync { + val original = path.readText() + listOf(TextEdit(Range(Position(0, 0), original.findLastPosition()), it)) + } + } + + override fun rangeFormatting(params: DocumentRangeFormattingParams) = supplyAsync { + val path = params.textDocument.uri.toPath() + val original = path.readText() + val section = original.substring(params.range) + val it = Formatter().format(section) + listOf(TextEdit(params.range, it)) + } + + override fun rangesFormatting(params: DocumentRangesFormattingParams): CompletableFuture> = + supplyAsync { + val path = params.textDocument.uri.toPath() + val original = path.readText() + params.ranges.map { r -> + val section = original.substring(r) + val it = Formatter().format(section) + TextEdit(r, it) + } + } +//endregion + + //region documentLink + override fun documentLink(params: DocumentLinkParams): CompletableFuture> = + get(params.textDocument.uri) + .thenApply { file -> + val base = params.textDocument.uri.toPath() + file.decls().one_include_statement().flatMap { include -> + include.one_include().map { + var s = it.text.trim('"') + if (!s.endsWith(".key")) s += ".key" + val path = base.parent.resolve(s) + DocumentLink(it.asRange, path.asUri) + } + } + } +//endregion + + + override fun documentHighlight(params: DocumentHighlightParams): CompletableFuture> = + CompletableFuture.completedFuture(listOf()) +} + +private fun JavaKeYLexer.asSequence(): Sequence { + return sequence { + var token: Token + do { + token = nextToken() + yield(token) + } while (token.type != JavaKeYLexer.EOF) + } +} + +internal fun SyntaxErrorReporter.ParserException.toDiagnostics(): List = errors.map { + Diagnostic( + it.location.toRange, + it.message, + DiagnosticSeverity.Error, + "KeY-Parser" + ) +} + +private fun ParseCancellationException.toDiagnostics(): List = listOf( + Diagnostic( + Range(Position(0, 0), Position(0, 0)), // TODO + message ?: (" " + this), + DiagnosticSeverity.Error, + "KeY-Parser" + ) +) + + +internal fun String.substring(range: Range) = substring(range.start, range.end) + +internal fun String.findLastPosition(): Position { + val line = count { it == '\n' } + val column = if (line == 0) { + length + } else { + length - lastIndexOf('\n') + } + return Position(line, column) +} + +internal fun String.indexOf(position: Position): Int { + var currentLine = 0 + for ((index, ch) in withIndex()) { + if (ch == '\n') currentLine++ + if (position.line == currentLine) { + return index + position.character + } + } + return -1 +} + +fun String.toPath(): Path = if (startsWith("jar:file:")) { + IOUtil.openFileInJar(URI.create(this)) +} else { + Paths.get(this.replace("file://", "")) +} + +internal fun String.substring(startIndex: Position, endIndex: Position): String { + var start: Int = -1 + var end: Int = -1 + var currentLine = 0 + for ((index, ch) in this.withIndex()) { + if (ch == '\n') currentLine++ + if (startIndex.line == currentLine) { + start = index + startIndex.character + } + if (endIndex.line == currentLine) { + end = index + endIndex.character + } + if (start != -1 && end != -1) break + } + return substring(min(start, end), max(start, end)) +} + +internal operator fun ParseTree.contains(position: Position): Boolean = + when (this) { + is ParserRuleContext -> start <= position && position <= stop + is TerminalNode -> symbol <= position && position <= symbol + else -> false + } + +internal operator fun Pair.compareTo(o: Pair): Int { + val (a, b) = this + val (x, y) = o + + val q = a - x + if (q != 0) { + return q + } + return b - y +} + +internal operator fun Token.compareTo(position: Position): Int = + (line to charPositionInLine).compareTo(position.line to position.character) + +internal operator fun Position.compareTo(tok: Token): Int { + val x = line - tok.line + if (x != 0) return x + return character - tok.charPositionInLine +} \ No newline at end of file diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyWorkspaceService.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyWorkspaceService.kt new file mode 100644 index 0000000000..8aee5faab7 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/services/KeyWorkspaceService.kt @@ -0,0 +1,110 @@ +package org.key_project.key.lsp.services + +import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter +import org.key_project.key.lsp.KeyLanguageServer +import org.eclipse.lsp4j.* +import org.eclipse.lsp4j.jsonrpc.messages.Either +import org.eclipse.lsp4j.services.WorkspaceService +import org.key_project.key.lsp.LOGGER +import org.key_project.key.lsp.symbols.KeyCatchSymbols +import org.key_project.util.java.IOUtil +import java.nio.file.FileSystems +import java.nio.file.Path +import java.util.concurrent.CompletableFuture +import kotlin.io.path.absolutePathString +import kotlin.io.path.extension +import kotlin.io.path.readText +import kotlin.io.path.walk + +val Path.asUri: String + get() { + if (FileSystems.getDefault() != this.fileSystem) { + return toUri().toString() + } + return "file://${this.absolutePathString()}" + } + +class KeyWorkspaceService(val server: KeyLanguageServer) : WorkspaceService { + val addKeyStandardFiles = true + internal val keyStandardFiles by lazy { + if (addKeyStandardFiles) { + val uri = javaClass.getResource("/de/uka/ilkd/key/proof/rules/ldt.key")!!.toURI() + val folder = IOUtil.openFileInJar(uri).parent + folder.walk().filter { it.extension == "key" } + } else { + emptySequence() + } + } + + override fun didChangeConfiguration(params: DidChangeConfigurationParams) {} + override fun didChangeWatchedFiles(params: DidChangeWatchedFilesParams) {} + + override fun textDocumentContent(params: TextDocumentContentParams): CompletableFuture = + CompletableFuture.supplyAsync { + TextDocumentContentResult(params.uri.toPath().readText()) + }.exceptionally { + LOGGER.error("Error reading file: {}", params.uri.toPath().toUri(), it ) + throw it + } + + override fun diagnostic(params: WorkspaceDiagnosticParams): CompletableFuture = + findKeyFiles().thenApplyAsync { it.map { parse(it) } } + .thenApplyAsync { it.map { WorkspaceDocumentDiagnosticReport(it.get()) } } + .thenApply { WorkspaceDiagnosticReport(it.toList()) } + + var version: Int = 0 + private fun parse(path: Path) = + server.keyTextDocumentService.get(path.asUri) + .thenApply { + WorkspaceFullDocumentDiagnosticReport(listOf(), path.asUri, version++) + }.exceptionally { e -> + var items = mutableListOf() + if (e is SyntaxErrorReporter.ParserException) { + items = e.errors.map { + Diagnostic( + it.location.toRange, + it.message, + DiagnosticSeverity.Error, + "KeY-Parser" + ) + }.toMutableList() + } + WorkspaceFullDocumentDiagnosticReport(items, path.asUri, version++) + } + + override fun executeCommand(params: ExecuteCommandParams): CompletableFuture = + CompletableFuture.supplyAsync { + val action = server.actions.firstOrNull { it.id == params.command } + action?.execute(params) + } + + override fun resolveWorkspaceSymbol(workspaceSymbol: WorkspaceSymbol): CompletableFuture = + CompletableFuture.completedFuture(workspaceSymbol) + + override fun symbol(params: WorkspaceSymbolParams): CompletableFuture, List>> = + findKeyFiles() + .thenApplyAsync { it.map { getSymbol(it) } } + .thenApplyAsync { seq -> seq.flatMap { it.get() }.toList() } + .thenApply { Either.forRight(it) } + + private fun getSymbol(path: Path) = + server.keyTextDocumentService.get(path.asUri) + .thenApplyAsync { + val uri = path.asUri + val v = KeyCatchSymbols() + val symbols = it.accept(v) + symbols?.map { + WorkspaceSymbol( + it.name, it.kind, Either.forLeft(Location(uri, it.range)), + ) + } ?: listOf() + } + + private fun findKeyFiles(): CompletableFuture> = + CompletableFuture.supplyAsync { + keyStandardFiles + + (server.initParams.workspaceFolders?.asSequence() ?: emptySequence()) + .map { it.uri.toPath() } + .flatMap { it.walk().filter { it.extension == "key" } } + } +} diff --git a/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/symbols/KeyCatchSymbols.kt b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/symbols/KeyCatchSymbols.kt new file mode 100644 index 0000000000..4f8925c3e5 --- /dev/null +++ b/keyext.lsp/src/main/kotlin/org/key_project/key/lsp/symbols/KeyCatchSymbols.kt @@ -0,0 +1,189 @@ +/* This file is part of jmltoolkit project - https://github.com/jmltoolkit + * jmltk is licensed under the Lesser GNU General Public License Version 2 and Apache License + * SPDX-License-Identifier: LGPL-3.0-or-later Apache-2.0 + */ +package org.key_project.key.lsp.symbols + +import de.uka.ilkd.key.nparser.JavaKeYParser +import de.uka.ilkd.key.nparser.JavaKeYParserBaseVisitor +import org.antlr.v4.runtime.ParserRuleContext +import org.antlr.v4.runtime.Token +import org.antlr.v4.runtime.tree.ParseTree +import org.eclipse.lsp4j.* + +internal val Token.asRange: Range + get() = Range(asStartPosition, asStopPosition) + +internal val Token.asStopPosition: Position + get() = Position(line - 1, charPositionInLine + startIndex - stopIndex) + + +internal val Token.asStartPosition: Position + get() = Position(line - 1, charPositionInLine) + +internal val ParserRuleContext.asRange: Range + get() = Range(start.asStartPosition, stop.asStopPosition) + +/** + * + * @author Alexander Weigl + * @version 1 (04.02.24) + */ +class KeyCatchSymbols : JavaKeYParserBaseVisitor?>() { + val declaredFunctions = mutableListOf() + + override fun visitFile(ctx: JavaKeYParser.FileContext): List = acceptAll(ctx.children) + + @JvmName("acceptAllPt") + private fun acceptAll(children: List?): List = + children?.filterIsInstance()?.flatMap { it.accept(this) ?: listOf() }?.toMutableList() + ?: listOf() + + private fun acceptAll(children: List): MutableList = + children.flatMap { it.accept(this) ?: listOf() }.toMutableList() + + override fun visitDecls(ctx: JavaKeYParser.DeclsContext): List = acceptAll(ctx.children) + + override fun visitSort_decls(ctx: JavaKeYParser.Sort_declsContext) = listOf( + DocumentSymbol( + "Sorts", SymbolKind.Namespace, ctx.asRange, + ctx.SORTS().symbol.asRange, + null, + acceptAll(ctx.one_sort_decl()) + ) + ) + + override fun visitOne_sort_decl(ctx: JavaKeYParser.One_sort_declContext): List = + ctx.sortIds?.simple_ident_dots_with_docs()?.flatMap { + symbol(it.text, SymbolKind.Class, it.asRange, it.asRange, ctx.doc?.text) + } ?: listOf() + + + override fun visitSchema_var_decls(ctx: JavaKeYParser.Schema_var_declsContext) = listOf( + DocumentSymbol( + "Schema Variables", SymbolKind.Namespace, ctx.asRange, + ctx.SCHEMAVARIABLES().symbol.asRange, + null, + acceptAll(ctx.one_schema_var_decl()) + ) + ) + + override fun visitOne_schema_var_decl(ctx: JavaKeYParser.One_schema_var_declContext): List = + ctx.simple_ident().map { + DocumentSymbol( + it.text, SymbolKind.Variable, it.asRange, it.asRange, + ctx.schema_modifiers().text + ) + } + + + private fun symbol( + name: String, + kind: SymbolKind, + range: Range, + selectionRange: Range, + detail: String? = null, + children: MutableList? = null + ): List = listOf( + DocumentSymbol(name, kind, range, selectionRange, detail, children) + ) + + override fun visitPreferences(ctx: JavaKeYParser.PreferencesContext): List = + symbol("Preferences", SymbolKind.String, ctx.KEYSETTINGS().symbol.asRange, ctx.asRange, ctx.text) + + override fun visitFunc_decls(ctx: JavaKeYParser.Func_declsContext): List = symbol( + "Functions", SymbolKind.Namespace, + ctx.asRange, + ctx.start.asRange, + null, + acceptAll(ctx.func_decl()) + ) + + override fun visitFunc_decl(ctx: JavaKeYParser.Func_declContext): List { + declaredFunctions.add(FunctionSignature.from(ctx)) + return symbol( + ctx.func_name.name.text, SymbolKind.Function, ctx.asRange, ctx.func_name.asRange, + "(${ctx.argSorts.sortId().joinToString(", ") { it.text }}) -> ${ctx.sortId().text}" + ) + } + + override fun visitRulesOrAxioms(ctx: JavaKeYParser.RulesOrAxiomsContext) = symbol( + (if (ctx.RULES() != null) "Rules" else "Axioms") + " ${ctx.choices?.text ?: ""}", + SymbolKind.Namespace, ctx.start.asRange, ctx.asRange, ctx.doc?.text, + acceptAll(ctx.taclet()) + ) + + override fun visitTaclet(ctx: JavaKeYParser.TacletContext) = + symbol("${ctx.name.text}", SymbolKind.Class, ctx.start.asRange, ctx.asRange, ctx.doc?.text) + + + override fun visitDatatype_decls(ctx: JavaKeYParser.Datatype_declsContext) = symbol( + "Datatypes", SymbolKind.Namespace, + ctx.asRange, + ctx.start.asRange, + null, + acceptAll(ctx.datatype_decl()) + ) + + override fun visitDatatype_decl(ctx: JavaKeYParser.Datatype_declContext) = symbol( + ctx.name.text, SymbolKind.Struct, ctx.asRange, ctx.name.asRange, + ctx.DOC_COMMENT()?.text?.substringBefore('\n') ?: "${ctx.datatype_constructor().size} constructors", + acceptAll(ctx.datatype_constructor()) + ) + + override fun visitDatatype_constructor(ctx: JavaKeYParser.Datatype_constructorContext): List = + symbol( + ctx.name.text, SymbolKind.Function, ctx.asRange, ctx.name.asRange, + "(${ctx.argSort.zip(ctx.argName).joinToString(", ") { (s, n) -> "${n.text}: ${s.text}" }})" + ) + + override fun visitOneProgramSource(ctx: JavaKeYParser.OneProgramSourceContext?): List? { + return super.visitOneProgramSource(ctx) + } + + override fun visitClassPaths(ctx: JavaKeYParser.ClassPathsContext) = + symbol("Classpath", SymbolKind.String, ctx.asRange, ctx.asRange, ctx.text) + + override fun visitBootClassPath(ctx: JavaKeYParser.BootClassPathContext) = + symbol("Boot Classpath", SymbolKind.String, ctx.asRange, ctx.asRange, ctx.text) + + override fun visitProgramSource(ctx: JavaKeYParser.ProgramSourceContext) = + symbol("Program Source", SymbolKind.String, ctx.asRange, ctx.asRange, ctx.text) + + + override fun visitProblem(ctx: JavaKeYParser.ProblemContext) = + symbol("Problem", SymbolKind.String, ctx.asRange, ctx.asRange, ctx.text) + + + override fun visitProfile(ctx: JavaKeYParser.ProfileContext) = + symbol("Profile", SymbolKind.String, ctx.asRange, ctx.asRange, ctx.text) + + override fun visitProofScriptEntry(ctx: JavaKeYParser.ProofScriptEntryContext) = + symbol("Proof Script", SymbolKind.String, ctx.asRange, ctx.asRange, ctx.text) + + + override fun visitProof(ctx: JavaKeYParser.ProofContext) = + symbol("Proof", SymbolKind.String, ctx.PROOF().symbol.asRange, ctx.asRange, ctx.text) +} + +data class FunctionSignature( + val name: String, + val documentation: String, + val sortArgs: List, + val args: List +) { + companion object { + fun from(ctx: JavaKeYParser.Func_declContext): FunctionSignature { + val sortArgs = ctx.formal_sort_param_decls() + ?.formal_sort_param_decl() + ?.map { ParameterInformation(it.simple_ident().text) } + ?: listOf() + val args = ctx.argSorts.sortId().map { ParameterInformation(it.text) } + return FunctionSignature( + ctx.func_name.name.text, + ctx.DOC_COMMENT()?.text ?: "", + sortArgs, args + ) + } + } +} diff --git a/keyext.lsp/src/main/resources/META-INF/services/org.key_project.key.lsp.actions.LspAction b/keyext.lsp/src/main/resources/META-INF/services/org.key_project.key.lsp.actions.LspAction new file mode 100644 index 0000000000..e057d4fc86 --- /dev/null +++ b/keyext.lsp/src/main/resources/META-INF/services/org.key_project.key.lsp.actions.LspAction @@ -0,0 +1 @@ +org.key_project.key.lsp.actions.StartKey \ No newline at end of file diff --git a/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/FormatterTest.kt b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/FormatterTest.kt new file mode 100644 index 0000000000..476800416b --- /dev/null +++ b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/FormatterTest.kt @@ -0,0 +1,31 @@ +package org.key_project.key.lsp + +import org.assertj.core.api.Assertions +import org.junit.jupiter.api.DynamicTest +import org.junit.jupiter.api.TestFactory +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.io.path.extension +import kotlin.io.path.readText +import kotlin.io.path.walk + +/** + * + * @author Alexander Weigl + * @version 1 (29.08.26) + */ +class FormatterTest { + @TestFactory + fun formatWorkspace(): Sequence { + return Paths.get("workspace").walk() + .filter { it.extension == "key" } + .map { DynamicTest.dynamicTest("$it") { formatPath(it) } } + } + + private fun formatPath(it: Path) { + val doc = Formatter().format(it) + val x = it.readText() + Assertions.assertThat(doc).isEqualTo(x) + } + +} \ No newline at end of file diff --git a/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/actions/StartKeyTest.kt b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/actions/StartKeyTest.kt new file mode 100644 index 0000000000..6b2c292d62 --- /dev/null +++ b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/actions/StartKeyTest.kt @@ -0,0 +1,25 @@ +package org.key_project.key.lsp.actions + +import org.eclipse.lsp4j.ExecuteCommandParams +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Test +import org.key_project.key.lsp.services.createServer + +/** + * + * @author Alexander Weigl + * @version 1 (29.08.26) + */ +class StartKeyTest { + @Test + @Disabled + fun test() { + val x = createServer() + x.workspaceService.executeCommand( + ExecuteCommandParams( + "org.key_project.key.lsp.actions.StartKey", + listOf("file:///home/weigl/work/key-rpc/keyext.lsp/workspace/complex.key") + ) + ).get() + } +} \ No newline at end of file diff --git a/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/services/KeyTextDocumentServiceTest.kt b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/services/KeyTextDocumentServiceTest.kt new file mode 100644 index 0000000000..60d4f2792f --- /dev/null +++ b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/services/KeyTextDocumentServiceTest.kt @@ -0,0 +1,287 @@ +package org.key_project.key.lsp.services + +import de.uka.ilkd.key.nparser.JavaKeYParser +import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter +import org.eclipse.lsp4j.* +import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.Test +import org.key_project.key.lsp.KeyLanguageServer +import org.key_project.key.lsp.highlighting.KeyDocumentHighlighter +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.Paths +import kotlin.io.path.absolute +import kotlin.io.path.readText + +val workspace = Paths.get("workspace").absolute() + +fun createServer(): KeyLanguageServer { + val server = KeyLanguageServer() + server.initialize( + InitializeParams().also { + it.workspaceFolders = listOf() + it.rootUri = "file:///tmp" + it.rootPath = "/tmp" + } + ) + return server +} + +class KeyTextDocumentServiceTest { + + /** + * Gets a file from the test workspace resources. + * Files are located in src/test/resources/workspace/ + */ + private fun getWorkspaceFile(path: String): Path = workspace.resolve(path) + + + // region File Management Tests + @Test + fun `test load valid key file`() { + val server = createServer() + val file = getWorkspaceFile("valid_complete.key") + + val ctx = server.keyTextDocumentService.get(file.asUri).get() + assertNotNull(ctx) + assertTrue(ctx is JavaKeYParser.FileContext) + } + + @Test + fun `test load invalid key file throws exception`() { + val server = createServer() + val file = getWorkspaceFile("diagnostics/invalid_missing_brace.key") + + assertThrows(SyntaxErrorReporter.ParserException::class.java) { + server.keyTextDocumentService.getSync(file.asUri) + } + } + + @Test + fun `test file cache stores parsed files`() { + val server = createServer() + val file = getWorkspaceFile("cache/cachable.key") + + val uri = file.asUri + assertFalse(uri in server.keyTextDocumentService.fileCache) + + server.keyTextDocumentService.getSync(uri) + + assertTrue(uri in server.keyTextDocumentService.fileCache) + } + + @Test + fun `test didOpen loads file into cache`() { + val server = createServer() + val file = getWorkspaceFile("lifecycle/single_sort.key") + + val params = DidOpenTextDocumentParams( + TextDocumentItem( + file.asUri, + "key", + 1, + Files.readString(file) + ) + ) + + server.keyTextDocumentService.didOpen(params) + + assertTrue(file.asUri in server.keyTextDocumentService.fileCache) + } + + @Test + fun `test didChange invalidates cache`() { + val server = createServer() + val file = getWorkspaceFile("lifecycle/single_sort.key") + + val uri = file.asUri + server.keyTextDocumentService.getSync(uri) + assertTrue(uri in server.keyTextDocumentService.fileCache) + + val params = DidChangeTextDocumentParams( + VersionedTextDocumentIdentifier(uri, 2), + listOf(TextDocumentContentChangeEvent("changed content")) + ) + + server.keyTextDocumentService.didChange(params) + + assertFalse(uri in server.keyTextDocumentService.fileCache) + } + // endregion + + // region Document Symbol Tests + @Test + fun `test document symbol extraction`() { + val server = createServer() + val file = getWorkspaceFile("symbols/full_example.key") + + val params = DocumentSymbolParams(TextDocumentIdentifier(file.asUri)) + val symbols = server.keyTextDocumentService.documentSymbol(params).get() + + assertNotNull(symbols) + assertTrue(symbols.isNotEmpty()) + } + + @Test + fun `test document symbol contains sorts`() { + val server = createServer() + val file = getWorkspaceFile("symbols/three_sorts.key") + + val params = DocumentSymbolParams(TextDocumentIdentifier(file.asUri)) + val symbols = server.keyTextDocumentService.documentSymbol(params).get() + + assertNotNull(symbols) + assertTrue(symbols.isNotEmpty()) + } + + @Test + fun `test document symbol contains functions`() { + val server = createServer() + val file = getWorkspaceFile("symbols/three_functions.key") + + val params = DocumentSymbolParams(TextDocumentIdentifier(file.asUri)) + val symbols = server.keyTextDocumentService.documentSymbol(params).get() + + assertNotNull(symbols) + assertTrue(symbols.isNotEmpty()) + } + // endregion + + // region Semantic Highlighting Tests + @Test + fun `test semantic highlighting returns tokens`() { + val server = createServer() + val file = getWorkspaceFile("highlighting/basic.key") + + val params = SemanticTokensParams(TextDocumentIdentifier(file.asUri)) + val tokens = server.keyTextDocumentService.semanticTokensFull(params).get() + + assertNotNull(tokens) + assertNotNull(tokens.data) + } + + @Test + fun `test semantic highlighting identifies keywords`() { + val text = getWorkspaceFile("highlighting/keywords.key").readText() + val highlighter = KeyDocumentHighlighter() + val tokens = highlighter.analyzeToken(text) + + assertNotNull(tokens) + assertTrue(tokens.data.isNotEmpty()) + } + + @Test + fun `test semantic highlighting identifies comments`() { + val text = getWorkspaceFile("highlighting/comments.key").readText() + val highlighter = KeyDocumentHighlighter() + val tokens = highlighter.analyzeToken(text) + + assertNotNull(tokens) + assertTrue(tokens.data.isNotEmpty()) + } + + @Test + fun `test semantic highlighting identifies numbers`() { + val text = getWorkspaceFile("highlighting/numbers.key").readText() + val highlighter = KeyDocumentHighlighter() + val tokens = highlighter.analyzeToken(text) + + assertNotNull(tokens) + assertTrue(tokens.data.isNotEmpty()) + } + + @Test + fun `test semantic highlighting identifies operators`() { + val text = Files.readString(getWorkspaceFile("highlighting/operators.key")) + val highlighter = KeyDocumentHighlighter() + val tokens = highlighter.analyzeToken(text) + + assertNotNull(tokens) + assertTrue(tokens.data.isNotEmpty()) + } + // endregion + + // region Folding Range Tests + @Test + fun `test folding range extraction`() { + val server = createServer() + val file = getWorkspaceFile("folding/nested.key") + + val params = FoldingRangeRequestParams(TextDocumentIdentifier(file.asUri)) + val ranges = server.keyTextDocumentService.foldingRange(params).get() + + assertNotNull(ranges) + assertTrue(ranges.isNotEmpty()) + } + // endregion + + // region Completion Tests + @Test + fun `test completion returns keyword suggestions`() { + val server = createServer() + val file = getWorkspaceFile("completion/basic.key") + + val params = CompletionParams( + TextDocumentIdentifier(file.asUri), + Position(0, 0) + ) + val result = server.keyTextDocumentService.completion(params).get() + + assertNotNull(result) + val items = result.left + assertNotNull(items) + assertTrue(items.isNotEmpty()) + } + // endregion + + // region Diagnostic Tests + @Test + fun `test diagnostic captures syntax errors`() { + val server = createServer() + val file = getWorkspaceFile("diagnostics/invalid_missing_brace.key") + + val params = DocumentDiagnosticParams(TextDocumentIdentifier(file.asUri)) + val report = server.keyTextDocumentService.diagnostic(params).get() + + assertNotNull(report) + } + + @Test + fun `test diagnostic empty for valid file`() { + val server = createServer() + val file = getWorkspaceFile("diagnostics/valid.key") + + val params = DocumentDiagnosticParams(TextDocumentIdentifier(file.asUri)) + val report = server.keyTextDocumentService.diagnostic(params).get() + + assertNotNull(report) + } + // endregion + + + @Test + fun testCodeLens() { + val server = createServer() + val file = getWorkspaceFile("complex.key") + val params = CodeLensParams(TextDocumentIdentifier(file.asUri)) + val report = server.keyTextDocumentService.codeLens(params).get() + println(report) + assertNotNull(report) + assertTrue(report.isNotEmpty()) + } + + @Test + fun testDocumentSymbol() { + val server = createServer() + val file = getWorkspaceFile("complex.key") + val params = DocumentSymbolParams(TextDocumentIdentifier(file.asUri)) + val report = server.keyTextDocumentService.documentSymbol(params).get() + println(report) + assertNotNull(report) + assertTrue(report.isNotEmpty()) + } +} + +// Extension property for URI conversion +val Path.asUri: String + get() = "file://${this.toAbsolutePath()}" diff --git a/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/services/KeyWorkspaceServiceTest.kt b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/services/KeyWorkspaceServiceTest.kt new file mode 100644 index 0000000000..254565a9d8 --- /dev/null +++ b/keyext.lsp/src/test/kotlin/org/key_project/key/lsp/services/KeyWorkspaceServiceTest.kt @@ -0,0 +1,29 @@ +package org.key_project.key.lsp.services + +import org.key_project.key.lsp.KeyLanguageServer +import org.eclipse.lsp4j.InitializeParams +import org.eclipse.lsp4j.WorkspaceSymbolParams +import org.junit.jupiter.api.Assertions +import org.junit.jupiter.api.Test + +class KeyWorkspaceServiceTest { + @Test + fun findKeyFiles() { + val files = KeyLanguageServer().keyWorkspaceService.keyStandardFiles.toList() + Assertions.assertTrue(files.isNotEmpty()) + } + + @Test + fun symbols() { + val server = KeyLanguageServer() + server.initialize( + InitializeParams().also { + it.workspaceFolders = listOf() + it.rootUri = "file:///tmp" + it.rootPath = "/tmp" + } + ) + val files = server.keyWorkspaceService.symbol(WorkspaceSymbolParams("")) + println(files.get().right.size) + } +} diff --git a/keyext.lsp/src/test/resources/workspace/complex.key b/keyext.lsp/src/test/resources/workspace/complex.key new file mode 100644 index 0000000000..6fe198e7bd --- /dev/null +++ b/keyext.lsp/src/test/resources/workspace/complex.key @@ -0,0 +1,29 @@ +\datatypes{ + struct Node { + int value; + Node next; + } +} + +\functions{ + Node createNode(int v); + int getValue(Node n); +} + +\predicates{ + bool isSorted(Node head); + bool contains(Node head, int val); +} + +\axioms{ + \forall int v; + getValue(createNode(v)) = v; + + \forall Node n, int v; + n != null --> getValue(n) >= 0; +} + +\problem{ + \forall Node head, int val; + isSorted(head) && contains(head, val) --> val >= 0 +} diff --git a/keyext.lsp/src/test/resources/workspace/grouping.key b/keyext.lsp/src/test/resources/workspace/grouping.key new file mode 100644 index 0000000000..e486ab991b --- /dev/null +++ b/keyext.lsp/src/test/resources/workspace/grouping.key @@ -0,0 +1,7 @@ +// Test file for grouping symbols +(a + b) * c +{x; y; z} +[arr[0], arr[1], arr[2]] +T +{(a + b) * [c, d]} +f(g(h(x))) diff --git a/keyext.lsp/src/test/resources/workspace/literals.key b/keyext.lsp/src/test/resources/workspace/literals.key new file mode 100644 index 0000000000..52334a0056 --- /dev/null +++ b/keyext.lsp/src/test/resources/workspace/literals.key @@ -0,0 +1,9 @@ +// Test file for literal formatting +int i = 42; +double d = 3.14159; +float f = 2.5f; +real r = 1.5r; +char c = 'a'; +String s = "hello world"; +binary bin = 0b1010; +hex hex = 0xFF; diff --git a/keyext.lsp/src/test/resources/workspace/operators.key b/keyext.lsp/src/test/resources/workspace/operators.key new file mode 100644 index 0000000000..6fe55e7d19 --- /dev/null +++ b/keyext.lsp/src/test/resources/workspace/operators.key @@ -0,0 +1,8 @@ +// Test file for operator formatting +a + b - c * d / e % f +x ** y + ~z +p && q || !r +a = b != c +x < y > z <= w >= v +alpha --> beta +phi <-> psi diff --git a/keyext.lsp/src/test/resources/workspace/simple.key b/keyext.lsp/src/test/resources/workspace/simple.key new file mode 100644 index 0000000000..1d82a3f34a --- /dev/null +++ b/keyext.lsp/src/test/resources/workspace/simple.key @@ -0,0 +1,7 @@ +\functions{ + int f(int); +} + +\problem{ + \forall int x; f(x) = x +} diff --git a/keyext.lsp/src/test/resources/workspace/unicode.key b/keyext.lsp/src/test/resources/workspace/unicode.key new file mode 100644 index 0000000000..31374ccaf2 --- /dev/null +++ b/keyext.lsp/src/test/resources/workspace/unicode.key @@ -0,0 +1,6 @@ +// Test file with unicode and special characters +∀x; ∃y; P(x, y) +α + β = γ +A ⊆ B ∪ C +x ≤ y ≥ z +// Grüße an alle diff --git a/keyext.lsp/workspace/README.md b/keyext.lsp/workspace/README.md new file mode 100644 index 0000000000..a546f1b9db --- /dev/null +++ b/keyext.lsp/workspace/README.md @@ -0,0 +1,71 @@ +# KeY Language Server Test Workspace + +This directory contains sample `.key` files used for testing the KeY Language Server. + +## Files + +### simple.key +A basic KeY file with minimal declarations including: +- Sort declarations +- Function declarations +- Simple program +- Basic axioms + +### complex.key +A more comprehensive KeY file demonstrating: +- Multiple sort declarations +- Various function types (arithmetic, list operations, tree operations) +- Complete Java-like program +- Multiple axiom categories +- Rule declarations + +### syntax_error.key +Intentionally malformed KeY file for testing error handling: +- Missing closing braces +- Incomplete function declarations +- Invalid syntax + +### program.key +KeY file with Java program verification example: +- Counter class with methods +- Main class with example usage +- Associated functions and axioms + +## Usage + +These files are automatically copied to the test temporary directory during test execution. +Tests use JUnit's `@TempDir` annotation to create isolated test environments. + +## Creating Additional Test Files + +When adding new test cases, create corresponding `.key` files here following these guidelines: + +1. **Keep files focused** - Each file should test a specific feature or scenario +2. **Include comments** - Document what the file is testing +3. **Use meaningful names** - File names should indicate their purpose +4. **Validate syntax** - Ensure valid `.key` files parse correctly in KeY + +## File Structure Example + +```key +// Comment describing the file's purpose +\sorts { + // Sort declarations +} + +\functions { + // Function declarations +} + +\program { + // Program code (optional) +} + +\axioms { + // Axiom declarations +} + +\rules { + // Rule declarations (optional) +} +``` diff --git a/keyext.lsp/workspace/cache/cachable.key b/keyext.lsp/workspace/cache/cachable.key new file mode 100644 index 0000000000..7c92907af0 --- /dev/null +++ b/keyext.lsp/workspace/cache/cachable.key @@ -0,0 +1,3 @@ +// Test fixture: File for cache storage tests +\sorts { Integer; MyType; } +\functions { int f(int); } diff --git a/keyext.lsp/workspace/completion/basic.key b/keyext.lsp/workspace/completion/basic.key new file mode 100644 index 0000000000..e270714796 --- /dev/null +++ b/keyext.lsp/workspace/completion/basic.key @@ -0,0 +1,2 @@ +// Test fixture: Basic file for completion tests +\sorts { Integer; } diff --git a/keyext.lsp/workspace/complex.key b/keyext.lsp/workspace/complex.key new file mode 100644 index 0000000000..fe2f7ea2d3 --- /dev/null +++ b/keyext.lsp/workspace/complex.key @@ -0,0 +1,53 @@ +// Complex KeY file with multiple declarations + +// \include "test.key"; + +\sorts { + Integer; + Real; + Object; + MyList; + MyTree; +} + +\datatypes { + Colors = Red | Yellow | Blue | Green; +} + +\functions { + // Arithmetic functions + int add(int, int); + int mult(int, int); + Real sqrt(Real); + + // List functions + MyList empty; + // MyList cons(Object, MyList); + Object head(MyList); + MyList tail(MyList); + int length(MyList); + + // Tree functions + MyTree leaf(Object); + MyTree node(MyTree, MyTree); + Object getValue(MyTree); +} + +\axioms { + a { \forall int x; add(x, 0) = x } + b { \forall int x, int y; add(x, y) = add(y, x) } + + // Multiplication axioms + m1 { \forall int x; mult(x, 0) = 0 } + m2 { \forall int x; mult(x, 1) = x } + + // List axioms + l1 { \forall Object o, MyList l; head(cons(o, l)) = o } + l2 { \forall Object o, MyList l; tail(cons(o, l)) = l } + l3 { length(empty()) = 0 } +} + +// Simplification rules +\problem { + (add(x, 0) = x) ==> add(x, 0) = x +} diff --git a/keyext.lsp/workspace/diagnostics/invalid_missing_brace.key b/keyext.lsp/workspace/diagnostics/invalid_missing_brace.key new file mode 100644 index 0000000000..7f106e4ec3 --- /dev/null +++ b/keyext.lsp/workspace/diagnostics/invalid_missing_brace.key @@ -0,0 +1,5 @@ +// Test fixture: Invalid KeY file with missing closing brace +// Used to test syntax error detection +\sorts { + Integer; + // Missing closing brace - intentional syntax error diff --git a/keyext.lsp/workspace/diagnostics/valid.key b/keyext.lsp/workspace/diagnostics/valid.key new file mode 100644 index 0000000000..9ef36bb39b --- /dev/null +++ b/keyext.lsp/workspace/diagnostics/valid.key @@ -0,0 +1,3 @@ +// Test fixture: Valid file for diagnostic tests (should have no errors) +\sorts { Integer; } +\functions { int f(int); } diff --git a/keyext.lsp/workspace/eglot.el b/keyext.lsp/workspace/eglot.el new file mode 100644 index 0000000000..4a1d994a98 --- /dev/null +++ b/keyext.lsp/workspace/eglot.el @@ -0,0 +1,56 @@ +;(require 'eglot) + +(setq path + "/home/weigl/work/key-rpc/keyext.lsp/build/install/keyext.lsp/bin/keyext.lsp") + ;(expand-file-name load-file-name)) + +(require 'cc-mode) +(define-derived-mode key-mode prog-mode "KEY" + "Major mode for editing KEY" + :syntax-table java-mode-syntax-table + (setq-local comment-start "//") + (setq-local comment-end "") + (setq-local indent-tabs-mode nil)) +(add-to-list 'auto-mode-alist '("\\.key\\'" . key-mode)) + +;(add-hook 'key-mode-hook 'eglot-ensure) +;(add-to-list 'eglot-server-programs +; `(key-mode ,path "--stdio")) + +(use-package lsp-mode + :ensure t + :init (setq lsp-keymap-prefix "C-c l") + :hook ((key-mode . lsp)) + :commands lsp + :config + + (add-to-list 'lsp-language-id-configuration '(key-mode . "key")) + + (lsp-register-client + (make-lsp-client + :new-connection (lsp-stdio-connection (list path "--stdio" "--trace" "-")) + :major-modes '(key-mode) + :server-id 'key-lsp))) + +(use-package lsp-ui :ensure t :commands lsp-ui-mode) +(setq lsp-print-io t) + +(use-package lsp-treemacs :ensure t) + + +(defun --key-hook () + (lsp) + (lsp-semantic-tokens-mode) + (lsp-ui-doc-enable t) + (lsp-modeline-diagnostics-mode) + (lsp-diagnostics-mode) + (lsp-modeline-code-actions-mode) + (lsp-modeline-workspace-status-mode) + (lsp-ui-sideline)) + +(add-hook 'key-mode-hook '--key-hook) + + +(with-eval-after-load 'lsp-mode + ;; :global/:workspace/:file + (setq lsp-modeline-diagnostics-scope :workspace)) diff --git a/keyext.lsp/workspace/folding/nested.key b/keyext.lsp/workspace/folding/nested.key new file mode 100644 index 0000000000..9c38f4ec80 --- /dev/null +++ b/keyext.lsp/workspace/folding/nested.key @@ -0,0 +1,11 @@ +// Test fixture: Nested declarations for folding range tests +\sorts { + Integer; + Real; + Object; +} + +\functions { + int f(int); + int g(int, int); +} diff --git a/keyext.lsp/workspace/highlighting/basic.key b/keyext.lsp/workspace/highlighting/basic.key new file mode 100644 index 0000000000..0e0fdcca21 --- /dev/null +++ b/keyext.lsp/workspace/highlighting/basic.key @@ -0,0 +1,3 @@ +// Test fixture: Basic file for semantic highlighting tests +\sorts { Integer; } +\functions { int f(int); } diff --git a/keyext.lsp/workspace/highlighting/comments.key b/keyext.lsp/workspace/highlighting/comments.key new file mode 100644 index 0000000000..e7bc0a1996 --- /dev/null +++ b/keyext.lsp/workspace/highlighting/comments.key @@ -0,0 +1,3 @@ +// Test fixture: Comment highlighting test +// This is a single-line comment +\sorts { Integer; } diff --git a/keyext.lsp/workspace/highlighting/keywords.key b/keyext.lsp/workspace/highlighting/keywords.key new file mode 100644 index 0000000000..ec99e372bc --- /dev/null +++ b/keyext.lsp/workspace/highlighting/keywords.key @@ -0,0 +1,2 @@ +// Test fixture: Keyword highlighting test +\sorts { Integer; } diff --git a/keyext.lsp/workspace/highlighting/numbers.key b/keyext.lsp/workspace/highlighting/numbers.key new file mode 100644 index 0000000000..706b4a1c2e --- /dev/null +++ b/keyext.lsp/workspace/highlighting/numbers.key @@ -0,0 +1,2 @@ +// Test fixture: Number literal highlighting test +\axioms { x = 42; y = 3.14; } diff --git a/keyext.lsp/workspace/highlighting/operators.key b/keyext.lsp/workspace/highlighting/operators.key new file mode 100644 index 0000000000..02d3ab1da3 --- /dev/null +++ b/keyext.lsp/workspace/highlighting/operators.key @@ -0,0 +1,2 @@ +// Test fixture: Operator highlighting test +\axioms { x + y = z; a >= b; } diff --git a/keyext.lsp/workspace/lifecycle/single_sort.key b/keyext.lsp/workspace/lifecycle/single_sort.key new file mode 100644 index 0000000000..070aa4bcf0 --- /dev/null +++ b/keyext.lsp/workspace/lifecycle/single_sort.key @@ -0,0 +1,2 @@ +// Test fixture: Simple file for lifecycle tests (didOpen, didChange) +\sorts { Integer; } diff --git a/keyext.lsp/workspace/program.key b/keyext.lsp/workspace/program.key new file mode 100644 index 0000000000..c519dbd862 --- /dev/null +++ b/keyext.lsp/workspace/program.key @@ -0,0 +1,35 @@ +// KeY file with Java program for verification +\program { + class Counter { + private int count; + + Counter() { + count = 0; + } + + void increment() { + count = count + 1; + } + + int getCount() { + return count; + } + } + + class Main { + public static void main(String[] args) { + Counter c = new Counter(); + c.increment(); + c.increment(); + int result = c.getCount(); + } + } +} + +\functions { + int get_count(Counter); +} + +\axioms { + \forall Counter c; get_count(c) >= 0; +} diff --git a/keyext.lsp/workspace/simple.key b/keyext.lsp/workspace/simple.key new file mode 100644 index 0000000000..820aba032b --- /dev/null +++ b/keyext.lsp/workspace/simple.key @@ -0,0 +1,16 @@ +// Simple KeY file for testing +\sorts { + Integer; + MyType; +} + +\functions { + int f(int); + MyType g(MyType, int); +} + +\problem { + f(x) >x= 0; +} + + diff --git a/keyext.lsp/workspace/symbols/full_example.key b/keyext.lsp/workspace/symbols/full_example.key new file mode 100644 index 0000000000..5e792cb42c --- /dev/null +++ b/keyext.lsp/workspace/symbols/full_example.key @@ -0,0 +1,10 @@ +// Test fixture: Complete example for document symbol extraction +\sorts { + Integer; + MyType; +} + +\functions { + int f(int); + MyType g(MyType, int); +} diff --git a/keyext.lsp/workspace/symbols/three_functions.key b/keyext.lsp/workspace/symbols/three_functions.key new file mode 100644 index 0000000000..0602d354f5 --- /dev/null +++ b/keyext.lsp/workspace/symbols/three_functions.key @@ -0,0 +1,6 @@ +// Test fixture: Three function declarations for symbol testing +\functions { + int add(int, int); + int mult(int, int); + Real sqrt(Real); +} diff --git a/keyext.lsp/workspace/symbols/three_sorts.key b/keyext.lsp/workspace/symbols/three_sorts.key new file mode 100644 index 0000000000..c53d8c3e2d --- /dev/null +++ b/keyext.lsp/workspace/symbols/three_sorts.key @@ -0,0 +1,6 @@ +// Test fixture: Three sort declarations for symbol testing +\sorts { + Integer; + Real; + Object; +} diff --git a/keyext.lsp/workspace/syntax_error.key b/keyext.lsp/workspace/syntax_error.key new file mode 100644 index 0000000000..e8b00e20b3 --- /dev/null +++ b/keyext.lsp/workspace/syntax_error.key @@ -0,0 +1,14 @@ +// This file has intentional syntax errors for testing +\sorts { + Integer; + // Missing closing brace + +\functions { + int broken( // Missing parameter and semicolon + MyType g(MyType, int); +} + +\axioms { + f(x) >= 0; + invalid syntax here!!! +} diff --git a/keyext.lsp/workspace/valid_complete.key b/keyext.lsp/workspace/valid_complete.key new file mode 100644 index 0000000000..b513c43657 --- /dev/null +++ b/keyext.lsp/workspace/valid_complete.key @@ -0,0 +1,3 @@ +// Test fixture: Complete valid KeY file for basic loading test +\sorts { Integer; } +\functions { int f(int); } diff --git a/settings.gradle.kts b/settings.gradle.kts index ac0d126294..773e6927c7 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -1,6 +1,11 @@ +pluginManagement { + plugins { + kotlin("kapt") version "2.4.0" + } +} plugins { id("org.gradle.toolchains.foojay-resolver-convention") version "1.0.0" } rootProject.name = "key-rpc" -include("keyext.api.app", "keyext.api", "keyext.api.doc", "keyext.api.client") +include("keyext.api.app", "keyext.api", "keyext.api.doc", "keyext.api.client", "keyext.lsp")