diff --git a/.run/GoalTest.testDeserializationLazyTraceChildrenToInteractiveResp.run.xml b/.run/GoalTest.testDeserializationLazyTraceChildrenToInteractiveResp.run.xml new file mode 100644 index 00000000..248e5e8e --- /dev/null +++ b/.run/GoalTest.testDeserializationLazyTraceChildrenToInteractiveResp.run.xml @@ -0,0 +1,19 @@ + + + + + + + + + \ No newline at end of file diff --git a/.run/GoalTest.testDeserializeLazyTraceChildrenToInteractiveResp.run.xml b/.run/GoalTest.testDeserializeLazyTraceChildrenToInteractiveResp.run.xml new file mode 100644 index 00000000..fecbc8cb --- /dev/null +++ b/.run/GoalTest.testDeserializeLazyTraceChildrenToInteractiveResp.run.xml @@ -0,0 +1,19 @@ + + + + + + + + + \ No newline at end of file diff --git a/.run/GoalTest.testDeserializeMsgEmbedTrace.run.xml b/.run/GoalTest.testDeserializeMsgEmbedTrace.run.xml new file mode 100644 index 00000000..cedfc239 --- /dev/null +++ b/.run/GoalTest.testDeserializeMsgEmbedTrace.run.xml @@ -0,0 +1,19 @@ + + + + + + + + + \ No newline at end of file diff --git a/CHANGELOG.md b/CHANGELOG.md index 02d63f91..85b86da1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,7 +9,7 @@ - a setting for the debouncing gap - some refactor on settings - setting for starting the language server eagerly or not -- setting for file progressing all open editors eagerly or not (requires lsp 0.8.0) +- setting for file progressing all open editors eagerly or not (requires lsp4ij 0.8.0) ## [0.1.5] - 2024-11-17 diff --git a/DEVELOP.md b/DEVELOP.md index bbb4deb6..864ead45 100644 --- a/DEVELOP.md +++ b/DEVELOP.md @@ -51,7 +51,53 @@ the swing infoview is a raw infoview implemented using intellij platform's swing Currently, the code is still very badly organized for requiring further development. The entrance point for rendering is at `LeanFile.updateCaret` which call `LeanInfoViewWindowFactory.updateGoal` when all lsp call finish. +### The design for `TaggedText` and `InfoViewContent` +The implementation for the internal infoview, especially the render part needs big refactor. + +Currently, the design for `TaggedText` and `InfoviewContent` is extremely complicated for not sure what the contract is. + +The generic class `TaggedText` is original designed for respecting the following structure in the lean source code `src/Lean/Widget/TaggedText.lean`. + +```lean4 +inductive TaggedText (α : Type u) where + | text : String → TaggedText α + /-- Invariants: + - non-empty + - no adjacent `text` elements (they should be collapsed) + - no directly nested `append`s (but `append #[tag _ (append ..)]` is okay) -/ + | append : Array (TaggedText α) → TaggedText α + | tag : α → TaggedText α → TaggedText α +``` + +That has three constructors. Here they are represented in three subclass: `TaggedTextText`, `TaggedTextAppend` and `TaggedTextTag`. +For the type α in the above lean source code, currently it's the interface `InfoViewContent` and the implementations are +- SubexprInfo +- MsgEmbed + - MsgEmbedExpr + - MsgEmbedGoal + - MsgEmbedTrace + - MsgUnsupported + +The implementation `SubexprInfo` corresponds to the following source code in the lean4 codebase in `Lean/Widget/InteractiveCode.lean` and is used for +displaying interactive goals/expecting types in the infoview: + +```lean4 +structure SubexprInfo where + /-- The `Elab.Info` node with the semantics of this part of the output. -/ + info : WithRpcRef Lean.Elab.InfoWithCtx + /-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`. -/ + subexprPos : Lean.SubExpr.Pos + -- TODO(WN): add fields for semantic highlighting + -- kind : Lsp.SymbolKind + /-- In certain situations such as when goal states change between positions in a tactic-mode proof, + we can show subexpression-level diffs between two expressions. This field asks the renderer to + display the subexpression as in a diff view (e.g. red/green like `git diff`). -/ + diffStatus? : Option DiffTag := none + deriving RpcEncodable +``` + +The `MsgEmbed` and its subclasses are used for displaying the messages. Almost all complexities came from this part. ## Developing in Intellij Idea Proxy issue (this should only happen in some specific region) diff --git a/src/main/kotlin/lean4ij/infoview/InfoviewMouseListener.kt b/src/main/kotlin/lean4ij/infoview/InfoviewMouseListener.kt new file mode 100644 index 00000000..956dc6bf --- /dev/null +++ b/src/main/kotlin/lean4ij/infoview/InfoviewMouseListener.kt @@ -0,0 +1,28 @@ +package lean4ij.infoview + +import com.intellij.openapi.editor.event.EditorMouseEvent +import com.intellij.openapi.editor.event.EditorMouseListener +import lean4ij.lsp.data.InfoviewRender + +class InfoviewMouseListener(private val infoviewRender: InfoviewRender) : EditorMouseListener { + + override fun mousePressed(event: EditorMouseEvent) { + super.mousePressed(event) + } + + override fun mouseClicked(event: EditorMouseEvent) { + infoviewRender.getClickAction(event.offset)?.invoke(event) + } + + override fun mouseReleased(event: EditorMouseEvent) { + super.mouseReleased(event) + } + + override fun mouseEntered(event: EditorMouseEvent) { + super.mouseEntered(event) + } + + override fun mouseExited(event: EditorMouseEvent) { + super.mouseExited(event) + } +} \ No newline at end of file diff --git a/src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt b/src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt index 90e81d24..5bbb3508 100644 --- a/src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt +++ b/src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt @@ -142,7 +142,7 @@ class InfoviewPopupDocumentation( ) val infoToInteractive = leanProjectService.languageServer.await() .infoToInteractive(rpcParams) - val sb = InfoviewRender() + val sb = InfoviewRender(project, file) val typeStr = infoToInteractive.type?.toInfoViewString(sb, null) ?: "" val exprStr = infoToInteractive.exprExplicit?.toInfoViewString(sb, null) ?: "" var htmlDoc: String? = null diff --git a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt index 8aafda51..0a34abad 100644 --- a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt +++ b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt @@ -6,8 +6,8 @@ import com.intellij.openapi.application.EDT import com.intellij.openapi.components.service import com.intellij.openapi.editor.EditorFactory import com.intellij.openapi.editor.FoldRegion -import com.intellij.openapi.editor.LogicalPosition import com.intellij.openapi.editor.ScrollType +import com.intellij.openapi.editor.event.EditorMouseListener import com.intellij.openapi.editor.event.EditorMouseMotionListener import com.intellij.openapi.editor.ex.EditorEx import com.intellij.openapi.editor.ex.FoldingListener @@ -145,11 +145,12 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru } private var mouseMotionListener : EditorMouseMotionListener? = null + private var mouseListener : EditorMouseListener? = null /** * // TODO this should add some UT for the rendering */ suspend fun updateEditorMouseMotionListener( - interactiveInfo: InfoviewRender, + infoviewRender: InfoviewRender, file: VirtualFile, position: Position, interactiveGoals: InteractiveGoals?, @@ -159,7 +160,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru ) { val editorEx: EditorEx = editor.await() editorEx.markupModel.removeAllHighlighters() - editorEx.document.setText(interactiveInfo.toString()) + editorEx.document.setText(infoviewRender.toString()) // TODO maybe a configuration for this // always move to the beginning while update goal, to avoid losing focus while all message expanded @@ -170,7 +171,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru editorEx.foldingModel.runBatchFoldingOperation { editorEx.foldingModel.clearFoldRegions() var allMessagesFoldRegion : FoldRegion? = null - for (folding in interactiveInfo.foldings) { + for (folding in infoviewRender.foldings) { val foldRegion = editorEx.foldingModel.addFoldRegion(folding.startOffset, folding.endOffset, folding.placeholderText) foldRegion?.isExpanded = folding.expanded if (folding.isAllMessages) { @@ -188,7 +189,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru } } // highlights - for (highlight in interactiveInfo.highlights) { + for (highlight in infoviewRender.highlights) { editorEx.markupModel.addRangeHighlighter(highlight.startOffset, highlight.endOffset, HighlighterLayer.SYNTAX, highlight.textAttributes, HighlighterTargetArea.EXACT_RANGE) } @@ -202,9 +203,16 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru if (mouseMotionListener != null) { editorEx.removeEditorMouseMotionListener(mouseMotionListener!!) } + // TODO this can be refactored to the InfoviewRender class, in that way the definition of hovering + // can be done in the same time when the rendering is defined mouseMotionListener = InfoviewMouseMotionListener(leanProject, this, editorEx, file, position, interactiveGoals, interactiveTermGoal, interactiveDiagnostics, interactiveDiagnosticsAllMessages) editorEx.addEditorMouseMotionListener(mouseMotionListener!!) + if (mouseListener != null) { + editorEx.removeEditorMouseListener(mouseListener!!) + } + mouseListener = InfoviewMouseListener(infoviewRender) + editorEx.addEditorMouseListener(mouseListener!!) } fun restartEditor() { diff --git a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt index 47774f65..35cf2cd7 100644 --- a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt +++ b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt @@ -73,7 +73,7 @@ class LeanInfoViewWindowFactory : ToolWindowFactory { } val infoViewWindow = getLeanInfoview(project) ?: return // TODO implement the fold/open logic - val infoviewRender = InfoviewRender() + val infoviewRender = InfoviewRender(project, file) val start = infoviewRender.length val header = "${file.name}:${position.line+1}:${position.character}" infoviewRender.append("${header}") diff --git a/src/main/kotlin/lean4ij/language/InlayHints.kt b/src/main/kotlin/lean4ij/language/InlayHints.kt index 7cc106e5..68efd4c0 100644 --- a/src/main/kotlin/lean4ij/language/InlayHints.kt +++ b/src/main/kotlin/lean4ij/language/InlayHints.kt @@ -259,7 +259,8 @@ class OmitTypeInlayHintsCollector(editor: Editor, project: Project?) : InlayHint // TODO what if the server not start? // will it hang and leak? val termGoal = file.getInteractiveTermGoal(interactiveTermGoalParams) ?: continue - val inlayHintType = ": ${termGoal.type.toInfoViewString(InfoviewRender(), null)}" + // TODO can here project be null?, the InfoviewRender mainly keeps nullable for it + val inlayHintType = ": ${termGoal.type.toInfoViewString(InfoviewRender(project, file.virtualFile), null)}" var hintPos = m.range.last - m.groupValues[3].length // anonymous have is slightly weird if (m.groupValues[1] != "have " || !m.groupValues[2].isEmpty()) { @@ -337,7 +338,8 @@ class GoalInlayHintsCollector(editor: Editor, project: Project?) : InlayHintBase val termGoals = file.getInteractiveGoals(interactiveGoalParams) if (termGoals != null && !termGoals.goals.isEmpty()) { - typeHint = termGoals.goals[0].type.toInfoViewString(InfoviewRender(), null) + // TODO can here project be null?, the InfoviewRender mainly keeps nullable for it + typeHint = termGoals.goals[0].type.toInfoViewString(InfoviewRender(project, file.virtualFile), null) } else { // non tactic mode @@ -345,7 +347,8 @@ class GoalInlayHintsCollector(editor: Editor, project: Project?) : InlayHintBase val interactiveTermGoalParams = InteractiveTermGoalParams(session, params, textDocument, position) val termGoal = file.getInteractiveTermGoal(interactiveTermGoalParams) - typeHint = termGoal?.type?.toInfoViewString(InfoviewRender(), null) ?: continue + // TODO can here project be null?, the InfoviewRender mainly keeps nullable for it + typeHint = termGoal?.type?.toInfoViewString(InfoviewRender(project, file.virtualFile), null) ?: continue } var hintPos = m.range.first + m.groupValues[1].length diff --git a/src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt b/src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt index aeb2955a..2db215c6 100644 --- a/src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt +++ b/src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt @@ -59,6 +59,11 @@ class LeanLanguageServer(val languageServer: InternalLeanLanguageServer) { return infoToInteractiveAsync(params).await() } + suspend fun lazyTraceChildrenToInteractive(params: LazyTraceChildrenToInteractiveParams): List>? { + return lazyTraceChildrenToInteractiveAsync(params).await() + } + + fun plainGoalAsync (params: PlainGoalParams): CompletableFuture { return languageServer.plainGoal(params) } @@ -103,6 +108,20 @@ class LeanLanguageServer(val languageServer: InternalLeanLanguageServer) { } } + /** + * the rpc call for showing trace in infoview + */ + fun lazyTraceChildrenToInteractiveAsync(params: LazyTraceChildrenToInteractiveParams) : CompletableFuture>?> { + return languageServer.rpcCall(params).thenApply { + // TODO check if this is necessary for two steps and the reason for it + val intermediate : List = gson.fromJson(it, object: TypeToken>(){}.type) + return@thenApply intermediate.map { + gson.fromJson(it, object: TypeToken>(){}.type) + } + } + } + + fun rpcKeepAlive(params: RpcKeepAliveParams) { return languageServer.rpcKeepAlive(params) } @@ -138,7 +157,10 @@ class LeanLanguageServer(val languageServer: InternalLeanLanguageServer) { return MsgEmbedGoal(f1) } if (p0.isJsonObject && p0.asJsonObject.has("trace")) { - return MsgUnsupported("Trace message is not supported yet. Please the jcef version infoview.") + @Suppress("NAME_SHADOWING") + val p1 = p0.asJsonObject.getAsJsonObject("trace") + val ret : MsgEmbedTrace = p2.deserialize(p1, MsgEmbedTrace::class.java) + return ret } if (p0.isJsonObject && p0.asJsonObject.has("widget")) { return MsgUnsupported("Widget message cannot be supported for technical reason. Please the jcef version infoview.") @@ -164,6 +186,27 @@ class LeanLanguageServer(val languageServer: InternalLeanLanguageServer) { throw IllegalStateException("Unsupported RPC method: $method") } }) + // TODO here it's quit idle too + .registerTypeAdapter(StrictOrLazy::class.java, object : JsonDeserializer>, ContextInfo>> { + override fun deserialize(p0: JsonElement, p1: Type, p2: JsonDeserializationContext): StrictOrLazy>, ContextInfo> { + if (p0.isJsonObject && p0.asJsonObject.has("strict")) { + val p0 = p0.asJsonObject.get("strict") + // TODO check if intermediate is necessary or not + // TODO DRY this + val intermediate = p2.deserialize>(p0, object :TypeToken>(){}.type) + val children = intermediate.map { + p2.deserialize>(it, object : TypeToken>(){}.type) + }.toList() + return StrictOrLazyStrict(children) + } + if (p0.isJsonObject && p0.asJsonObject.has("lazy")) { + val p0 = p0.asJsonObject.get("lazy") + val children = p2.deserialize(p0, object :TypeToken(){}.type) + return StrictOrLazyLazy(children) + } + throw IllegalStateException("$p0 cannot be deserialized to StrictOrLazy>, ContextInfo>") + } + }) .create() } } diff --git a/src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt b/src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt index 68af5e46..1916e19a 100644 --- a/src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt +++ b/src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt @@ -1,5 +1,11 @@ package lean4ij.lsp.data +import com.intellij.openapi.components.service +import kotlinx.coroutines.launch +import lean4ij.project.LeanProjectService +import lean4ij.util.LspUtil +import org.eclipse.lsp4j.TextDocumentIdentifier + /** * copy from src/Lean/Widget/InteractiveCode.lean:45 * The polymorphism is achieved via class inheritance @@ -8,7 +14,7 @@ package lean4ij.lsp.data * TODO this maybe should be renamed */ interface InfoViewContent { - fun toInfoViewString(sb : InfoviewRender) : String + fun toInfoViewString(render : InfoviewRender) : String fun contextInfo(offset: Int, startOffset: Int, endOffset : Int) : Triple? fun mayHighlight(sb: InfoviewRender, startOffset: Int, endOffset: Int) {} } @@ -113,8 +119,8 @@ class TaggedTextAppend(private val append: List>) : TaggedText< abstract class MsgEmbed : InfoViewContent class MsgEmbedExpr(val expr: TaggedText) : MsgEmbed() { - override fun toInfoViewString(sb: InfoviewRender): String { - return expr.toInfoViewString(sb, null) + override fun toInfoViewString(render: InfoviewRender): String { + return expr.toInfoViewString(render, null) } override fun contextInfo(offset: Int, startOffset: Int, endOffset : Int) : Triple? { @@ -123,8 +129,8 @@ class MsgEmbedExpr(val expr: TaggedText) : MsgEmbed() { } class MsgEmbedGoal(val goal: InteractiveGoal) : MsgEmbed() { - override fun toInfoViewString(sb: InfoviewRender): String { - return goal.toInfoViewString(sb, false) + override fun toInfoViewString(render: InfoviewRender): String { + return goal.toInfoViewString(render, false) } override fun contextInfo(offset: Int, startOffset: Int, endOffset : Int) : Triple? { @@ -138,11 +144,54 @@ class MsgEmbedGoal(val goal: InteractiveGoal) : MsgEmbed() { * TODO trace! Not implement yet, check src/Lean/Widget/InteractiveDiagnostic.lean" 221 lines --11%-- * the definition of MsgEmbed */ -abstract class MsgEmbedTrace(val indent: Int, val cls: String): MsgEmbed() +class MsgEmbedTrace(val indent: Int, val cls: String, private val collapsed: Boolean, + // TODO children: json like { "lazy" : { "p" : "31" } } + // this is a little idle using a map, it should be some type, check + // src/Lean/Widget/InteractiveDiagnostic.lean:248 + // private val children : Map, + private val children: StrictOrLazy>, ContextInfo>, + private val msg: TaggedTextAppend + ): MsgEmbed() { + override fun toInfoViewString(render: InfoviewRender): String { + val start = render.length + render.append("[$cls] ") + msg.toInfoViewString(render, null) + render.append(" ▶") + render.addClickAction(start, render.length) { + val project = render.project?:return@addClickAction + val file = render.file?:return@addClickAction + val contextInfo = (children as? StrictOrLazyLazy)?.lazy?:return@addClickAction + val leanProjectService = project.service() + val logicalPosition = it.logicalPosition + val position = Position(logicalPosition.line, logicalPosition.column) + leanProjectService.scope.launch { + val languageServer = leanProjectService.languageServer.await() + val session = leanProjectService.file(file).getSession() + val textDocument = TextDocumentIdentifier(LspUtil.quote(file.path)) + val rpcParams = LazyTraceChildrenToInteractiveParams( + sessionId = session, + params = contextInfo, + textDocument = textDocument, + position = position + ) + val resp = languageServer.lazyTraceChildrenToInteractive(rpcParams) + TODO() + } + + } + return render.substring(start, render.length) + } + + override fun contextInfo(offset: Int, startOffset: Int, endOffset: Int): Triple? { + // TODO + return null + // TODO("Not yet implemented") + } +} class MsgUnsupported(val message: String) : MsgEmbed() { - override fun toInfoViewString(sb: InfoviewRender): String { - sb.append(message) + override fun toInfoViewString(render: InfoviewRender): String { + render.append(message) return message } @@ -150,3 +199,13 @@ class MsgUnsupported(val message: String) : MsgEmbed() { return null } } + +/** + * class corresponding to the lean inductive with the same name + * in Lean/Widget/InteractiveDiagnostic.lean:15 + * This is kind of same as Either + * Strict or lazy may largely be used by kotlin + */ +abstract class StrictOrLazy +data class StrictOrLazyStrict(val strict: A) : StrictOrLazy() +data class StrictOrLazyLazy(val lazy: B) : StrictOrLazy() diff --git a/src/main/kotlin/lean4ij/lsp/data/InteractiveGoals.kt b/src/main/kotlin/lean4ij/lsp/data/InteractiveGoals.kt index fdaa660f..e19c09da 100644 --- a/src/main/kotlin/lean4ij/lsp/data/InteractiveGoals.kt +++ b/src/main/kotlin/lean4ij/lsp/data/InteractiveGoals.kt @@ -2,9 +2,49 @@ package lean4ij.lsp.data import com.intellij.openapi.editor.colors.EditorColorsManager import com.intellij.openapi.editor.colors.TextAttributesKey +import com.intellij.openapi.editor.event.EditorMouseEvent import com.intellij.openapi.editor.markup.TextAttributes +import com.intellij.openapi.project.Project +import com.intellij.openapi.vfs.VirtualFile import lean4ij.infoview.TextAttributesKeys +/** + * A quite naive implementation for an interval tree? Some code like + * [com.intellij.openapi.editor.impl.IntervalTreeImpl] in Intellij + * may help + * TODO The name maybe not suitable since it's not an interval tree maybe + */ +class IntervalTree( + private val start: Int, + private val end: Int, + private val elem: T, + private val childrens: MutableList> +) { + + fun getElemAt(offset: Int) : T? { + return getNodeAt(offset)?.elem + } + + private fun getNodeAt(offset: Int) : IntervalTree? { + if (offset !in start.. get() = _foldings.toList() val highlights : List get() = _highlights.toList() + + /** + * TODO here a specific class should be defined for () -> Unit + */ + private val clickActions : IntervalTree<(EditorMouseEvent) -> Unit> = IntervalTree(0, Int.MAX_VALUE, {}, mutableListOf()) + + fun addClickAction(start: Int, end: Int, action: (EditorMouseEvent) -> Unit) { + clickActions.insertRange(start, end, action) + } + + fun getClickAction(offset: Int) : ((EditorMouseEvent) -> Unit)? { + return clickActions.getElemAt(offset) + } } /** diff --git a/src/main/kotlin/lean4ij/lsp/data/LazyTraceChildrenToInteractiveParams.kt b/src/main/kotlin/lean4ij/lsp/data/LazyTraceChildrenToInteractiveParams.kt new file mode 100644 index 00000000..f73bd25d --- /dev/null +++ b/src/main/kotlin/lean4ij/lsp/data/LazyTraceChildrenToInteractiveParams.kt @@ -0,0 +1,11 @@ +package lean4ij.lsp.data + +import lean4ij.util.Constants +import org.eclipse.lsp4j.TextDocumentIdentifier + +class LazyTraceChildrenToInteractiveParams( + sessionId : String, + textDocument: TextDocumentIdentifier, + position: Position, + val params: ContextInfo, +) : RpcCallParams(sessionId, Constants.RPC_METHOD_LAZY_TRACE_CHILDREN_TO_INTERACTIVE, textDocument, position) \ No newline at end of file diff --git a/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt b/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt index c60caaae..a634e89c 100644 --- a/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt +++ b/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt @@ -6,7 +6,7 @@ import lean4ij.infoview.TextAttributesKeys * see: tests/lean/interactive/run.lean:11 */ data class SubexprInfo (val subexprPos: String, val info: ContextInfo, val diffStatus: String?) : InfoViewContent { - override fun toInfoViewString(sb: InfoviewRender): String { + override fun toInfoViewString(render: InfoviewRender): String { // TODO SubexprInfo seems totally independent with render? return "" } diff --git a/src/main/kotlin/lean4ij/project/LeanFile.kt b/src/main/kotlin/lean4ij/project/LeanFile.kt index cb98ba94..ee35fb23 100644 --- a/src/main/kotlin/lean4ij/project/LeanFile.kt +++ b/src/main/kotlin/lean4ij/project/LeanFile.kt @@ -252,6 +252,7 @@ class LeanFile(private val leanProjectService: LeanProjectService, private val f val interactiveGoals = interactiveGoalsAsync.await() val interactiveTermGoal = interactiveTermGoalAsync.await() val interactiveDiagnostics = interactiveDiagnosticsAsync.await() + // TODO the arguments are passing very deep, need some refactor LeanInfoViewWindowFactory.updateInteractiveGoal(editor, project, virtualFile!!, position, interactiveGoals, interactiveTermGoal, interactiveDiagnostics, allMessage) } } diff --git a/src/main/kotlin/lean4ij/util/Constants.kt b/src/main/kotlin/lean4ij/util/Constants.kt index 1d674b89..8be57def 100644 --- a/src/main/kotlin/lean4ij/util/Constants.kt +++ b/src/main/kotlin/lean4ij/util/Constants.kt @@ -16,6 +16,7 @@ object Constants { const val RPC_METHOD_GET_INTERACTIVE_GOALS = "Lean.Widget.getInteractiveGoals" const val RPC_METHOD_GET_INTERACTIVE_TERM_GOAL = "Lean.Widget.getInteractiveTermGoal" const val RPC_METHOD_GET_INTERACTIVE_DIAGNOSTICS = "Lean.Widget.getInteractiveDiagnostics" + const val RPC_METHOD_LAZY_TRACE_CHILDREN_TO_INTERACTIVE = "Lean.Widget.lazyTraceChildrenToInteractive" const val FILE_PROGRESS = "\$/lean/fileProgress" /** diff --git a/src/test/kotlin/lean4ij/infoview/GoalTest.kt b/src/test/kotlin/lean4ij/infoview/GoalTest.kt index e293bd1a..d6ffe874 100644 --- a/src/test/kotlin/lean4ij/infoview/GoalTest.kt +++ b/src/test/kotlin/lean4ij/infoview/GoalTest.kt @@ -1,15 +1,39 @@ package lean4ij.infoview -import lean4ij.lsp.data.* import com.google.common.io.Resources -import com.google.gson.* +import com.google.gson.JsonObject +import com.google.gson.reflect.TypeToken import com.intellij.testFramework.TestDataPath -import lean4ij.lsp.LeanLanguageServer.Companion.gson +import com.intellij.testFramework.fixtures.BasePlatformTestCase +import junit.framework.TestCase +import lean4ij.lsp.LeanLanguageServer +import lean4ij.lsp.data.MsgEmbed +import lean4ij.lsp.data.MsgEmbedTrace +import lean4ij.lsp.data.TaggedText +import lean4ij.lsp.data.TaggedTextTag import org.junit.Test -import java.lang.reflect.Type import java.nio.charset.StandardCharsets @TestDataPath("\$CONTENT_ROOT/src/test/testData") -class GoalTest { +class GoalTest : BasePlatformTestCase() { + + @Test + fun testDeserializeLazyTraceChildrenToInteractiveResp() { + val s = Resources.toString(Resources.getResource("lsp/lazyTraceChildrenToInteractive_resp_sample1.json"), StandardCharsets.UTF_8) + // TODO no sure what happened but it seems it must be seperated into two part + val r = LeanLanguageServer.gson.fromJson>(s, object : TypeToken>() {}.type) + .map { + LeanLanguageServer.gson.fromJson>(it, object : TypeToken>() {}.type) + }.toList() + assertEquals(r.size, 5) + } + + @Test + fun testDeserializeMsgEmbedTrace() { + val s = Resources.toString(Resources.getResource("lsp/msgEmbedTrace_sample1.json"), StandardCharsets.UTF_8) + // TODO no sure what happened but it seems it must be seperated into two part + val r = LeanLanguageServer.gson.fromJson(s, object : TypeToken() {}.type) + TestCase.assertNotNull(r) + } } diff --git a/src/test/resources/lsp/lazyTraceChildrenToInteractive_resp_sample.json b/src/test/resources/lsp/lazyTraceChildrenToInteractive_resp_sample.json new file mode 100644 index 00000000..609c487d --- /dev/null +++ b/src/test/resources/lsp/lazyTraceChildrenToInteractive_resp_sample.json @@ -0,0 +1,631 @@ +[ + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "new goal " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "69" + } + }, + { + "append": [ + { + "text": "HasEquiv " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "70" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance", + "children": { + "lazy": { + "p": "71" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "✅" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " apply " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "72" + } + }, + { + "text": "@instHasEquivOfSetoid" + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " to " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "73" + } + }, + { + "append": [ + { + "text": "HasEquiv " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "74" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance", + "children": { + "lazy": { + "p": "75" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "✅" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " apply " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "76" + } + }, + { + "text": "inst✝" + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " to " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "77" + } + }, + { + "append": [ + { + "text": "Setoid " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "78" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance", + "children": { + "lazy": { + "p": "79" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "propagating " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "80" + } + }, + { + "append": [ + { + "text": "Setoid " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "81" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " to subgoal " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "82" + } + }, + { + "append": [ + { + "text": "Setoid " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "83" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " of " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "84" + } + }, + { + "append": [ + { + "text": "HasEquiv " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "85" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance.resume", + "children": { + "lazy": { + "p": "86" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "result " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "87" + } + }, + { + "text": "instHasEquivOfSetoid" + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": false, + "cls": "Meta.synthInstance", + "children": { + "strict": [] + } + } + }, + { + "text": "" + } + ] + } +] \ No newline at end of file diff --git a/src/test/resources/lsp/lazyTraceChildrenToInteractive_resp_sample1.json b/src/test/resources/lsp/lazyTraceChildrenToInteractive_resp_sample1.json new file mode 100644 index 00000000..8296e905 --- /dev/null +++ b/src/test/resources/lsp/lazyTraceChildrenToInteractive_resp_sample1.json @@ -0,0 +1,631 @@ +[ + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "new goal " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "21" + } + }, + { + "append": [ + { + "text": "HasEquiv " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "22" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance", + "children": { + "lazy": { + "p": "23" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "✅" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " apply " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "24" + } + }, + { + "text": "@instHasEquivOfSetoid" + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " to " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "25" + } + }, + { + "append": [ + { + "text": "HasEquiv " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "26" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance", + "children": { + "lazy": { + "p": "27" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "✅" + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " apply " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "28" + } + }, + { + "text": "inst✝" + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " to " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "29" + } + }, + { + "append": [ + { + "text": "Setoid " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "30" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance", + "children": { + "lazy": { + "p": "31" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "propagating " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "32" + } + }, + { + "append": [ + { + "text": "Setoid " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "33" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " to subgoal " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "34" + } + }, + { + "append": [ + { + "text": "Setoid " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "35" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": " of " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "36" + } + }, + { + "append": [ + { + "text": "HasEquiv " + }, + { + "tag": [ + { + "subexprPos": "/1", + "info": { + "p": "37" + } + }, + { + "text": "α" + } + ] + } + ] + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": true, + "cls": "Meta.synthInstance.resume", + "children": { + "lazy": { + "p": "38" + } + } + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "result " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "39" + } + }, + { + "text": "instHasEquivOfSetoid" + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": false, + "cls": "Meta.synthInstance", + "children": { + "strict": [] + } + } + }, + { + "text": "" + } + ] + } +] \ No newline at end of file diff --git a/src/test/resources/lsp/msgEmbedTrace_sample.json b/src/test/resources/lsp/msgEmbedTrace_sample.json new file mode 100644 index 00000000..ca04c4f9 --- /dev/null +++ b/src/test/resources/lsp/msgEmbedTrace_sample.json @@ -0,0 +1,73 @@ +{ + "trace" : { + "msg" : { + "append" : [ { + "tag" : [ { + "expr" : { + "text" : "" + } + }, { + "text" : "" + } ] + }, { + "tag" : [ { + "expr" : { + "text" : "✅" + } + }, { + "text" : "" + } ] + }, { + "tag" : [ { + "expr" : { + "text" : " " + } + }, { + "text" : "" + } ] + }, { + "tag" : [ { + "expr" : { + "tag" : [ { + "subexprPos" : "/", + "info" : { + "p" : "309" + } + }, { + "append" : [ { + "text" : "Setoid " + }, { + "tag" : [ { + "subexprPos" : "/1", + "info" : { + "p" : "310" + } + }, { + "text" : "α" + } ] + } ] + } ] + } + }, { + "text" : "" + } ] + }, { + "tag" : [ { + "expr" : { + "text" : "" + } + }, { + "text" : "" + } ] + } ] + }, + "indent" : 0, + "collapsed" : true, + "cls" : "Meta.synthInstance", + "children" : { + "lazy" : { + "p" : "311" + } + } + } +} diff --git a/src/test/resources/lsp/msgEmbedTrace_sample1.json b/src/test/resources/lsp/msgEmbedTrace_sample1.json new file mode 100644 index 00000000..203d590c --- /dev/null +++ b/src/test/resources/lsp/msgEmbedTrace_sample1.json @@ -0,0 +1,60 @@ +{ + "trace": { + "msg": { + "append": [ + { + "tag": [ + { + "expr": { + "text": "result " + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "tag": [ + { + "subexprPos": "/", + "info": { + "p": "39" + } + }, + { + "text": "instHasEquivOfSetoid" + } + ] + } + }, + { + "text": "" + } + ] + }, + { + "tag": [ + { + "expr": { + "text": "" + } + }, + { + "text": "" + } + ] + } + ] + }, + "indent": 2, + "collapsed": false, + "cls": "Meta.synthInstance", + "children": { + "strict": [] + } + } +} \ No newline at end of file