Physlib.Meta.TransverseTactics

Operating within the Lean frontend monad `Frontend.FrontendM`, this function processes the commands of a source file to produce a list of pairs $(E, I)$. Each pair consists of the `Environment` $E$ and the `InfoState` $I$ representing the state of the system immediately before each command is processed.

The function `transverseTactics.visitInfo` processes a node `info` from a Lean information tree. Given a file path $f$, a Lean environment $\mathcal{E}$, a callback function $v$ (which operates on tactic information), context information $c$, and an accumulator list of IO actions $A$, the function checks if `info` corresponds to tactic information $t$. If it does, the function prepends a new IO action to $A$. This action, when executed, sets the environment to $\mathcal{E}$ and invokes $v(f, c, t)$, while catching and reporting any metadata errors. If `info` is not a tactic node, the function returns the original list $A$ unchanged.

Given a file path $f$, a callback function $v$ for processing tactic information, and a list of steps $S = [(\mathcal{E}_1, \mathcal{I}_1), (\mathcal{E}_2, \mathcal{I}_2), \dots]$ where each $\mathcal{E}$ is an environment and each $\mathcal{I}$ is an information state, the function `traverseForest` iterates through each pair in $S$. For every information tree within an information state $\mathcal{I}$, it performs a fold operation using the function `visitInfo` with the corresponding environment $\mathcal{E}$ and callback $v$. This process collects and flattens the resulting IO actions into a single list of type $\text{List}(\text{IO Unit})$.

The function `transverseTactics` processes a Lean source file located at path $f$ and applies a user-provided callback function $v$ to every tactic execution node within that file. Specifically, it performs the following steps: 1. **Environment Setup:** It initializes the Lean search path, reads the content of $f$, and processes the file header to establish the required environment $\mathcal{E}$ and module dependencies. 2. **Command Processing:** It elaborates the entire file within the `FrontendM` monad to generate a sequence of pairs $(\mathcal{E}_i, \mathcal{I}_i)$, where each $\mathcal{E}_i$ is the environment and $\mathcal{I}_i$ is the information state (containing information trees) after each command. 3. **Tactic Traversal:** It utilizes `traverseForest` to iterate through the information trees. For every tactic information node $t$ with associated context $c$ found in these trees, it executes the callback $v(f, c, t)$ within the `MetaM` monad. The function ensures that all IO actions resulting from the tactics are executed and handles any errors that arise during the import or traversal phases.