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.

Equations

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

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 Nat

  Maps keys to index in tries array.

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

  Lazy entries for root of trie.

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

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree.default = { root := default, tries := default }

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

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree = { default := Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree.default }

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

Add an entry to the PreDiscrTree.

Equations

• d.push k e = Lean.Meta.RefinedDiscrTree.PreDiscrTree.modifyAt✝ d k fun (x : Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)) => x.push e

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

Convert a PreDiscrTree to a RefinedDiscrTree.

Equations

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

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

Merge two PreDiscrTrees.

Equations

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

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

Equations

• Lean.Meta.RefinedDiscrTree.PreDiscrTree.instAppend = { append := Lean.Meta.RefinedDiscrTree.PreDiscrTree.append }

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

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

Equations

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

def Lean.Meta.RefinedDiscrTree.InitResults.append {α : Type} (x y : Lean.Meta.RefinedDiscrTree.InitResults✝ α) : Lean.Meta.RefinedDiscrTree.InitResults✝¹ α

Combine two initial results.

Equations

• Lean.Meta.RefinedDiscrTree.InitResults.append { tree := yv, errors := ye } { tree := yv_1, errors := ye_1 } = { tree := yv ++ yv_1, errors := ye ++ ye_1 }

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

Equations

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

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; addConstToPreDiscrTree calls this helper. This uses parallel computation.

Equations

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

@[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.

Equations

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

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.

Equations

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

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.

Equations

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