(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 {s : Bool} : Lean.Meta.DiscrTree.Key s → Nat

Equations

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

def Lean.Meta.DiscrTree.Key.lt {s : Bool} : Lean.Meta.DiscrTree.Key s → Lean.Meta.DiscrTree.Key s → Bool

Equations

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

instance Lean.Meta.DiscrTree.instLTKey {s : Bool} : LT (Lean.Meta.DiscrTree.Key s)

Equations

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

instance Lean.Meta.DiscrTree.instDecidableLtKeyInstLTKey {s : Bool} (a : Lean.Meta.DiscrTree.Key s) (b : Lean.Meta.DiscrTree.Key s) : 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 {s : Bool} : Lean.Meta.DiscrTree.Key s → Lean.Format

Equations

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

instance Lean.Meta.DiscrTree.instToFormatKey {s : Bool} : Lean.ToFormat (Lean.Meta.DiscrTree.Key s)

Equations

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

def Lean.Meta.DiscrTree.Key.arity {s : Bool} : Lean.Meta.DiscrTree.Key s → Nat

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.DiscrTree.mkNoindexAnnotation e = Lean.mkAnnotation `noindex e

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

Equations

• Lean.Meta.DiscrTree.hasNoindexAnnotation e = Option.isSome (Lean.annotation? `noindex e)

partial def Lean.Meta.DiscrTree.reduce (e : Lean.Expr) (simpleReduce : Bool) : Lean.MetaM Lean.Expr

Reduction procedure for the discrimination tree indexing. The parameter simpleReduce controls how aggressive the term is reduced. The parameter at type DiscrTree controls this value. See comment at DiscrTree.

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

whnf for the discrimination tree module

Equations

• Lean.Meta.DiscrTree.reduceDT e root simpleReduce = if root = true then Lean.Meta.DiscrTree.reduceUntilBadKey e simpleReduce else Lean.Meta.DiscrTree.reduce e simpleReduce

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

def Lean.Meta.DiscrTree.mkPath {s : Bool} (e : Lean.Expr) : Lean.MetaM (Array (Lean.Meta.DiscrTree.Key s))

Equations

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

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

Equations

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

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

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} {s : Bool} (d : Lean.Meta.DiscrTree α s) (e : Lean.Expr) : Lean.MetaM (Array α)

Find values that match e in d.

Equations

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

def Lean.Meta.DiscrTree.getMatchWithExtra {α : Type} {s : Bool} (d : Lean.Meta.DiscrTree α s) (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} {s : Bool} (d : Lean.Meta.DiscrTree α s) (k : Lean.Meta.DiscrTree.Key s) : Lean.MetaM Bool

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

def Lean.Meta.DiscrTree.getUnify {α : Type} {s : Bool} (d : Lean.Meta.DiscrTree α s) (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} {s : Bool} (skip : Nat) (todo : Array Lean.Expr) (c : Lean.Meta.DiscrTree.Trie α s) (result : Array α) : Lean.MetaM (Array α)