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 createImportedDiscrTree. 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.

inductive Lean.Meta.LazyDiscrTree.Key : Type

Discrimination tree key.

• const : Name → Nat → Key
• fvar : FVarId → Nat → Key
• lit : Literal → Key
• star : Key
• other : Key
• arrow : Key
• proj : Name → Nat → Nat → Key

instance Lean.Meta.LazyDiscrTree.instInhabitedKey : Inhabited Key

Equations

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

instance Lean.Meta.LazyDiscrTree.instBEqKey : BEq Key

Equations

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

instance Lean.Meta.LazyDiscrTree.instReprKey : Repr Key

Equations

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

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

Hash function

Equations

• (Lean.Meta.LazyDiscrTree.Key.const a a_1).hash = mixHash 5237 (mixHash a.hash (hash a_1))
• (Lean.Meta.LazyDiscrTree.Key.fvar a a_1).hash = mixHash 3541 (mixHash (hash a) (hash a_1))
• (Lean.Meta.LazyDiscrTree.Key.lit a).hash = mixHash 1879 (hash a)
• Lean.Meta.LazyDiscrTree.Key.star.hash = 7883
• Lean.Meta.LazyDiscrTree.Key.other.hash = 2411
• Lean.Meta.LazyDiscrTree.Key.arrow.hash = 17
• (Lean.Meta.LazyDiscrTree.Key.proj a a_1 a_2).hash = mixHash (hash a_2) (mixHash (hash a) (hash a_1))

instance Lean.Meta.LazyDiscrTree.Key.instHashable : Hashable Key

Equations

• Lean.Meta.LazyDiscrTree.Key.instHashable = { hash := Lean.Meta.LazyDiscrTree.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 := ∅ } }

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.

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

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

• roots : Std.HashMap Key Lean.Meta.LazyDiscrTree.TrieIndex✝

  Map from discriminator trie roots to the index.

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

Equations

• Lean.Meta.LazyDiscrTree.instInhabited = { default := { } }

def Lean.Meta.LazyDiscrTree.patternPath (e : Expr) : MetaM (Array Key)

Create a key path from an expression using the function used for patterns.

This differs from Lean.Meta.DiscrTree.mkPath and targetPath in that the expression should uses free variables rather than meta-variables for holes.

Equations

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

def Lean.Meta.LazyDiscrTree.targetPath (e : Expr) : MetaM (Array Key)

Create a key path from an expression we are matching against.

This should have mvars instantiated where feasible.

Equations

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

def Lean.Meta.LazyDiscrTree.dropKeyAux {α : Type} (next : Lean.Meta.LazyDiscrTree.TrieIndex✝) (rest : List Key) : Lean.Meta.LazyDiscrTree.MatchM✝ α Unit

Equations

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

def Lean.Meta.LazyDiscrTree.dropKey {α : Type} (t : LazyDiscrTree α) (path : List Key) : MetaM (LazyDiscrTree α)

This drops a specific key from the lazy discrimination tree so that all the entries matching that key exactly are removed.

Equations

• t.dropKey [] = pure t
• t.dropKey (k :: r) = Prod.snd <$> Lean.Meta.LazyDiscrTree.runMatch✝ t (Lean.Meta.LazyDiscrTree.dropKeyAux (t.roots.getD k 0) r)

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

A match result contains the terms formed from matching a term against patterns in the discrimination tree.

• elts : Array (Array (Array α))

  The elements in the match result.

  The top-level array represents an array from score values to the results with that score. A score is the number of non-star matches in a pattern against the term, and thus bounded by the size of the term being matched against. The elements of this array are themselves arrays of non-empty arrays so that we can defer concatenating results until needed.

def Lean.Meta.LazyDiscrTree.MatchResult.size {α : Type} (mr : MatchResult α) : Nat

Number of elements in result

Equations

• mr.size = Array.foldl (fun (i : Nat) (a : Array (Array α)) => Array.foldl (fun (n : Nat) (a : Array α) => n + a.size) i a) 0 mr.elts

