# Representing collected and deduplicated definitions and usages #

source
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 }

Instances For

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

Instances For

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

Instances For

source
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 `Reference`s of the identifier in a single module.

Instances For

source
def Lean.Server.RefInfo.empty :
RefInfo

No definition, no usages.

Equations

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

Instances For

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

Instances For

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

Instances For

source
@[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

Instances For

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

Instances For

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

Instances For

source
def Lean.Lsp.RefInfo.empty :
RefInfo

No definition, no usages

Equations

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

Instances For

source
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 }

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
instance Lean.Server.instFromJsonIlean :
FromJson Ilean
Equations

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

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

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

Instances For

source
instance Lean.Server.instToJsonIlean :
ToJson Ilean
Equations

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

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

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

Instances For

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

Instances For

# Collecting and deduplicating definitions and usages #

source
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

Instances For

source
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

Instances For

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

Instances For

source
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:

- `FVarId`s 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 `Reference`s 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.

Instances For

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

Instances For

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

Instances For

# Collecting and maintaining reference info from different sources #

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

Instances For

source
instance Lean.Server.instInhabitedModuleImport :
Inhabited ModuleImport
Equations

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

source
def Lean.Server.instInhabitedModuleImport.default :
ModuleImport
Equations

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

Instances For

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

Instances For

source
@[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

Instances For

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

Instances For

source
instance Lean.Server.instEmptyCollectionDirectImports :
EmptyCollection DirectImports
Equations

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

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

Instances For

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

Instances For

source
@[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

Instances For

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

Instances For

source
@[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

Instances For

source
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

Instances For

source
def Lean.Server.instInhabitedReferences.default :
References
Equations

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

Instances For

source
instance Lean.Server.instInhabitedReferences :
Inhabited References
Equations

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

source
def Lean.Server.References.empty :
References

No ilean files, no information from workers.

Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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 }

Instances For

source
@[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

Instances For

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

Instances For

source
@[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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For