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

⟨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.

Instances For
    partial def Lean.Meta.DiscrTree.reduce (e : Lean.Expr) (simpleReduce : Bool) :

    Reduction procedure for the discrimination tree indexing. The parameter simpleReduce controls how aggressive the term is reduced. The parameter at type DiscrTree controls this value. See comment at DiscrTree.

    whnf for the discrimination tree module

    Instances For
      Instances For
        def Lean.Meta.DiscrTree.insert {α : Type} {s : Bool} [BEq α] (d : Lean.Meta.DiscrTree α s) (e : Lean.Expr) (v : α) :
        Instances For

          Find values that match e in d.

          Instances For

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

            Instances For
              partial def Lean.Meta.DiscrTree.getMatchWithExtra.go {α : Type} {s : Bool} (d : Lean.Meta.DiscrTree α s) (e : Lean.Expr) (numExtra : Nat) (result : Array (α × Nat)) :
              Instances For
                partial def Lean.Meta.DiscrTree.getUnify.process {α : Type} {s : Bool} (skip : Nat) (todo : Array Lean.Expr) (c : Lean.Meta.DiscrTree.Trie α s) (result : Array α) :