feat: add call hierarchy support

RELEASES.md

@@ -192,7 +192,9 @@ example : x + foo 2 = 12 + x := by
   ought to be applied to multiple functions, the `decreasing_by` clause has to
   be repeated at each of these functions.
 
-* Modify `InfoTree.context` to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the `InfoTree` manually instead of going through the functions in `InfoUtils.lean`, as well as those manually creating and saving `InfoTree`s. See https://github.com/leanprover/lean4/pull/3159 for how to migrate your code.
+* Modify `InfoTree.context` to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the `InfoTree` manually instead of going through the functions in `InfoUtils.lean`, as well as those manually creating and saving `InfoTree`s. See [PR #3159](https://github.com/leanprover/lean4/pull/3159) for how to migrate your code.
+
+* Add language server support for [call hierarchy requests](https://devblogs.microsoft.com/cppblog/c-extension-in-vs-code-1-16-release-call-hierarchy-more/) ([PR #3082](https://github.com/leanprover/lean4/pull/3082)). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again.
 
 
 v4.5.0

src/Lean/Data/HashMap.lean

@@ -227,3 +227,17 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
       match m.find? p.fst with
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
+end Lean.HashMap
+
+/--
+Groups all elements `x`, `y` in `xs` with `key x == key y` into the same array
+`(xs.groupByKey key).find! (key x)`. Groups preserve the relative order of elements in `xs`.
+-/
+def Array.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : Array β)
+    : Lean.HashMap α (Array β) := Id.run do
+  let mut groups := ∅
+  for x in xs do
+    let group := groups.findD (key x) #[]
+    groups := groups.erase (key x) -- make `group` referentially unique
+    groups := groups.insert (key x) (group.push x)
+  return groups

src/Lean/Data/Lsp/Capabilities.lean

@@ -74,6 +74,7 @@ structure ServerCapabilities where
   declarationProvider       : Bool                           := false
   typeDefinitionProvider    : Bool                           := false
   referencesProvider        : Bool                           := false
+  callHierarchyProvider     : Bool                           := false
   renameProvider?           : Option RenameOptions           := none
   workspaceSymbolProvider   : Bool                           := false
   foldingRangeProvider      : Bool                           := false

src/Lean/Data/Lsp/Internal.lean

@@ -8,6 +8,8 @@ Authors: Joscha Mennicken
 import Lean.Expr
 import Lean.Data.Lsp.Basic
 
+set_option linter.missingDocs true -- keep it documented
+
 /-! This file contains types for communication between the watchdog and the
 workers. These messages are not visible externally to users of the LSP server.
 -/
@@ -17,17 +19,27 @@ namespace Lean.Lsp
 /-! Most reference-related types have custom FromJson/ToJson implementations to
 reduce the size of the resulting JSON. -/
 
+/--
+Identifier of a reference.
+-/
 inductive RefIdent where
+  /-- Named identifier. These are used in all references that are globally available. -/
   | const : Name → RefIdent
-  | fvar : FVarId → RefIdent
+  /-- Unnamed identifier. These are used for all local references. -/
+  | fvar  : FVarId → RefIdent
   deriving BEq, Hashable, Inhabited
 
 namespace RefIdent
 
+/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
 def toString : RefIdent → String
   | RefIdent.const n => s!"c:{n}"
   | RefIdent.fvar id => s!"f:{id.name}"
 
+/--
+Converts the string representation of a reference identifier back to a reference identifier.
+The string representation must have been created by `RefIdent.toString`.
+-/
 def fromString (s : String) : Except String RefIdent := do
   let sPrefix := s.take 2
   let sName := s.drop 2
@@ -43,33 +55,92 @@ def fromString (s : String) : Except String RefIdent := do
     | "f:" => return RefIdent.fvar <| FVarId.mk name
     | _ => throw "string must start with 'c:' or 'f:'"
 
+instance : FromJson RefIdent where
+  fromJson?
+    | (s : String) => fromString s
+    | j => Except.error s!"expected a String, got {j}"
+
+instance : ToJson RefIdent where
+  toJson ident := toString ident
+
 end RefIdent
 
+/-- Information about the declaration surrounding a reference. -/
+structure RefInfo.ParentDecl where
+  /-- Name of the declaration surrounding a reference. -/
+  name           : Name
+  /-- Range of the declaration surrounding a reference. -/
+  range          : Lsp.Range
+  /-- Selection range of the declaration surrounding a reference. -/
+  selectionRange : Lsp.Range
+  deriving ToJson
+
+/--
+Denotes the range of a reference, as well as the parent declaration of the reference.
+If the reference is itself a declaration, then it contains no parent declaration.
+-/
+structure RefInfo.Location where
+  /-- Range of the reference. -/
+  range       : Lsp.Range
+  /-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
+  parentDecl? : Option RefInfo.ParentDecl
+
+/-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
 structure RefInfo where
-  definition : Option Lsp.Range
-  usages : Array Lsp.Range
+  /-- Definition site of the reference. May be `none` when we cannot find a definition site. -/
+  definition? : Option RefInfo.Location
+  /-- Usage sites of the reference. -/
+  usages      : Array RefInfo.Location
 
 instance : ToJson RefInfo where
   toJson i :=
     let rangeToList (r : Lsp.Range) : List Nat :=
       [r.start.line, r.start.character, r.end.line, r.end.character]
+    let parentDeclToList (d : RefInfo.ParentDecl) : List Json :=
+      let name := d.name.toString |> toJson
+      let range := rangeToList d.range |>.map toJson
+      let selectionRange := rangeToList d.selectionRange |>.map toJson
+      [name] ++ range ++ selectionRange
+    let locationToList (l : RefInfo.Location) : List Json :=
+      let range := rangeToList l.range |>.map toJson
+      let parentDecl := l.parentDecl?.map parentDeclToList |>.getD []
+      range ++ parentDecl
     Json.mkObj [
-      ("definition", toJson $ i.definition.map rangeToList),
-      ("usages", toJson $ i.usages.map rangeToList)
+      ("definition", toJson $ i.definition?.map locationToList),
+      ("usages", toJson $ i.usages.map locationToList)
     ]
 
 instance : FromJson RefInfo where
   fromJson? j := do
-    let listToRange (l : List Nat) : Except String Lsp.Range := match l with
+    let toRange : List Nat → Except String Lsp.Range
       | [sLine, sChar, eLine, eChar] => pure ⟨⟨sLine, sChar⟩, ⟨eLine, eChar⟩⟩
-      | _ => throw s!"Expected list of length 4, not {l.length}"
-    let definition ← j.getObjValAs? (Option $ List Nat) "definition"
-    let definition ← match definition with
+      | l => throw s!"Expected list of length 4, not {l.length}"
+    let toParentDecl (a : Array Json) : Except String RefInfo.ParentDecl := do
+      let name := String.toName <| ← fromJson? a[0]!
+      let range ← a[1:5].toArray.toList |>.mapM fromJson?
+      let range ← toRange range
+      let selectionRange ← a[5:].toArray.toList |>.mapM fromJson?
+      let selectionRange ← toRange selectionRange
+      return ⟨name, range, selectionRange⟩
+    let toLocation (l : List Json) : Except String RefInfo.Location := do
+      let l := l.toArray
+      if l.size != 4 && l.size != 13 then
+        .error "Expected list of length 4 or 13, not {l.size}"
+      let range ← l[:4].toArray.toList |>.mapM fromJson?
+      let range ← toRange range
+      if l.size == 13 then
+        let parentDecl ← toParentDecl l[4:].toArray
+        return ⟨range, parentDecl⟩
+      else
+        return ⟨range, none⟩
+
+    let definition? ← j.getObjValAs? (Option $ List Json) "definition"
+    let definition? ← match definition? with
       | none => pure none
-      | some list => some <$> listToRange list
-    let usages ← j.getObjValAs? (Array $ List Nat) "usages"
-    let usages ← usages.mapM listToRange
-    pure { definition, usages }
+      | some list => some <$> toLocation list
+    let usages ← j.getObjValAs? (Array $ List Json) "usages"
+    let usages ← usages.mapM toLocation
+    pure { definition?, usages }
 
 /-- References from a single module/file -/
 def ModuleRefs := HashMap RefIdent RefInfo
@@ -88,7 +159,8 @@ instance : FromJson ModuleRefs where
 Contains the file's definitions and references. -/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
-  version : Nat
+  version    : Nat
+  /-- All references for the file. -/
   references : ModuleRefs
   deriving FromJson, ToJson