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

source
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

Instances For

source
instance Lean.Meta.LazyDiscrTree.instInhabitedKey :
Inhabited Key
Equations

- Lean.Meta.LazyDiscrTree.instInhabitedKey = { default := Lean.Meta.LazyDiscrTree.instInhabitedKey.default }

source
def Lean.Meta.LazyDiscrTree.instInhabitedKey.default :
Key
Equations

- Lean.Meta.LazyDiscrTree.instInhabitedKey.default = Lean.Meta.LazyDiscrTree.Key.const default default

Instances For

source
instance Lean.Meta.LazyDiscrTree.instBEqKey :
BEq Key
Equations

- Lean.Meta.LazyDiscrTree.instBEqKey = { beq := Lean.Meta.LazyDiscrTree.instBEqKey.beq }

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

- Lean.Meta.LazyDiscrTree.instBEqKey.beq (Lean.Meta.LazyDiscrTree.Key.const a a_1) (Lean.Meta.LazyDiscrTree.Key.const b b_1) = (a == b && a_1 == b_1)
- Lean.Meta.LazyDiscrTree.instBEqKey.beq (Lean.Meta.LazyDiscrTree.Key.fvar a a_1) (Lean.Meta.LazyDiscrTree.Key.fvar b b_1) = (a == b && a_1 == b_1)
- Lean.Meta.LazyDiscrTree.instBEqKey.beq (Lean.Meta.LazyDiscrTree.Key.lit a) (Lean.Meta.LazyDiscrTree.Key.lit b) = (a == b)
- Lean.Meta.LazyDiscrTree.instBEqKey.beq Lean.Meta.LazyDiscrTree.Key.star Lean.Meta.LazyDiscrTree.Key.star = true
- Lean.Meta.LazyDiscrTree.instBEqKey.beq Lean.Meta.LazyDiscrTree.Key.other Lean.Meta.LazyDiscrTree.Key.other = true
- Lean.Meta.LazyDiscrTree.instBEqKey.beq Lean.Meta.LazyDiscrTree.Key.arrow Lean.Meta.LazyDiscrTree.Key.arrow = true
- Lean.Meta.LazyDiscrTree.instBEqKey.beq (Lean.Meta.LazyDiscrTree.Key.proj a a_1 a_2) (Lean.Meta.LazyDiscrTree.Key.proj b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
- Lean.Meta.LazyDiscrTree.instBEqKey.beq x✝¹ x✝ = false

Instances For

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

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

Instances For

source
instance Lean.Meta.LazyDiscrTree.instReprKey :
Repr Key
Equations

- Lean.Meta.LazyDiscrTree.instReprKey = { reprPrec := Lean.Meta.LazyDiscrTree.instReprKey.repr }

source
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))

Instances For

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

- Lean.Meta.LazyDiscrTree.Key.instHashable = { hash := Lean.Meta.LazyDiscrTree.Key.hash }

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

