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

Equations

• Lean.Server.RefInfo.empty = { definition := none, usages := #[] }

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.RefInfo.toLspRefInfo (i : Lean.Server.RefInfo) : IO Lean.Lsp.RefInfo

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.ModuleRefs : Type

Equations

• Lean.Server.ModuleRefs = Lean.HashMap Lean.Lsp.RefIdent Lean.Server.RefInfo

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

Equations

• Lean.Server.ModuleRefs.addRef self ref = let refInfo := Lean.HashMap.findD self ref.ident Lean.Server.RefInfo.empty; Lean.HashMap.insert self ref.ident (Lean.Server.RefInfo.addRef refInfo ref)

def Lean.Server.ModuleRefs.toLspModuleRefs (refs : Lean.Server.ModuleRefs) : IO Lean.Lsp.ModuleRefs

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Lsp.RefInfo.empty = { definition? := none, usages := #[] }

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

Equations

• Lean.Lsp.RefInfo.merge a b = { definition? := Option.orElse b.definition? fun (x : Unit) => a.definition?, usages := Array.append a.usages b.usages }

def Lean.Lsp.RefInfo.findRange? (self : Lean.Lsp.RefInfo) (pos : Lean.Lsp.Position) (includeStop : optParam Bool false) : Option Lean.Lsp.Range

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.RefInfo.findRange?.contains (includeStop : optParam Bool false) (range : Lean.Lsp.Range) (pos : Lean.Lsp.Position) : Bool

Equations

• Lean.Lsp.RefInfo.findRange?.contains includeStop range pos = (decide (range.start ≤ pos) && if includeStop = true then decide (pos ≤ range.end) else decide (pos < range.end))

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

Equations

• Lean.Lsp.RefInfo.contains self pos includeStop = Id.run (Option.isSome (Lean.Lsp.RefInfo.findRange? self pos includeStop))

def Lean.Lsp.ModuleRefs.findAt (self : Lean.Lsp.ModuleRefs) (pos : Lean.Lsp.Position) (includeStop : optParam Bool false) : Array Lean.Lsp.RefIdent

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ModuleRefs.findRange? (self : Lean.Lsp.ModuleRefs) (pos : Lean.Lsp.Position) (includeStop : optParam Bool false) : Option Lean.Lsp.Range

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.Ilean : Type

Content of individual .ilean files

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

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

Equations

• Lean.Server.instFromJsonIlean = { fromJson? := Lean.Server.fromJsonIlean✝ }

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

Equations

• Lean.Server.instToJsonIlean = { toJson := Lean.Server.toJsonIlean✝ }

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

Equations

• One or more equations did not get rendered due to their size.

Collecting and deduplicating definitions and usages

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

There are several different identifiers that should be considered equal for the purpose of finding all references of an identifier:

• FVarIds of a function parameter in the function's signature and body
• Chains of helper definitions like those created for do-reassignment x := e
• Overlapping definitions like those defined by where declarations that define both an FVar (for local usage) and a constant (for non-local usage)
• Identifiers connected by FVarAliasInfo such as variables before and after match generalization

In the first three cases that are not explicitly denoted as aliases with an FVarAliasInfo, the corresponding References have the exact same range. This function finds all definitions that have the exact same range as another definition or usage and collapses them into a single identifier. It also collapses identifiers connected by an FVarAliasInfo. When collapsing identifiers, it prefers using a RefIdent.const name over a RefIdent.fvar id for all identifiers that are being collapsed into one.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.combineIdents.useConstRepresentatives (idMap : Lean.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent) : Lean.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.combineIdents.findCanonicalRepresentative (idMap : Lean.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent) (id : Lean.Lsp.RefIdent) : Lean.Lsp.RefIdent

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.combineIdents.insertIdMap (id : Lean.Lsp.RefIdent) (baseId : Lean.Lsp.RefIdent) : StateT (Lean.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent) Id Unit

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Server.References.empty = { ileans := Lean.HashMap.empty, workers := Lean.HashMap.empty }

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

Equations

• Lean.Server.References.addIlean self path ilean = { ileans := Lean.HashMap.insert self.ileans ilean.module (path, ilean.references), workers := self.workers }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Server.References.removeWorkerRefs self name = { ileans := self.ileans, workers := Lean.HashMap.erase self.workers name }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.References.findRange? (self : Lean.Server.References) (module : Lake.Name) (pos : Lean.Lsp.Position) (includeStop : optParam Bool false) : Option Lean.Lsp.Range

Equations

• Lean.Server.References.findRange? self module pos includeStop = do let refs ← Lean.HashMap.find? (Lean.Server.References.allRefs self) module Lean.Lsp.ModuleRefs.findRange? refs pos includeStop

structure Lean.Server.References.DocumentRefInfo : Type

• location : Lean.Lsp.Location
• parentInfo? : Option Lean.Lsp.RefInfo.ParentDecl

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.Server.References.DocumentRefInfo)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.