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 public 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_reducible]

instance Lean.Meta.LazyDiscrTree.instInhabitedKey : Inhabited Key

@[instance_reducible]

instance Lean.Meta.LazyDiscrTree.instBEqKey : BEq Key

def Lean.Meta.LazyDiscrTree.instBEqKey.beq : Key → Key → Bool

@[instance_reducible]

instance Lean.Meta.LazyDiscrTree.instReprKey : Repr Key

def Lean.Meta.LazyDiscrTree.instReprKey.repr : Key → Nat → Format

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

Hash function

@[instance_reducible]

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

def Lean.Meta.LazyDiscrTree.MatchClone.tmpMVarId : MVarId

def Lean.Meta.LazyDiscrTree.MatchClone.tmpStar : Expr

def Lean.Meta.LazyDiscrTree.MatchClone.ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool

Returns true iff the argument should be treated as a "wildcard" by the discrimination tree.

This includes proofs, instance implicit arguments, implicit arguments, and terms of the form noIndexing t

This is a clone of Lean.Meta.DiscrTree.ignoreArg and mainly added to avoid coupling between DiscrTree and LazyDiscrTree while both are potentially subject to independent changes.

partial def Lean.Meta.LazyDiscrTree.MatchClone.pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr)

partial def Lean.Meta.LazyDiscrTree.MatchClone.isNumeral (e : Expr) : Bool

Returns true if e is one of the following

• A nat literal (numeral)
• Nat.zero
• Nat.succ x where isNumeral x
• OfNat.ofNat _ x _ where isNumeral x

def Lean.Meta.LazyDiscrTree.MatchClone.toNatLit? (e : Expr) : Option Literal

def Lean.Meta.LazyDiscrTree.MatchClone.isNatType (e : Expr) : MetaM Bool

def Lean.Meta.LazyDiscrTree.MatchClone.isNatOffset (fName : Name) (e : Expr) : MetaM Bool

Returns true if e is one of the following

• Nat.add _ k where isNumeral k
• Add.add Nat _ _ k where isNumeral k
• HAdd.hAdd _ Nat _ _ k where isNumeral k
• Nat.succ _ This function assumes e.isAppOf fName

def Lean.Meta.LazyDiscrTree.MatchClone.shouldAddAsStar (fName : Name) (e : Expr) : MetaM Bool

This is a hook to determine if we should add an expression as a wildcard pattern.

Clone of Lean.Meta.DiscrTree.shouldAddAsStar. See it for more discussion.

def Lean.Meta.LazyDiscrTree.MatchClone.elimLooseBVarsByBeta (e : Expr) : CoreM Expr

Eliminate loose bound variables via beta-reduction.

This is primarily used to reduce pi-terms ∀(x : P), T into non-dependent functions P → T. The latter has a more specific discrimination tree key .arrow.. and this improves the accuracy of the discrimination tree.

Clone of Lean.Meta.DiscrTree.elimLooseBVarsByBeta. See it for more discussion.

def Lean.Meta.LazyDiscrTree.MatchClone.getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr)

@[reducible, inline]

abbrev Lean.Meta.LazyDiscrTree.MatchClone.getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr)

Given an expression we are looking for patterns that match, return the key and sub-expressions.

@[reducible, inline]

abbrev Lean.Meta.LazyDiscrTree.LazyEntry (α : Type u_1) : Type u_1

An unprocessed entry in the lazy discrimination tree.

@[reducible]

def Lean.Meta.LazyDiscrTree.TrieIndex : Type

Index identifying trie in a discrimination tree.

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

Discrimination tree trie. See LazyDiscrTree.

• node :: (
• values : Array α

  Values for matches ending at this trie.

• star : TrieIndex

  Index of trie matching star.

• children : Std.HashMap Key TrieIndex

  Following matches based on key of trie.

• pending : Array (LazyEntry α)

  Lazy entries at this trie that are not processed.

• )

@[instance_reducible]

instance Lean.Meta.LazyDiscrTree.instInhabitedTrie {a✝ : Type} : Inhabited (Trie a✝)

@[instance_reducible]

instance Lean.Meta.LazyDiscrTree.instEmptyCollectionTrie {α : Type} : EmptyCollection (Trie α)

def Lean.Meta.LazyDiscrTree.Trie.pushPending {α : Type} : Trie α → LazyEntry α → Trie α

Push lazy entry to trie.

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 (Trie α)

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

• roots : Std.HashMap Key TrieIndex

  Map from discriminator trie roots to the index.

@[instance_reducible]

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

def Lean.Meta.LazyDiscrTree.pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr)

Specialization of Lean.Meta.DiscrTree.pushArgs

