Constructing a RefinedDiscrTree

RefinedDiscrTree is lazy, so to add an entry, we need to compute the first Key and a LazyEntry. These are computed by initializeLazyEntry.

We provide RefinedDiscrTree.insert for directly performing this insert.

For initializing a RefinedDiscrTree using all imported constants, we provide createImportedDiscrTree, which loops through all imported constants, and does this with a parallel computation.

There is also createModuleDiscrTree which does the same but with the constants from the current file.

def Lean.Meta.RefinedDiscrTree.insert {α : Type} (d : RefinedDiscrTree α) (key : Key) (entry : LazyEntry × α) : RefinedDiscrTree α

Directly insert a Key, LazyEntry pair into a RefinedDiscrTree.

structure Lean.Meta.RefinedDiscrTree.PreDiscrTree (α : Type) : Type

Structure for quickly initializing a lazy discrimination tree with a large number of elements using concurrent functions for generating entries.

This preliminary structure is converted to a RefinedDiscrTree via toRefinedDiscrTree.

• root : Std.HashMap Key ℕ

  Maps keys to index in tries array.

• tries : Array (Array (LazyEntry × α))

  Lazy entries for root of trie.

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree {a✝ : Type} : Inhabited (PreDiscrTree a✝)

def Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree.default {a✝ : Type} : PreDiscrTree a✝

def Lean.Meta.RefinedDiscrTree.PreDiscrTree.push {α : Type} (d : PreDiscrTree α) (k : Key) (e : LazyEntry × α) : PreDiscrTree α

Add an entry to the PreDiscrTree.

def Lean.Meta.RefinedDiscrTree.PreDiscrTree.toRefinedDiscrTree {α : Type} (d : PreDiscrTree α) : RefinedDiscrTree α

Convert a PreDiscrTree to a RefinedDiscrTree.

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

Merge two PreDiscrTrees.

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.PreDiscrTree.instAppend {α : Type} : Append (PreDiscrTree α)

def Lean.Meta.RefinedDiscrTree.blacklistInsertion (env : Environment) (declName : Name) : Bool

Return true if declName is automatically generated, or otherwise unsuitable as a lemma suggestion.

def Lean.Meta.RefinedDiscrTree.createImportedDiscrTree {α : Type} (ngen : NameGenerator) (env : Environment) (act : Name → ConstantInfo → MetaM (List (α × List (Key × LazyEntry)))) (constantsPerTask capacityPerTask : ℕ) : CoreM (RefinedDiscrTree α)

Create a RefinedDiscrTree consisting of all entries generated by act from imported constants; addConstToPreDiscrTree calls this helper. This uses parallel computation.

structure Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef (α : Type) : Type

A discriminator tree for the current module's declarations only.

Note: We use different discrimination trees for imported and current module declarations since imported declarations are typically much more numerous but not changed while the current module is edited.

• ref : IO.Ref (RefinedDiscrTree α)

  The reference to the RefinedDiscrTree.

def Lean.Meta.RefinedDiscrTree.createModuleDiscrTree {α : Type} (act : Name → ConstantInfo → MetaM (List (α × List (Key × LazyEntry)))) : CoreM (RefinedDiscrTree α)

Create a RefinedDiscrTree for current module declarations, consisting of all entries generated by act from constants in the current file. This is called by addConstToPreDiscrTree.

def Lean.Meta.RefinedDiscrTree.createModuleTreeRef {α : Type} (act : Name → ConstantInfo → MetaM (List (α × List (Key × LazyEntry)))) : MetaM (ModuleDiscrTreeRef α)

Create a reference for a RefinedDiscrTree for current module declarations.