Documentation

Lean.Meta.DiscrTree

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

The edges are labeled by keys:

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.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
  • Lean.Meta.DiscrTree.instToFormatTrie = { format := Lean.Meta.DiscrTree.Trie.format }
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Lean.Meta.DiscrTree.instToFormatDiscrTree = { format := Lean.Meta.DiscrTree.format }
Equations
  • One or more equations did not get rendered due to their size.

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.

whnf for the discrimination tree module

Equations

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

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.
Equations
  • One or more equations did not get rendered due to their size.
Equations

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.

Find values that match e in d.

Equations

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.go {α : Type} (d : Lean.Meta.DiscrTree α) (config : Lean.Meta.WhnfCoreConfig) (e : Lean.Expr) (numExtra : Nat) (result : Array (α × Nat)) :
Equations
  • One or more equations did not get rendered due to their size.
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 : σ) :

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
  • One or more equations did not get rendered due to their size.
partial def Lean.Meta.DiscrTree.Trie.foldValuesM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] (f : σαm σ) (init : σ) :

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

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
  • One or more equations did not get rendered due to their size.
@[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
@[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
@[inline]

Check for the presence of a value satisfying a predicate.

Equations
@[inline]

Extract the values stored in a DiscrTree.

Equations
@[inline]

Extract the keys and values stored in a DiscrTree.

Equations
  • One or more equations did not get rendered due to their size.
@[inline]

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

Equations
  • One or more equations did not get rendered due to their size.
partial def Lean.Meta.DiscrTree.Trie.mapArraysM {m : TypeType} [Monad m] {α : Type} {β : Type} (t : Lean.Meta.DiscrTree.Trie α) (f : Array αm (Array β)) :

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

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

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

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

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

Equations