b25bb78e2a
Try to improve the performance issue described at #587. The issue is that Mathlib contains thousands of theorems where the associated key for the discrimination tree is just `Key.other`. The indexing is not effective for them. This happens because 1- Lambda expressions are indexed using `Key.other`. The discrimination tree mainly focus on the first-order structure. 2- It unfolds reducible constants when inserting and retrieving entries. The motivation is that users expect simp theorems to fire modulo reducible constants. Then, we have many theorems such as ```lean map ?g ∘ map ?f = map (?g ∘ ?f) ``` when we expand the function composition on the left-hand side, we get ```lean fun (x : List ?α) => map ?g (map ?f x) ``` Which is indexed as `Key.other`. We should not avoid the `Array`s in the discrimination tree nodes If the index is working effectively, these arrays are all very small. In this commit, we try to address the problem by using a different approach. When processing the root of a pattern, we interrupt reduction as soon as the we hit something that would be indexed as `Key.other`. Note that, in Lean 3, the root of a pattern also receives special treatment. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| leanpkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||