- Lean.Meta.LazyDiscrTree.MatchClone.tmpMVarId = { name := `_discr_tree_tmp }

Instances For

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

- Lean.Meta.LazyDiscrTree.MatchClone.tmpStar = Lean.mkMVar Lean.Meta.LazyDiscrTree.MatchClone.tmpMVarId

Instances For

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

Equations

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

Instances For

source
partial def Lean.Meta.LazyDiscrTree.MatchClone.pushArgsAux (infos : Array ParamInfo) :
Nat → Expr → Array Expr → MetaM (Array Expr)
source
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`

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

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

Instances For

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

- Lean.Meta.LazyDiscrTree.MatchClone.isNatType e = do let __do_lift ← Lean.Meta.whnf e pure (__do_lift.isConstOf `Nat)

Instances For

source
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`

Equations

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

Instances For

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

- Lean.Meta.LazyDiscrTree.MatchClone.shouldAddAsStar fName e = Lean.Meta.LazyDiscrTree.MatchClone.isNatOffset fName e

Instances For

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

Equations

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

Instances For

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

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

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.LazyDiscrTree.MatchClone.getMatchKeyArgs (e : Expr) (root : Bool) :
MetaM (Key × Array Expr)
Equations

- Lean.Meta.LazyDiscrTree.MatchClone.getMatchKeyArgs e root = Lean.Meta.LazyDiscrTree.MatchClone.getKeyArgs e true root

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.LazyDiscrTree.LazyEntry (α : Type u_1) :
Type u_1

An unprocessed entry in the lazy discrimination tree.

Equations

- Lean.Meta.LazyDiscrTree.LazyEntry α = (Array Lean.Expr × (Lean.LocalContext × Lean.LocalInstances) × α)

Instances For

source
@[reducible]
def Lean.Meta.LazyDiscrTree.TrieIndex :
Type

Index identifying trie in a discrimination tree.

Equations

- Lean.Meta.LazyDiscrTree.TrieIndex = Nat

Instances For

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

- )

Instances For

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

- Lean.Meta.LazyDiscrTree.instInhabitedTrie = { default := Lean.Meta.LazyDiscrTree.instInhabitedTrie.default }

source
def Lean.Meta.LazyDiscrTree.instInhabitedTrie.default {a✝ : Type} :
Trie a✝
Equations

- Lean.Meta.LazyDiscrTree.instInhabitedTrie.default = { values := default, star := default, children := default, pending := default }

Instances For

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

- Lean.Meta.LazyDiscrTree.instEmptyCollectionTrie = { emptyCollection := { values := #[], star := 0, children := ∅ } }

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

Push lazy entry to trie.

Equations

- { values := vs, star := star, children := cs, pending := p }.pushPending x✝ = { values := vs, star := star, children := cs, pending := p.push x✝ }

Instances For

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

Instances For

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

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

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

Specialization of Lean.Meta.DiscrTree.pushArgs

Equations

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

Instances For

source
def Lean.Meta.LazyDiscrTree.initCapacity :
Nat

Initial capacity for key and todo vector.

Equations

- Lean.Meta.LazyDiscrTree.initCapacity = 8

Instances For

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

Equations

- Lean.Meta.LazyDiscrTree.rootKey e = Lean.Meta.LazyDiscrTree.pushArgs true (Array.mkEmpty Lean.Meta.LazyDiscrTree.initCapacity) e

Instances For

source
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)
source
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.

Instances For

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

Instances For

source
@[reducible]
def Lean.Meta.LazyDiscrTree.MatchM (α : Type) :
Type → Type
Equations

- Lean.Meta.LazyDiscrTree.MatchM α = StateRefT' IO.RealWorld (Array (Lean.Meta.LazyDiscrTree.Trie α)) Lean.MetaM

Instances For

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

- { tries := a, roots := r }.runMatch m = do let __discr ← Lean.Meta.withReducible (StateRefT'.run m a) match __discr with | (result, a) => pure (result, { tries := a, roots := r })

Instances For

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

- Lean.Meta.LazyDiscrTree.setTrie i v = modify fun (x : Array (Lean.Meta.LazyDiscrTree.Trie α)) => x.set! i v

Instances For

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

Equations

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

Instances For

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

Add a lazy entry to an existing trie.

Equations

- Lean.Meta.LazyDiscrTree.addLazyEntryToTrie i e = modify fun (x : Array (Lean.Meta.LazyDiscrTree.Trie α)) => x.modify i fun (x : Lean.Meta.LazyDiscrTree.Trie α) => x.pushPending e

Instances For

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

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

Instances For

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

Equations

- Lean.Meta.LazyDiscrTree.evalLazyEntries values starIdx children entries = Array.foldlM Lean.Meta.LazyDiscrTree.evalLazyEntry (values, starIdx, children) entries

Instances For

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

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

Instances For

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

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

Instances For

source
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 <$> t.runMatch (Lean.Meta.LazyDiscrTree.dropKeyAux (t.roots.getD k 0) r)

Instances For

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

Instances For

source
def Lean.Meta.LazyDiscrTree.MatchResult.push {α : Type} (r : MatchResult α) (score : Nat) (e : Array α) :
MatchResult α
Equations

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

Instances For

source
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

Instances For

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

Instances For

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

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

Instances For

source
structure Lean.Meta.LazyDiscrTree.PartialMatch :
Type

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

Instances For

source
instance Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch :
Inhabited PartialMatch
Equations

- Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch = { default := Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch.default }

source
def Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch.default :
PartialMatch
Equations

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

Instances For

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

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

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

Instances For

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

- Lean.Meta.LazyDiscrTree.pushRootCase r k args cases = match r[k]? with | none => cases | some c => cases.push { todo := args, score := 1, c := c }

Instances For

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

Find values that match `e` in `root`.

Equations

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

Instances For

source
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 (d.runMatch (Lean.Meta.LazyDiscrTree.getMatchCore d.roots e))

Instances For

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

Instances For

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

- Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree = { default := Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree.default }

source
def Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree.default {a✝ : Type} :
PreDiscrTree a✝
Equations

- Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree.default = { roots := default, tries := default }

Instances For

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

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

Instances For

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

Add an entry to the pre-discrimination tree.

Equations

- d.push k e = d.modifyAt k fun (x : Array (Lean.Meta.LazyDiscrTree.LazyEntry α)) => x.push e

Instances For

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

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

Equations

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

Instances For

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

Merge two discrimination trees.

Equations

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

Instances For

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

- Lean.Meta.LazyDiscrTree.PreDiscrTree.instAppend = { append := Lean.Meta.LazyDiscrTree.PreDiscrTree.append }

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
structure Lean.Meta.LazyDiscrTree.ImportData :
Type

Information generation from imported modules.

- errors : IO.Ref (Array ImportFailure)

Instances For

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

- Lean.Meta.LazyDiscrTree.ImportData.new = do let errors ← IO.mkRef #[] pure { errors := errors }

Instances For

source
structure Lean.Meta.LazyDiscrTree.Cache :
Type

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

Instances For

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

- Lean.Meta.LazyDiscrTree.Cache.empty ngen = { ngen := ngen, core := { }, «meta» := { } }

Instances For

source
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)

Instances For

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

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

Instances For

source
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

Instances For

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

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

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

Combine two initial results.

Equations

- { tree := yv, errors := ye }.append { tree := yv_1, errors := ye_1 } = { tree := yv ++ yv_1, errors := ye ++ ye_1 }

Instances For

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

- Lean.Meta.LazyDiscrTree.InitResults.instAppend = { append := Lean.Meta.LazyDiscrTree.InitResults.append }

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

- Lean.Meta.LazyDiscrTree.toFlat d tree = do let de ← ST.Ref.swap d.errors #[] pure { tree := tree, errors := de }

Instances For

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

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

Instances For

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

Get the results of each task and merge using combining function

Equations

- Lean.Meta.LazyDiscrTree.combineGet z tasks = Array.foldl (fun (x : α) (t : Task α) => x ++ t.get) z tasks

Instances For

source
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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

Instances For

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

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

Equations

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

Instances For

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

Instances For

source
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 α)

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For