(Imperfect) discrimination trees. We use a hybrid representation.

• A PersistentHashMap for the root node which usually contains many children.
• A sorted array of key/node pairs for inner nodes.

The edges are labeled by keys:

• Constant names (and arity). Universe levels are ignored.
• Free variables (and arity). Thus, an entry in the discrimination tree may reference hypotheses from the local context.
• Literals
• Star/Wildcard. We use them to represent metavariables and terms we want to ignore. We ignore implicit arguments and proofs.
• Other. We use to represent other kinds of terms (e.g., nested lambda, forall, sort, etc).

We reduce terms using TransparencyMode.reducible. Thus, all reducible definitions in an expression e are unfolded before we insert it into the discrimination tree.

Recall that projections from classes are NOT reducible. For example, the expressions Add.add α (ringAdd ?α ?s) ?x ?x and Add.add Nat Nat.hasAdd a b generates paths with the following keys respctively

⟨Add.add, 4⟩, *, *, *, *
⟨Add.add, 4⟩, *, *, ⟨a,0⟩, ⟨b,0⟩

That is, we don't reduce Add.add Nat inst a b into Nat.add a b. We say the Add.add applications are the de-facto canonical forms in the metaprogramming framework. Moreover, it is the metaprogrammer's responsibility to re-pack applications such as Nat.add a b into Add.add Nat inst a b.

Remark: we store the arity in the keys 1- To be able to implement the "skip" operation when retrieving "candidate" unifiers. 2- Distinguish partial applications f a, f a b, and f a b c.

def Lean.Meta.DiscrTree.Key.ctorIdx : Lean.Meta.DiscrTree.Key → Nat

Equations

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

def Lean.Meta.DiscrTree.Key.lt : Lean.Meta.DiscrTree.Key → Lean.Meta.DiscrTree.Key → Bool

Equations

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

instance Lean.Meta.DiscrTree.instLTKey : LT Lean.Meta.DiscrTree.Key

Equations

• Lean.Meta.DiscrTree.instLTKey = { lt := fun a b => Lean.Meta.DiscrTree.Key.lt a b = true }

instance Lean.Meta.DiscrTree.instDecidableLtKeyInstLTKey (a : Lean.Meta.DiscrTree.Key) (b : Lean.Meta.DiscrTree.Key) : Decidable (a < b)

Equations

• Lean.Meta.DiscrTree.instDecidableLtKeyInstLTKey a b = inferInstanceAs (Decidable (Lean.Meta.DiscrTree.Key.lt a b = true))

def Lean.Meta.DiscrTree.Key.format : Lean.Meta.DiscrTree.Key → Lean.Format

Equations

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

instance Lean.Meta.DiscrTree.instToFormatKey : Lean.ToFormat Lean.Meta.DiscrTree.Key

Equations

• Lean.Meta.DiscrTree.instToFormatKey = { format := Lean.Meta.DiscrTree.Key.format }

def Lean.Meta.DiscrTree.Key.arity : Lean.Meta.DiscrTree.Key → Nat

Equations

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

instance Lean.Meta.DiscrTree.instInhabitedTrie {α : Type} : Inhabited (Lean.Meta.DiscrTree.Trie α)

Equations

