Representing collected and deduplicated definitions and usages

structure Lean.Server.Reference : Type

• ident : Lean.Lsp.RefIdent
• aliases : Array Lean.Lsp.RefIdent

  FVarIds that are logically identical to this reference

• range : Lean.Lsp.Range
• stx : Lean.Syntax
• ci : Lean.Elab.ContextInfo
• info : Lean.Elab.Info
• isBinder : Bool

structure Lean.Server.RefInfo : Type

• definition : Option Lean.Server.Reference
• usages : Array Lean.Server.Reference

def Lean.Server.RefInfo.empty : Lean.Server.RefInfo

def Lean.Server.RefInfo.addRef : Lean.Server.RefInfo → Lean.Server.Reference → Lean.Server.RefInfo

instance Lean.Server.RefInfo.instCoeRefInfoRefInfo : Coe Lean.Server.RefInfo Lean.Lsp.RefInfo

def Lean.Server.ModuleRefs : Type

def Lean.Server.ModuleRefs.addRef (self : Lean.Server.ModuleRefs) (ref : Lean.Server.Reference) : Lean.Server.ModuleRefs

instance Lean.Server.ModuleRefs.instCoeModuleRefsModuleRefs : Coe Lean.Server.ModuleRefs Lean.Lsp.ModuleRefs

def Lean.Lsp.RefInfo.empty : Lean.Lsp.RefInfo

def Lean.Lsp.RefInfo.merge (a : Lean.Lsp.RefInfo) (b : Lean.Lsp.RefInfo) : Lean.Lsp.RefInfo

def Lean.Lsp.RefInfo.contains (self : Lean.Lsp.RefInfo) (pos : Lean.Lsp.Position) : Bool

def Lean.Lsp.RefInfo.contains.contains (range : Lean.Lsp.Range) (pos : Lean.Lsp.Position) : Bool

def Lean.Lsp.ModuleRefs.findAt (self : Lean.Lsp.ModuleRefs) (pos : Lean.Lsp.Position) : Array Lean.Lsp.RefIdent

structure Lean.Server.Ilean : Type

• version : Nat
• module : Lake.Name
• references : Lean.Lsp.ModuleRefs

Content of individual .ilean files

instance Lean.Server.instFromJsonIlean : Lean.FromJson Lean.Server.Ilean

instance Lean.Server.instToJsonIlean : Lean.ToJson Lean.Server.Ilean

def Lean.Server.Ilean.load (path : Lake.FilePath) : IO Lean.Server.Ilean

Collecting and deduplicating definitions and usages

def Lean.Server.identOf : Lean.Elab.Info → Option (Lean.Lsp.RefIdent × Bool)

def Lean.Server.findReferences (text : Lean.FileMap) (trees : Array Lean.Elab.InfoTree) : Array Lean.Server.Reference

def Lean.Server.combineFvars (trees : Array Lean.Elab.InfoTree) (refs : Array Lean.Server.Reference) : Array Lean.Server.Reference

The FVarIds of a function parameter in the function's signature and body differ. However, they have TermInfo nodes with binder := true in the exact same position. Moreover, macros such as do-reassignment x := e may create chains of variable definitions where a helper definition overlaps with a use of a variable.

This function changes every such group to use a single FVarId (the head of the chain/DAG) and gets rid of duplicate definitions.

partial def Lean.Server.combineFvars.findCanonicalBinder (idMap : Lean.HashMap Lean.FVarId Lean.FVarId) (id : Lean.FVarId) : Lean.FVarId

def Lean.Server.combineFvars.applyIdMap : Lean.HashMap Lean.FVarId Lean.FVarId → Lean.Lsp.RefIdent → Lean.Lsp.RefIdent

def Lean.Server.combineFvars.buildIdMap (trees : Array Lean.Elab.InfoTree) (refs : Array Lean.Server.Reference) (posMap : Lean.HashMap Lean.Lsp.Range Lean.FVarId) : Lean.HashMap Lean.FVarId Lean.FVarId

def Lean.Server.combineFvars.insertIdMap (id : Lean.FVarId) (baseId : Lean.FVarId) : StateT (Lean.HashMap Lean.FVarId Lean.FVarId) Id Unit

def Lean.Server.dedupReferences (refs : Array Lean.Server.Reference) (allowSimultaneousBinderUse : optParam Bool false) : Array Lean.Server.Reference

def Lean.Server.findModuleRefs (text : Lean.FileMap) (trees : Array Lean.Elab.InfoTree) (localVars : optParam Bool true) (allowSimultaneousBinderUse : optParam Bool false) : Lean.Server.ModuleRefs

Collecting and maintaining reference info from different sources

structure Lean.Server.References : Type

• ileans : Lean.HashMap Lake.Name (Lake.FilePath × Lean.Lsp.ModuleRefs)

  References loaded from ilean files

• workers : Lean.HashMap Lake.Name (Nat × Lean.Lsp.ModuleRefs)

  References from workers, overriding the corresponding ilean files

def Lean.Server.References.empty : Lean.Server.References

def Lean.Server.References.addIlean (self : Lean.Server.References) (path : Lake.FilePath) (ilean : Lean.Server.Ilean) : Lean.Server.References

def Lean.Server.References.removeIlean (self : Lean.Server.References) (path : Lake.FilePath) : Lean.Server.References

def Lean.Server.References.updateWorkerRefs (self : Lean.Server.References) (name : Lake.Name) (version : Nat) (refs : Lean.Lsp.ModuleRefs) : Lean.Server.References

def Lean.Server.References.finalizeWorkerRefs (self : Lean.Server.References) (name : Lake.Name) (version : Nat) (refs : Lean.Lsp.ModuleRefs) : Lean.Server.References

def Lean.Server.References.removeWorkerRefs (self : Lean.Server.References) (name : Lake.Name) : Lean.Server.References

def Lean.Server.References.allRefs (self : Lean.Server.References) : Lean.HashMap Lake.Name Lean.Lsp.ModuleRefs

def Lean.Server.References.findAt (self : Lean.Server.References) (module : Lake.Name) (pos : Lean.Lsp.Position) : Array Lean.Lsp.RefIdent

def Lean.Server.References.referringTo (self : Lean.Server.References) (identModule : Lake.Name) (ident : Lean.Lsp.RefIdent) (srcSearchPath : Lean.SearchPath) (includeDefinition : optParam Bool true) : IO (Array Lean.Lsp.Location)

def Lean.Server.References.definitionOf? (self : Lean.Server.References) (ident : Lean.Lsp.RefIdent) (srcSearchPath : Lean.SearchPath) : IO (Option Lean.Lsp.Location)

def Lean.Server.References.definitionsMatching {α : Type} (self : Lean.Server.References) (srcSearchPath : Lean.SearchPath) (filter : Lake.Name → Option α) (maxAmount? : optParam (Option Nat) none) : IO (Array (α × Lean.Lsp.Location))