FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Optimize name resolution in desugaring #3586

Closed nikswamy closed 1 month ago

nikswamy commented 1 month ago

Another fix prompted by @LukeXuan (thanks!)

Resolving names during desugaring involved a linear scan of a list of names in scope.

For modules with a large number of definitions, this exposes quadratic behavior in desugaring.

This PR fixes the problem by coalescing streaks of local bindings and top-level definitions in the environment into maps for faster lookup.