nets.ml: speed up discrimination-net lookup#183
Open
aqjune-aws wants to merge 2 commits into
Open
Conversation
Replace the single (term_label * 'a net) list of edges in each net node with a record that splits children by label kind: a direct vnet field for the catchall Vnet edge plus persistent Map.Make balanced trees for Cnet/Lcnet (keyed by name+arity) and Lnet (keyed by arity). This is an algorithmic improvement to discrimination-net lookup: - Vnet branch is O(1) instead of an O(n) scan over edges. - Other lookups are O(log n) per bucket via balanced trees. - Comparators are monomorphic (String.compare / int compare) so the speedup is visible in bytecode as well as native code. Tips remain a sorted list because they are read in bulk (tryfind in REWRITES_CONV) and typically very short. Also annotate the head-classifier helpers (label_to_store / label_for_lookup) and net_update / follow with explicit term_label types so that grepping for term_label finds every place it flows. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Contributor
Author
|
The CI check failures are resolved! |
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.
Replace the single (term_label * 'a net) list of edges in each net node
with a record that splits children by label kind: a direct vnet field
for the catchall Vnet edge plus persistent Map.Make balanced trees for
Cnet/Lcnet (keyed by name+arity) and Lnet (keyed by arity).
This is an algorithmic improvement to discrimination-net lookup:
speedup is visible in bytecode as well as native code.
The speedup of running times of a couple of s2n-bignum proofs is as follows:
Also, at most 20% & in average 5% speedup is found from holtest.
This patch is purely written by Claude Code.
Also, this PR fixes holtest.mk's TacticTrace so that it doesn't have to rely on external
HOLLIGHT_DIRsetup.