(Imperfect) discrimination trees. We use a hybrid representation.
PersistentHashMapfor 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.
- 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
⟨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"
2- Distinguish partial applications
f a b, and
f a b c.
Reduction procedure for the discrimination tree indexing.
simpleReduce controls how aggressive the term is reduced.
The parameter at type
DiscrTree controls this value.
See comment at