diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 65af0996d5..157c376e05 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -269,19 +269,22 @@ 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 it like an assignment + -- Imperative call in expression position: lift to an assignment + let prePrepends ← takePrepends + let seqArgs ← args.reverse.mapM transformExpr + let argPrepends ← takePrepends + let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩ let callResultVar ← freshCondVar let callResultType ← computeType expr let liftedCall := [ ⟨ (.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 }; "