Conversation
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
This adds several mark bits to IL nodes that track whether a term is in normal form. This is meant as an optimisation to avoid redundant work when reducing again, or when substituting into closed terms.
Three NFs are distinguished: closed (the term is essentially a value), dynamic (the term is the result of regular reduction and hasn't failed), static (the term is the result of static reduction that stops short of the failure steps). Closed implies dynamic implies static NF.
The result is a 10+% improvement of runtime for the test suite.
Before this optimisation:
make test 340.31s user 11.95s system 100% cpu 5:49.03 total
make test-frontend 45.78s user 6.45s system 117% cpu 44.284 total
After this optimisation:
make test 295.00s user 11.93s system 101% cpu 5:03.42 total
make test-frontend 40.71s user 5.91s system 120% cpu 38.785 total
(Each make was run after
make clean; make)Presumably, most of the win comes from the running times of the IL validator.