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⟩, *, *, ⟨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.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          Equations
          Instances For
            Equations
            • Lean.Meta.DiscrTree.instToFormatTrie = { format := Lean.Meta.DiscrTree.Trie.format }
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              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
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    Instances For

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