• Lean.Meta.DiscrTree.instInhabitedTrie = { default := Lean.Meta.DiscrTree.Trie.node #[] #[] }

def Lean.Meta.DiscrTree.empty {α : Type} : Lean.Meta.DiscrTree α

Equations

• Lean.Meta.DiscrTree.empty = { root := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }

partial def Lean.Meta.DiscrTree.Trie.format {α : Type} [inst : Lean.ToFormat α] : Lean.Meta.DiscrTree.Trie α → Lean.Format

instance Lean.Meta.DiscrTree.instToFormatTrie {α : Type} [inst : Lean.ToFormat α] : Lean.ToFormat (Lean.Meta.DiscrTree.Trie α)

Equations

• Lean.Meta.DiscrTree.instToFormatTrie = { format := Lean.Meta.DiscrTree.Trie.format }

def Lean.Meta.DiscrTree.format {α : Type} [inst : Lean.ToFormat α] (d : Lean.Meta.DiscrTree α) : Lean.Format

Equations

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

instance Lean.Meta.DiscrTree.instToFormatDiscrTree {α : Type} [inst : Lean.ToFormat α] : Lean.ToFormat (Lean.Meta.DiscrTree α)

Equations

• Lean.Meta.DiscrTree.instToFormatDiscrTree = { format := Lean.Meta.DiscrTree.format }

instance Lean.Meta.DiscrTree.instInhabitedDiscrTree {α : Type} : Inhabited (Lean.Meta.DiscrTree α)

Equations

• Lean.Meta.DiscrTree.instInhabitedDiscrTree = { default := { root := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }

def Lean.Meta.DiscrTree.mkNoindexAnnotation (e : Lean.Expr) : Lean.Expr

Equations

• Lean.Meta.DiscrTree.mkNoindexAnnotation e = Lean.mkAnnotation (Lean.Name.mkStr1 "noindex") e

def Lean.Meta.DiscrTree.hasNoindexAnnotation (e : Lean.Expr) : Bool

Equations

• Lean.Meta.DiscrTree.hasNoindexAnnotation e = Option.isSome (Lean.annotation? (Lean.Name.mkStr1 "noindex") e)

def Lean.Meta.DiscrTree.whnfDT (e : Lean.Expr) (root : Bool) : Lean.MetaM Lean.Expr

whnf for the discrimination tree module

Equations

• Lean.Meta.DiscrTree.whnfDT e root = if root = true then Lean.Meta.DiscrTree.whnfUntilBadKey e else Lean.Meta.DiscrTree.whnfEta e

partial def Lean.Meta.DiscrTree.mkPathAux (root : Bool) (todo : Array Lean.Expr) (keys : Array Lean.Meta.DiscrTree.Key) : Lean.MetaM (Array Lean.Meta.DiscrTree.Key)

def Lean.Meta.DiscrTree.mkPath (e : Lean.Expr) : Lean.MetaM (Array Lean.Meta.DiscrTree.Key)

Equations

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

def Lean.Meta.DiscrTree.insertCore {α : Type} [inst : BEq α] (d : Lean.Meta.DiscrTree α) (keys : Array Lean.Meta.DiscrTree.Key) (v : α) : Lean.Meta.DiscrTree α

Equations

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

def Lean.Meta.DiscrTree.insert {α : Type} [inst : BEq α] (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) (v : α) : Lean.MetaM (Lean.Meta.DiscrTree α)

Equations

• Lean.Meta.DiscrTree.insert d e v = do let keys ← Lean.Meta.DiscrTree.mkPath e pure (Lean.Meta.DiscrTree.insertCore d keys v)

def Lean.Meta.DiscrTree.getMatch {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) : Lean.MetaM (Array α)

Find values that match e in d.

Equations

• Lean.Meta.DiscrTree.getMatch d e = do let a ← Lean.Meta.DiscrTree.getMatchCore d e pure a.snd

def Lean.Meta.DiscrTree.getMatchWithExtra {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) : Lean.MetaM (Array (α × Nat))

Similar to getMatch, but returns solutions that are prefixes of e. We store the number of ignored arguments in the result.

Equations

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

partial def Lean.Meta.DiscrTree.getMatchWithExtra.mayMatchPrefix {α : Type} (d : Lean.Meta.DiscrTree α) (k : Lean.Meta.DiscrTree.Key) : Lean.MetaM Bool

partial def Lean.Meta.DiscrTree.getMatchWithExtra.go {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) (numExtra : Nat) (result : Array (α × Nat)) : Lean.MetaM (Array (α × Nat))

def Lean.Meta.DiscrTree.getUnify {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) : Lean.MetaM (Array α)

Equations

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

partial def Lean.Meta.DiscrTree.getUnify.process {α : Type} (skip : Nat) (todo : Array Lean.Expr) (c : Lean.Meta.DiscrTree.Trie α) (result : Array α) : Lean.MetaM (Array α)