Skip to content

Commit

Permalink
feat: sorted call hierarchy items & no private prefix
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi committed Feb 23, 2024
1 parent 4d94147 commit 52d831f
Showing 3 changed files with 54 additions and 10 deletions.
16 changes: 15 additions & 1 deletion src/Lean/Data/Json/Basic.lean
Original file line number Diff line number Diff line change
@@ -8,14 +8,15 @@ prelude
import Init.Data.List.Control
import Init.Data.Range
import Init.Data.OfScientific
import Init.Data.Hashable
import Lean.Data.RBMap
namespace Lean

-- mantissa * 10^-exponent
structure JsonNumber where
mantissa : Int
exponent : Nat
deriving DecidableEq
deriving DecidableEq, Hashable

namespace JsonNumber

@@ -205,6 +206,19 @@ private partial def beq' : Json → Json → Bool
instance : BEq Json where
beq := beq'

private partial def hash' : Json → UInt64
| null => 11
| bool b => mixHash 13 <| hash b
| num n => mixHash 17 <| hash n
| str s => mixHash 19 <| hash s
| arr elems =>
mixHash 23 <| elems.foldl (init := 7) fun r a => mixHash r (hash' a)
| obj kvPairs =>
mixHash 29 <| kvPairs.fold (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v)

instance : Hashable Json where
hash := hash'

-- HACK(Marc): temporary ugliness until we can use RBMap for JSON objects
def mkObj (o : List (String × Json)) : Json :=
obj <| Id.run do
2 changes: 1 addition & 1 deletion src/Lean/Data/Lsp/LanguageFeatures.lean
Original file line number Diff line number Diff line change
@@ -274,7 +274,7 @@ structure CallHierarchyItem where
uri : DocumentUri
range : Range
selectionRange : Range
-- data? : Option unknown
data? : Option Json := none
deriving FromJson, ToJson, BEq, Hashable, Inhabited

structure CallHierarchyIncomingCallsParams where
46 changes: 38 additions & 8 deletions src/Lean/Server/Watchdog.lean
Original file line number Diff line number Diff line change
@@ -395,6 +395,17 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
result := result.append <| identRefs.map (·.location)
return result

/-- Used in `CallHierarchyItem.data?` to retain the full call hierarchy item name. -/
structure CallHierarchyItemData where
name : Name
deriving FromJson, ToJson

/--
Extracts the CallHierarchyItemData from `item.data?` and returns `none` if this is not possible.
-/
def CallHierarchyItemData.fromItem? (item : CallHierarchyItem) : Option CallHierarchyItemData := do
fromJson? (← item.data?) |>.toOption

private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSearchPath : SearchPath)
: IO (Option CallHierarchyItem) := do
let some ⟨definitionLocation, parentDecl?⟩ ← refs.definitionOf? ident srcSearchPath
@@ -406,23 +417,31 @@ private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSear
-- If `callHierarchyItemOf?` is used either on the name of a definition itself or e.g. an
-- `inductive` constructor, this is the right thing to do and using the parent decl is
-- the wrong thing to do.

-- Remove private header from name
let label := Lean.privateToUserName? definitionName |>.getD definitionName
return some {
name := definitionName.toString
name := label.toString
kind := SymbolKind.constant
uri := definitionLocation.uri
range := definitionLocation.range,
selectionRange := definitionLocation.range
data? := toJson { name := definitionName : CallHierarchyItemData }
}
| _ =>
let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl?
| return none

-- Remove private header from name
let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName

return some {
name := parentDeclName.toString
name := label.toString
kind := SymbolKind.constant
uri := definitionLocation.uri
range := parentDeclRange,
selectionRange := parentDeclSelectionRange
data? := toJson { name := parentDeclName : CallHierarchyItemData }
}

def handlePrepareCallHierarchy (p : CallHierarchyPrepareParams)
@@ -438,10 +457,13 @@ def handlePrepareCallHierarchy (p : CallHierarchyPrepareParams)
let idents := references.findAt module p.position (includeStop := true)

let items ← idents.filterMapM fun ident => callHierarchyItemOf? references ident srcSearchPath
return items
return items.qsort (·.name < ·.name)

def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams)
: ServerM (Array CallHierarchyIncomingCall) := do
let some itemData := CallHierarchyItemData.fromItem? p.item
| return #[]

let some path := fileUriToPath? p.item.uri
| return #[]

@@ -450,24 +472,29 @@ def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams)
| return #[]

let references ← (← read).references.get
let identRefs ← references.referringTo module (.const p.item.name.toName) srcSearchPath false
let identRefs ← references.referringTo module (.const itemData.name) srcSearchPath false

let incomingCalls := identRefs.filterMap fun ⟨location, parentDecl?⟩ => Id.run do

let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl?
| return none

-- Remove private header from name
let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName

return some {
«from» := {
name := parentDeclName.toString
name := label.toString
kind := SymbolKind.constant
uri := location.uri
range := parentDeclRange
selectionRange := parentDeclSelectionRange
data? := toJson { name := parentDeclName : CallHierarchyItemData }
}
fromRanges := #[location.range]
}

return collapseSameIncomingCalls incomingCalls
return collapseSameIncomingCalls incomingCalls |>.qsort (·.«from».name < ·.«from».name)

where

@@ -482,6 +509,9 @@ where

def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams)
: ServerM (Array CallHierarchyOutgoingCall) := do
let some itemData := CallHierarchyItemData.fromItem? p.item
| return #[]

let some path := fileUriToPath? p.item.uri
| return #[]

@@ -498,7 +528,7 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams)
let outgoingUsages := info.usages.filter fun usage => Id.run do
let some parentDecl := usage.parentDecl?
| return false
return p.item.name.toName == parentDecl.name
return itemData.name == parentDecl.name

let outgoingUsages := outgoingUsages.map (·.range)
if outgoingUsages.isEmpty then
@@ -513,7 +543,7 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams)

return some ⟨item, outgoingUsages⟩

return collapseSameOutgoingCalls items
return collapseSameOutgoingCalls items |>.qsort (·.to.name < ·.to.name)

where

0 comments on commit 52d831f

Please sign in to comment.