Physlib.Meta.Basic

Given an array of arrays $A = [a_0, a_1, \dots, a_{n-1}]$ where each element $a_i$ is an array of elements of type $\alpha$, this function computes the total number of elements contained within all the inner arrays. Mathematically, it returns the sum of the sizes of the constituent arrays: $$\sum_{i=0}^{n-1} \text{size}(a_i)$$ This corresponds to the size of the resulting array if $A$ were to be flattened into a single-dimensional array.

Given a monad $m$ and a monadic predicate $p : \alpha \to m(\text{Bool})$, this function calculates the total number of elements in an array of arrays $A$ that satisfy $p$. Specifically, it iterates through each inner array in $A$, applies the monadic filter $p$ to its elements, and returns the sum of the sizes of the resulting filtered arrays within the monad $m$. This is equivalent to the size of the flattened array after element-wise filtering.

The function `Physlib.allImports` is an IO operation that retrieves an array containing all modules imported by the `Physlib` library, excluding the core `Init` module. It achieves this by locating the compiled object file (`.olean`) for the `Physlib` module, reading its metadata, and filtering the list of dependencies.

The function `Physlib.noImports` is an IO operation that returns a natural number representing the total number of modules (files) within the `Physlib` library. It calculates this value by determining the size of the array of all module imports associated with `Physlib`, excluding the core `Init` module.

Given a module import $imp$, this function retrieves an array containing the metadata (represented as `ConstantInfo` objects) for all constants, such as definitions, theorems, and axioms, defined within that module.

Given a Lean module import $imp$, this function retrieves an array of `ConstantInfo` objects representing the user-defined constants (such as definitions, theorems, and axioms) within that module. It filters the complete set of constants in the module to exclude internal names, auto-generated recursors (including `casesOn`, `recOn`, `noConfusion`, and `brecOn`), and specific syntax-related declarations such as `TensorTree.indexExprTT.quot`. The result is returned within the `CoreM` monad.

The function converts a Lean name $c$ into a system file path. It processes the name by splitting its string representation at each dot (".") to create a sequence of directory segments and then appends the ".lean" file extension.

For a given import $imp$, the function returns an $IO$ action that reads the content of the corresponding `.lean` source file and provides it as an array of strings, where each element represents a line from the file. It accomplishes this by converting the module name associated with $imp$ into a file path and retrieving the lines from that file.

The function converts a Lean name $c$ into a relative system file path. It does so by joining the current directory path `.` with the file path derived from the name $c$. Effectively, this transforms a hierarchical Lean identifier into a string representing the relative path of its corresponding `.lean` source file.

Given a Lean module name $c$ and a line number $n \in \mathbb{N}$, this function constructs a string representing the GitHub URL that points to the specific line $n$ within the source file of module $c$ in the `physlib` repository. The URL is generated by appending the file path associated with $c$ and the line anchor `#L{n}` to the base path `https://github.com/leanprover-community/physlib/blob/master/`.

Given a declaration name $c$, this function retrieves and returns the line number in the source file where $c$ is defined as a natural number $n \in \mathbb{N}$. The function operates within a monad $m$ that provides access to the environment's declaration metadata.

Given a declaration name $c$, this function returns the name of the module (or file) where $c$ is defined, as recorded in the current environment of the monad $m$.

For a given declaration name $c$, this function retrieves its source code location and returns it as a string. The output string is formatted by concatenating the relative file path of the module where $c$ is defined, the line number of the declaration, and the name $c$ itself (e.g., `"path/to/file.lean:line_number c"`). The function operates within a monad $m$ that provides access to the global environment and metadata.

For a given declaration name $c$, this function returns a boolean value indicating whether $c$ has an associated source code location (position information) within the environment.

Given a declaration name $c$, this function checks the current environment to determine whether $c$ has an associated documentation string, returning a boolean value within the `CoreM` monad.

Given a declaration identifier $c$ of type `Name`, the function `Lean.Name.getDocString` retrieves its associated documentation string from the current environment. If a standard documentation string exists for $c$, it is returned as a `String`; otherwise, if no documentation is found or if it is in an alternative format (such as a Verso docstring), the function returns an empty string. This computation is performed within the `CoreM` monad.

