9b29572604
Before this commit, given a term `let x : t := v in b`, `infer_type` would return `let x : t := v in T` where `T` is the type of `b` in the local context extended with declaration `x : t := v`. This is correct, but it produces unnecessarily large terms in the new compiler stack which makes a heavy use of let-expressions. We noticed the problem when the size of some .olean files were 100x bigger. For example, `repr.olean` increased from 136Kb to 13Mb after we started saving the `._cstage1` (code after after simplification) in the `.olean` files. The new implementation relies on the fact that `T` seldom depends on `x`. So, in most cases, the result is just `T` instead of `let x : t := v in T` After this change, the new .olean files are at most 56% bigger than .olean files not containing `._cstate1` code. This seems reasonable since most of our .olean files only contain code and we are storing a copy of each function. @kha The new lcnf format keeps exposing problems :) |
||
|---|---|---|
| .. | ||
| cmake | ||
| frontends/lean | ||
| init | ||
| kernel | ||
| library | ||
| runtime | ||
| shared | ||
| shell | ||
| tests | ||
| util | ||
| CMakeLists.txt | ||
| CTestConfig.cmake | ||
| CTestCustom.cmake.in | ||
| Doxyfile | ||
| githash.h.in | ||
| memcheck.supp | ||
| version.h.in | ||