Add support for function declaration statements #352

MikaelMayer · 2026-01-27T17:14:50Z

Add support for function declarations within statement blocks

This PR adds the ability to declare functions as a statement Stmt.funcDecl in Strata Core, enabling local function definitions within procedures.

Changes

Added Stmt.funcDecl for declaring functions within statement blocks
Implemented statement-level operations (variable analysis, substitution, type erasure) for funcDecl
Added type checking that converts between PureFunc and Function representations
Extended all program transformations to handle funcDecl

Semantics

Refactored semantics to thread the evaluator δ (SemanticEval) as state through EvalStmt and EvalBlock
When a function is declared, the evaluator is extended with the new function definition
Closure capture semantics: free variables from the enclosing scope are captured by value (lexical scoping)
Updated EvalCmdParam signature to include δ' output parameter for evaluator changes
Updated transformation correctness proofs to work with the new evaluator threading

Testing

Added tests demonstrating funcDecl functionality including polymorphic functions with type parameters. Existing tests pass.

…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)

…checking

joscoh

Overall looks good, had a few questions about polymorphism. Also, do the small step semantics for Statements (StmtSemanticsSmallStep.lean) need to be updated?

Strata/DL/Lambda/Factory.lean

Strata/Languages/Core/StatementEval.lean

Strata/Languages/Core/StatementType.lean

StrataTest/Languages/Core/StatementEvalTests.lean

…lBlock

MikaelMayer · 2026-02-02T19:30:42Z

I updated StmtSemanticsSmallStep.lean to support function declaration semantics. Because functions are closures, I had to add support for a generic free variable replacement so that it works for any Func , not just LFunc

Strata/DL/Imperative/CmdSemantics.lean

Strata/DL/Imperative/StmtSemanticsSmallStep.lean

Strata/DL/Imperative/PureExpr.lean

Strata/Transform/DetToNondetCorrect.lean

- 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

Strata/DL/Imperative/CmdSemantics.lean

Strata/Languages/Core/StatementSemantics.lean

Strata/Transform/ProcedureInlining.lean

Strata/Languages/Core/StatementSemantics.lean

Strata/DL/Imperative/SemanticsProps.lean

Strata/DL/Imperative/Stmt.lean

Strata/DL/Lambda/Factory.lean

Strata/DL/Util/Func.lean

Strata/Languages/Core/StatementSemanticsProps.lean

Strata/Languages/Core/StatementType.lean

Strata/Transform/DetToNondetCorrect.lean

Strata/Transform/ProcedureInlining.lean

Strata/DL/Util/Func.lean

Strata/DL/Lambda/Factory.lean

Strata/DL/Imperative/StmtSemanticsSmallStep.lean

Strata/Languages/Core/StatementType.lean

Strata/Languages/Core/WF.lean

