Cache for the lifting/unlifting transformations

Transforming an equality repeatedly synthesizes the same instances (MeasurableSpace X, IsSFiniteKernel κ, ...) and rebuilds the same terms (measurable equivalences, types of kernels, ...). This file provides a cache, reset at the beginning of each transformation, that memoizes these computations.

Main declarations

• synthInstanceCached: synthInstance with memoization.
• inferTypeCached: inferType with memoization.
• memoized: memoization of an arbitrary computation returning expressions, keyed by a tag and an expression.
• resetTransformCache: empties the cache.

structure TransformCache : Type

The cache of the lifting/unlifting transformations.

• insts : Std.HashMap Lean.Expr Lean.Expr

  Synthesized instances, keyed by the class application.

• types : Std.HashMap Lean.Expr Lean.Expr

  Inferred types, keyed by the expression.

• memo : Std.HashMap (Lean.Name × Lean.Expr) (Array Lean.Expr)

  Memoized computations, keyed by a tag and an expression.

@[instance_reducible]

instance instInhabitedTransformCache : Inhabited TransformCache

Equations

• instInhabitedTransformCache = { default := instInhabitedTransformCache.default }

def resetTransformCache : Lean.MetaM Unit

Empties the cache. To be called at the beginning of each transformation.

Equations

• resetTransformCache = ST.Ref.set transformCacheRef✝ { }

def synthInstanceCached (type : Lean.Expr) : Lean.MetaM Lean.Expr

synthInstance with memoization.

Equations

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

def inferTypeCached (e : Lean.Expr) : Lean.MetaM Lean.Expr

inferType with memoization.

Equations

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

def memoized (tag : Lean.Name) (key : Lean.Expr) (f : Lean.MetaM (Array Lean.Expr)) : Lean.MetaM (Array Lean.Expr)

Memoizes the computation f, keyed by tag and key.

Equations

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