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

feat: add RPC call to retrieve defn/decl/type defn

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-05-18 16:13:06 -04:00 • committed by Sebastian Ullrich
parent 9c058a5798
commit aef8d32d0b
2 changed files with 57 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -59,15 +59,14 @@ def handleHover (p : HoverParams)
inductive GoToKind
| declaration | definition | type
deriving BEq
deriving BEq, ToJson, FromJson
open Elab GoToKind in
partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
: RequestM (RequestTask (Array LocationLink)) := do
def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info)
(infoTree? : Option InfoTree := none) : RequestM (Array LocationLink) := do
let rc ← read
let doc ← readDoc
let text := doc.meta.text
let hoverPos := text.lspPosToUtf8Pos p.position
let documentUriFromModule (modName : Name) : MetaM (Option DocumentUri) := do
let some modFname ← rc.srcSearchPath.findModuleWithExt "lean" modName
@ -97,15 +96,15 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
return #[ll]
return #[]
let locationLinksFromBinder (t : InfoTree) (i : Elab.Info) (id : FVarId) := do
if let some i' := t.findInfo? fun
let locationLinksFromBinder (i : Elab.Info) (id : FVarId) := do
if let some i' := infoTree? >>= InfoTree.findInfo? fun
| Info.ofTermInfo { isBinder := true, expr := Expr.fvar id' .., .. } => id' == id
| _ => false then
if let some r := i'.range? then
let r := r.toLspRange text
let ll : LocationLink := {
originSelectionRange? := (·.toLspRange text) <$> i.range?
targetUri := p.textDocument.uri
targetUri := doc.meta.uri
targetRange := r
targetSelectionRange := r
}
@ -117,7 +116,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
if let some modUri ← documentUriFromModule name then
let range := { start := ⟨0, 0⟩, «end» := ⟨0, 0⟩ : Range }
let ll : LocationLink := {
originSelectionRange? := none
originSelectionRange? := (·.toLspRange text) <$> i.stx[2].getRange?
targetUri := modUri
targetRange := range
targetSelectionRange := range
@ -125,36 +124,47 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
return #[ll]
return #[]
if let Info.ofTermInfo ti := i then
let mut expr := ti.expr
if kind == type then
expr ← ci.runMetaM i.lctx do
return Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
match expr with
| Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
| Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
| _ => pure ()
if let Info.ofFieldInfo fi := i then
if kind == type then
let expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType fi.val)
if let some n := expr.getAppFn.constName? then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
else
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName
if let Info.ofCommandInfo ⟨`import, _⟩ := i then
if kind == definition || kind == declaration then
return ← ci.runMetaM i.lctx <| locationLinksFromImport i
-- If other go-tos fail, we try to show the elaborator or parser
if let some ei := i.toElabInfo? 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 GoToKind in
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
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := pure #[]) fun snap => do
if let some (ci, i) := snap.infoTree.hoverableInfoAt? (includeStop := true /- #767 -/) hoverPos then
if let Info.ofTermInfo ti := i then
let mut expr := ti.expr
if kind == type then
expr ← ci.runMetaM i.lctx do
return Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
match expr with
| Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
| Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder snap.infoTree i id
| _ => pure ()
if let Info.ofFieldInfo fi := i then
if kind == type then
let expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType fi.val)
if let some n := expr.getAppFn.constName? then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
else
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName
if let Info.ofCommandInfo ⟨`import, _⟩ := i then
if kind == definition || kind == declaration then
return ← ci.runMetaM i.lctx <| locationLinksFromImport i
-- If other go-tos fail, we try to show the elaborator or parser
if let some ei := i.toElabInfo? 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 #[]
locationLinksOfInfo kind ci i snap.infoTree
else return #[]
open RequestM in
def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Widget.InteractiveGoals)) := do

12
src/Lean/Server/FileWorker/WidgetRequests.lean
View file

@ -102,4 +102,16 @@ builtin_initialize
(Array InteractiveDiagnostic)
getInteractiveDiagnostics
builtin_initialize
registerBuiltinRpcProcedure
`Lean.Widget.getGoToLocation
(WithRpcRef InfoWithCtx × FileWorker.GoToKind)
(Option Lsp.Location)
fun (⟨i⟩, kind) => RequestM.asTask do
let ls ← FileWorker.locationLinksOfInfo kind i.ctx i.info
return ls.back?.map fun lnk => {
uri := lnk.targetUri
range := lnk.targetSelectionRange
}
end Lean.Widget