(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
.
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
Reduction procedure for the discrimination tree indexing.
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
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
Fold the values stored in a Trie
.
Equations
Instances For
The number of values stored in a Trie
.
Fold over the values stored in a DiscrTree
.
Equations
Instances For
Extract the values stored in a DiscrTree
.
Equations
Instances For
Get the number of values stored in a DiscrTree
. O(n) in the size of the tree.