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.

• root : Std.HashMap Key Nat

  Maps keys to index in tries array.

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

  Lazy entries for root of trie.

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

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

Add an entry to the pre-discrimination tree.

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

Convert a pre-discrimination tree to a RefinedDiscrTree.

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

Merge two discrimination trees.

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.InitResults.append {α : Type} (x y : Lean.Meta.RefinedDiscrTree.InitResults✝ α) : Lean.Meta.RefinedDiscrTree.InitResults✝ α

Combine two initial results.

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

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

Create a RefinedDiscrTree consisting of all entries generated by act from imported constants. (it gets called by addConstToPreDiscrTree). This uses parallel computation.

@[irreducible]

def Lean.Meta.RefinedDiscrTree.createImportedDiscrTree.go {α : Type} (env : Environment) (act : Name → ConstantInfo → MetaM (List (α × List (Key × LazyEntry)))) (constantsPerTask capacityPerTask : Nat) (cctx : Core.Context) (ngen : NameGenerator) (tasks : Array (Task (Lean.Meta.RefinedDiscrTree.InitResults✝ α))) (start cnt idx : Nat) : CoreM (Array (Task (Lean.Meta.RefinedDiscrTree.InitResults✝ α)))

Allocate constants to tasks according to constantsPerTask.

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. (it gets 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.