feat: sorted call hierarchy items & no private prefix (#3482)

Sorts call hierarchy items and strips the private prefix to make the
call hierarchy more readable.

src/Lean/Data/Json/Basic.lean

@@ -8,6 +8,7 @@ prelude
 import Init.Data.List.Control
 import Init.Data.Range
 import Init.Data.OfScientific
+import Init.Data.Hashable
 import Lean.Data.RBMap
 namespace Lean
 
@@ -15,7 +16,7 @@ namespace Lean
 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

src/Lean/Data/Lsp/LanguageFeatures.lean

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

src/Lean/Server/Watchdog.lean

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