Module discrimination 

First-order discrimination tree: the shared pattern index under simp rule lookup, exact?/apply? library search, and crush’s E-matching.

How it works

A pattern is flattened to its preorder key sequence — head symbols carrying their arity, with * at each pattern-variable position — and inserted into a trie. Retrieval walks the trie in step with the query’s own flattening: a symbol edge must match the query symbol exactly; a * edge skips one complete query subterm (the arity annotations make subterm extents computable without re-walking the term).

The contract

Retrieval NEVER MISSES: every inserted pattern that one-sided matches the query (per crate::unify::match_term_pattern) is among the candidates. It may over-approximate — variable positions are treated independently, so the non-linear pattern f(x, x) is retrieved for f(a, b) — and the matcher is the arbiter. The value of the tree is pruning: a query touches only patterns sharing its head structure, not the whole rule set.

Quantified subexpressions flatten to * on both sides (opaque), which preserves never-miss at the cost of extra candidates — the conservative choice for shapes the matcher itself treats conservatively.

Structs

DiscTree

A discrimination tree mapping term/expression patterns to payloads.