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.

• 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✝)

Equations

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

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

Add an entry to the pre-discrimination tree.

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 pre-discrimination tree 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 discrimination trees.

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.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. (it gets called by addConstToPreDiscrTree). 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. (it gets 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.