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.
- 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
Definition and usages of an identifier within a single module.
All usage
Reference
s of the identifier in a single module.
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
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
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
Instances For
Find all identifiers in self
with a reference in this module that contains pos
in its range.
Equations
Instances For
Finds the first range in self
that contains pos
.
Equations
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.
- references : Lsp.ModuleRefs
All references of this module.
Instances For
Reads and parses the .ilean file at path
.
Equations
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
Instances For
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 aftermatch
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
Instances For
Equations
Instances For
Equations
Instances For
Equations
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
Instances For
Finds all references in trees
and deduplicates the result.
See dedupReferences
and combineIdents
.
Equations
Instances For
Collecting and maintaining reference info from different sources #
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.
- refs : Lsp.ModuleRefs
Reference information from this ILean.
Instances For
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.
- refs : Lsp.ModuleRefs
References provided by the worker.
Instances For
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
Instances For
Removes the ilean file data at path
from self
.
Equations
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
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
Instances For
Erases all worker references in self
for the worker managing name
.
Equations
Instances For
All references for a module. 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
Instances For
Gets the references for mod
.
The current references in a file worker take precedence over those in .ilean files.
Equations
Instances For
Yields all references in self
for ident
, as well as the DocumentUri
that each
reference occurs in.
Equations
Instances For
Yields all references in module
at pos
.
Equations
Instances For
Yields the first reference in module
at pos
.
Equations
Instances For
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
Yields locations and parent declaration for all references referring to ident
.
Equations
Instances For
Yields the definition location of ident
.
Equations
Instances For
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
Yields all definitions matching the given filter
.