def Lean.Meta.LazyDiscrTree.initCapacity : Nat

Initial capacity for key and todo vector.

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

Get the root key and rest of terms of an expression using the specified config.

partial def Lean.Meta.LazyDiscrTree.buildPath (op : Bool → Array Expr → Expr → MetaM (Key × Array Expr)) (root : Bool) (todo : Array Expr) (keys : Array Key) : MetaM (Array Key)

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.

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.

@[reducible]

def Lean.Meta.LazyDiscrTree.MatchM (α : Type) : Type → Type

def Lean.Meta.LazyDiscrTree.runMatch {α β : Type} (d : LazyDiscrTree α) (m : MatchM α β) : MetaM (β × LazyDiscrTree α)

def Lean.Meta.LazyDiscrTree.setTrie {α : Type} (i : TrieIndex) (v : Trie α) : MatchM α Unit

def Lean.Meta.LazyDiscrTree.newTrie {m : Type → Type u_1} {α : Type} [Monad m] [MonadState (Array (Trie α)) m] (e : LazyEntry α) : m TrieIndex

Create a new trie with the given lazy entry.

def Lean.Meta.LazyDiscrTree.addLazyEntryToTrie {α : Type} (i : TrieIndex) (e : LazyEntry α) : MatchM α Unit

Add a lazy entry to an existing trie.

def Lean.Meta.LazyDiscrTree.evalLazyEntry {α : Type} (p : Array α × TrieIndex × Std.HashMap Key TrieIndex) (entry : LazyEntry α) : MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex)

def Lean.Meta.LazyDiscrTree.evalLazyEntries {α : Type} (values : Array α) (starIdx : TrieIndex) (children : Std.HashMap Key TrieIndex) (entries : Array (LazyEntry α)) : MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex)

This evaluates all lazy entries in a trie and updates values, starIdx, and children accordingly.

def Lean.Meta.LazyDiscrTree.evalNode {α : Type} (c : TrieIndex) : MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex)

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

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.

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.push {α : Type} (r : MatchResult α) (score : Nat) (e : Array α) : MatchResult α

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

Number of elements in result

