Documentation

Lean.Server.References

Representing collected and deduplicated definitions and usages #

Converts an Import to its LSP-internal representation.

Equations
Instances For

    Collects ImportInfo for all import statements in headerStx.

    Equations
    Instances For

      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.

      • Identifiers that are logically identical to this reference.

      • range : Lsp.Range

        Range where this reference occurs.

      • stx : Syntax

        Syntax of this reference.

      • 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

        Definition and usages of an identifier within a single module.

        Instances For

          No definition, no usages.

          Equations
          Instances For

            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

              Converts i to a JSON-serializable Lsp.RefInfo.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible, inline]

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

                Equations
                Instances For

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

                  Equations
                  Instances For

                    Converts refs to a JSON-serializable Lsp.ModuleRefs.

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

                      No definition, no usages

                      Equations
                      Instances For

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

                        Equations
                        Instances For

                          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
                            Equations
                            Instances For
                              def Lean.Lsp.RefInfo.contains (self : RefInfo) (pos : Position) (includeStop : Bool := false) :

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

                              Equations
                              Instances For
                                def Lean.Lsp.ModuleRefs.findAt (self : ModuleRefs) (pos : Position) (includeStop : Bool := false) :

                                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
                                  def Lean.Lsp.ModuleRefs.findRange? (self : ModuleRefs) (pos : Position) (includeStop : Bool := false) :

                                  Finds the first range in self that contains pos.

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

                                    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

                                      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 #

                                        Gets the name of the module that contains declName.

                                        Equations
                                        Instances For

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

                                          Equations
                                          Instances For

                                            Finds all references in trees.

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

                                              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.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def Lean.Server.dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse : Bool := false) :

                                                        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
                                                          def Lean.Server.findModuleRefs (text : FileMap) (trees : Array Elab.InfoTree) (localVars : Bool := true) (allowSimultaneousBinderUse : Bool := false) :

                                                          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 #

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

                                                            • module : Name

                                                              Module name of the module that is imported.

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

                                                            • Kind of meta annotation on this import.

                                                            Instances For
                                                              Equations

                                                              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
                                                                @[reducible, inline]

                                                                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
                                                                Instances For

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

                                                                  • Imports as they occurred in the module.

                                                                  • 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

                                                                    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

                                                                      Reference information from a loaded ILean file.

                                                                      Instances For
                                                                        @[reducible, inline]

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

                                                                        Equations
                                                                        Instances For

                                                                          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.

                                                                          • References provided by the worker.

                                                                          Instances For
                                                                            @[reducible, inline]

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

                                                                            Equations
                                                                            Instances For

                                                                              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

                                                                                No ilean files, no information from workers.

                                                                                Equations
                                                                                Instances For

                                                                                  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

                                                                                    Removes the ilean file data at path from self.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      def Lean.Server.References.updateWorkerImports (self : References) (name : Name) (moduleUri : Lsp.DocumentUri) (version : Nat) (directImports : Array Lsp.ImportInfo) :

                                                                                      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
                                                                                        def Lean.Server.References.updateWorkerRefs (self : References) (name : Name) (moduleUri : Lsp.DocumentUri) (version : Nat) (refs : Lsp.ModuleRefs) :

                                                                                        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

                                                                                          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

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

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[reducible, inline]

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

                                                                                              Equations
                                                                                              Instances For

                                                                                                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
                                                                                                  @[reducible, inline]

                                                                                                  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
                                                                                                  Instances For

                                                                                                    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

                                                                                                      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

                                                                                                        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

                                                                                                          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
                                                                                                            def Lean.Server.References.findAt (self : References) (module : Name) (pos : Lsp.Position) (includeStop : Bool := false) :

                                                                                                            Yields all references in module at pos.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              def Lean.Server.References.findRange? (self : References) (module : Name) (pos : Lsp.Position) (includeStop : Bool := false) :

                                                                                                              Yields the first reference in module at pos.

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                Location and parent declaration of a reference.

                                                                                                                Instances For

                                                                                                                  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

                                                                                                                    Yields the definition location of ident.

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

                                                                                                                      A match in References.definitionsMatching.

                                                                                                                      • mod : Name

                                                                                                                        Result of filterMapMod.

                                                                                                                      • URI for mod.

                                                                                                                      • ident : α

                                                                                                                        Result of filterMapIdent.

                                                                                                                      • range : Lsp.Range

                                                                                                                        Definition range of matched identifier.

                                                                                                                      Instances For
                                                                                                                        def Lean.Server.References.definitionsMatching {α : Type} (self : References) (filterMapIdent : NameOption α) (cancelTk? : Option IO.CancelToken := none) :

                                                                                                                        Yields all definitions matching the given filter.

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

                                                                                                                          Yields all imports that import the given requestedMod.

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