Add support for function declaration statements #352
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
MikaelMayer
changed the title
MikaelMayer
changed the title
MikaelMayer
force-pushed
the
add-func-decl-to-statements
branch
from
6016b5a to
b8ec252
Compare
…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)
joscoh
reviewed
Jan 30, 2026
Contributor
joscoh
left a comment
joscoh
left a comment
There was a problem hiding this comment.
Overall looks good, had a few questions about polymorphism. Also, do the small step semantics for Statements (StmtSemanticsSmallStep.lean) need to be updated?
| -/ | ||
| structure LFuncWF {T : LExprParams} (f : LFunc T) extends FuncWF f where | ||
| -- Free variables of body must be arguments. | ||
| body_freevars: |
Contributor
There was a problem hiding this comment.
Why doesn't this hold for general Func? Is it because there is no generic notion of "variable in an expression"?
|
|
||
| -- LFuncWF.concreteEval_argmatch is not decidable. | ||
| -- FuncWF.concreteEval_argmatch and LFuncWF.concreteEval_argmatch are not decidable.-- FuncWF.body_freevars is commented out as it's expression-type specific | ||
| -- FuncWF.concreteEval_argmatch is not decidable. |
Contributor
There was a problem hiding this comment.
Repeated comment. Also, Why would FuncWF.body_freevars be commented out?
| typeArgs := decl.typeArgs, | ||
| isConstr := decl.isConstr, | ||
| inputs := decl.inputs.map (fun (id, ty) => (id, Lambda.LTy.toMonoTypeUnsafe ty)), | ||
| output := Lambda.LTy.toMonoTypeUnsafe decl.output, |
Contributor
There was a problem hiding this comment.
Does the unsafe cause any problems with polymorphism?
| axioms := decl.axioms | ||
| } | ||
| let (func', Env) ← Function.typeCheck C Env func |>.mapError DiagnosticModel.fromFormat | ||
| -- Convert back by wrapping monotypes in trivial polytypes |
Contributor
There was a problem hiding this comment.
Again, what happens to polymorphic functions?
Contributor
There was a problem hiding this comment.
I would like to see a test with a polymorphic function decl, followed by using one (or even better, multiple) concrete instantiations of this function. For example, something like:
function toInt (x: a) : int { 1 }
assert (toInt(3) == toInt(true));
Just to make sure there are no type variables captured.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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 support for function declarations within statement blocks
This PR adds the ability to declare functions as a statement
Stmt.funDeclin Strata Core, enabling local function definitions within procedures.Changes
Testing
Added tests demonstrating funcDecl functionality: declaring helper functions within statement blocks and using them in subsequent statements, including symbolic variable capture from enclosing scope.