(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`.

source
def Lean.Meta.DiscrTree.Key.lt :
Key → 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)

Instances For

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

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

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

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

source
def Lean.Meta.DiscrTree.Key.format :
Key → 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 = Std.format v
- (Lean.Meta.DiscrTree.Key.lit (Lean.Literal.strVal v)).format = repr v
- (Lean.Meta.DiscrTree.Key.const k a).format = Std.format k
- (Lean.Meta.DiscrTree.Key.proj s i a).format = Std.format s ++ Std.Format.text "." ++ Std.format i
- (Lean.Meta.DiscrTree.Key.fvar k a).format = Std.format k.name
- Lean.Meta.DiscrTree.Key.arrow.format = Std.Format.text "∀"

Instances For

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

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

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

Instances For

source
def Lean.Meta.DiscrTree.Key.arity :
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

Instances For

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

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

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

- Lean.Meta.DiscrTree.empty = { }

Instances For

source
partial def Lean.Meta.DiscrTree.Trie.format {α : Type} [ToFormat α] :
Trie α → Format
source
instance Lean.Meta.DiscrTree.instToFormatTrie {α : Type} [ToFormat α] :
ToFormat (Trie α)
Equations

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

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

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

Instances For

source
instance Lean.Meta.DiscrTree.instToFormat {α : Type} [ToFormat α] :
ToFormat (DiscrTree α)
Equations

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

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

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

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

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

Instances For

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

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

Instances For

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

Reduction procedure for the discrimination tree indexing.

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

whnf for the discrimination tree module

Equations

- Lean.Meta.DiscrTree.reduceDT e root = if root = true then Lean.Meta.DiscrTree.reduceUntilBadKey✝ e else Lean.Meta.DiscrTree.reduce e

Instances For

source
partial def Lean.Meta.DiscrTree.mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (noIndexAtArgs : Bool) :
MetaM (Array 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

source
def Lean.Meta.DiscrTree.mkPath (e : Expr) (noIndexAtArgs : Bool := false) :
MetaM (Array 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.

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

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

Equations

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

Instances For

source
def Lean.Meta.DiscrTree.getMatchWithExtra {α : Type} (d : DiscrTree α) (e : Expr) :
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.

Instances For

source
def Lean.Meta.DiscrTree.getMatchKeyRootFor (e : Expr) :
MetaM (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.

Instances For

source
def Lean.Meta.DiscrTree.getMatchLiberal {α : Type} (d : DiscrTree α) (e : Expr) :
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.

Instances For

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

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

Instances For

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

Monadically fold the keys and values stored in a `Trie`.

source
@[inline]
def Lean.Meta.DiscrTree.Trie.fold {σ : Type u_1} {α : Type} (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ) (t : 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

Instances For

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

Monadically fold the values stored in a `Trie`.

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

Fold the values stored in a `Trie`.

Equations

- Lean.Meta.DiscrTree.Trie.foldValues f init t = (Lean.Meta.DiscrTree.Trie.foldValuesM (fun (x1 : σ) (x2 : α) => pure (f x1 x2)) init t).run

Instances For

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

The number of values stored in a `Trie`.

source
@[inline]
def Lean.Meta.DiscrTree.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] (f : σ → Array Key → α → m σ) (init : σ) (t : 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

Instances For

source
@[inline]
def Lean.Meta.DiscrTree.fold {σ : Type u_1} {α : Type} (f : σ → Array Key → α → σ) (init : σ) (t : 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

Instances For

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

Monadically fold over the values stored in a `DiscrTree`.

Equations

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

Instances For

source
@[inline]
def Lean.Meta.DiscrTree.foldValues {σ : Type u_1} {α : Type} (f : σ → α → σ) (init : σ) (t : DiscrTree α) :
σ

Fold over the values stored in a `DiscrTree`.

Equations

- Lean.Meta.DiscrTree.foldValues f init t = (Lean.Meta.DiscrTree.foldValuesM (fun (x1 : σ) (x2 : α) => pure (f x1 x2)) init t).run

Instances For

source
@[inline]
def Lean.Meta.DiscrTree.containsValueP {α : Type} (t : 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

Instances For

source
@[inline]
def Lean.Meta.DiscrTree.values {α : Type} (t : DiscrTree α) :
Array α

Extract the values stored in a `DiscrTree`.

Equations

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

Instances For

source
@[inline]
def Lean.Meta.DiscrTree.toArray {α : Type} (t : DiscrTree α) :
Array (Array 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

Instances For

source
@[inline]
def Lean.Meta.DiscrTree.size {α : Type} (t : 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

Instances For

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

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

source
def Lean.Meta.DiscrTree.mapArraysM {m : Type → Type} [Monad m] {α β : Type} (d : DiscrTree α) (f : Array α → m (Array β)) :
m (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 }

Instances For

source
def Lean.Meta.DiscrTree.mapArrays {α β : Type} (d : DiscrTree α) (f : Array α → Array β) :
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

Instances For