@[specialize #[]]

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

Append results to array

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

structure Lean.Meta.LazyDiscrTree.PartialMatch : Type

A partial match captures the intermediate state of a match execution.

N.B. The discriminator tree in Lean has non-determinism due to star and function arrows, so matching loop maintains a stack of partial match results.

• todo : Array Expr
• score : Nat
• c : TrieIndex

@[instance_reducible]

instance Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch : Inhabited PartialMatch

partial def Lean.Meta.LazyDiscrTree.getMatchLoop {α : Type} (cases : Array PartialMatch) (result : MatchResult α) : MatchM α (MatchResult α)

Evaluate all partial matches and add resulting matches to MatchResult.

The partial matches are stored in an array that is used as a stack. When adding multiple partial matches to explore next, to ensure the order of results matches user expectations, this code must add paths we want to prioritize and return results earlier are added last.

def Lean.Meta.LazyDiscrTree.getStarResult {α : Type} (root : Std.HashMap Key TrieIndex) : MatchM α (MatchResult α)

def Lean.Meta.LazyDiscrTree.pushRootCase (r : Std.HashMap Key TrieIndex) (k : Key) (args : Array Expr) (cases : Array PartialMatch) : Array PartialMatch

Add partial match to cases if discriminator tree root map has potential matches.

def Lean.Meta.LazyDiscrTree.getMatchCore {α : Type} (root : Std.HashMap Key TrieIndex) (e : Expr) : MatchM α (MatchResult α)

Find values that match e in root.

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.

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

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

• roots : Std.HashMap Key Nat

  Maps keys to index in tries array.

• tries : Array (Array (LazyEntry α))

  Lazy entries for root of trie.

@[instance_reducible]

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

def Lean.Meta.LazyDiscrTree.PreDiscrTree.modifyAt {α : Type} (d : PreDiscrTree α) (k : Key) (f : Array (LazyEntry α) → Array (LazyEntry α)) : PreDiscrTree α

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

Add an entry to the pre-discrimination tree.

def Lean.Meta.LazyDiscrTree.PreDiscrTree.toLazy {α : Type} (d : PreDiscrTree α) : LazyDiscrTree α

Convert a pre-discrimination tree to a lazy discrimination tree.

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

Merge two discrimination trees.

@[instance_reducible]

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

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

Initial entry in lazy discrimination tree

• key : Key

  Return root key for an entry.

• entry : 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.

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.

structure Lean.Meta.LazyDiscrTree.ImportFailure : Type

Information about a failed import.

• module : Name

  Module with constant that import failed on.

• const : Name

  Constant that import failed on.

• exception : Exception

  Exception that triggers error.

structure Lean.Meta.LazyDiscrTree.ImportData : Type

Information generation from imported modules.

• errors : IO.Ref (Array ImportFailure)

def Lean.Meta.LazyDiscrTree.ImportData.new : BaseIO ImportData

structure Lean.Meta.LazyDiscrTree.Cache : Type

• ngen : NameGenerator
• core : Core.Cache
• meta : Meta.Cache

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

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

def Lean.Meta.LazyDiscrTree.addConstImportData {α : Type} (cctx : Core.Context) (env : Environment) (modName : Name) (d : ImportData) (cacheRef : IO.Ref Cache) (tree : PreDiscrTree α) (act : Name → AsyncConstantInfo → MetaM (Array (InitEntry α))) (c : AsyncConstantInfo) : BaseIO (PreDiscrTree α)

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

Contains the pre discrimination tree and any errors occurring during initialization of the library search tree.

• tree : PreDiscrTree α
• errors : Array ImportFailure

@[instance_reducible]

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

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

Combine two initial results.

@[instance_reducible]

instance Lean.Meta.LazyDiscrTree.InitResults.instAppend {α : Type} : Append (InitResults α)

def Lean.Meta.LazyDiscrTree.toFlat {α : Type} (d : ImportData) (tree : PreDiscrTree α) : BaseIO (InitResults α)

partial def Lean.Meta.LazyDiscrTree.loadImportedModule {α : Type} (cctx : Core.Context) (env : Environment) (act : Name → AsyncConstantInfo → MetaM (Array (InitEntry α))) (d : ImportData) (cacheRef : IO.Ref Cache) (tree : PreDiscrTree α) (mname : Name) (mdata : ModuleData) (i : Nat := 0) : BaseIO (PreDiscrTree α)

def Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq {α : Type} (cctx : Core.Context) (ngen : NameGenerator) (env : Environment) (act : Name → AsyncConstantInfo → MetaM (Array (InitEntry α))) (start stop : Nat) : BaseIO (InitResults α)

def Lean.Meta.LazyDiscrTree.combineGet {α : Type u_1} [Append α] (z : α) (tasks : Array (Task α)) : α

Get the results of each task and merge using combining function

def Lean.Meta.LazyDiscrTree.getChildNgen {M : Type → Type} [Monad M] [MonadNameGenerator M] : M NameGenerator

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

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

partial def Lean.Meta.LazyDiscrTree.collectSubtreeAux {α : Type} (next : TrieIndex) : MatchM α (Array α)

Collect all values from a subtree recursively and clear them.

def Lean.Meta.LazyDiscrTree.extractKeyAux {α : Type} (next : TrieIndex) (rest : List Key) : MatchM α (Array α)

Navigate to a key path and return all values in that subtree, then drop them.

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

Extract and drop entries at a specific key, returning the dropped entries.

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

Extract entries at the given keys and also drop them from the tree.

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

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 → AsyncConstantInfo → MetaM (Array (InitEntry α))) (constantsPerTask : Nat := 1000) : m (LazyDiscrTree α)

Create a discriminator tree for imported environment.

def Lean.Meta.LazyDiscrTree.createTreeCtx (ctx : Core.Context) : Core.Context

Creates the core context used for initializing a tree using the current context.

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

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 → AsyncConstantInfo → MetaM (Array (InitEntry α))) : CoreM (LazyDiscrTree α)

Create a discriminator tree for current module declarations.

def Lean.Meta.LazyDiscrTree.createModuleTreeRef {α : Type} (entriesForConst : Name → AsyncConstantInfo → MetaM (Array (InitEntry α))) (droppedKeys : List (List Key)) (droppedEntriesRef : Option (IO.Ref (Option (Array α))) := none) : MetaM (ModuleDiscrTreeRef α)

Creates reference for lazy discriminator tree that only contains this module's definitions. If droppedEntriesRef is provided, dropped entries (e.g., star-indexed lemmas) are extracted and appended to the array in the reference.

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.

def Lean.Meta.LazyDiscrTree.findMatchesExt {α β : Type} (moduleTreeRef : ModuleDiscrTreeRef α) (ref : IO.Ref (Option (LazyDiscrTree α))) (addEntry : Name → AsyncConstantInfo → MetaM (Array (InitEntry α))) (droppedKeys : List (List Key) := []) (constantsPerTask : Nat := 1000) (droppedEntriesRef : Option (IO.Ref (Option (Array α))) := none) (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.
• ref is a process-global 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.

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

findMatches searches for entries in a lazily initialized discriminator tree.

• ref is a process-global 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.
• droppedEntriesRef optionally stores entries dropped from the tree for later use.