feat: Extract constant array and slice literals as single data-carrying builtins - #312
Open
TomAFrench wants to merge 2 commits into
Open
feat: Extract constant array and slice literals as single data-carrying builtins#312TomAFrench wants to merge 2 commits into
TomAFrench wants to merge 2 commits into
Conversation
…ltins An n-element array literal previously extracted to n nested letIns feeding mkArray, so every tactic pass over the goal was linear in n and steps' per-statement machinery made proofs about large arrays super-quadratic (256 elements: ~2 minutes and 5GB; 512: stack overflow). The nesting also made extracted files above ~256 elements fail to elaborate at default recursion limits. All-literal #_mkArray/#_mkVector calls now elaborate to one callBuiltin of Builtin.mkValArray/mkValVector, with the element values hoisted into an auxiliary List definition (chunked appends keep nesting bounded at any size). Goals about a table then contain a single shallow constant, so proof cost is independent of the array length: a 1024-element table spec now costs ~1s instead of failing outright. Arrays with any non-constant element keep the existing path.
Add inline explanations to each piece of the mkValArray/mkValVector pipeline: the length-proof construction in valArray, the shape of the data-carrying builtins, the reducible Tp projections and their role in unification, the literal-hoisting rewrite in the elaborator, and the closing terms emitted by the steps tactic.
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.
An n-element array literal previously extracted to n nested letIns feeding mkArray, so every tactic pass over the goal was linear in n and steps' per-statement machinery made proofs about large arrays super-quadratic (256 elements: ~2 minutes and 5GB; 512: stack overflow). The nesting also made extracted files above ~256 elements fail to elaborate at default recursion limits.
All-literal #_mkArray/#_mkVector calls now elaborate to one callBuiltin of Builtin.mkValArray/mkValVector, with the element values hoisted into an auxiliary List definition (chunked appends keep nesting bounded at any size). Goals about a table then contain a single shallow constant, so proof cost is independent of the array length: a 1024-element table spec now costs ~1s instead of failing outright. Arrays with any non-constant element keep the existing path.