Lazy Discrimination Tree

This file defines a new type of discrimination tree optimized for rapid population of imported modules for use in tactics. It uses a lazy initialization strategy.

The discrimination tree can be created through createImportedEnvironment. This creates a discrimination tree from all imported modules in an environment using a callback that provides the entries as InitEntry values.

The function getMatch can be used to get the values that match the expression as well as an updated lazy discrimination tree that has elaborated additional parts of the tree.

instance Lean.Meta.LazyDiscrTree.MatchClone.instInhabitedKey : Inhabited Lean.Meta.LazyDiscrTree.MatchClone.Key

Equations

• Lean.Meta.LazyDiscrTree.MatchClone.instInhabitedKey = { default := Lean.Meta.LazyDiscrTree.MatchClone.Key.const default default }

instance Lean.Meta.LazyDiscrTree.MatchClone.instBEqKey : BEq Lean.Meta.LazyDiscrTree.MatchClone.Key

Equations

• Lean.Meta.LazyDiscrTree.MatchClone.instBEqKey = { beq := Lean.Meta.LazyDiscrTree.MatchClone.beqKey✝ }

instance Lean.Meta.LazyDiscrTree.MatchClone.instReprKey : Repr Lean.Meta.LazyDiscrTree.MatchClone.Key

Equations

• Lean.Meta.LazyDiscrTree.MatchClone.instReprKey = { reprPrec := Lean.Meta.LazyDiscrTree.MatchClone.reprKey✝ }

def Lean.Meta.LazyDiscrTree.MatchClone.Key.hash : Lean.Meta.LazyDiscrTree.MatchClone.Key → UInt64

Hash function

Equations

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

instance Lean.Meta.LazyDiscrTree.MatchClone.Key.instHashableKey : Hashable Lean.Meta.LazyDiscrTree.MatchClone.Key

Equations

• Lean.Meta.LazyDiscrTree.MatchClone.Key.instHashableKey = { hash := Lean.Meta.LazyDiscrTree.MatchClone.Key.hash }

instance Lean.Meta.LazyDiscrTree.instInhabitedTrie : {a : Type} → Inhabited (Lean.Meta.LazyDiscrTree.Trie a)

Equations

• Lean.Meta.LazyDiscrTree.instInhabitedTrie = { default := { values := default, star := default, children := default, pending := default } }

instance Lean.Meta.LazyDiscrTree.instEmptyCollectionTrie {α : Type} : EmptyCollection (Lean.Meta.LazyDiscrTree.Trie α)

Equations

