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
    Instances For
      Equations
        Instances For
          Equations
            Instances For

              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
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For

                                  Reduction procedure for the discrimination tree indexing.

                                  whnf for the discrimination tree module

                                  Equations
                                    Instances For
                                      partial def Lean.Meta.DiscrTree.mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (noIndexAtArgs : Bool) :

                                      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 : Expr) (noIndexAtArgs : Bool := false) :

                                      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
                                        Instances For
                                          def Lean.Meta.DiscrTree.insertCore {α : Type} [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) :
                                          Equations
                                            Instances For
                                              def Lean.Meta.DiscrTree.insert {α : Type} [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (noIndexAtArgs : Bool := false) :
                                              Equations
                                                Instances For
                                                  def Lean.Meta.DiscrTree.insertIfSpecific {α : Type} [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (noIndexAtArgs : Bool := false) :

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

                                                  Equations
                                                    Instances For
                                                      def Lean.Meta.DiscrTree.getMatch {α : Type} (d : DiscrTree α) (e : Expr) :

                                                      Find values that match e in d.

                                                      Equations
                                                        Instances For

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

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

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

                                                              Equations
                                                                Instances For

                                                                  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
                                                                    Instances For
                                                                      def Lean.Meta.DiscrTree.getUnify {α : Type} (d : DiscrTree α) (e : Expr) :
                                                                      Equations
                                                                        Instances For
                                                                          partial def Lean.Meta.DiscrTree.getUnify.process {α : Type} (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) :
                                                                          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.

                                                                          @[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
                                                                            Instances For
                                                                              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.

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

                                                                              Fold the values stored in a Trie.

                                                                              Equations
                                                                                Instances For
                                                                                  partial def Lean.Meta.DiscrTree.Trie.size {α : Type} :
                                                                                  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 Keyαm σ) (init : σ) (t : DiscrTree α) :
                                                                                  m σ

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

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[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
                                                                                        Instances For
                                                                                          @[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
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def Lean.Meta.DiscrTree.foldValues {σ : Type u_1} {α : Type} (f : σασ) (init : σ) (t : DiscrTree α) :
                                                                                              σ

                                                                                              Fold over the values stored in a DiscrTree.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Lean.Meta.DiscrTree.containsValueP {α : Type} (t : DiscrTree α) (f : αBool) :

                                                                                                  Check for the presence of a value satisfying a predicate.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[inline]

                                                                                                      Extract the values stored in a DiscrTree.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          @[inline]

                                                                                                          Extract the keys and values stored in a DiscrTree.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              @[inline]

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

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  partial def Lean.Meta.DiscrTree.Trie.mapArraysM {m : TypeType} [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.

                                                                                                                  def Lean.Meta.DiscrTree.mapArraysM {m : TypeType} [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
                                                                                                                    Instances For
                                                                                                                      def Lean.Meta.DiscrTree.mapArrays {α β : Type} (d : DiscrTree α) (f : Array αArray β) :

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

                                                                                                                      Equations
                                                                                                                        Instances For