Once-per-file cache for tactics #
This file defines cache data structures for tactics that are initialized the first time they are accessed. Since Lean 4 starts one process per file, these caches are once-per-file and can for example be used to cache information about the imported modules.
The Cache α
data structure is
the most generic version we define.
It is created using Cache.mk f
where f : MetaM α
performs
the initialization of the cache:
initialize numberOfImports : Cache Nat ← Cache.mk do
(← getEnv).imports.size
-- (does not work in the same module where the cache is defined)
#eval show MetaM Nat from numberOfImports.get
The DeclCache α
data structure computes
a fold over the environment's constants:
DeclCache.mk empty f
constructs such a cache
where empty : α
and f : Name → ConstantInfo → α → MetaM α
.
The result of the constants in the imports is cached
between tactic invocations,
while for constants defined in the same file
f
is evaluated again every time.
This kind of cache can be used e.g.
to populate discrimination trees.
Once-per-file cache.
Equations
- Mathlib.Tactic.Cache α = IO.Ref (Lean.MetaM α ⊕ Task (Except Lean.Exception α))
Creates a cache with an initialization function.
Equations
- Mathlib.Tactic.Cache.mk init = liftM (IO.mkRef (Sum.inl init))
Access the cache. Calling this function for the first time will initialize the cache with the function provided in the constructor.
Equations
- One or more equations did not get rendered due to their size.
Cached fold over the environment's declarations,
where a given function is applied to α
for every constant.
Equations
- Mathlib.Tactic.DeclCache α = (Mathlib.Tactic.Cache α × (Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α))
Creates a DeclCache
.
The cached structure α
is initialized with empty
,
and then addDecl
is called for every constant in the environment.
Calls to addDecl
for imported constants are cached.
Equations
- One or more equations did not get rendered due to their size.
Access the cache. Calling this function for the first time will initialize the cache with the function provided in the constructor.
Equations
- One or more equations did not get rendered due to their size.