@[specialize #[]]

def Lean.Meta.LazyDiscrTree.MatchResult.appendResultsAux {α : Type} {β : Type u_1} (mr : MatchResult α) (a : Array β) (f : Nat → α → β) : Array β

Append results to array

Equations

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

def Lean.Meta.LazyDiscrTree.MatchResult.appendResults {α : Type} (mr : MatchResult α) (a : Array α) : Array α

Equations

• mr.appendResults a = mr.appendResultsAux a fun (x : Nat) (a : α) => a

structure Lean.Meta.LazyDiscrTree.PartialMatch : Type

• todo : Array Expr
• score : Nat
• c : Lean.Meta.LazyDiscrTree.TrieIndex✝

instance Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch : Inhabited PartialMatch

Equations

• Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch = { default := { todo := default, score := default, c := default } }

def Lean.Meta.LazyDiscrTree.getMatch {α : Type} (d : LazyDiscrTree α) (e : Expr) : MetaM (MatchResult α × 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

• d.getMatch e = Lean.Meta.withReducible (Lean.Meta.LazyDiscrTree.runMatch✝ d (Lean.Meta.LazyDiscrTree.getMatchCore✝ d.roots e))

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 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 }

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

Initial entry in lazy discrimination tree

• key : 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 : Expr) (value : α) : MetaM (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 : InitEntry α) (idx : Nat) (value : α) : MetaM (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 : NameGenerator
• core : Core.Cache
• meta : Meta.Cache

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

Equations

• Lean.Meta.LazyDiscrTree.Cache.empty ngen = { ngen := ngen, core := { }, meta := { } }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.LazyDiscrTree.blacklistInsertion env declName = (!Lean.Meta.allowCompletion env declName || declName == `sorryAx || declName.isInternalDetail || false || false)

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

Equations

• Lean.Meta.LazyDiscrTree.instInhabitedInitResults = { default := { } }

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

Combine two initial results.

Equations

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

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.getChildNgen {M : Type → Type} [Monad M] [MonadNameGenerator M] : M NameGenerator

Equations

• Lean.Meta.LazyDiscrTree.getChildNgen = do let ngen ← Lean.getNGen match ngen.mkChild with | (cngen, ngen) => do Lean.setNGen ngen pure cngen

def Lean.Meta.LazyDiscrTree.createLocalPreDiscrTree {α : Type} (cctx : Core.Context) (ngen : NameGenerator) (env : Environment) (d : Lean.Meta.LazyDiscrTree.ImportData✝) (act : Name → ConstantInfo → MetaM (Array (InitEntry α))) : BaseIO (Lean.Meta.LazyDiscrTree.PreDiscrTree✝ α)

Equations

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

def Lean.Meta.LazyDiscrTree.dropKeys {α : Type} (t : LazyDiscrTree α) (keys : List (List Key)) : MetaM (LazyDiscrTree α)

Equations

• t.dropKeys keys = List.foldlM (fun (x1 : Lean.Meta.LazyDiscrTree α) (x2 : List Lean.Meta.LazyDiscrTree.Key) => x1.dropKey x2) t keys

def Lean.Meta.LazyDiscrTree.logImportFailure {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (f : Lean.Meta.LazyDiscrTree.ImportFailure✝) : m Unit

Equations

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

def Lean.Meta.LazyDiscrTree.createImportedDiscrTree {m : Type → Type} {α : Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT BaseIO m] (cctx : Core.Context) (ngen : NameGenerator) (env : Environment) (act : Name → ConstantInfo → MetaM (Array (InitEntry α))) (constantsPerTask : Nat := 1000) : m (LazyDiscrTree α)

Create a discriminator tree for imported environment.

Equations

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

@[irreducible]

def Lean.Meta.LazyDiscrTree.createImportedDiscrTree.go {m : Type → Type} {α : Type} [Monad m] [MonadLiftT BaseIO m] (cctx : Core.Context) (env : Environment) (act : Name → ConstantInfo → MetaM (Array (InitEntry α))) (constantsPerTask : Nat := 1000) (n : Nat) (ngen : NameGenerator) (tasks : Array (Task (Lean.Meta.LazyDiscrTree.InitResults✝ α))) (start cnt idx : Nat) : m (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.

def Lean.Meta.LazyDiscrTree.findImportMatches {α : Type} (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α)))) (addEntry : Name → ConstantInfo → MetaM (Array (InitEntry α))) (droppedKeys : List (List Key) := []) (constantsPerTask : Nat := 1000) (ty : Expr) : MetaM (MatchResult α)

Equations

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

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

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

Note. We use different discriminator trees for imported and current module declarations since imported declarations are typically much more numerous but not changed after the environment is created.

• ref : IO.Ref (LazyDiscrTree α)

def Lean.Meta.LazyDiscrTree.createModuleDiscrTree {α : Type} (entriesForConst : Name → ConstantInfo → MetaM (Array (InitEntry α))) : CoreM (LazyDiscrTree α)

Create a discriminator tree for current module declarations.

Equations

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

def Lean.Meta.LazyDiscrTree.createModuleTreeRef {α : Type} (entriesForConst : Name → ConstantInfo → MetaM (Array (InitEntry α))) (droppedKeys : List (List Key)) : MetaM (ModuleDiscrTreeRef α)

Creates reference for lazy discriminator tree that only contains this module's definitions.

Equations

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

def Lean.Meta.LazyDiscrTree.findModuleMatches {α : Type} (moduleRef : ModuleDiscrTreeRef α) (ty : Expr) : MetaM (MatchResult α)

Returns candidates from this module in this module that match the expression.

• moduleRef is a references to a lazy discriminator tree only containing this module's definitions.

Equations

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

def Lean.Meta.LazyDiscrTree.findMatchesExt {α β : Type} (moduleTreeRef : ModuleDiscrTreeRef α) (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α)))) (addEntry : Name → ConstantInfo → MetaM (Array (InitEntry α))) (droppedKeys : List (List Key) := []) (constantsPerTask : Nat := 1000) (adjustResult : Nat → α → β) (ty : Expr) : MetaM (Array β)

findMatchesExt searches for entries in a lazily initialized discriminator tree.

It provides some additional capabilities beyond findMatches to adjust results based on priority and cache module declarations

• modulesTreeRef points to the discriminator tree for local environment. Used for caching and created by createLocalTree.
• ext should be an environment extension with an IO.Ref for caching the import lazy discriminator tree.
• addEntry is the function for creating discriminator tree entries from constants.
• droppedKeys contains keys we do not want to consider when searching for matches. It is used for dropping very general keys.
• constantsPerTask stores number of constants in imported modules used to decide when to create new task.
• adjustResult takes the priority and value to produce a final result.
• ty is the expression type.

Equations

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

def Lean.Meta.LazyDiscrTree.findMatches {α : Type} (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α)))) (addEntry : Name → ConstantInfo → MetaM (Array (InitEntry α))) (droppedKeys : List (List Key) := []) (constantsPerTask : Nat := 1000) (ty : Expr) : MetaM (Array α)

findMatches searches for entries in a lazily initialized discriminator tree.

• ext should be an environment extension with an IO.Ref for caching the import lazy discriminator tree.
• addEntry is the function for creating discriminator tree entries from constants.
• droppedKeys contains keys we do not want to consider when searching for matches. It is used for dropping very general keys.

Equations

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