max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: go-to for structure fields

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-07-01 16:18:07 -07:00 • committed by Sebastian Ullrich
parent 24dcdad832
commit dfcdc57302
4 changed files with 31 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Elab/InfoTree.lean
View file

@ -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

5
src/Lean/Elab/StructInst.lean
View file

@ -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 }

27
src/Lean/Server/FileWorker/RequestHandling.lean
View file

@ -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

4
src/Lean/Server/InfoUtils.lean
View file

@ -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