…Check - Simplify FuncWF.body_freevars to use subset notation (porting PR #386) - Simplify FuncWF.body_freevars_decidable to a 1-line proof - Extract PureFunc.typeCheck helper in FunctionType.lean to reduce code duplication - Update StatementType.lean to use the shared PureFunc.typeCheck helper

- Changed extendEval from existential parameter inside step_funcDecl to explicit parameter of StepStmt inductive type - Updated StepStmtStar, EvalStmtSmall, EvalStmtsSmall, IsTerminal to accept extendEval parameter - Updated evalStmtsSmallNil and terminalIsTerminal theorems accordingly - Also includes PureFunc.typeCheck returning Function to avoid duplicate conversion in StatementType.lean

Address PR review comment: LFuncWF is now a type alias (abbreviation) of FuncWF, instantiated with Lambda-specific getName and getVarNames functions. This maintains the same semantics while reducing code duplication.

…ta-org/Strata into add-func-decl-to-statements

Add support for function declarations within statement blocks

99ba9b8

MikaelMayer changed the title ~~Add support for function declarations within statement blocks~~ Add support for function declarations statements Jan 27, 2026

MikaelMayer changed the title ~~Add support for function declarations statements~~ Add support for function declaration statements Jan 27, 2026

MikaelMayer added 3 commits January 27, 2026 17:12

Fix Factory_wf proof using rotate_left to reorder goals

6b1cdc2

Remove unnecessary Lambda namespace opening in Statement.lean

a8a4a0c

Remove unnecessary Lambda namespace opening in Program.lean

b8ec252

MikaelMayer force-pushed the add-func-decl-to-statements branch from 6016b5a to b8ec252 Compare January 28, 2026 18:21

MikaelMayer added 5 commits January 28, 2026 14:10

Remove B3 .gitignore (moved to .git/info/exclude for local use)

ed1f8ac

Clean up: revert ProcedureWF.lean to main, remove unnecessary comment

c6ede80

Merge main into add-func-decl-to-statements

77eb4fa

- Resolved conflict in Factory.lean (Factory_wf moved to FactoryWF.lean in main) - Applied rotate_left fix to FactoryWF.lean

Fix merge: add missing funcDecl cases in ProcedureInlining and apply …

62a5f70

…rotate_left fix to FactoryWF

MikaelMayer marked this pull request as ready for review January 29, 2026 20:27

MikaelMayer requested a review from a team as a code owner January 29, 2026 20:27

MikaelMayer and others added 6 commits January 29, 2026 14:35

Merge branch 'main' into add-func-decl-to-statements

a13b470

Fix merge: convert Format to String for EvalError.Misc

6797599

Fix merge: convert Format errors to DiagnosticModel in funcDecl type …

86f6c90

…checking

Merge branch 'main' into add-func-decl-to-statements

776a87d

joscoh reviewed Jan 30, 2026

View reviewed changes

MikaelMayer added 3 commits February 2, 2026 13:20

Add polymorphic function test for funcDecl with evaluation verification

dbfe96e

Update semantics and proofs for FuncContext parameter in EvalStmt/Eva…

ebbab10

…lBlock

Merge branch 'main' into add-func-decl-to-statements

494dedc

MikaelMayer enabled auto-merge February 2, 2026 19:53

shigoel reviewed Feb 2, 2026

View reviewed changes

Strata/DL/Imperative/CmdSemantics.lean Outdated Show resolved Hide resolved

joscoh reviewed Feb 2, 2026

View reviewed changes

Strata/DL/Imperative/StmtSemanticsSmallStep.lean Outdated Show resolved Hide resolved

Fix eval_stmts_set_comm proof after FuncContext refactor

c588f0c

shigoel reviewed Feb 3, 2026

View reviewed changes

Strata/DL/Imperative/PureExpr.lean Show resolved Hide resolved

MikaelMayer commented Feb 3, 2026

View reviewed changes

Strata/Transform/DetToNondetCorrect.lean Outdated Show resolved Hide resolved

MikaelMayer added 2 commits February 3, 2026 15:13

Update comment: funcDecl WF checks are TODO, not always true

dc17906

atomb reviewed Feb 4, 2026

View reviewed changes

Strata/DL/Imperative/CmdSemantics.lean Outdated Show resolved Hide resolved

Strata/DL/Imperative/CmdSemantics.lean Outdated Show resolved Hide resolved

MikaelMayer added 5 commits February 4, 2026 17:02

Add extendEval parameter to DetToNondetCorrect theorems

e673135

Merge main into add-func-decl-to-statements

e1ce657

Fix FactoryWF.lean to use LFuncWF instead of FuncWF after merge

049bff4

Merge branch 'main' into add-func-decl-to-statements

3183890

Fix unused section variable warning in LFunc.type_inputs_nodup

80c1833

MikaelMayer commented Feb 5, 2026

View reviewed changes

Strata/Languages/Core/StatementSemantics.lean Show resolved Hide resolved

Strata/Transform/ProcedureInlining.lean Show resolved Hide resolved

MikaelMayer commented Feb 5, 2026

View reviewed changes

Strata/Languages/Core/StatementSemantics.lean Show resolved Hide resolved

shigoel mentioned this pull request Feb 5, 2026

Transform.runProgram return an extra updated bool result, add analysis cache, and updates to ProcedureInlining #377

Merged

MikaelMayer added 2 commits February 5, 2026 13:25

Merge branch 'main' into add-func-decl-to-statements

f6de32b

Merge branch 'main' into add-func-decl-to-statements

d0d8073

joscoh reviewed Feb 5, 2026

View reviewed changes

aqjune-aws reviewed Feb 5, 2026

View reviewed changes

MikaelMayer and others added 4 commits February 5, 2026 16:18

Make LFuncWF an abbreviation of FuncWF

c90b4d6

Address PR review comment: LFuncWF is now a type alias (abbreviation) of FuncWF, instantiated with Lambda-specific getName and getVarNames functions. This maintains the same semantics while reducing code duplication.

Merge branch 'main' into add-func-decl-to-statements

8ae4092

aqjune-aws previously approved these changes Feb 6, 2026

View reviewed changes

MikaelMayer added 2 commits February 6, 2026 14:07

Remaining last two comments

ea70ba9

Merge branch 'add-func-decl-to-statements' of https://github.com/stra…

de892c1

…ta-org/Strata into add-func-decl-to-statements

MikaelMayer dismissed aqjune-aws’s stale review via de892c1 February 6, 2026 20:11

joscoh approved these changes Feb 6, 2026

View reviewed changes

aqjune-aws approved these changes Feb 6, 2026

View reviewed changes

MikaelMayer added this pull request to the merge queue Feb 6, 2026

Merged via the queue into main with commit faa0874 Feb 6, 2026
15 checks passed

MikaelMayer deleted the add-func-decl-to-statements branch February 6, 2026 20:54

Add support for function declaration statements #352

Add support for function declaration statements #352

Uh oh!

Conversation

MikaelMayer commented Jan 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Semantics

Testing

Uh oh!

joscoh left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MikaelMayer commented Feb 2, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

MikaelMayer commented Jan 27, 2026 •

edited

Loading