84f15ac93a
This PR fixes a bug in `simp` where it was not resetting the set of zeta-delta reduced let definitions between `simp` calls. It also fixes a bug where `simp` would report zeta-delta reduced let definitions that weren't given as simp arguments (these extraneous let definitions appear due to certain processes temporarily setting `zetaDelta := true`). This PR also modifies the metaprogramming interface for the zeta-delta tracking functions to be re-entrant and to prevent this kind of no-reset bug from occurring again. Closes #6655. Re-entrance of this metaprogramming interface is not needed to fix #6655, but it is needed for some future PRs. The `tests/lean/run/6655.lean` file has an example of a deficiency of `simp?`, where `simp?` still over-reports unfolded let declarations. This is likely due to `withInferTypeConfig` setting `zetaDelta := true` from within `isDefEq`, but I did not verify this. This PR supersedes #7539. The difference is that this PR has `withResetZetaDeltaFVarIds` save and restore `zetaDeltaFVarIds`, but that PR saves and then extends `zetaDeltaFVarIds` to persist unfolded fvars. The behavior in this PR lets metaprograms control whether they want to persist any of the unfolded fvars in this context themselves. In practice, metaprograms that use `withResetZetaDeltaFVarIds` are creating many temporary fvars and are doing dependence computations. These temporary fvars shouldn't be persisted, and also dependence shouldn't be inferred from the fact that a dependence calculation was done. (Concrete example: the let-to-have transformation in an upcoming PR can be run from within simp. Just because let-to-have unfolds an fvar while calculating dependencies of lets doesn't mean that this fvar should be included by `simp?`.) |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||