(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 respectively

⟨Add.add, 4⟩, α, *, *, *
⟨Add.add, 4⟩, Nat, *, ⟨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

• Lean.Meta.DiscrTree.Key.star.ctorIdx = 0
• Lean.Meta.DiscrTree.Key.other.ctorIdx = 1
• (Lean.Meta.DiscrTree.Key.lit a).ctorIdx = 2
• (Lean.Meta.DiscrTree.Key.fvar a a_1).ctorIdx = 3
• (Lean.Meta.DiscrTree.Key.const a a_1).ctorIdx = 4
• Lean.Meta.DiscrTree.Key.arrow.ctorIdx = 5
• (Lean.Meta.DiscrTree.Key.proj a a_1 a_2).ctorIdx = 6

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

Equations

• (Lean.Meta.DiscrTree.Key.lit v₁).lt (Lean.Meta.DiscrTree.Key.lit v₂) = decide (v₁ < v₂)
• (Lean.Meta.DiscrTree.Key.fvar n₁ a₁).lt (Lean.Meta.DiscrTree.Key.fvar n₂ a₂) = (n₁.name.quickLt n₂.name || n₁ == n₂ && decide (a₁ < a₂))
• (Lean.Meta.DiscrTree.Key.const n₁ a₁).lt (Lean.Meta.DiscrTree.Key.const n₂ a₂) = (n₁.quickLt n₂ || n₁ == n₂ && decide (a₁ < a₂))
• (Lean.Meta.DiscrTree.Key.proj s₁ i₁ a₁).lt (Lean.Meta.DiscrTree.Key.proj s₂ i₂ a₂) = (s₁.quickLt s₂ || s₁ == s₂ && decide (i₁ < i₂) || s₁ == s₂ && i₁ == i₂ && decide (a₁ < a₂))
• x✝.lt x = decide (x✝.ctorIdx < x.ctorIdx)

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.DiscrTree.Key.star.format = Std.Format.text "*"
• Lean.Meta.DiscrTree.Key.other.format = Std.Format.text "◾"
• (Lean.Meta.DiscrTree.Key.lit (Lean.Literal.natVal v)).format = Lean.format v
• (Lean.Meta.DiscrTree.Key.lit (Lean.Literal.strVal v)).format = repr v
• (Lean.Meta.DiscrTree.Key.const k a).format = Lean.format k
• (Lean.Meta.DiscrTree.Key.proj s i a).format = Lean.format s ++ Std.Format.text "." ++ Lean.format i
• (Lean.Meta.DiscrTree.Key.fvar k a).format = Lean.format k.name
• Lean.Meta.DiscrTree.Key.arrow.format = Std.Format.text "∀"

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.keysAsPattern (keys : Array Lean.Meta.DiscrTree.Key) : Lean.CoreM Lean.MessageData

Helper function for converting an entry (i.e., Array Key) to the discrimination tree into MessageData that is more user-friendly. We use this function to implement diagnostic information.

Equations

• Lean.Meta.DiscrTree.keysAsPattern keys = (Lean.Meta.DiscrTree.keysAsPattern.go false).run' keys.toList

def Lean.Meta.DiscrTree.keysAsPattern.next? : StateRefT' IO.RealWorld (List Lean.Meta.DiscrTree.Key) Lean.CoreM (Option Lean.Meta.DiscrTree.Key)

Equations

• Lean.Meta.DiscrTree.keysAsPattern.next? = do let __discr ← get match __discr with | key :: keys => do set keys pure (some key) | x => pure none

def Lean.Meta.DiscrTree.keysAsPattern.mkApp (f : Lean.MessageData) (args : Array Lean.MessageData) (parenIfNonAtomic : Bool) : Lean.CoreM Lean.MessageData

Equations

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

partial def Lean.Meta.DiscrTree.keysAsPattern.go (parenIfNonAtomic : Bool := true) : StateRefT' IO.RealWorld (List Lean.Meta.DiscrTree.Key) Lean.CoreM Lean.MessageData

partial def Lean.Meta.DiscrTree.keysAsPattern.goN (num : Nat) : StateRefT' IO.RealWorld (List Lean.Meta.DiscrTree.Key) Lean.CoreM (Array Lean.MessageData)

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

Equations

• (Lean.Meta.DiscrTree.Key.const a a_1).arity = a_1
• (Lean.Meta.DiscrTree.Key.fvar a a_1).arity = a_1
• Lean.Meta.DiscrTree.Key.arrow.arity = 1
• (Lean.Meta.DiscrTree.Key.proj a a_1 a_2).arity = 1 + a_2
• x.arity = 0

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

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

instance Lean.Meta.DiscrTree.instToFormatTrie {α : Type} [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} [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.instToFormat {α : Type} [Lean.ToFormat α] : Lean.ToFormat (Lean.Meta.DiscrTree α)

Equations

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

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

Equations

• Lean.Meta.DiscrTree.instInhabited = { default := { root := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } } }

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 = (Lean.annotation? `noindex e).isSome

partial def Lean.Meta.DiscrTree.reduce (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) : Lean.MetaM Lean.Expr

Reduction procedure for the discrimination tree indexing. The parameter config controls how aggressively 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) (config : Lean.Meta.WhnfCoreConfig) : Lean.MetaM Lean.Expr

whnf for the discrimination tree module

Equations

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

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

When noIndexAtArgs := true, pushArgs assumes function application arguments have a no_index annotation. That is, f a b is indexed as it was f (no_index a) (no_index b). This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670. In this issue, we have a local hypotheses (h : ∀ p : α × β, f p p.2 = p.2), and users expect it to be applicable to f (a, b) b = b. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing (h : ∀ p : α × β, f p (no_index p.2) = p.2), but this is very inconvenient when the hypotheses was not written by the user in first place. For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to simp (e.g., simp [h]), we use noIndexAtArgs := true. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365

def Lean.Meta.DiscrTree.mkPath (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) (noIndexAtArgs : Bool := false) : Lean.MetaM (Array Lean.Meta.DiscrTree.Key)

When noIndexAtArgs := true, pushArgs assumes function application arguments have a no_index annotation. That is, f a b is indexed as it was f (no_index a) (no_index b). This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670. In this issue, we have a local hypotheses (h : ∀ p : α × β, f p p.2 = p.2), and users expect it to be applicable to f (a, b) b = b. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing (h : ∀ p : α × β, f p (no_index p.2) = p.2), but this is very inconvenient when the hypotheses was not written by the user in first place. For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to simp (e.g., simp [h]), we use noIndexAtArgs := true. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365

Equations

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

def Lean.Meta.DiscrTree.insertCore {α : Type} [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} [BEq α] (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) (v : α) (config : Lean.Meta.WhnfCoreConfig) (noIndexAtArgs : Bool := false) : Lean.MetaM (Lean.Meta.DiscrTree α)

Equations

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

def Lean.Meta.DiscrTree.insertIfSpecific {α : Type} [BEq α] (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) (v : α) (config : Lean.Meta.WhnfCoreConfig) (noIndexAtArgs : Bool := false) : Lean.MetaM (Lean.Meta.DiscrTree α)

Inserts a value into a discrimination tree, but only if its key is not of the form #[*] or #[=, *, *, *].

Equations

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

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

Find values that match e in d.

Equations

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

def Lean.Meta.DiscrTree.getMatchWithExtra {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) : 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 α) (config : Lean.Meta.WhnfCoreConfig) (e : Lean.Expr) (numExtra : Nat) (result : Array (α × Nat)) : Lean.MetaM (Array (α × Nat))

def Lean.Meta.DiscrTree.getMatchKeyRootFor (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) : Lean.MetaM (Lean.Meta.DiscrTree.Key × Nat)

Return the root symbol for e, and the number of arguments after reduceDT.

Equations

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

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

A liberal version of getMatch which only takes the root symbol of e into account. We use this method to simulate Lean 3's indexing.

The natural number in the result is the number of arguments in e after reduceDT.

Equations

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

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

Equations

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

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

partial def Lean.Meta.DiscrTree.Trie.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] (initialKeys : Array Lean.Meta.DiscrTree.Key) (f : σ → Array Lean.Meta.DiscrTree.Key → α → m σ) (init : σ) : Lean.Meta.DiscrTree.Trie α → m σ

Monadically fold the keys and values stored in a Trie.

@[inline]

def Lean.Meta.DiscrTree.Trie.fold {σ : Type u_1} {α : Type} (initialKeys : Array Lean.Meta.DiscrTree.Key) (f : σ → Array Lean.Meta.DiscrTree.Key → α → σ) (init : σ) (t : Lean.Meta.DiscrTree.Trie α) : σ

Fold the keys and values stored in a Trie.

Equations

• Lean.Meta.DiscrTree.Trie.fold initialKeys f init t = (Lean.Meta.DiscrTree.Trie.foldM initialKeys (fun (s : σ) (k : Array Lean.Meta.DiscrTree.Key) (a : α) => pure (f s k a)) init t).run

partial def Lean.Meta.DiscrTree.Trie.foldValuesM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] (f : σ → α → m σ) (init : σ) : Lean.Meta.DiscrTree.Trie α → m σ

Monadically fold the values stored in a Trie.

@[inline]

def Lean.Meta.DiscrTree.Trie.foldValues {σ : Type u_1} {α : Type} (f : σ → α → σ) (init : σ) (t : Lean.Meta.DiscrTree.Trie α) : σ

Fold the values stored in a Trie.

Equations

• Lean.Meta.DiscrTree.Trie.foldValues f init t = (Lean.Meta.DiscrTree.Trie.foldValuesM f init t).run

partial def Lean.Meta.DiscrTree.Trie.size {α : Type} : Lean.Meta.DiscrTree.Trie α → Nat

The number of values stored in a Trie.

@[inline]

def Lean.Meta.DiscrTree.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] (f : σ → Array Lean.Meta.DiscrTree.Key → α → m σ) (init : σ) (t : Lean.Meta.DiscrTree α) : m σ

Monadically fold over the keys and values stored in a DiscrTree.

Equations

• Lean.Meta.DiscrTree.foldM f init t = t.root.foldlM (fun (s : σ) (k : Lean.Meta.DiscrTree.Key) (t : Lean.Meta.DiscrTree.Trie α) => Lean.Meta.DiscrTree.Trie.foldM #[k] f s t) init

@[inline]

def Lean.Meta.DiscrTree.fold {σ : Type u_1} {α : Type} (f : σ → Array Lean.Meta.DiscrTree.Key → α → σ) (init : σ) (t : Lean.Meta.DiscrTree α) : σ

Fold over the keys and values stored in a DiscrTree

Equations

• Lean.Meta.DiscrTree.fold f init t = (Lean.Meta.DiscrTree.foldM (fun (s : σ) (keys : Array Lean.Meta.DiscrTree.Key) (a : α) => pure (f s keys a)) init t).run

@[inline]

def Lean.Meta.DiscrTree.foldValuesM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] (f : σ → α → m σ) (init : σ) (t : Lean.Meta.DiscrTree α) : m σ

Monadically fold over the values stored in a DiscrTree.

Equations

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

@[inline]

def Lean.Meta.DiscrTree.foldValues {σ : Type u_1} {α : Type} (f : σ → α → σ) (init : σ) (t : Lean.Meta.DiscrTree α) : σ

Fold over the values stored in a DiscrTree.

Equations

• Lean.Meta.DiscrTree.foldValues f init t = (Lean.Meta.DiscrTree.foldValuesM f init t).run

@[inline]

def Lean.Meta.DiscrTree.containsValueP {α : Type} (t : Lean.Meta.DiscrTree α) (f : α → Bool) : Bool

Check for the presence of a value satisfying a predicate.

Equations

• t.containsValueP f = Lean.Meta.DiscrTree.foldValues (fun (r : Bool) (a : α) => r || f a) false t

@[inline]

def Lean.Meta.DiscrTree.values {α : Type} (t : Lean.Meta.DiscrTree α) : Array α

Extract the values stored in a DiscrTree.

Equations

• t.values = Lean.Meta.DiscrTree.foldValues (fun (as : Array α) (a : α) => as.push a) #[] t

@[inline]

def Lean.Meta.DiscrTree.toArray {α : Type} (t : Lean.Meta.DiscrTree α) : Array (Array Lean.Meta.DiscrTree.Key × α)

Extract the keys and values stored in a DiscrTree.

Equations

• t.toArray = Lean.Meta.DiscrTree.fold (fun (as : Array (Array Lean.Meta.DiscrTree.Key × α)) (keys : Array Lean.Meta.DiscrTree.Key) (a : α) => as.push (keys, a)) #[] t

@[inline]

def Lean.Meta.DiscrTree.size {α : Type} (t : Lean.Meta.DiscrTree α) : Nat

Get the number of values stored in a DiscrTree. O(n) in the size of the tree.

Equations

• t.size = t.root.foldl (fun (n : Nat) (x : Lean.Meta.DiscrTree.Key) (t : Lean.Meta.DiscrTree.Trie α) => n + t.size) 0

partial def Lean.Meta.DiscrTree.Trie.mapArraysM {m : Type → Type} [Monad m] {α β : Type} (t : Lean.Meta.DiscrTree.Trie α) (f : Array α → m (Array β)) : m (Lean.Meta.DiscrTree.Trie β)

Apply a monadic function to the array of values at each node in a DiscrTree.

def Lean.Meta.DiscrTree.mapArraysM {m : Type → Type} [Monad m] {α β : Type} (d : Lean.Meta.DiscrTree α) (f : Array α → m (Array β)) : m (Lean.Meta.DiscrTree β)

Apply a monadic function to the array of values at each node in a DiscrTree.

Equations

• d.mapArraysM f = do let __do_lift ← d.root.mapM fun (t : Lean.Meta.DiscrTree.Trie α) => t.mapArraysM f pure { root := __do_lift }

def Lean.Meta.DiscrTree.mapArrays {α β : Type} (d : Lean.Meta.DiscrTree α) (f : Array α → Array β) : Lean.Meta.DiscrTree β

Apply a function to the array of values at each node in a DiscrTree.

Equations

• d.mapArrays f = (d.mapArraysM fun (A : Array α) => pure (f A)).run