Store max-bound variable in terms

[brendanzab]

Lean (apparently) stores the maximum bound variable to improve the performance of its locally nameless representation.

Here is a quote from section 3.3 in Elaboration in Dependent Type Theory (note that 'instantiate/abstract' maps to 'open/close' respectively in our nomenclature):

Although the locally nameless approach greatly simplifies the implementation effort, there is a performance penalty. Given a term t of size n with m binders, it takes O(nm) time to visit t while making sure there are no dangling bound variables. In [21], the authors suggest that this cost can be minimized by generalizing abstract and instantiate to process sequences of free and bound variables. This optimization is particularly effective when visiting terms containing several consecutive binders, such as λx₁ : A₁, λx₂ : A₂, … , λx_n : A_n, t. Nonetheless, we observed that these two operations were still a performance bottleneck for several files in the Lean standard library. We have addressed this problem using a very simple complementary optimization. For each term t, we store a bound B such that all de Bruijn indices occurring in t are in the range [0,B). This bound can easily be computed when we create new terms: the bound for the de Bruijn variable with index n is n + 1, and given terms t and s with bounds Bt and Bs respectively, the bound for the application (t s) is max(Bt,Bs), and the bound for (λx:t,s) is max(Bt,_Bs_−1). We use the bound B to optimize the instantiate operation. The idea is simple: B enables us to decide quickly whether any subterm contains a bound variable being instantiated or not. If it does not, then our instantiate procedure does not even visit the subterm. Similarly, for each term t, we store a bit that is set to “true” if and only if t contains a free variable. We use this bit to optimize the abstract operation, since it enables us to decide quickly whether a subterm contains a free variable.

These optimizations are crucial to our implementation. The Lean standard library currently contains 172 files, and 41,700 lines of Lean code. With the optimizations, the whole library can be compiled in 71.06 seconds using an Intel Core i7 3.6Ghz processor with 32Gb of memory. Without the optimizations, it takes 2,189.97 seconds to compile the same set of files.

Perhaps our Scope<P, T> type could include this binding depth as a field?

[brendanzab]

The range seems to be defined here: https://github.com/leanprover/lean/blob/d36b859c6579ce1b86f257a494bb99417c7cdac1/src/kernel/expr.h#L594-L600

This is used in instantiate here: https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/src/kernel/instantiate.cpp#L80-L111