Representing collected and deduplicated definitions and usages

def Lean.Server.ImportInfo.ofImport (i : Import) : Lsp.ImportInfo

Converts an Import to its LSP-internal representation.

Equations

• Lean.Server.ImportInfo.ofImport i = { module := i.module.toString, isPrivate := !i.isExported, isAll := i.importAll, isMeta := i.isMeta }

def Lean.Server.collectImports (headerStx : Elab.HeaderSyntax) : Array Lsp.ImportInfo

Collects ImportInfo for all import statements in headerStx.

Equations

• Lean.Server.collectImports headerStx = Array.map Lean.Server.ImportInfo.ofImport (Lean.Elab.headerToImports headerStx false)

structure Lean.Server.Reference : Type

Global reference. Used by the language server to figure out which identifiers refer to which other identifiers across the whole project.

• ident : Lsp.RefIdent

  Identifier of this reference.

• aliases : Array Lsp.RefIdent

  Identifiers that are logically identical to this reference.

• range : Lsp.Range

  Range where this reference occurs.

• stx : Syntax

  Syntax of this reference.

• ci : Elab.ContextInfo

  ContextInfo at the point of elaboration of this reference.

• info : Elab.Info

  Additional InfoTree information for this reference.

• isBinder : Bool

  Whether this reference declares ident.

structure Lean.Server.RefInfo : Type

Definition and usages of an identifier within a single module.

• definition : Option Reference

  Definition Reference of the identifier. Is equal to none if e.g. the definition is outside of the module where this RefInfo is used.

• usages : Array Reference

  All usage References of the identifier in a single module.

def Lean.Server.RefInfo.empty : RefInfo

No definition, no usages.

Equations

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

def Lean.Server.RefInfo.addRef (i : RefInfo) (ref : Reference) : RefInfo

Adds ref to i. If i has no definition and ref is a declaration, it becomes the definition. If i already has a definition and ref is also a declaration, it is not added to i. Otherwise, ref is added to i.usages.

Equations

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

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

Converts i to a JSON-serializable Lsp.RefInfo.

Equations

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

@[reducible, inline]

abbrev Lean.Server.ModuleRefs : Type

All references from within a module for all identifiers used in a single module.

Equations

• Lean.Server.ModuleRefs = Std.TreeMap Lean.Lsp.RefIdent Lean.Server.RefInfo compare

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

Adds ref to the RefInfo corresponding to ref.ident in self. See RefInfo.addRef.

Equations

• self.addRef ref = Std.TreeMap.insert self ref.ident ((Std.TreeMap.getD self ref.ident Lean.Server.RefInfo.empty).addRef ref)

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

Converts refs to a JSON-serializable Lsp.ModuleRefs.

Equations

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

def Lean.Lsp.RefInfo.empty : RefInfo

No definition, no usages

Equations

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

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

Combines the usages of a and b and prefers the definition? of b over that of a.

Equations

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

def Lean.Lsp.RefInfo.findReferenceLocation? (self : RefInfo) (pos : Position) (includeStop : Bool := false) : Option Location

Finds the first definition or usage in self where the RefInfo.Location.range contains the given pos. The includeStop parameter can be used to toggle between closed-interval and half-open-interval behavior for the range. Closed-interval behavior matches the expectation of VSCode when selecting an identifier at a cursor position (see #767).

Equations

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

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

Checks whether any of the ranges in self.definition? or self.usages contains pos.

Equations

• self.contains pos includeStop = Id.run (self.findReferenceLocation? pos includeStop).isSome

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

Find all identifiers in self with a reference in this module that contains pos in its range.

Equations

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

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

Finds the first range in self that contains pos.

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

  Version number of the ilean format.

• module : Name

  Name of the module that this ilean data has been collected for.

• directImports : Array Lsp.ImportInfo

  Direct imports of the module.

• references : Lsp.ModuleRefs

  All references of this module.

instance Lean.Server.instFromJsonIlean : FromJson Ilean

Equations

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

def Lean.Server.instFromJsonIlean.fromJson : Json → Except String Ilean

Equations

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

instance Lean.Server.instToJsonIlean : ToJson Ilean

Equations

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

def Lean.Server.instToJsonIlean.toJson : Ilean → Json

Equations

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

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

Reads and parses the .ilean file at path.

Equations

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

Collecting and deduplicating definitions and usages

def Lean.Server.getModuleContainingDecl? (env : Environment) (declName : Name) : Option Name

Gets the name of the module that contains declName.

Equations

• Lean.Server.getModuleContainingDecl? env declName = match env.getModuleIdxFor? declName with | some modIdx => env.allImportedModuleNames[modIdx]? | x => some env.header.mainModule

def Lean.Server.identOf (ci : Elab.ContextInfo) (i : Elab.Info) : Option (Lsp.RefIdent × Bool)

Determines the RefIdent for the Info i of an identifier in module and whether it is a declaration.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.identOf ci i = none

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

Finds all references in trees.

Equations

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

def Lean.Server.combineIdents (trees : Array Elab.InfoTree) (refs : Array Reference) : Array 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.dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse : Bool := false) : Array Reference

