Motivated by a bug report for @karthikbhargavan in which a file was taking excessive memory to typecheck (even if admitting queries). I tracked it down (with some help from #3384) to the normalizer, and particularly the function inline_closure_env which closes a term being normalized to not depend on the KAM's environment. This process is really just a substitution of free indices by some well defined values, so this PR:
1- Removes that function altogether.
2- Introduces env_subst which computes a substitution given a KAM environment.
3- This substitution is cached, so as to not recompute it for the same environment repeatedly.
4- Reimplements closure_as_term by computing the substitution and applying it. This has the enormous benefit of being lazy, so it's O(1) if the term happens to not be forced.
5- Finally, this function adds a pass to still respect DefaultUnivsToZero.
For the file that triggered this change, it used to blow up in memory to at least 30GB and >2m, while now it finished in 45s with 1.6GB. A perf comparison over the F* regressions suite shows that this is somewhat of an improvement (somefiles are 3x faster, like Test.QuickCode). I would like to run an everest comparison too.
Motivated by a bug report for @karthikbhargavan in which a file was taking excessive memory to typecheck (even if admitting queries). I tracked it down (with some help from #3384) to the normalizer, and particularly the function
inline_closure_envwhich closes a term being normalized to not depend on the KAM's environment. This process is really just a substitution of free indices by some well defined values, so this PR:1- Removes that function altogether. 2- Introduces
env_substwhich computes a substitution given a KAM environment. 3- This substitution is cached, so as to not recompute it for the same environment repeatedly. 4- Reimplementsclosure_as_termby computing the substitution and applying it. This has the enormous benefit of being lazy, so it's O(1) if the term happens to not be forced. 5- Finally, this function adds a pass to still respectDefaultUnivsToZero.For the file that triggered this change, it used to blow up in memory to at least 30GB and >2m, while now it finished in 45s with 1.6GB. A perf comparison over the F* regressions suite shows that this is somewhat of an improvement (somefiles are 3x faster, like Test.QuickCode). I would like to run an everest comparison too.