Discrimination-tree-indexed environment extensions

This file provides an API for scoped environment extensions whose declarations are indexed by elaborated expression patterns in a DiscrTree.

Implimentation Notes

The inclusion tactic uses two seperate types of DiscrTree indexed environment extensions. These have nearly identical APIs except the stored values are different types (one is InclusionExts and the other is HypothesisExts). This file essentially generalizes the DiscrTree valued environment extension API from the implimentation for the norm_num tactic so that it can take arbitrary values.

TODO

Investigate the possibility of using this API for other tactics in Mathlib with DiscrTree indexed environment extensions such as norm_num and positivity. This should perhaps be part of a wider investigation into whether more API from the environment extensions of various Mathlib tactics could be unified.

def DiscrTreeExt.evalDecl (α : Type) (typeName declName : Lean.Name) : Lean.ImportM α

Evaluate declName as a value of type α, checking that its Lean type is typeName.

Equations

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

@[reducible, inline]

abbrev DiscrTreeExt.Entry : Type

The discrimination-tree paths and declaration name stored in an .olean entry.

Equations

• DiscrTreeExt.Entry = (Array (Array Lean.Meta.DiscrTree.Key) × Lean.Name)

structure DiscrTreeExt.State (α : Type) : Type

The state of a discrimination-tree environment extension.

• tree : Lean.Meta.DiscrTree α

  The discrimination tree of the extension.

@[instance_reducible]

instance DiscrTreeExt.instInhabitedState {a✝ : Type} : Inhabited (State a✝)

Equations

• DiscrTreeExt.instInhabitedState = { default := DiscrTreeExt.instInhabitedState.default }

@[reducible, inline]

abbrev DiscrTreeExt.EnvExt (α : Type) : Type

A scoped environment extension containing declaration values indexed by expression patterns.

Equations

• DiscrTreeExt.EnvExt α = Lean.ScopedEnvExtension DiscrTreeExt.Entry (DiscrTreeExt.Entry × α) (DiscrTreeExt.State α)

def DiscrTreeExt.State.getMatch {α : Type} (state : State α) (e : Lean.Expr) : Lean.MetaM (Array α)

Return the declaration values whose DiscrTree keys match e.

Equations

• state.getMatch e = state.tree.getMatch e

def DiscrTreeExt.recordRegisteringModule (kind : Lean.AttributeKind) : Lean.CoreM Unit

When the current module registers an attribute, record for shake that modules importing the current one should continue to do so.

kind indicates the scope at which the attribute is registered.

TODO: This is an overly conservative approximation: better would be to record at the use site which tagged declarations are actually used.

Equations

• DiscrTreeExt.recordRegisteringModule kind = if (kind == Lean.AttributeKind.local) = true then pure () else Lean.recordExtraRevUseOfCurrentModule

def DiscrTreeExt.initializeEnvExt {α : Type} (typeName : Lean.Name) (envExtName : Lean.Name := by exact decl_name%) : IO (EnvExt α)

Create a scoped environment extension whose declarations have type typeName. By default, the environment extension is named after the declaration in which this function is called.

Equations

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

def DiscrTreeExt.EnvExt.register {α : Type} (ext : EnvExt α) (entry : Entry × α) (kind : Lean.AttributeKind) : Lean.CoreM Unit

Register entry in ext, recording the current module as one shake should preserve.

Prefer this over ScopedEnvExtension.add when adding an entry from an attribute handler, so that the registration and the shake bookkeeping cannot drift apart.

Equations

• ext.register entry kind = do Lean.ScopedEnvExtension.add ext entry kind DiscrTreeExt.recordRegisteringModule kind

def DiscrTreeExt.elabExtKeys (patterns : Array Lean.Syntax) : Lean.CoreM (Array (Array Lean.Meta.DiscrTree.Key))

Elaborate expression patterns into DiscrTree paths.

Equations

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