Given a declaration identifier $n$ of type `Name`, the function `Lean.Name.getDeclString` retrieves the literal source code defining $n$ from its corresponding `.lean` file. The function determines the file location and the character range (from the starting position to the end position) associated with the definition of $n$ in the current environment, reads the file's content, and extracts the specific substring, including any associated documentation strings. The result is returned as a `String` within the `CoreM` monad.

Given a declaration identifier $n$ of type `Name`, the function `Lean.Name.getDeclStringNoDoc` retrieves the source code of the declaration $n$ from its corresponding `.lean` file, excluding any preceding documentation strings or comments. The function first obtains the full declaration string, then identifies the first line starting with a keyword such as `def`, `lemma`, `theorem`, `inductive`, `structure`, `instance`, or `abbrev`, and returns the content starting from that line. The result is returned as a `String` within the `CoreM` monad.

The function `Physlib.noDefs` calculates the total count of user-defined definitions within the `Physlib` library. It retrieves all constants from the modules imported by `Physlib` and filters for those that are classified as definitions (where `isDef` is true) and possess an associated source code location. The resulting sum is returned as a natural number $n \in \mathbb{N}$ within the `CoreM` monad.

The function `Physlib.noLemmas` computes the total number of lemmas (theorems) contained within the `Physlib` library. It aggregates all user-defined constants from the modules imported by `Physlib` and returns the count of those that are not classified as definitions (where `isDef` is false) and possess an associated source code location. The result is returned as a natural number $n \in \mathbb{N}$ within the `CoreM` monad.

The function `Physlib.allDocStrings` retrieves a collection of all documentation strings associated with user-defined constants (such as definitions and theorems) within the `Physlib` library. It operates by identifying all modules imported by `Physlib`, gathering the user-defined constants from each module, and then extracting the documentation string for every constant. The result is returned as an array of strings, $\text{Array}(\text{String})$, within the `CoreM` monad.

The function `Physlib.noDefsNoDocString` calculates the total number of user-defined definitions within the `Physlib` library that lack an associated documentation string. It retrieves all constants from the modules imported by `Physlib` and counts those that satisfy three conditions: the constant is a definition (rather than a theorem or axiom), it has an associated source code location, and it does not have a docstring. The result is returned as a natural number $n \in \mathbb{N}$ within the `CoreM` monad.

The function `Physlib.noLemmasNoDocString` calculates the total number of user-defined lemmas and theorems within the `Physlib` library that lack an associated documentation string. It retrieves all constants from the modules imported by `Physlib` and counts those that satisfy three criteria: the constant is not a definition (indicating it is a theorem or lemma), it has an associated source code location, and it does not have a docstring. The final count is returned as a natural number $n \in \mathbb{N}$ within the `CoreM` monad.

The function `Physlib.noLines` is an $IO$ action that computes the total number of lines of source code in the `Physlib` library. It retrieves the set of all modules $M$ imported by `Physlib` (excluding the core `Init` library), reads the content of the source file for each module $m \in M$ as an array of strings representing its lines $L_m$, and returns the total count $\sum_{m \in M} |L_m|$ as a natural number $n \in \mathbb{N}$.

The function `Physlib.noTODOs` is an $IO$ action that calculates the total number of "TODO" items within the `Physlib` library. It retrieves the set of all modules $M$ imported by `Physlib` (excluding the core `Init` library) and, for each module $m \in M$, reads the lines $L_m$ of its source code. The function then counts and returns the total number of lines across all files that start with the prefix "TODO " as a natural number $n \in \mathbb{N}$.

The function `Physlib.noFilesWithTODOs` is an $IO$ action that calculates the number of source files within the `Physlib` library that contain at least one "TODO" item. It identifies the set of all modules $M$ imported by `Physlib` (excluding the core `Init` library), retrieves the lines $L_m$ of the source code for each module $m \in M$, and filters for the subset of files where at least one line $l \in L_m$ starts with the prefix "TODO ". The final result is the size of this subset as a natural number $n \in \mathbb{N}$.

The function `Physlib.allUserConsts` retrieves an array of all user-defined declarations (such as definitions, theorems, and axioms) within the `Physlib` library. This is achieved by aggregating the constants from all modules returned by `Physlib.allImports`, filtering them via `Physlib.Imports.getUserConsts` to exclude internal names and auto-generated recursors. The operation is performed within the `CoreM` monad.