Groups refs by identifier and range s.t. references with the same identifier and range are added to the aliases of the representative of the group. Yields to separate groups for declaration and usages if allowSimultaneousBinderUse is set.

Equations

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

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

Finds all references in trees and deduplicates the result. See dedupReferences and combineIdents.

Equations

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

Collecting and maintaining reference info from different sources

structure Lean.Server.ModuleImport : Type

Represents a direct import of a module in the references data structure.

• module : Name

  Module name of the module that is imported.

• uri : Lsp.DocumentUri

  URI of the module that is imported.

• isAll : Bool

  Whether the all flag is set on this import.

• isPrivate : Bool

  Whether the private flag is set on this import.

• metaKind : Lsp.LeanImportMetaKind

  Kind of meta annotation on this import.

instance Lean.Server.instInhabitedModuleImport : Inhabited ModuleImport

Equations

• Lean.Server.instInhabitedModuleImport = { default := Lean.Server.instInhabitedModuleImport.default }

def Lean.Server.instInhabitedModuleImport.default : ModuleImport

Equations

• Lean.Server.instInhabitedModuleImport.default = { module := default, uri := default, isAll := default, isPrivate := default, metaKind := default }

def Lean.Server.ModuleImport.collapseIdenticalImports? (identicalImports : Array ModuleImport) : Option ModuleImport

Reduces identicalImports with the same module name by merging their flags. Yields none if identicalImports is empty or identicalImports contains an import that has a name or uri that is not identical to the others.

Equations

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

@[reducible, inline]

abbrev Lean.Server.ModuleImportIndex : Type

Index that allows efficiently looking up the imports of a module by module name. Since the same module can be imported multiple times with different attributes, each module name maps to an array of imports.

Equations

• Lean.Server.ModuleImportIndex = Std.TreeMap Lean.Name (Array Lean.Server.ModuleImport) Lean.Name.quickCmp

structure Lean.Server.DirectImports : Type

Direct imports of a module, containing an ordered representation and an index for fast lookups.

• ordered : Array ModuleImport

  Imports as they occurred in the module.

• index : ModuleImportIndex

  Index that allows efficiently looking up the imports of a module by module name. Since the same module can be imported multiple times with different attributes, each module name maps to an array of imports.

instance Lean.Server.instEmptyCollectionDirectImports : EmptyCollection DirectImports

Equations

