diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 7c63b6870f..ff47dc3a1a 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -272,16 +272,25 @@ 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. + -- + -- 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⟩ let outputs := match model.get callee with | .staticProcedure proc => proc.outputs | .instanceProcedure _ proc => proc.outputs @@ -294,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 ++ liftedCall} + modify fun s => { s with prependedStmts := s.prependedStmts ++ argPrepends ++ siblingPrepends ++ 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 }; "