• Lean.Meta.LazyDiscrTree.instEmptyCollectionTrie = { emptyCollection := { values := #[], star := 0, children := ∅, pending := #[] } }

structure Lean.Meta.LazyDiscrTree (α : Type) : Type

LazyDiscrTree is a variant of the discriminator tree datatype DiscrTree in Lean core that is designed to be efficiently initializable with a large number of patterns. This is useful in contexts such as searching an entire Lean environment for expressions that match a pattern.

Lazy discriminator trees achieve good performance by minimizing the amount of work that is done up front to build the discriminator tree. When first adding patterns to the tree, only the root discriminator key is computed and processing the remaining terms is deferred until demanded by a match.

• config : Lean.Meta.WhnfCoreConfig

  Configuration for normalization.

• tries : Array (Lean.Meta.LazyDiscrTree.Trie α)

  Backing array of trie entries. Should be owned by this trie.

• roots : Lean.HashMap Lean.Meta.LazyDiscrTree.MatchClone.Key Lean.Meta.LazyDiscrTree.TrieIndex

  Map from discriminator trie roots to the index.

instance Lean.Meta.LazyDiscrTree.instInhabitedLazyDiscrTree {α : Type} : Inhabited (Lean.Meta.LazyDiscrTree α)

Equations

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

def Lean.Meta.LazyDiscrTree.getMatch {α : Type} (d : Lean.Meta.LazyDiscrTree α) (e : Lean.Expr) : Lean.MetaM (Array α × Lean.Meta.LazyDiscrTree α)

Find values that match e in d.

The results are ordered so that the longest matches in terms of number of non-star keys are first with ties going to earlier operators first.

Equations

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

instance Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree : {a : Type} → Inhabited (Lean.Meta.LazyDiscrTree.PreDiscrTree a)

Equations

• Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree = { default := { roots := default, tries := default } }

def Lean.Meta.LazyDiscrTree.PreDiscrTree.append {α : Type} (x : Lean.Meta.LazyDiscrTree.PreDiscrTree α) (y : Lean.Meta.LazyDiscrTree.PreDiscrTree α) : Lean.Meta.LazyDiscrTree.PreDiscrTree α

Merge two discrimination trees.

Equations

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

instance Lean.Meta.LazyDiscrTree.PreDiscrTree.instAppendPreDiscrTree {α : Type} : Append (Lean.Meta.LazyDiscrTree.PreDiscrTree α)

Equations

• Lean.Meta.LazyDiscrTree.PreDiscrTree.instAppendPreDiscrTree = { append := Lean.Meta.LazyDiscrTree.PreDiscrTree.append }

@[reducible]

structure Lean.Meta.LazyDiscrTree.InitEntry (α : Type) : Type

Initial entry in lazy discrimination tree

• key : Lean.Meta.LazyDiscrTree.MatchClone.Key

  Return root key for an entry.

• entry : Lean.Meta.LazyDiscrTree.LazyEntry α

  Returns rest of entry for later insertion.

def Lean.Meta.LazyDiscrTree.InitEntry.fromExpr {α : Type} (expr : Lean.Expr) (value : α) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) : Lean.MetaM (Lean.Meta.LazyDiscrTree.InitEntry α)

Constructs an initial entry from an expression and value.

Equations

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

def Lean.Meta.LazyDiscrTree.InitEntry.mkSubEntry {α : Type} (e : Lean.Meta.LazyDiscrTree.InitEntry α) (idx : Nat) (value : α) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) : Lean.MetaM (Lean.Meta.LazyDiscrTree.InitEntry α)

Creates an entry for a subterm of an initial entry.

This is slightly more efficient than using fromExpr on subterms since it avoids a redundant call to whnf.

Equations

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

structure Lean.Meta.LazyDiscrTree.Cache : Type

• ngen : Lean.NameGenerator
• core : Lean.Core.Cache
• meta : Lean.Meta.Cache

def Lean.Meta.LazyDiscrTree.Cache.empty (ngen : Lean.NameGenerator) : Lean.Meta.LazyDiscrTree.Cache

Equations

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

instance Lean.Meta.LazyDiscrTree.instInhabitedInitResults {α : Type} : Inhabited (Lean.Meta.LazyDiscrTree.InitResults α)

Equations

• Lean.Meta.LazyDiscrTree.instInhabitedInitResults = { default := { tree := { roots := ∅, tries := #[] }, errors := #[] } }

def Lean.Meta.LazyDiscrTree.InitResults.append {α : Type} (x : Lean.Meta.LazyDiscrTree.InitResults α) (y : Lean.Meta.LazyDiscrTree.InitResults α) : Lean.Meta.LazyDiscrTree.InitResults α

Combine two initial results.

Equations

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

instance Lean.Meta.LazyDiscrTree.InitResults.instAppendInitResults {α : Type} : Append (Lean.Meta.LazyDiscrTree.InitResults α)

Equations

• Lean.Meta.LazyDiscrTree.InitResults.instAppendInitResults = { append := Lean.Meta.LazyDiscrTree.InitResults.append }

def Lean.Meta.LazyDiscrTree.createImportedEnvironment {α : Type} (ngen : Lean.NameGenerator) (env : Lean.Environment) (act : Lake.Name → Lean.ConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) (constantsPerTask : optParam Nat 1000) : EIO Lean.Exception (Lean.Meta.LazyDiscrTree α)

Create an imported environment for tree.

Equations

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

def Lean.Meta.LazyDiscrTree.createImportedEnvironment.go {α : Type} (env : Lean.Environment) (act : Lake.Name → Lean.ConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) (constantsPerTask : optParam Nat 1000) (n : Nat) (ngen : Lean.NameGenerator) (tasks : Array (Task (Lean.Meta.LazyDiscrTree.InitResults α))) (start : Nat) (cnt : Nat) (idx : Nat) : EIO Lean.Exception (Array (Task (Lean.Meta.LazyDiscrTree.InitResults α)))

Allocate constants to tasks according to constantsPerTask.

Equations

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