• Lean.Server.instEmptyCollectionDirectImports = { emptyCollection := { ordered := #[], index := ∅ } }

def Lean.Server.DirectImports.convertImportInfos (infos : Array Lsp.ImportInfo) : IO DirectImports

Converts a list of LSP module imports to the module imports of the references data structure. Removes all imports for which we cannot resolve the corresponding DocumentUri.

Equations

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

structure Lean.Server.LoadedILean : Type

Reference information from a loaded ILean file.

• moduleUri : Lsp.DocumentUri

  URI of the module of this ILean.

• ileanPath : System.FilePath

  Path to the ILean file.

• directImports : DirectImports

  Direct imports of the module of this ILean.

• refs : Lsp.ModuleRefs

  Reference information from this ILean.

@[reducible, inline]

abbrev Lean.Server.ILeanMap : Type

Paths and module references for every module name. Loaded from .ilean files.

Equations

• Lean.Server.ILeanMap = Std.TreeMap Lean.Name Lean.Server.LoadedILean Lean.Name.quickCmp

structure Lean.Server.TransientWorkerILean : Type

Transient reference information from a file worker. We track this information so that we have up-to-date reference information before a file has been built.

• moduleUri : Lsp.DocumentUri

  URI of the module that the file worker is associated with.

• version : Nat

  Document version for which these references have been collected.

• directImports : DirectImports

  Direct imports of the module that the file worker is associated with.

• refs : Lsp.ModuleRefs

  References provided by the worker.

@[reducible, inline]

abbrev Lean.Server.WorkerRefMap : Type

Document versions and module references for every module name. Loaded from the current state in a file worker.

Equations

• Lean.Server.WorkerRefMap = Std.TreeMap Lean.Name Lean.Server.TransientWorkerILean Lean.Name.quickCmp

structure Lean.Server.References : Type

References from ilean files and current ilean information from file workers.

• ileans : ILeanMap

  References loaded from ilean files

• workers : WorkerRefMap

  References from workers, overriding the corresponding ilean files

def Lean.Server.instInhabitedReferences.default : References

Equations

• Lean.Server.instInhabitedReferences.default = { ileans := default, workers := default }

instance Lean.Server.instInhabitedReferences : Inhabited References

Equations

• Lean.Server.instInhabitedReferences = { default := Lean.Server.instInhabitedReferences.default }

def Lean.Server.References.empty : References

No ilean files, no information from workers.

Equations

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

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

Adds the contents of an ilean file ilean at path to self.

Equations

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

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

Removes the ilean file data at path from self.

Equations

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

def Lean.Server.References.updateWorkerImports (self : References) (name : Name) (moduleUri : Lsp.DocumentUri) (version : Nat) (directImports : Array Lsp.ImportInfo) : IO References

Replaces the direct imports of a worker for the module name in self with a new set of direct imports.

Equations

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

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

Updates the worker references in self with the refs of the worker managing the module name. Replaces the current references with refs if version is newer than the current version managed in refs and otherwise merges the reference data if version is equal to the current version.

Equations

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

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

Replaces the worker references in self with the refs of the worker managing the module name if version is newer than the current version managed in refs.

Equations

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

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

Erases all worker references in self for the worker managing name.

Equations

• self.removeWorkerRefs name = { ileans := self.ileans, workers := Std.TreeMap.erase self.workers name }

@[reducible, inline]

abbrev Lean.Server.References.AllRefsMap : Type

Map from each module to all of its references. The current references in a file worker take precedence over those in .ilean files.

Equations

• Lean.Server.References.AllRefsMap = Std.TreeMap Lean.Name (Lean.Lsp.DocumentUri × Lean.Lsp.ModuleRefs) Lean.Name.quickCmp

def Lean.Server.References.allRefs (self : References) : AllRefsMap

Yields a map from all modules to all of their references.

Equations

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

@[reducible, inline]

abbrev Lean.Server.References.AllDirectImportsMap : Type

Map from each module to all of its direct imports. The current references in a file worker take precedence over those in .ilean files.

Equations

• Lean.Server.References.AllDirectImportsMap = Std.TreeMap Lean.Name (Lean.Lsp.DocumentUri × Lean.Server.DirectImports) Lean.Name.quickCmp

def Lean.Server.References.allDirectImports (self : References) : AllDirectImportsMap

Yields a map from all modules to all of their direct imports.

Equations

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

def Lean.Server.References.getModuleRefs? (self : References) (mod : Name) : Option (Lsp.DocumentUri × Lsp.ModuleRefs)

Gets the references for mod. The current references in a file worker take precedence over those in .ilean files.

Equations

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

def Lean.Server.References.getDirectImports? (self : References) (mod : Name) : Option DirectImports

Gets the direct imports of mod. The current imports in a file worker take precedence over those in .ilean files.

Equations

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

def Lean.Server.References.allRefsFor (self : References) (ident : Lsp.RefIdent) : Array (Lsp.DocumentUri × Name × Lsp.RefInfo)

Yields all references in self for ident, as well as the DocumentUri that each reference occurs in.

Equations

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

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

Yields all references in module at pos.

Equations

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

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

Yields the first reference in module at pos.

Equations

• self.findRange? module pos includeStop = do let __discr ← self.getModuleRefs? module match __discr with | (fst, refs) => refs.findRange? pos includeStop

structure Lean.Server.References.DocumentRefInfo : Type

Location and parent declaration of a reference.

• location : Lsp.Location

  Location of the reference.

• module : Name

  Module name of the reference.

• parentInfo? : Option Lsp.RefInfo.ParentDecl

  Parent declaration of the reference.

def Lean.Server.References.referringTo (self : References) (ident : Lsp.RefIdent) (includeDefinition : Bool := true) : Array DocumentRefInfo

Yields locations and parent declaration for all references referring to ident.

Equations

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

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

Yields the definition location of ident.

Equations

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

structure Lean.Server.References.MatchedDefinition (α : Type) : Type

A match in References.definitionsMatching.

• mod : Name

  Result of filterMapMod.

• modUri : Lsp.DocumentUri

  URI for mod.

• ident : α

  Result of filterMapIdent.

• range : Lsp.Range

  Definition range of matched identifier.

def Lean.Server.References.definitionsMatching {α : Type} (self : References) (filterMapIdent : Name → Option α) (cancelTk? : Option IO.CancelToken := none) : BaseIO (Array (MatchedDefinition α))

Yields all definitions matching the given filter.

Equations

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

def Lean.Server.References.importedBy (self : References) (requestedMod : Name) : Array ModuleImport

Yields all imports that import the given requestedMod.

Equations

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