From a8140fff1deabf72ddb8c811bc613be19dcf707c Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Wed, 6 May 2026 15:37:48 +0000 Subject: [PATCH] Fix LiftImperativeExpression: save and reorder prepends for imperative calls When lifting an imperative call in expression position, save the previously accumulated prepended statements (from expressions processed earlier in right-to-left traversal) and place them after the lifted call. This ensures the call's declaration and assignment appear before the side-effects of expressions that follow it in program order. Also use the procedure's declared output type (from SemanticModel) when available, falling back to computeType only for multi-output or unknown cases. Fixes #39 --- .../Laurel/LiftImperativeExpressions.lean | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 65af0996d5..adbae73587 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -274,14 +274,21 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do if model.isFunction callee then return seqCall else - -- Imperative call in expression position: lift it like an assignment + -- Imperative call in expression position: lift to an assignment. + let previousPrependedStmts ← takePrepends + let outputs := match model.get callee with + | .staticProcedure proc => proc.outputs + | .instanceProcedure _ proc => proc.outputs + | _ => [] let callResultVar ← freshCondVar - let callResultType ← computeType expr + let callResultType ← match outputs with + | [single] => pure single.type + | _ => computeType expr let liftedCall := [ - ⟨ (.Var (.Declare ⟨callResultVar, callResultType⟩)), source ⟩, - ⟨.Assign [⟨ .Local callResultVar, source⟩] seqCall, source⟩ + ⟨.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 ++ liftedCall ++ previousPrependedStmts} return bare (.Var (.Local callResultVar)) | .IfThenElse cond thenBranch elseBranch =>