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.

ink

def Mathlib.Tactic.Cache (α : Type) : Type

Once-per-file cache.

Equations

• Mathlib.Tactic.Cache α = IO.Ref (Lean.MetaM α ⊕ Task (Except Lean.Exception α))

ink

instance Mathlib.Tactic.instNonemptyCache {α : Type} : Nonempty (Mathlib.Tactic.Cache α)

Equations

• @Mathlib.Tactic.instNonemptyCache = @Mathlib.Tactic.instNonemptyCache.proof_1

ink

def Mathlib.Tactic.Cache.mk {α : Type} (init : Lean.MetaM α) : IO (Mathlib.Tactic.Cache α)

Creates a cache with an initialization function.

Equations

• Mathlib.Tactic.Cache.mk init = liftM (IO.mkRef (Sum.inl init))

ink

def Mathlib.Tactic.Cache.get {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadLog m] [inst : Lean.MonadOptions m] [inst : MonadLiftT BaseIO m] [inst : MonadExcept Lean.Exception m] (cache : Mathlib.Tactic.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.

ink

def Mathlib.Tactic.DeclCache (α : Type) : Type

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 α))

ink

instance Mathlib.Tactic.instNonemptyDeclCache {α : Type} : Nonempty (Mathlib.Tactic.DeclCache α)

Equations

• @Mathlib.Tactic.instNonemptyDeclCache = @Mathlib.Tactic.instNonemptyDeclCache.proof_1

ink

def Mathlib.Tactic.DeclCache.mk {α : Type} (profilingName : String) (empty : α) (addDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) : IO (Mathlib.Tactic.DeclCache α)

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.

ink

def Mathlib.Tactic.DeclCache.get {α : Type} (cache : Mathlib.Tactic.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.