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.

instance Lean.Server.RefInfo.instCoeRefInfoRefInfo : Coe Lean.Server.RefInfo 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)

instance Lean.Server.ModuleRefs.instCoeModuleRefsModuleRefs : Coe Lean.Server.ModuleRefs 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 => a.definition, usages := Array.append a.usages b.usages }

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

Equations

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

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

Equations

• Lean.Lsp.RefInfo.contains.contains range pos = (decide (range.start ≤ pos) && decide (pos < range.end))

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

Equations

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

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

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

Equations

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

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

Equations

• Lean.Server.combineFvars.applyIdMap x x = match x, x with | m, Lean.Lsp.RefIdent.fvar id => Lean.Lsp.RefIdent.fvar (Lean.Server.combineFvars.findCanonicalBinder m id) | x, ident => ident

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

Equations

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

def Lean.Server.combineFvars.insertIdMap (id : Lean.FVarId) (baseId : Lean.FVarId) : StateT (Lean.HashMap Lean.FVarId Lean.FVarId) 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) : Array Lean.Lsp.RefIdent

Equations

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

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)

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.Lsp.Location)

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.