Support functions with multiple outputs (EliminateMultipleOutputs pass)#18
Support functions with multiple outputs (EliminateMultipleOutputs pass)#18keyboardDrummer-bot wants to merge 4 commits intomainfrom
Conversation
- Change LocalVariable from (name, type, init) to (List Parameter, init) to support multi-output destructuring - Add EliminateMultipleOutputs pass that transforms functional procedures with multiple outputs into procedures returning a synthesized result datatype, rewriting call sites to destructure via generated accessors - The pass checks .isFunctional to determine which procedures to handle - Add pass call in runLaurelPasses after constrained type elimination - Add test for functions with multiple outputs - Update all pattern matches across the codebase (~18 files)
|
@keyboardDrummer-bot please remove from this PR the change We can have functions with multiple outputs without supporting locals with multiple targets. Just use a destructive assignment in the test as a LHS for the function with multiple outputs |
…er) form Reverts the LocalVariable AST change from (parameters : List Parameter) back to (name : Identifier) (type : AstNode HighType) (initializer : ...). The EliminateMultipleOutputs pass now works with the original LocalVariable form. It rewrites both multi-target Assign and single-target LocalVariable/ Assign call sites to use the synthesized result datatype destructors. The test uses a destructuring assignment (single-target assign) as the LHS for the multi-output function call.
keyboardDrummer-bot
force-pushed
the
extract-eliminate-multiple-outputs
branch
from
106588f to
d8fa4d4
Compare
|
Done. I've reverted the Changes made:
All tests pass (the only failure is the pre-existing |
|
|
||
| procedure testMultiOut() { | ||
| var a: int; | ||
| a := twoOutputs(5); |
There was a problem hiding this comment.
@keyboardDrummer-bot
Why is this not throwing an error? twoOutputs MUST be assigned using two LHS targets. If the number of LHS and RHS elements does not match, this should emit an error.
There was a problem hiding this comment.
Fixed. The EliminateMultipleOutputs pass now validates that the number of LHS targets matches the number of function outputs before transforming. When there's a mismatch (like assigning a 2-output function to 1 target), it emits an error and skips the transformation entirely.
The test now expects:
a := twoOutputs(5)
// ^^^^^^^^^^^^^ error: call to 'twoOutputs' has 1 assignment target(s), but the function returns 2 output(s)
All existing tests pass (only pre-existing TestGen jar failure).
The EliminateMultipleOutputs pass now validates that the number of assignment targets matches the number of outputs for multi-output function calls. When there is a mismatch (e.g., assigning a 2-output function to a single variable), the pass emits a diagnostic error and skips the transformation entirely. Changes: - Added validation phase that scans all call sites before transforming - eliminateMultipleOutputs now returns Program × List DiagnosticModel - Pipeline collects and reports the new diagnostics - Updated test to expect the mismatch error
| function twoOutputs(x: int) | ||
| returns (a: int, b: int); | ||
|
|
||
| procedure testMultiOut() { |
There was a problem hiding this comment.
@keyboardDrummer-bot Can you also add a test, which will need to be in another program, where there is no error?
github-actions
Bot
added
the
Git conflicts
2 participants
Extracted from #16 as requested by @keyboardDrummer.
Summary
Adds support for functions with multiple output parameters by introducing the
EliminateMultipleOutputspass.Changes
EliminateMultipleOutputspass (Strata/Languages/Laurel/EliminateMultipleOutputs.lean): Transforms functional procedures (.isFunctional = true) with multiple outputs into procedures that return a single synthesized result datatype. Call sites are rewritten to destructure the result using generated accessors. For a functionfoo(x: int) returns (a: int, b: int), the pass:foo$resultdatatype with fieldsout0,out1footo returnfoo$resultAssigncall sites to use a temp variable + destructor callsLocalVariablecall sites (single-target) to extract the first outputPipeline integration: The pass is called in
runLaurelPassesafter constrained type elimination, followed by a re-resolution step.Test: Added
T22_MultipleOutputs.leanwith a test for a function with multiple outputs, using a single-target assignment as the LHS.Note: The
LocalVariableAST node is unchanged — it retains its original(name : Identifier) (type : AstNode HighType) (initializer : ...)form. Multi-output functions are handled entirely through theEliminateMultipleOutputspass without modifying the AST.