From f75a84ec54c3b9fc8b36d038921dfa0e5781fcd9 Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Wed, 6 May 2026 15:52:03 +0000 Subject: [PATCH 1/2] Fix prepend ordering for imperative calls in expression position Save prepends before processing arguments so that: 1. Argument side-effects execute first (defining snapshot variables) 2. Outer prepends (from sibling expressions) execute next (defining their snapshot variables that the call may reference) 3. The lifted call executes last (after all referenced variables exist) Also uncomments the addProcCaller test case. The correct assertion value is 15 (not 14): addProc(1,11)=12, plus (x:=3)=3, total 15. Closes #39 --- .../Languages/Laurel/LiftImperativeExpressions.lean | 11 +++++++---- .../Examples/Fundamentals/T2_ImpureExpressions.lean | 10 +++------- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 7c63b6870f..d0661238fe 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -272,16 +272,19 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do | .StaticCall callee args => let model := (← get).model - let seqArgs ← args.reverse.mapM transformExpr - let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩ if model.isFunction callee then - return seqCall + let seqArgs ← args.reverse.mapM transformExpr + return ⟨.StaticCall callee seqArgs.reverse, source⟩ else -- Imperative call in expression position: lift to an assignment. -- Only valid for single-output procedures (or unresolved ones where we -- fall back to a single target). Multi-output procedures in expression -- position are a bug in the upstream translation — Resolution should -- emit a diagnostic for that case. + let prePrepends ← takePrepends + let seqArgs ← args.reverse.mapM transformExpr + let argPrepends ← takePrepends + let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩ let outputs := match model.get callee with | .staticProcedure proc => proc.outputs | .instanceProcedure _ proc => proc.outputs @@ -294,7 +297,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do ⟨.Var (.Declare ⟨callResultVar, callResultType⟩), source⟩, ⟨.Assign [⟨.Local callResultVar, source⟩] seqCall, source⟩ ] - modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall} + modify fun s => { s with prependedStmts := s.prependedStmts ++ argPrepends ++ prePrepends ++ liftedCall} return bare (.Var (.Local callResultVar)) | .IfThenElse cond thenBranch elseBranch => diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index e65d283f57..0988eee94f 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -139,13 +139,9 @@ procedure addProcCaller(): int { var x: int := 0; var y: int := addProc({x := 1; x}, {x := x + 10; x}); - assert y == 11 - - // The next statement is not translated correctly. - // I think it's a bug in the handling of StaticCall - // Where a reference is substituted when it should not be - // var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3); - // assert z == 14 + assert y == 11; + var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3); + assert z == 15 }; " From d85768b0c78f9f9db6d276172a5a5a52849d2d65 Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Fri, 8 May 2026 16:12:29 +0000 Subject: [PATCH 2/2] Improve comments: rename prePrepends to siblingPrepends, document ordering invariant --- Strata/Languages/Laurel/LiftImperativeExpressions.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index d0661238fe..ff47dc3a1a 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -281,7 +281,13 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do -- fall back to a single target). Multi-output procedures in expression -- position are a bug in the upstream translation — Resolution should -- emit a diagnostic for that case. - let prePrepends ← takePrepends + -- + -- We isolate prepends into three explicit groups so the ordering is + -- visible: argPrepends ++ siblingPrepends ++ liftedCall. + -- NOTE: this ordering places sibling effects before the call. A future + -- fix for correct left-to-right evaluation should use + -- argPrepends ++ liftedCall ++ siblingPrepends instead. + let siblingPrepends ← takePrepends let seqArgs ← args.reverse.mapM transformExpr let argPrepends ← takePrepends let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩ @@ -297,7 +303,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do ⟨.Var (.Declare ⟨callResultVar, callResultType⟩), source⟩, ⟨.Assign [⟨.Local callResultVar, source⟩] seqCall, source⟩ ] - modify fun s => { s with prependedStmts := s.prependedStmts ++ argPrepends ++ prePrepends ++ liftedCall} + modify fun s => { s with prependedStmts := s.prependedStmts ++ argPrepends ++ siblingPrepends ++ liftedCall} return bare (.Var (.Local callResultVar)) | .IfThenElse cond thenBranch elseBranch =>