From dfcdc573023abbd9c5ba189bb7e1ee496ba68abb Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 1 Jul 2021 16:18:07 -0700 Subject: [PATCH] feat: go-to for structure fields --- src/Lean/Elab/InfoTree.lean | 13 +++++---- src/Lean/Elab/StructInst.lean | 5 ++-- .../Server/FileWorker/RequestHandling.lean | 27 ++++++++++++------- src/Lean/Server/InfoUtils.lean | 4 ++- 4 files changed, 31 insertions(+), 18 deletions(-) diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index eea75395cb..8bd57827ba 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -60,10 +60,13 @@ def CompletionInfo.stx : CompletionInfo → Syntax | tactic stx .. => stx structure FieldInfo where - name : Name - lctx : LocalContext - val : Expr - stx : Syntax + /-- Name of the projection. -/ + projName : Name + /-- Name of the field as written. -/ + fieldName : Name + lctx : LocalContext + val : Expr + stx : Syntax deriving Inhabited /- We store the list of goals before and after the execution of a tactic. @@ -182,7 +185,7 @@ def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := d def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do ctx.runMetaM info.lctx do - return f!"{info.name} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}" + return f!"{info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}" def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format := if goals.isEmpty then diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index d18bdd3519..c3b38f4a84 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -558,9 +558,10 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term | [FieldLHS.fieldName ref fieldName] => do let type ← whnfForall type match type with - | Expr.forallE _ d b c => + | Expr.forallE _ d b _ => let cont (val : Expr) (field : Field Struct) : TermElabM (Expr × Expr × Fields) := do - pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo { lctx := (← getLCtx), val := val, name := fieldName, stx := ref } + pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo { + projName := s.structName.append fieldName, fieldName, lctx := (← getLCtx), val, stx := ref } let e := mkApp e val let type := b.instantiate1 val let field := { field with expr? := some val } diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 69206d0a00..13a0fd4fcf 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -56,15 +56,18 @@ partial def handleHover (p : HoverParams) return none -open Elab in -partial def handleDefinition (goToType? : Bool) (p : TextDocumentPositionParams) +inductive GoToKind | declaration | definition | type +deriving DecidableEq + +open Elab GoToKind in +partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams) : RequestM (RequestTask (Array LocationLink)) := do let rc ← read let doc ← readDoc let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position - let locationLinksFromDecl i n := do + let locationLinksFromDecl (i : Elab.Info) (n : Name) := do let mod? ← findModuleOf? n let modUri? ← match mod? with | some modName => @@ -92,16 +95,20 @@ partial def handleDefinition (goToType? : Bool) (p : TextDocumentPositionParams) if let some (ci, i) := t.hoverableInfoAt? hoverPos then if let Info.ofTermInfo ti := i then let mut expr := ti.expr - if goToType? then + if kind = type then expr ← ci.runMetaM i.lctx do Meta.instantiateMVars (← Meta.inferType expr) if let some n := expr.constName? then return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n + if let Info.ofFieldInfo fi := i then + if kind ≠ type then + return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName + -- If other go-tos fail, we try to show the elaborator or parser if let some ei := i.toElabInfo? then - if ci.env.contains ei.elaborator then - return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator - if ci.env.contains ei.stx.getKind then + if kind = declaration ∧ ci.env.contains ei.stx.getKind then return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind + if kind = definition ∧ ci.env.contains ei.elaborator then + return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator return #[] open Elab in @@ -339,9 +346,9 @@ builtin_initialize registerLspRequestHandler "textDocument/waitForDiagnostics" WaitForDiagnosticsParams WaitForDiagnostics handleWaitForDiagnostics registerLspRequestHandler "textDocument/completion" CompletionParams CompletionList handleCompletion registerLspRequestHandler "textDocument/hover" HoverParams (Option Hover) handleHover - registerLspRequestHandler "textDocument/declaration" TextDocumentPositionParams (Array LocationLink) (handleDefinition (goToType? := false)) - registerLspRequestHandler "textDocument/definition" TextDocumentPositionParams (Array LocationLink) (handleDefinition (goToType? := false)) - registerLspRequestHandler "textDocument/typeDefinition" TextDocumentPositionParams (Array LocationLink) (handleDefinition (goToType? := true)) + registerLspRequestHandler "textDocument/declaration" TextDocumentPositionParams (Array LocationLink) (handleDefinition GoToKind.declaration) + registerLspRequestHandler "textDocument/definition" TextDocumentPositionParams (Array LocationLink) (handleDefinition GoToKind.definition) + registerLspRequestHandler "textDocument/typeDefinition" TextDocumentPositionParams (Array LocationLink) (handleDefinition GoToKind.type) registerLspRequestHandler "textDocument/documentHighlight" DocumentHighlightParams DocumentHighlightResult handleDocumentHighlight registerLspRequestHandler "textDocument/documentSymbol" DocumentSymbolParams DocumentSymbolResult handleDocumentSymbol registerLspRequestHandler "textDocument/semanticTokens/full" SemanticTokensParams SemanticTokens handleSemanticTokensFull diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 26d9770a60..55149a6b3c 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -157,13 +157,15 @@ where let tp ← Meta.inferType fi.val let tpFmt ← Meta.ppExpr tp return some f!"```lean -{fi.name} : {tpFmt} +{fi.fieldName} : {tpFmt} ```" | _ => return none fmtDoc? := do if let Info.ofTermInfo ti := i then if let some n := ti.expr.constName? then return ← findDocString? n + if let Info.ofFieldInfo fi := i then + return ← findDocString? fi.projName if let some ei := i.toElabInfo? then return ← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind return none