Documentation

Lean.Server.References

Representing collected and deduplicated definitions and usages #

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

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

            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
                    • a.merge b = { definition? := b.definition?.orElse fun (x : Unit) => a.definition?, usages := a.usages.append b.usages }
                    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

                          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

                            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

                              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 : Lake.Name

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

                                • references : Lean.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
                                    • One or more equations did not get rendered due to their size.
                                    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

                                                    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 : Lean.FileMap) (trees : Array Lean.Elab.InfoTree) (localVars : optParam Bool true) (allowSimultaneousBinderUse : optParam 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 #

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

                                                        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
                                                            • self.addIlean path ilean = { ileans := self.ileans.insert ilean.module (path, ilean.references), workers := self.workers }
                                                            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

                                                                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
                                                                    • self.removeWorkerRefs name = { ileans := self.ileans, workers := self.workers.erase name }
                                                                    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

                                                                        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

                                                                          Yields all references in module at pos.

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

                                                                            Yields the first reference in module at pos.

                                                                            Equations
                                                                            • self.findRange? module pos includeStop = do let refsself.allRefs[module]? refs.findRange? pos includeStop
                                                                            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
                                                                                    def Lean.Server.References.definitionsMatching {α : Type} (self : Lean.Server.References) (srcSearchPath : Lean.SearchPath) (filter : Lake.NameOption α) (maxAmount? : optParam (Option Nat) none) :

                                                                                    Yields all definitions matching the given filter.

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