From 932c0c4886aa4475830a9e0a4358a52bfa670aaf Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Wed, 22 Apr 2026 16:30:59 +0000 Subject: [PATCH 1/2] Split Assign into local variable and field assignment Add a new FieldAssign constructor to StmtExpr that takes a target expression, a member Identifier, and a value. The existing Assign constructor now only accepts Identifier LHS targets. Previously, field assignments were represented as Assign [FieldSelect target member] value, requiring pattern matching on the target list to distinguish field writes from local variable assignments. The new FieldAssign constructor makes this distinction explicit in the type. Closes #19 --- .../Laurel/CoreGroupingAndOrdering.lean | 2 + Strata/Languages/Laurel/FilterPrelude.lean | 2 + .../AbstractToConcreteTreeTranslator.lean | 3 ++ .../ConcreteToAbstractTreeTranslator.lean | 4 +- .../Laurel/HeapParameterization.lean | 50 ++++++++----------- Strata/Languages/Laurel/InferHoleTypes.lean | 3 ++ Strata/Languages/Laurel/Laurel.lean | 6 ++- .../Laurel/LaurelToCoreTranslator.lean | 5 ++ Strata/Languages/Laurel/LaurelTypes.lean | 1 + .../Laurel/LiftImperativeExpressions.lean | 1 + Strata/Languages/Laurel/MapStmtExpr.lean | 2 + Strata/Languages/Laurel/Resolution.lean | 8 +++ Strata/Languages/Laurel/TypeHierarchy.lean | 10 ++++ Strata/Languages/Python/PythonToLaurel.lean | 15 +++--- 14 files changed, 73 insertions(+), 39 deletions(-) diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean index 1d8596235a..96fdb19b5e 100644 --- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean +++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean @@ -65,6 +65,8 @@ def collectStaticCallNames (expr : StmtExprMd) : List String := | .Assign targets v => targets.flatMap (fun t => collectStaticCallNames t) ++ collectStaticCallNames v + | .FieldAssign t _ v => + collectStaticCallNames t ++ collectStaticCallNames v | .LocalVariable _ _ initOption => match initOption with | some init => collectStaticCallNames init diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean index 7fb914a613..2a97cdb4cc 100644 --- a/Strata/Languages/Laurel/FilterPrelude.lean +++ b/Strata/Languages/Laurel/FilterPrelude.lean @@ -101,6 +101,8 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do collectExprNames body | .Assign targets value => collectExprNames value; targets.forM collectExprNames + | .FieldAssign target _ value => + collectExprNames target; collectExprNames value | .FieldSelect target _ => collectExprNames target | .PureFieldUpdate target _ newVal => collectExprNames target; collectExprNames newVal diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean index a4b67f27d4..3de4edbdd0 100644 --- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean @@ -105,6 +105,9 @@ where | t :: _ => stmtExprToArg t | [] => laurelOp "identifier" #[ident "_"] laurelOp "assign" #[targetArg, stmtExprToArg value] + | .FieldAssign target member value => + let fieldAccess := laurelOp "fieldAccess" #[stmtExprToArg target, ident member.text] + laurelOp "assign" #[fieldAccess, stmtExprToArg value] | .FieldSelect target field => laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text] | .StaticCall callee args => diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index 77f223a66c..71ae95bf5d 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -248,7 +248,9 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do | q`Laurel.assign, #[arg0, arg1] => let target ← translateStmtExpr arg0 let value ← translateStmtExpr arg1 - return mkStmtExprMd (.Assign [target] value) src + match target.val with + | .FieldSelect obj member => return mkStmtExprMd (.FieldAssign obj member value) src + | _ => return mkStmtExprMd (.Assign [target] value) src | q`Laurel.new, #[nameArg] => let name ← translateIdent nameArg return mkStmtExprMd (.New name) src diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index 0a3b9bf029..d0ed7e49b1 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -67,14 +67,12 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do | .While c invs d b => collectExprMd c; collectExprMd b; for inv in invs do collectExprMd inv; if let some x := d then collectExprMd x | .Return v => if let some x := v then collectExprMd x | .Assign assignTargets v => - -- Check if any target is a field assignment (heap write) for ⟨assignTarget, _⟩ in assignTargets.attach do - match assignTarget.val with - | .FieldSelect _ _ => - modify fun s => { s with writesHeapDirectly := true } - | _ => pure () collectExprMd assignTarget collectExprMd v + | .FieldAssign target _ v => + modify fun s => { s with writesHeapDirectly := true } + collectExprMd target; collectExprMd v | .PureFieldUpdate t _ v => collectExprMd t; collectExprMd v | .PrimitiveOp _ args => for a in args do collectExprMd a | .New _ => modify fun s => { s with writesHeapDirectly := true } @@ -318,31 +316,23 @@ where let v' ← match v with | some x => some <$> recurse x | none => pure none return ⟨ .Return v', source, md ⟩ | .Assign targets v => - match targets with - | [⟨.FieldSelect target fieldName, _, _fieldSelectMd⟩] => - let some qualifiedName := resolveQualifiedFieldName model fieldName - | return ⟨ .Hole, source, md ⟩ - let valTy := (model.get fieldName).getType - let target' ← recurse target - let v' ← recurse v - -- Wrap value in Box constructor - recordBoxConstructor model valTy.val - let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [v'] - let heapAssign := ⟨ .Assign [mkMd (.Identifier heapVar)] - (mkMd (.StaticCall "updateField" [mkMd (.Identifier heapVar), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source, md ⟩ - if valueUsed then - return ⟨ .Block [heapAssign, v'] none, source, md ⟩ - else - return heapAssign - | [fieldSelectMd] => - let tgt' ← recurse fieldSelectMd - return ⟨ .Assign [tgt'] (← recurse v), source, md ⟩ - | [] => - return ⟨ .Assign [] (← recurse v), source, md ⟩ - | tgt :: rest => - let tgt' ← recurse tgt - let targets' ← rest.mapM (recurse ·) - return ⟨ .Assign (tgt' :: targets') (← recurse v), source, md ⟩ + let tgt' ← targets.mapM (recurse ·) + return ⟨ .Assign tgt' (← recurse v), source, md ⟩ + | .FieldAssign target fieldName v => + let some qualifiedName := resolveQualifiedFieldName model fieldName + | return ⟨ .Hole, source, md ⟩ + let valTy := (model.get fieldName).getType + let target' ← recurse target + let v' ← recurse v + -- Wrap value in Box constructor + recordBoxConstructor model valTy.val + let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [v'] + let heapAssign := ⟨ .Assign [mkMd (.Identifier heapVar)] + (mkMd (.StaticCall "updateField" [mkMd (.Identifier heapVar), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source, md ⟩ + if valueUsed then + return ⟨ .Block [heapAssign, v'] none, source, md ⟩ + else + return heapAssign | .PureFieldUpdate t f v => return ⟨ .PureFieldUpdate (← recurse t) f (← recurse v), source, md ⟩ | .PrimitiveOp op args => let args' ← args.mapM (recurse ·) diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean index 616de0c1ac..fad13a3fdf 100644 --- a/Strata/Languages/Laurel/InferHoleTypes.lean +++ b/Strata/Languages/Laurel/InferHoleTypes.lean @@ -129,6 +129,9 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol | target :: _ => computeExprType model target | _ => defaultHoleType return ⟨.Assign targets (← inferExpr value targetType), source, md⟩ + | .FieldAssign target member value => + let targetType := (model.get member).getType + return ⟨.FieldAssign target member (← inferExpr value targetType), source, md⟩ | .LocalVariable name ty init => match init with | some initExpr => return ⟨.LocalVariable name ty (some (← inferExpr initExpr ty)), source, md⟩ diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index 806c490eec..db3c621d46 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -258,9 +258,11 @@ inductive StmtExpr : Type where | LiteralDecimal (value : Decimal) /-- A variable reference by name. -/ | Identifier (name : Identifier) - /-- Assignment to one or more targets. Multiple targets are only allowed when the value is a `StaticCall` to a procedure with multiple outputs. -/ + /-- Assignment to one or more local variable targets. Multiple targets are only allowed when the value is a `StaticCall` to a procedure with multiple outputs. -/ | Assign (targets : List (AstNode StmtExpr)) (value : AstNode StmtExpr) - /-- Read a field from a target expression. Combined with `Assign` for field writes. -/ + /-- Assignment to a field on a target expression. -/ + | FieldAssign (target : AstNode StmtExpr) (member : Identifier) (value : AstNode StmtExpr) + /-- Read a field from a target expression. -/ | FieldSelect (target : AstNode StmtExpr) (fieldName : Identifier) /-- Update a field on a pure (value) type, producing a new value. -/ | PureFieldUpdate (target : AstNode StmtExpr) (fieldName : Identifier) (newValue : AstNode StmtExpr) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index cb305cfad0..bf0f826c86 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -267,6 +267,8 @@ def translateExpr (expr : StmtExprMd) return .eq () re1 re2 | .Assign _ _ => disallowed md "destructive assignments are not supported in functions or contracts" + | .FieldAssign _ _ _ => + disallowed md "field assignments are not supported in functions or contracts" | .While _ _ _ _ => disallowed md "loops are not supported in functions or contracts" | .Exit _ => disallowed md "exit is not supported in expression position" @@ -457,6 +459,9 @@ def translateStmt (stmt : StmtExprMd) | _ => emitDiagnostic $ md.toDiagnostic "Assignments with multiple target but without a RHS call should not be constructed" returnNone + | .FieldAssign _ _ _ => + emitDiagnostic $ md.toDiagnostic "FieldAssign should have been eliminated by heap parameterization" DiagnosticType.StrataBug + returnNone | .IfThenElse cond thenBranch elseBranch => let bcond ← translateExpr cond let bthen ← translateStmt thenBranch diff --git a/Strata/Languages/Laurel/LaurelTypes.lean b/Strata/Languages/Laurel/LaurelTypes.lean index 0abc0cdcc2..8192f3b7b5 100644 --- a/Strata/Languages/Laurel/LaurelTypes.lean +++ b/Strata/Languages/Laurel/LaurelTypes.lean @@ -80,6 +80,7 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd := | .Exit _ => ⟨ .TVoid, source, md ⟩ | .Return _ => ⟨ .TVoid, source, md ⟩ | .Assign _ value => computeExprType model value + | .FieldAssign _ _ value => computeExprType model value | .Assert _ => ⟨ .TVoid, source, md ⟩ | .Assume _ => ⟨ .TVoid, source, md ⟩ -- Instance related diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 9aa9045606..a8f8729b80 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -163,6 +163,7 @@ def containsAssignmentOrImperativeCall (model: SemanticModel) (expr : StmtExprMd | AstNode.mk val _ _ => match val with | .Assign .. => true + | .FieldAssign .. => true | .StaticCall name args1 => (match model.get name with | .staticProcedure proc => !proc.isFunctional diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean index 3ca5fd7beb..51eb9f31be 100644 --- a/Strata/Languages/Laurel/MapStmtExpr.lean +++ b/Strata/Languages/Laurel/MapStmtExpr.lean @@ -50,6 +50,8 @@ def mapStmtExprM [Monad m] (f : StmtExprMd → m StmtExprMd) (expr : StmtExprMd) pure ⟨.Return (← v.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source, md⟩ | .Assign targets value => pure ⟨.Assign (← targets.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e) (← mapStmtExprM f value), source, md⟩ + | .FieldAssign target member value => + pure ⟨.FieldAssign (← mapStmtExprM f target) member (← mapStmtExprM f value), source, md⟩ | .FieldSelect target fieldName => pure ⟨.FieldSelect (← mapStmtExprM f target) fieldName, source, md⟩ | .PureFieldUpdate target fieldName newValue => diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index f6950ca634..8f111fbb49 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -335,6 +335,11 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let targets' ← targets.mapM resolveStmtExpr let value' ← resolveStmtExpr value pure (.Assign targets' value') + | .FieldAssign target member value => + let target' ← resolveStmtExpr target + let member' ← resolveFieldRef target' member coreMd + let value' ← resolveStmtExpr value + pure (.FieldAssign target' member' value') | .FieldSelect target fieldName => let target' ← resolveStmtExpr target let fieldName' ← resolveFieldRef target' fieldName coreMd @@ -601,6 +606,9 @@ private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExp | .Assign targets value => let map := targets.foldl collectStmtExpr map collectStmtExpr map value + | .FieldAssign target _ value => + let map := collectStmtExpr map target + collectStmtExpr map value | .FieldSelect target _ => collectStmtExpr map target | .PureFieldUpdate target _ newVal => let map := collectStmtExpr map target diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean index 30c3602393..e3d9f6746f 100644 --- a/Strata/Languages/Laurel/TypeHierarchy.lean +++ b/Strata/Languages/Laurel/TypeHierarchy.lean @@ -137,6 +137,16 @@ def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel) | .Assign targets value => let targetErrors := targets.attach.foldl (fun acc ⟨t, _⟩ => acc ++ validateDiamondFieldAccessesForStmtExpr model t) [] targetErrors ++ validateDiamondFieldAccessesForStmtExpr model value + | .FieldAssign target member value => + let targetErrors := validateDiamondFieldAccessesForStmtExpr model target + let fieldError := match (computeExprType model target).val with + | .UserDefined typeName => + if isDiamondInheritedField model typeName member then + let fileRange := (Imperative.getFileRange member.md).getD (expr.source.getD FileRange.unknown) + [DiagnosticModel.withRange fileRange s!"fields that are inherited multiple times can not be accessed."] + else [] + | _ => [] + targetErrors ++ fieldError ++ validateDiamondFieldAccessesForStmtExpr model value | .IfThenElse c t e => let errs := validateDiamondFieldAccessesForStmtExpr model c ++ validateDiamondFieldAccessesForStmtExpr model t diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index c2a55b7f27..06e2d3c38f 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1225,9 +1225,7 @@ partial def translateAssign (ctx : TranslationContext) | .Name _ name _ => if name.val == "self" && ctx.currentClassName.isSome then -- self.field : type = value in a method - let fieldAccess := mkStmtExprMd (StmtExpr.FieldSelect - (mkStmtExprMd (StmtExpr.Identifier "self")) - attr.val) + let selfExpr := mkStmtExprMd (StmtExpr.Identifier "self") -- When the annotation is a composite type, the RHS (which is Any) -- cannot be assigned directly; use New to initialize the field. let rhs' ← match annotation with @@ -1237,12 +1235,17 @@ partial def translateAssign (ctx : TranslationContext) pure (mkStmtExprMd (StmtExpr.New (mkId laurelName))) else pure rhs_trans | none => pure rhs_trans - let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [fieldAccess] rhs') md + let assignStmt := mkStmtExprMdWithLoc (StmtExpr.FieldAssign selfExpr attr.val rhs') md return (ctx, [assignStmt], true) else let targetExpr ← translateExpr ctx lhs -- This will handle self.field via translateExpr - let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md - return (ctx, [assignStmt], true) + match targetExpr.val with + | .FieldSelect obj member => + let assignStmt := mkStmtExprMdWithLoc (StmtExpr.FieldAssign obj member rhs_trans) md + return (ctx, [assignStmt], true) + | _ => + let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md + return (ctx, [assignStmt], true) | _ => throw (.unsupportedConstruct "Assignment targets not yet supported" (toString (repr lhs))) | _ => throw (.unsupportedConstruct "Assignment targets not yet supported" (toString (repr lhs))) From 35809b71e495cbf02c55b5acba323f093bbbc9ff Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Wed, 22 Apr 2026 17:02:36 +0000 Subject: [PATCH 2/2] Change Assign targets to List (AstNode Identifier) and add multiAssign grammar rule - Assign constructor now takes (targets : List (AstNode Identifier)) instead of (targets : List (AstNode StmtExpr)), enforcing at the type level that assign targets are identifiers (not arbitrary expressions). - Added multiAssign grammar rule: (a, b) := value for multi-target assignments. Single-target assign still uses: a := value. - Updated all passes to work with the new target type: - Passes that recursed into targets (MapStmtExpr, FilterPrelude, Resolution, CoreGroupingAndOrdering, TypeHierarchy, HeapParameterization) no longer need to since targets are just identifiers. - LaurelToCoreTranslator, ConstrainedTypeElim, LiftImperativeExpressions, InferHoleTypes simplified by accessing .val directly as Identifier. - PythonToLaurel updated to construct AstNode Identifier targets. --- .../Languages/Laurel/ConstrainedTypeElim.lean | 17 ++++---- .../Laurel/CoreGroupingAndOrdering.lean | 3 +- .../Laurel/EliminateValueReturns.lean | 3 +- Strata/Languages/Laurel/FilterPrelude.lean | 4 +- .../AbstractToConcreteTreeTranslator.lean | 12 +++--- .../ConcreteToAbstractTreeTranslator.lean | 13 +++++- .../Laurel/Grammar/LaurelGrammar.lean | 2 +- .../Languages/Laurel/Grammar/LaurelGrammar.st | 1 + .../Laurel/HeapParameterization.lean | 17 ++++---- Strata/Languages/Laurel/InferHoleTypes.lean | 2 +- Strata/Languages/Laurel/Laurel.lean | 2 +- .../Laurel/LaurelToCoreTranslator.lean | 15 +++---- .../Laurel/LiftImperativeExpressions.lean | 28 +++++-------- Strata/Languages/Laurel/MapStmtExpr.lean | 2 +- Strata/Languages/Laurel/Resolution.lean | 5 +-- Strata/Languages/Laurel/TypeHierarchy.lean | 7 ++-- Strata/Languages/Python/PythonToLaurel.lean | 40 ++++++++++++------- 17 files changed, 88 insertions(+), 85 deletions(-) diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean index c55c817331..c4427f94fc 100644 --- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean +++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean @@ -137,15 +137,14 @@ def elimStmt (ptMap : ConstrainedTypeMap) | some _ => (init, callOpt.toList.map fun c => ⟨.Assert c, source, md⟩) pure ([⟨.LocalVariable name ty init', source, md⟩] ++ check) - | .Assign [target] _ => match target.val with - | .Identifier name => do - match (← get).get? name.text with - | some ty => - let assert := (constraintCallFor ptMap ty name md (src := source)).toList.map - fun c => ⟨.Assert c, source, md⟩ - pure ([stmt] ++ assert) - | none => pure [stmt] - | _ => pure [stmt] + | .Assign [target] _ => do + let name := target.val + match (← get).get? name.text with + | some ty => + let assert := (constraintCallFor ptMap ty name md (src := source)).toList.map + fun c => ⟨.Assert c, source, md⟩ + pure ([stmt] ++ assert) + | none => pure [stmt] | .Block stmts sep => let stmtss ← inScope (stmts.mapM (elimStmt ptMap)) diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean index 96fdb19b5e..2565a1ff02 100644 --- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean +++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean @@ -62,8 +62,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String := | some eelse => collectStaticCallNames eelse | none => [] | .Block stmts _ => stmts.flatMap (fun s => collectStaticCallNames s) - | .Assign targets v => - targets.flatMap (fun t => collectStaticCallNames t) ++ + | .Assign _targets v => collectStaticCallNames v | .FieldAssign t _ v => collectStaticCallNames t ++ collectStaticCallNames v diff --git a/Strata/Languages/Laurel/EliminateValueReturns.lean b/Strata/Languages/Laurel/EliminateValueReturns.lean index f5df423cc7..8d224a98f8 100644 --- a/Strata/Languages/Laurel/EliminateValueReturns.lean +++ b/Strata/Languages/Laurel/EliminateValueReturns.lean @@ -27,8 +27,7 @@ private def eliminateValueReturnNode (outParam : Identifier) (stmt : StmtExprMd) match stmt.val with | .Return (some value) => -- Synthesized nodes use default metadata since no diagnostics should be reported on them - let target : StmtExprMd := ⟨.Identifier outParam, none, .empty⟩ - let assign : StmtExprMd := ⟨.Assign [target] value, none, .empty⟩ + let assign : StmtExprMd := ⟨.Assign [⟨outParam, none, .empty⟩] value, none, .empty⟩ let ret : StmtExprMd := ⟨.Return none, stmt.source, stmt.md⟩ ⟨.Block [assign, ret] none, none, .empty⟩ | _ => stmt diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean index 2a97cdb4cc..9062c387a4 100644 --- a/Strata/Languages/Laurel/FilterPrelude.lean +++ b/Strata/Languages/Laurel/FilterPrelude.lean @@ -99,8 +99,8 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do collectExprNames cond; invs.forM collectExprNames dec.forM collectExprNames collectExprNames body - | .Assign targets value => - collectExprNames value; targets.forM collectExprNames + | .Assign _targets value => + collectExprNames value | .FieldAssign target _ value => collectExprNames target; collectExprNames value | .FieldSelect target _ => collectExprNames target diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean index 3de4edbdd0..578dedc579 100644 --- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean @@ -100,11 +100,11 @@ where let initOpt := optionArg (init.map fun e => laurelOp "initializer" #[stmtExprToArg e]) laurelOp "varDecl" #[ident name.text, typeOpt, initOpt] | .Assign targets value => - -- Grammar only supports single-target assign; use first target or placeholder - let targetArg := match targets with - | t :: _ => stmtExprToArg t - | [] => laurelOp "identifier" #[ident "_"] - laurelOp "assign" #[targetArg, stmtExprToArg value] + match targets with + | [t] => laurelOp "assign" #[laurelOp "identifier" #[ident t.val.text], stmtExprToArg value] + | _ => + let targetArgs := targets.map fun t => ident t.val.text + laurelOp "multiAssign" #[commaSep targetArgs.toArray, stmtExprToArg value] | .FieldAssign target member value => let fieldAccess := laurelOp "fieldAccess" #[stmtExprToArg target, ident member.text] laurelOp "assign" #[fieldAccess, stmtExprToArg value] @@ -164,7 +164,7 @@ where | .Abstract => laurelOp "identifier" #[ident "abstract"] | .All => laurelOp "identifier" #[ident "all"] | .PureFieldUpdate target field value => - -- Not directly in grammar; emit as assignment to field + -- Not directly in grammar; emit as field assignment laurelOp "assign" #[ laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text], stmtExprToArg value diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index 71ae95bf5d..89c9d32d86 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -250,7 +250,18 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do let value ← translateStmtExpr arg1 match target.val with | .FieldSelect obj member => return mkStmtExprMd (.FieldAssign obj member value) src - | _ => return mkStmtExprMd (.Assign [target] value) src + | .Identifier name => return mkStmtExprMd (.Assign [⟨name, src, .empty⟩] value) src + | _ => TransM.error s!"assign target must be an identifier or field access" + | q`Laurel.multiAssign, #[arg0, arg1] => + let targets ← match arg0 with + | .seq _ .comma args => args.toList.mapM fun a => do + let name ← translateIdent a + pure (⟨name, src, .empty⟩ : AstNode Identifier) + | _ => do + let name ← translateIdent arg0 + pure [⟨name, src, .empty⟩] + let value ← translateStmtExpr arg1 + return mkStmtExprMd (.Assign targets value) src | q`Laurel.new, #[nameArg] => let name ← translateIdent nameArg return mkStmtExprMd (.New name) src diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean index fa35ae23fc..3d2a829947 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean @@ -9,7 +9,7 @@ module -- Laurel dialect definition, loaded from LaurelGrammar.st -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system. -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st. --- Last grammar change: parameterized bvType with arbitrary width +-- Last grammar change: assign now takes CommaSepBy Ident targets for multi-assign public import Strata.DDM.Integration.Lean public meta import Strata.DDM.Integration.Lean diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st index 3dec015888..a7f93aacd3 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st @@ -47,6 +47,7 @@ op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")"; // Assignment op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target " := " value; +op multiAssign (targets: CommaSepBy Ident, value: StmtExpr): StmtExpr => @[prec(10)] "(" targets ") := " value; // Binary operators op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " + " rhs; diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index d0ed7e49b1..2a62976f4a 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -66,9 +66,7 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do | .LocalVariable _ _ i => if let some x := i then collectExprMd x | .While c invs d b => collectExprMd c; collectExprMd b; for inv in invs do collectExprMd inv; if let some x := d then collectExprMd x | .Return v => if let some x := v then collectExprMd x - | .Assign assignTargets v => - for ⟨assignTarget, _⟩ in assignTargets.attach do - collectExprMd assignTarget + | .Assign _assignTargets v => collectExprMd v | .FieldAssign target _ v => modify fun s => { s with writesHeapDirectly := true } @@ -277,11 +275,11 @@ where let freshVar ← freshVarName let varDecl := mkMd (.LocalVariable freshVar (computeExprType model exprMd) none) let callWithHeap := ⟨ .Assign - [mkMd (.Identifier heapVar), mkMd (.Identifier freshVar)] + [⟨heapVar, none, default⟩, ⟨freshVar, none, default⟩] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩), source, md ⟩ return ⟨ .Block [varDecl, callWithHeap, mkMd (.Identifier freshVar)] none, source, md ⟩ else - return ⟨ .Assign [mkMd (.Identifier heapVar)] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩), source, md ⟩ + return ⟨ .Assign [⟨heapVar, none, default⟩] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩), source, md ⟩ else if calleeReadsHeap then return ⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩ else @@ -316,8 +314,7 @@ where let v' ← match v with | some x => some <$> recurse x | none => pure none return ⟨ .Return v', source, md ⟩ | .Assign targets v => - let tgt' ← targets.mapM (recurse ·) - return ⟨ .Assign tgt' (← recurse v), source, md ⟩ + return ⟨ .Assign targets (← recurse v), source, md ⟩ | .FieldAssign target fieldName v => let some qualifiedName := resolveQualifiedFieldName model fieldName | return ⟨ .Hole, source, md ⟩ @@ -327,7 +324,7 @@ where -- Wrap value in Box constructor recordBoxConstructor model valTy.val let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [v'] - let heapAssign := ⟨ .Assign [mkMd (.Identifier heapVar)] + let heapAssign := ⟨ .Assign [⟨heapVar, none, default⟩] (mkMd (.StaticCall "updateField" [mkMd (.Identifier heapVar), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source, md ⟩ if valueUsed then return ⟨ .Block [heapAssign, v'] none, source, md ⟩ @@ -401,7 +398,7 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform let body' ← match proc.body with | .Transparent bodyExpr => -- First assign $heap_in to $heap, then transform body using $heap - let assignHeap := mkMd (.Assign [mkMd (.Identifier heapName)] (mkMd (.Identifier heapInName))) + let assignHeap := mkMd (.Assign [⟨heapName, none, default⟩] (mkMd (.Identifier heapInName))) let bodyExpr' ← heapTransformExpr heapName model bodyExpr bodyValueIsUsed pure (.Transparent (mkMd (.Block [assignHeap, bodyExpr'] none))) | .Opaque postconds impl modif => @@ -409,7 +406,7 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform let postconds' ← postconds.mapM (heapTransformExpr heapName model ·) let impl' ← match impl with | some implExpr => - let assignHeap := mkMd (.Assign [mkMd (.Identifier heapName)] (mkMd (.Identifier heapInName))) + let assignHeap := mkMd (.Assign [⟨heapName, none, default⟩] (mkMd (.Identifier heapInName))) let implExpr' ← heapTransformExpr heapName model implExpr bodyValueIsUsed pure (some (mkMd (.Block [assignHeap, implExpr'] none))) | none => pure none diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean index fad13a3fdf..f59f32662a 100644 --- a/Strata/Languages/Laurel/InferHoleTypes.lean +++ b/Strata/Languages/Laurel/InferHoleTypes.lean @@ -126,7 +126,7 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol return ⟨.Block (← inferBlockStmts stmts expectedType) label, source, md⟩ | .Assign targets value => let targetType := match targets with - | target :: _ => computeExprType model target + | target :: _ => (model.get target.val).getType | _ => defaultHoleType return ⟨.Assign targets (← inferExpr value targetType), source, md⟩ | .FieldAssign target member value => diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index db3c621d46..ed6ac6469a 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -259,7 +259,7 @@ inductive StmtExpr : Type where /-- A variable reference by name. -/ | Identifier (name : Identifier) /-- Assignment to one or more local variable targets. Multiple targets are only allowed when the value is a `StaticCall` to a procedure with multiple outputs. -/ - | Assign (targets : List (AstNode StmtExpr)) (value : AstNode StmtExpr) + | Assign (targets : List (AstNode Identifier)) (value : AstNode StmtExpr) /-- Assignment to a field on a target expression. -/ | FieldAssign (target : AstNode StmtExpr) (member : Identifier) (value : AstNode StmtExpr) /-- Read a field from a target expression. -/ diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index bf0f826c86..79d2eaab5b 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -405,7 +405,7 @@ def translateStmt (stmt : StmtExprMd) return [Core.Statement.init ident coreType .nondet md] | .Assign targets value => match targets with - | [⟨ .Identifier targetId, _, _ ⟩] => + | [⟨ targetId, _, _ ⟩] => let ident := ⟨targetId.text, ()⟩ -- Check if RHS is a procedure call (not a function) match value.val with @@ -444,18 +444,13 @@ def translateStmt (stmt : StmtExprMd) match value.val with | .StaticCall callee args => let coreArgs ← args.mapM (fun a => translateExpr a) - let lhsIdents := targets.filterMap fun t => - match t.val with - | .Identifier name => some (⟨name.text, ()⟩) - | _ => none + let lhsIdents := targets.map fun t => ⟨t.val.text, ()⟩ return [Core.Statement.call lhsIdents callee.text coreArgs (astNodeToCoreMd value)] | .InstanceCall .. => -- Instance method call: havoc all target variables - let havocStmts := targets.filterMap fun t => - match t.val with - | .Identifier name => some (Core.Statement.havoc ⟨name.text, ()⟩ md) - | _ => none - return (havocStmts) + let havocStmts := targets.map fun t => + Core.Statement.havoc ⟨t.val.text, ()⟩ md + return havocStmts | _ => emitDiagnostic $ md.toDiagnostic "Assignments with multiple target but without a RHS call should not be constructed" returnNone diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index a8f8729b80..24456db8ca 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -202,20 +202,18 @@ Shared logic for lifting an assignment in expression position: prepends the assignment, creates before-snapshots for all targets, and updates substitutions. The value should already be transformed by the caller. -/ -private def liftAssignExpr (targets : List StmtExprMd) (seqValue : StmtExprMd) +private def liftAssignExpr (targets : List (AstNode Identifier)) (seqValue : StmtExprMd) (source : Option FileRange) (md : Imperative.MetaData Core.Expression) : LiftM Unit := do -- Prepend the assignment itself prepend (⟨.Assign targets seqValue, source, md⟩) -- Create a before-snapshot for each target and update substitutions for target in targets do - match target.val with - | .Identifier varName => - let snapshotName ← freshTempFor varName - let varType ← computeType target - -- Snapshot goes before the assignment (cons pushes to front) - prepend (⟨.LocalVariable snapshotName varType (some (⟨.Identifier varName, source, md⟩)), source, md⟩) - setSubst varName snapshotName - | _ => pure () + let varName := target.val + let snapshotName ← freshTempFor varName + let varType ← computeType (⟨.Identifier varName, target.source, target.md⟩) + -- Snapshot goes before the assignment (cons pushes to front) + prepend (⟨.LocalVariable snapshotName varType (some (⟨.Identifier varName, source, md⟩)), source, md⟩) + setSubst varName snapshotName mutual /-- @@ -244,11 +242,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do | head :: _ => pure head | _ => return expr - let resultExpr ← match firstTarget.val with - | .Identifier varName => pure (⟨.Identifier (← getSubst varName), source, md⟩) - | _ => - dbg_trace "Strata bug: non-identifier targets should have been removed before the lift expression phase"; - return expr + let resultExpr := ⟨.Identifier (← getSubst firstTarget.val), source, md⟩ -- Use the original value (not seqValue) for the prepended assignment, -- because prepended statements execute in program order and don't need substitutions. @@ -273,7 +267,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do let callResultType ← computeType expr let liftedCall := [ ⟨ (.LocalVariable callResultVar callResultType none), source, md ⟩, - ⟨.Assign [bare (.Identifier callResultVar)] seqCall, source, md⟩ + ⟨.Assign [⟨callResultVar, none, emptyMd⟩] seqCall, source, md⟩ ] modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall} return bare (.Identifier callResultVar) @@ -295,14 +289,14 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do modify fun s => { s with prependedStmts := [], subst := [] } let seqThen ← transformExpr thenBranch let thenPrepends ← takePrepends - let thenBlock := bare (.Block (thenPrepends ++ [⟨.Assign [bare (.Identifier condVar)] seqThen, source, md⟩]) none) + let thenBlock := bare (.Block (thenPrepends ++ [⟨.Assign [⟨condVar, none, emptyMd⟩] seqThen, source, md⟩]) none) -- Process else-branch from scratch modify fun s => { s with prependedStmts := [], subst := [] } let seqElse ← match elseBranch with | some e => do let se ← transformExpr e let elsePrepends ← takePrepends - pure (some (bare (.Block (elsePrepends ++ [⟨.Assign [bare (.Identifier condVar)] se, source, md⟩]) none))) + pure (some (bare (.Block (elsePrepends ++ [⟨.Assign [⟨condVar, none, emptyMd⟩] se, source, md⟩]) none))) | none => pure none -- Restore outer state modify fun s => { s with subst := savedSubst, prependedStmts := savedPrepends } diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean index 51eb9f31be..60e1a8f275 100644 --- a/Strata/Languages/Laurel/MapStmtExpr.lean +++ b/Strata/Languages/Laurel/MapStmtExpr.lean @@ -49,7 +49,7 @@ def mapStmtExprM [Monad m] (f : StmtExprMd → m StmtExprMd) (expr : StmtExprMd) | .Return v => pure ⟨.Return (← v.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source, md⟩ | .Assign targets value => - pure ⟨.Assign (← targets.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e) (← mapStmtExprM f value), source, md⟩ + pure ⟨.Assign targets (← mapStmtExprM f value), source, md⟩ | .FieldAssign target member value => pure ⟨.FieldAssign (← mapStmtExprM f target) member (← mapStmtExprM f value), source, md⟩ | .FieldSelect target fieldName => diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index 8f111fbb49..926dd4804a 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -332,7 +332,7 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let ref' ← resolveRef ref coreMd pure (.Identifier ref') | .Assign targets value => - let targets' ← targets.mapM resolveStmtExpr + let targets' ← targets.mapM fun t => do pure { t with val := ← resolveRef t.val coreMd } let value' ← resolveStmtExpr value pure (.Assign targets' value') | .FieldAssign target member value => @@ -603,8 +603,7 @@ private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExp collectStmtExpr map body | .Return val => match val with | some v => collectStmtExpr map v | none => map | .Identifier _ => map - | .Assign targets value => - let map := targets.foldl collectStmtExpr map + | .Assign _targets value => collectStmtExpr map value | .FieldAssign target _ value => let map := collectStmtExpr map target diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean index e3d9f6746f..8c63d4b382 100644 --- a/Strata/Languages/Laurel/TypeHierarchy.lean +++ b/Strata/Languages/Laurel/TypeHierarchy.lean @@ -134,9 +134,8 @@ def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel) targetErrors ++ fieldError | .Block stmts _ => stmts.flatMap (fun s => validateDiamondFieldAccessesForStmtExpr model s) - | .Assign targets value => - let targetErrors := targets.attach.foldl (fun acc ⟨t, _⟩ => acc ++ validateDiamondFieldAccessesForStmtExpr model t) [] - targetErrors ++ validateDiamondFieldAccessesForStmtExpr model value + | .Assign _targets value => + validateDiamondFieldAccessesForStmtExpr model value | .FieldAssign target member value => let targetErrors := validateDiamondFieldAccessesForStmtExpr model target let fieldError := match (computeExprType model target).val with @@ -226,7 +225,7 @@ def lowerNew (name : Identifier) (source : Option FileRange) (md : Imperative.Me let getCounter := mkMd (.StaticCall "Heap..nextReference!" [mkMd (.Identifier heapVar)]) let saveCounter := mkMd (.LocalVariable freshVar ⟨.TInt, none, #[]⟩ (some getCounter)) let newHeap := mkMd (.StaticCall "increment" [mkMd (.Identifier heapVar)]) - let updateHeap := mkMd (.Assign [mkMd (.Identifier heapVar)] newHeap) + let updateHeap := mkMd (.Assign [⟨heapVar, none, #[]⟩] newHeap) let compositeResult := mkMd (.StaticCall "MkComposite" [mkMd (.Identifier freshVar), mkMd (.StaticCall (name.text ++ "_TypeTag") [])]) return ⟨ .Block [saveCounter, updateHeap, compositeResult] none, source, md ⟩ diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 06e2d3c38f..00442f87d2 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -178,6 +178,10 @@ def mkCoreType (s: String): HighTypeMd := def mkStmtExprMd (expr : StmtExpr) : StmtExprMd := { val := expr, source := none } +/-- Create an AstNode Identifier with default metadata -/ +def mkIdNode (name : String) : AstNode Identifier := + { val := name, source := none } + /-- Create a StmtExprMd with source location metadata. NOTE: stores location in `md` (legacy); a follow-up should migrate to `source`. -/ def mkStmtExprMdWithLoc (expr : StmtExpr) (md : Imperative.MetaData Core.Expression) : StmtExprMd := @@ -1098,8 +1102,9 @@ def withException (ctx : TranslationContext) (funcname: String) : Bool := | none => false def freeVar (name: String) := mkStmtExprMd (.Identifier name) -def maybeExceptVar := freeVar "maybe_except" -def nullcall_var := freeVar "nullcall_ret" +def freeVarTarget (name: String) : AstNode Identifier := mkIdNode name +def maybeExceptVar := freeVarTarget "maybe_except" +def nullcall_var := freeVarTarget "nullcall_ret" partial def translateAssign (ctx : TranslationContext) (lhs: Python.expr SourceRange) @@ -1142,8 +1147,7 @@ partial def translateAssign (ctx : TranslationContext) match lhs with | .Name _ n _ => if n.val ∈ ctx.variableTypes.unzip.1 then - let targetExpr := mkStmtExprMd (StmtExpr.Identifier n.val) - return (ctx, [mkStmtExprMd (StmtExpr.Assign [targetExpr] rhs_trans)] ++ exceptHavoc, true) + return (ctx, [mkStmtExprMd (StmtExpr.Assign [mkIdNode n.val] rhs_trans)] ++ exceptHavoc, true) else -- Use type annotation if it matches a known composite type let annType := annotation.map (fun a => pyExprToString a) |>.getD "Any" @@ -1161,7 +1165,7 @@ partial def translateAssign (ctx : TranslationContext) let mut newctx := ctx match lhs with | .Name _ n _ => - let targetExpr := mkStmtExprMd (StmtExpr.Identifier n.val) + let targetNode := mkIdNode n.val let assignStmts := match rhs_trans.val with | .StaticCall fnname args => if let some (ImportedSymbol.compositeType laurelName) := ctx.importedSymbols[fnname.text]? then @@ -1171,23 +1175,23 @@ partial def translateAssign (ctx : TranslationContext) let selfRef := mkStmtExprMd (StmtExpr.Identifier n.val) let initStmt := mkInstanceMethodCall laurelName "__init__" selfRef args md if n.val ∈ ctx.variableTypes.unzip.1 then - let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] newExpr) md + let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetNode] newExpr) md [assignStmt, initStmt] else let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable n.val varType (some newExpr)) md [newStmt, initStmt] else if withException ctx fnname.text then - [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr, maybeExceptVar] rhs_trans) md] + [mkStmtExprMdWithLoc (StmtExpr.Assign [targetNode, maybeExceptVar] rhs_trans) md] else - [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md] + [mkStmtExprMdWithLoc (StmtExpr.Assign [targetNode] rhs_trans) md] | .New className => if n.val ∈ ctx.variableTypes.unzip.1 then - [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md] + [mkStmtExprMdWithLoc (StmtExpr.Assign [targetNode] rhs_trans) md] else let varType := mkHighTypeMd (.UserDefined className) let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable n.val varType (some rhs_trans)) md [newStmt] - | _ => [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md] + | _ => [mkStmtExprMdWithLoc (StmtExpr.Assign [targetNode] rhs_trans) md] newctx := match rhs_trans.val with | .StaticCall fnname _ => if let some (ImportedSymbol.compositeType laurelName) := ctx.importedSymbols[fnname.text]? then @@ -1217,7 +1221,10 @@ partial def translateAssign (ctx : TranslationContext) let slices ← slices.mapM (translateExpr ctx) let md := sourceRangeToMetaData ctx.filePath lhs.toAst.ann let anySetsExpr := mkStmtExprMdWithLoc (StmtExpr.StaticCall "Any_sets!" [ListAny_mk slices, target, rhs_trans]) md - let assignStmts := [mkStmtExprMdWithLoc (StmtExpr.Assign [target] anySetsExpr) md] + let targetId := match target.val with + | .Identifier name => mkIdNode name.text + | _ => mkIdNode "_" + let assignStmts := [mkStmtExprMdWithLoc (StmtExpr.Assign [targetId] anySetsExpr) md] return (ctx,assignStmts, false) | _ => throw (.internalError "Invalid Subscript Expr") | .Attribute _ obj attr _ => @@ -1244,7 +1251,10 @@ partial def translateAssign (ctx : TranslationContext) let assignStmt := mkStmtExprMdWithLoc (StmtExpr.FieldAssign obj member rhs_trans) md return (ctx, [assignStmt], true) | _ => - let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md + let targetId := match targetExpr.val with + | .Identifier name => mkIdNode name.text + | _ => mkIdNode "_" + let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetId] rhs_trans) md return (ctx, [assignStmt], true) | _ => throw (.unsupportedConstruct "Assignment targets not yet supported" (toString (repr lhs))) | _ => throw (.unsupportedConstruct "Assignment targets not yet supported" (toString (repr lhs))) @@ -1447,7 +1457,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let exceptionCheck := getExceptionAssertions ctx e -- Coerce Composite return values to Any for LaurelResult : Any let e ← coerceToAny ctx expr e - let assign := mkStmtExprMdWithLoc (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier PyLauFuncReturnVar)] e) md + let assign := mkStmtExprMdWithLoc (StmtExpr.Assign [mkIdNode PyLauFuncReturnVar] e) md .ok $ exceptionCheck ++ [assign, mkStmtExprMdWithLoc (StmtExpr.Exit "$body") md] | none => .ok [mkStmtExprMdWithLoc (StmtExpr.Exit "$body") md] return (ctx, stmts) @@ -1578,7 +1588,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let varName := pyExprToString varExpr if varName ∈ currentCtx.variableTypes.unzip.fst then let assignStmt := mkStmtExprMd (StmtExpr.Assign - [mkStmtExprMd (StmtExpr.Identifier varName)] enterCall) + [mkIdNode varName] enterCall) setupStmts := setupStmts ++ [mgrDecl, assignStmt] else -- New variable — declare outside the block so it's visible after @@ -1880,7 +1890,7 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun let inputTypes := funcDecl.args.map (λ arg => match arg.tys with | [ty] => (arg.name, ty) | _ => (arg.name, PyLauType.Any)) let (bodyBlock, newCtx) ← translateFunctionBody ctx inputTypes body - let noneReturn := mkStmtExprMd (.Assign [mkStmtExprMd (.Identifier PyLauFuncReturnVar)] AnyNone) + let noneReturn := mkStmtExprMd (.Assign [mkIdNode PyLauFuncReturnVar] AnyNone) let (renamedInputs, paramCopies) := renameInputParams inputs (match funcDecl.kwargsName with | some kw => (· == kw) | none => fun _ => false) let bodyBlock : StmtExprMd := match bodyBlock.val with