Introduce and use a red-black tree implementation for sets #3261
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This 'set' is somewhat inefficient and problematic. Make the name reflect that, and use the class so replacing some instances of FlatSet for better implementations is seamless.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The implementation of
FStar.Compiler.Setis based on lists, and is very slow. We unfortunately rely on this fact in some places, such as for keeping the order of the generalized universe variables (iirc) and we cannot just switch the implementation.However, now with functional dependencies (#3260), we can abstract the set implementation into a
setlikeclass, so clients can be written parametrically in the set implementation, and many can coexist.This PR introduces an RBSet module with an implementation of sets based on red-black trees, and updates some old code to use this instead of the old set (which is now renamed FlatSet).
Further PRs should change instances of
FlatSet.ttoRBSet.t. I'm not trying to switch all of them right now. No big performance improvement yet.