Make type of Assign more specific with Variable inductive#36
Draft
keyboardDrummer-bot wants to merge 3 commits intomainfrom
Draft
Make type of Assign more specific with Variable inductive#36keyboardDrummer-bot wants to merge 3 commits intomainfrom
keyboardDrummer-bot wants to merge 3 commits intomainfrom
Conversation
- Introduce Variable inductive with Local and Field constructors - Change Assign targets from List (AstNode StmtExpr) to List (AstNode Variable) - Replace StmtExpr.Identifier with StmtExpr.Variable (.Local name) - Replace StmtExpr.FieldSelect with StmtExpr.Variable (.Field target fieldName) - Add multi-target assignment (multiAssign) to Laurel grammar - Update all Laurel passes and Python-to-Laurel translator Closes #21
…ion proofs - Rename 'variable' field to 'ref' in StmtExpr.Variable (Lean keyword conflict) - Rename 'variable' local in ConcreteToAbstractTreeTranslator (same) - Fix multiAssign grammar: use CommaSepBy Ident with parenthesized syntax to avoid leading-symbol recursion and parsing ambiguity - Add Variable.sizeOf_field_target lemma for termination proofs - Fix termination in MapStmtExpr, CoreGroupingAndOrdering, Resolution, HeapParameterization, TypeHierarchy by adding 'have' annotations - Inline resolveVariable into resolveStmtExpr to avoid mutual recursion - Inline recurseVariable in HeapParameterization - Fix PythonToLaurel: use freeVarTarget for Assign targets, fix missing newline and parenthesis - Fix TypeHierarchy diamond field check for Assign targets - Fix test references to removed StmtExpr.Identifier constructor
The docs build uses --wfail which treats warnings as errors. The unused variable linter flagged h1 and h2 in HeapParameterization.lean.
Collaborator
Author
|
I investigated the CI failure. The only failing check is "Run internal benchmarks of Strata" which requires AWS credentials ( All other 13 checks passed (Lean build+test, Python tests on 3.11–3.14, CBMC tests, lint, documentation, etc.). Locally, |
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
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.
Summary
Implements the refactoring requested in #21: makes the type of
Assigntargets more specific by introducing aVariableinductive type.Changes
Core type change (
Laurel.lean)Variableinductive inside the mutual block:AssignfromList (AstNode StmtExpr)toList (AstNode Variable)StmtExpr.IdentifierwithStmtExpr.Variable (.Local name)StmtExpr.FieldSelect, replaced withStmtExpr.Variable (.Field target fieldName)VariableMdabbreviationGrammar (
LaurelGrammar.st)multiAssignoperator for multi-target assignment syntaxUpdated passes
MapStmtExpr.lean— updated traversal for new constructorsResolution.lean— addedresolveVariablein mutual block withresolveStmtExprHeapParameterization.lean— updated field detection and heap variable referencesLaurelToCoreTranslator.lean— updated pattern matching on targetsLiftImperativeExpressions.lean— updated assign target handlingFilterPrelude.lean,CoreGroupingAndOrdering.lean,InferHoleTypes.lean,ConstrainedTypeElim.lean,EliminateHoles.lean,EliminateValueReturns.lean,ModifiesClauses.lean,TypeHierarchy.lean,LaurelTypes.leanNotes
Closes #21