# 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.

source
def Batteries.Tactic.Cache (α : Type) :
Type

Once-per-file cache.

Equations

- Batteries.Tactic.Cache α = IO.Ref (Lean.MetaM α ⊕ Task (Except Lean.Exception α))

Instances For

source
instance Batteries.Tactic.instNonemptyCache {α : Type} :
Nonempty (Cache α)
source
def Batteries.Tactic.Cache.mk {α : Type} (init : Lean.MetaM α) :
IO (Cache α)

Creates a cache with an initialization function.

Equations

- Batteries.Tactic.Cache.mk init = liftM (IO.mkRef (Sum.inl init))

Instances For

source
def Batteries.Tactic.Cache.get {m : Type → Type} {α : Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadLog m] [Lean.MonadOptions m] [MonadLiftT BaseIO m] [MonadExcept Lean.Exception m] (cache : Cache α) :
m α

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.

Instances For

source
structure Batteries.Tactic.DeclCache (α : Type) :
Type

Cached fold over the environment's declarations, where a given function is applied to `α` for every constant.

- mk' :: (

- cache : Cache α

  The cached data.

- addDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α

  Function for adding a declaration from the current file to the cache.

- addLibraryDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α

  Function for adding a declaration from the library to the cache. Defaults to the same behaviour as adding a declaration from the current file.

- )

Instances For

source
instance Batteries.Tactic.instNonemptyDeclCache {α✝ : Type} [Nonempty α✝] :
Nonempty (DeclCache α✝)
source
def Batteries.Tactic.DeclCache.mk {α : Type} (profilingName : String) (pre : Lean.MetaM α := failure) (empty : α) (addDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) (addLibraryDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α := addDecl) (post : α → Lean.MetaM α := fun (a : α) => pure a) :
IO (DeclCache α)

Creates a `DeclCache`.

First, if `pre` is nonempty, run that for a value, and if successful populate the cache with that value.

If `pre` is empty, or it fails, the cached structure `α` is initialized with `empty`, and then `addLibraryDecl` is called for every imported constant. After all imported constants have been added, we run `post`. Finally, the result is cached.

When `get` is called, `addDecl` is also called for every constant in the current file.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Batteries.Tactic.DeclCache.get {α : Type} (cache : DeclCache α) :
Lean.MetaM α

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.

Instances For

source
@[reducible]
def Batteries.Tactic.DiscrTreeCache (α : Type) :
Type

A type synonym for a `DeclCache` containing a pair of discrimination trees. The first will store declarations in the current file, the second will store declarations from imports (and will hopefully be "read-only" after creation).

Equations

- Batteries.Tactic.DiscrTreeCache α = Batteries.Tactic.DeclCache (Lean.Meta.DiscrTree α × Lean.Meta.DiscrTree α)

Instances For

source
def Batteries.Tactic.DiscrTreeCache.mk {α : Type} [BEq α] (profilingName : String) (processDecl : Lean.Name → Lean.ConstantInfo → Lean.MetaM (Array (Array Lean.Meta.DiscrTree.Key × α))) (post? : Option (Array α → Array α) := none) (init : Lean.MetaM (Lean.Meta.DiscrTree α) := failure) :
IO (DiscrTreeCache α)

Build a `DiscrTreeCache`, from a function that returns a collection of keys and values for each declaration.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Batteries.Tactic.DiscrTreeCache.getMatch {α : Type} (c : DiscrTreeCache α) (e : Lean.Expr) :
Lean.MetaM (Array α)

Get matches from both the discrimination tree for declarations in the current file, and for the imports.

Note that if you are calling this multiple times with the same environment, it will rebuild the discrimination tree for the current file multiple times, and it would be more efficient to call `c.get` once, and then call `DiscrTree.getMatch` multiple times.

Equations

- One or more equations did not get rendered due to their size.

Instances For