Add DDM support for parsing functions that are not top-level + Strata Core support to parse function statements #379
+187
−8
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
…or Func - Added ToFormat for generic Func with proper constraints - Added [ToFormat T.IDMeta] to Factory.lean section variables - Removed unnecessary ToFormat instances from test files and Program.lean - Removed custom Env.format function (now uses default ToFormat) - Function bodies now display properly instead of showing <body>
- Resolved conflict in Factory.lean (Factory_wf moved to FactoryWF.lean in main) - Applied rotate_left fix to FactoryWF.lean
…rotate_left fix to FactoryWF
- Modified testFuncDeclSymbolic to show functions capture variables by reference - Function declared with n=10, then n mutated to 20, function uses n=20 at call time - Proof obligation correctly shows result should be 25 (5+20), not 15 (5+10) - Reverted Env.lean to main (custom scope formatting not needed)
…claration time - Functions now capture variable values at declaration time, not by reference - Free variables in function body are substituted with their current values from environment - Test demonstrates: n=10 at declaration, n=20 after mutation, function uses n=10 - Proof obligation correctly shows result is 15 (5+10), not 25 (5+20)
MikaelMayer
force-pushed
the
add-function-statements-ddm
branch
from
bc38faa to
10713a3
Compare
…duplication - Move generic Func structure to Strata/DL/Util/Func.lean - Add PureFunc to Imperative, removing Lambda->Imperative dependency - Fix funcDecl type checking to add function to type context - Remove duplicate renameLhs/substFvar from ProcedureInlining - Extract captureFreevars helper in StatementEval - Refine getVars to exclude formal parameters for funcDecl - Add type checking test for funcDecl
- Add WFfuncDeclProp structure in WF.lean checking input parameter uniqueness - Add LFunc.type_inputs_nodup theorem in Factory.lean - Add Function.typeCheck_inputs_nodup theorem in FunctionType.lean - Add listMap_keys_map_snd helper lemma in StatementWF.lean - Replace sorry in funcDecl case with complete proof
- Add funcDecl_statement operator to DDM Parse.lean - Support function declarations within statement blocks - Include proper scoping and inline attribute support - Add compilation test to verify DDM syntax correctness - Extends DDM to support the new .funcDecl statement type
The DDM doesn't actually support function declaration statements syntax yet. The funcDecl_statement operator was added but the full parsing integration is not complete.
- Add case for .bvar with arguments to handle locally declared function calls - Translates arguments and creates function application using .mkApp
- Remove @[scope(b)] annotation from funcDecl_statement body parameter to prevent function parameter leakage into global scope - Add function to local freeVars for subsequent statement access - Add test demonstrating function declaration statements work correctly - Resolves translateExpr out-of-range bound variable errors
- Restore scope annotations in DDM parser for proper parameter access - Fix translation layer to handle function calls correctly - Isolate issue to function call translation, not declaration
MikaelMayer
force-pushed
the
add-function-statements-ddm
branch
from
16716b7 to
d415650
Compare
- Fix function body translation to use only function parameters as bound variables - Fix function call translation to convert out-of-range bound variables to function calls - Handle case where parser treats function names as bound variables but translation needs them as free variables - Resolves translateExpr out-of-range bound variable errors for function declarations in statements
The funcDecl_statement translation was not correctly setting up bound variables for the function body. Fixed by: - Using LExpr.fvar with type information (like translateFunction does) - Including the function name in boundVars for recursive calls - Appending to existing boundVars to allow access to outer scope variables This allows function bodies to reference their own parameters, the function itself for recursion, and outer scope variables like procedure parameters. Note: SMT verification of locally declared functions is not yet supported (function axioms are not generated). This is documented in the test file.
MikaelMayer
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Add DDM support for parsing functions that are not top-level + Strata Core support to parse function statements
Extends Core DDM with:
All tests pass.