Complete Phase 3c: attr assignment, string formatting, with statement, raise from

- Attribute access on dict-objects falls through to check dict entries (for class dicts)
- Attribute assignment (obj.attr = value) and augmented (obj.attr += 1) on dicts
- String % formatting: %s, %d, %i, %f, %r, %x, %o, %%
- String .format() method: {}, {0}, {1}, {{, }}
- Context managers (with statement) with __enter__/__exit__ protocol
- Exception chaining (raise X from Y) evaluates and validates cause
- 17 new test assertions

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: pirapira

LeanPython/Interpreter/Eval.lean

@@ -436,9 +436,16 @@ partial def getAttributeValue (obj : Value) (attr : String) : InterpM Value := d
   | .list _ =>
     if knownListMethods.contains attr then return .boundMethod obj attr
     else throwAttributeError s!"'list' object has no attribute '{attr}'"
-  | .dict _ =>
+  | .dict ref =>
     if knownDictMethods.contains attr then return .boundMethod obj attr
-    else throwAttributeError s!"'dict' object has no attribute '{attr}'"
+    else do
+      -- Check dict entries as attributes (for class/object dicts)
+      let pairs ← heapGetDict ref
+      for (k, v) in pairs do
+        match k with
+        | .str s => if s == attr then return v
+        | _ => pure ()
+      throwAttributeError s!"'dict' object has no attribute '{attr}'"
   | .set _ =>
     if knownSetMethods.contains attr then return .boundMethod obj attr
     else throwAttributeError s!"'set' object has no attribute '{attr}'"
@@ -548,7 +555,22 @@ partial def assignToTarget (target : Expr) (value : Value) : InterpM Unit := do
       | _ => pure ()
       for i in [:after.length] do
         assignToTarget after[i]! items[items.size - after.length + i]!
-  | .attribute _obj _attr _ => throwNotImplemented "attribute assignment"
+  | .attribute obj attr _ => do
+    let objVal ← evalExpr obj
+    match objVal with
+    | .dict ref => do
+      let pairs ← heapGetDict ref
+      let key := Value.str attr
+      let mut newPairs := pairs
+      let mut found := false
+      for i in [:pairs.size] do
+        if pairs[i]!.1 == key then
+          newPairs := newPairs.set! i (key, value)
+          found := true
+          break
+      if !found then newPairs := newPairs.push (key, value)
+      heapSetDict ref newPairs
+    | _ => throwAttributeError s!"'{typeName objVal}' object attribute '{attr}' is read-only"
   | .starred inner _ => assignToTarget inner value
   | _ => throwRuntimeError (.runtimeError "invalid assignment target")
 
@@ -699,7 +721,15 @@ partial def execStmt (s : Stmt) : InterpM Unit := do
     let classVal ← allocDict entries
     setVariable cd.name classVal
 
-  | .raise_ exprOpt _cause _ => do
+  | .raise_ exprOpt cause _ => do
+    -- Evaluate cause if present (for validation; chaining info not stored yet)
+    if let some causeExpr := cause then
+      let causeVal ← evalExpr causeExpr
+      match causeVal with
+      | .exception _ _ => pure ()
+      | .none => pure ()
+      | .builtin _ => pure ()
+      | _ => throwTypeError "exception cause must be None or derive from BaseException"
     match exprOpt with
     | some e => do
       let v ← evalExpr e
@@ -783,7 +813,74 @@ partial def execStmt (s : Stmt) : InterpM Unit := do
       modify fun st => { st with activeException := none }
     | some other => do execStmts finally_; throw other
 
-  | .with_ _items _body _ => throwNotImplemented "with statements"
+  | .with_ items body _ => do
+    -- Evaluate context managers and call __enter__
+    let mut managers : List (Value × Value) := []
+    for item in items do
+      let mgr ← evalExpr item.contextExpr
+      -- Try to call __enter__ on the manager
+      let entered ← match mgr with
+        | .dict ref => do
+          let pairs ← heapGetDict ref
+          let mut enterFn : Option Value := none
+          for (k, v) in pairs do
+            match k with
+            | .str s => if s == "__enter__" then enterFn := some v
+            | _ => pure ()
+          match enterFn with
+          | some fn => callValueDispatch fn [mgr] []
+          | none => pure mgr
+        | _ => pure mgr
+      if let some target := item.optionalVars then
+        assignToTarget target entered
+      managers := managers ++ [(mgr, entered)]
+    -- Execute body with cleanup
+    let mut bodyError : Option Signal := none
+    try execStmts body
+    catch
+    | sig@(.error _) => bodyError := some sig
+    | other => do
+      -- For control flow signals (return/break), still call __exit__ then re-throw
+      for (mgr, _) in managers.reverse do
+        match mgr with
+        | .dict ref => do
+          let pairs ← heapGetDict ref
+          for (k, v) in pairs do
+            match k with
+            | .str s =>
+              if s == "__exit__" then do
+                let _ ← callValueDispatch v [mgr, .none, .none, .none] []
+            | _ => pure ()
+        | _ => pure ()
+      throw other
+    -- Call __exit__ on each manager in reverse order
+    let mut suppressed := false
+    for (mgr, _) in managers.reverse do
+      match mgr with
+      | .dict ref => do
+        let pairs ← heapGetDict ref
+        let mut exitFn : Option Value := none
+        for (k, v) in pairs do
+          match k with
+          | .str s => if s == "__exit__" then exitFn := some v
+          | _ => pure ()
+        match exitFn with
+        | some fn =>
+          let exitArgs := match bodyError with
+            | none => [mgr, .none, .none, .none]
+            | some (.error e) =>
+              let excType := Value.str (runtimeErrorTypeName e)
+              let excVal := Value.exception (runtimeErrorTypeName e) (runtimeErrorMessage e)
+              [mgr, excType, excVal, .none]
+            | _ => [mgr, .none, .none, .none]
+          let result ← callValueDispatch fn exitArgs []
+          if ← isTruthy result then suppressed := true
+        | none => pure ()
+      | _ => pure ()
+    -- Re-raise body error if not suppressed
+    match bodyError with
+    | some sig => if !suppressed then throw sig
+    | none => pure ()
   | .import_ _aliases _ => throwNotImplemented "import statements"
   | .importFrom _ _aliases _ _ => throwNotImplemented "import-from statements"
 
@@ -1253,7 +1350,53 @@ partial def callStrMethod (s : String) (method : String) (args : List Value)
       let padding := String.ofList (List.replicate (w - s.length) '0')
       return .str (padding ++ s)
     | _ => throwTypeError "zfill() takes 1 argument"
-  | "format" => return .str s
+  | "format" => do
+    -- Python str.format(): supports {}, {0}, {1}, {{, }}
+    let chars := s.toList
+    let mut result : List Char := []
+    let mut i := 0
+    let mut autoIdx := 0
+    while i < chars.length do
+      let c := chars[i]!
+      if c == '{' then
+        if i + 1 < chars.length && chars[i + 1]! == '{' then
+          result := result ++ ['{']
+          i := i + 2
+        else
+          -- Find closing }
+          let mut j := i + 1
+          while j < chars.length && chars[j]! != '}' do j := j + 1
+          if j >= chars.length then
+            throwValueError "Single '{' encountered in format string"
+          let fieldContent := String.ofList (chars.drop (i + 1) |>.take (j - i - 1))
+          -- Strip format spec after ':'
+          let fieldName := match fieldContent.splitOn ":" with
+            | name :: _ => name
+            | [] => ""
+          let argVal ←
+            if fieldName.isEmpty then do
+              if autoIdx >= args.length then throwIndexError "Replacement index out of range for positional args tuple"
+              let v := args[autoIdx]!
+              autoIdx := autoIdx + 1
+              pure v
+            else match fieldName.toNat? with
+              | some idx =>
+                if idx >= args.length then throwIndexError s!"Replacement index {idx} out of range for positional args tuple"
+                pure args[idx]!
+              | none => throwKeyError s!"'{fieldName}'"
+          let valStr ← valueToStr argVal
+          result := result ++ valStr.toList
+          i := j + 1
+      else if c == '}' then
+        if i + 1 < chars.length && chars[i + 1]! == '}' then
+          result := result ++ ['}']
+          i := i + 2
+        else
+          throwValueError "Single '}' encountered in format string"
+      else
+        result := result ++ [c]
+        i := i + 1
+    return .str (String.ofList result)
   | "count" =>
     match args with
     | [.str sub] => return .int (stringCount s sub)

LeanPython/Runtime/Ops.lean

@@ -208,6 +208,73 @@ partial def valueRepr (v : Value) : InterpM String :=
 
 end
 
+-- ============================================================
+-- String % formatting
+-- ============================================================
+
+/-- Python-style `%` string formatting. Supports %s, %d, %i, %f, %r, %x, %o, %%. -/
+partial def formatPercent (fmt : String) (args : Array Value) : InterpM String := do
+  let chars := fmt.toList
+  let mut result : List Char := []
+  let mut i := 0
+  let mut argIdx := 0
+  while i < chars.length do
+    let c := chars[i]!
+    if c == '%' then
+      if i + 1 < chars.length then
+        let spec := chars[i + 1]!
+        match spec with
+        | '%' => result := result ++ ['%']; i := i + 2
+        | 's' =>
+          if argIdx >= args.size then throwTypeError "not enough arguments for format string"
+          let s ← valueToStr args[argIdx]!
+          result := result ++ s.toList; argIdx := argIdx + 1; i := i + 2
+        | 'r' =>
+          if argIdx >= args.size then throwTypeError "not enough arguments for format string"
+          let s ← valueRepr args[argIdx]!
+          result := result ++ s.toList; argIdx := argIdx + 1; i := i + 2
+        | 'd' | 'i' =>
+          if argIdx >= args.size then throwTypeError "not enough arguments for format string"
+          let s := match args[argIdx]! with
+            | .int n => toString n
+            | .bool b => toString (if b then 1 else 0)
+            | .float f => toString f.toUInt64.toNat
+            | v => Value.toStr v
+          result := result ++ s.toList; argIdx := argIdx + 1; i := i + 2
+        | 'f' =>
+          if argIdx >= args.size then throwTypeError "not enough arguments for format string"
+          let s := match args[argIdx]! with
+            | .float f => toString f
+            | .int n => toString (Float.ofInt n)
+            | v => Value.toStr v
+          result := result ++ s.toList; argIdx := argIdx + 1; i := i + 2
+        | 'x' =>
+          if argIdx >= args.size then throwTypeError "not enough arguments for format string"
+          let s := match args[argIdx]! with
+            | .int n =>
+              let hexChars := Nat.toDigits 16 n.natAbs
+              let hexStr := if hexChars.isEmpty then "0" else String.ofList hexChars
+              if n < 0 then "-" ++ hexStr else hexStr
+            | v => Value.toStr v
+          result := result ++ s.toList; argIdx := argIdx + 1; i := i + 2
+        | 'o' =>
+          if argIdx >= args.size then throwTypeError "not enough arguments for format string"
+          let s := match args[argIdx]! with
+            | .int n =>
+              let octChars := Nat.toDigits 8 n.natAbs
+              let octStr := if octChars.isEmpty then "0" else String.ofList octChars
+              if n < 0 then "-" ++ octStr else octStr
+            | v => Value.toStr v
+          result := result ++ s.toList; argIdx := argIdx + 1; i := i + 2
+        | _ =>
+          -- Unknown specifier, pass through
+          result := result ++ ['%', spec]; i := i + 2
+      else
+        result := result ++ ['%']; i := i + 1
+    else
+      result := result ++ [c]; i := i + 1
+  return String.ofList result
+
 -- ============================================================
 -- Membership test (for `in` operator)
 -- ============================================================
@@ -335,9 +402,12 @@ partial def evalBinOp (op : BinOp) (left right : Value) : InterpM Value := do
     | .int a, .int b =>
       if b == 0 then throwZeroDivision "integer division or modulo by zero"
       else return .int (Int.fmod a b)
-    | .str fmt, _ => do
-      -- Basic % string formatting (stub)
-      return .str fmt
+    | .str fmt, right => do
+      let args := match right with
+        | .tuple arr => arr
+        | v => #[v]
+      let result ← formatPercent fmt args
+      return .str result
     | _, _ =>
       match toFloat left, toFloat right with
       | some a, some b =>

LeanPythonTest/Interpreter.lean

@@ -318,3 +318,42 @@ private def assertPyError (source errSubstr : String) : IO Unit := do
 #eval assertPy "print(\"hello_world\".upper())\n" "HELLO_WORLD\n"
 #eval assertPy "print(\"a_b_c\".split(\"_\"))\n" "['a', 'b', 'c']\n"
 #eval assertPy "print(\"test_string\".startswith(\"test\"))\n" "True\n"
+
+-- ============================================================
+-- Attribute access and assignment on dict-objects (class dicts)
+-- ============================================================
+
+#eval assertPy "class Foo:\n    x = 10\nprint(Foo.x)\n" "10\n"
+#eval assertPy "class Foo:\n    x = 10\nFoo.x = 20\nprint(Foo.x)\n" "20\n"
+#eval assertPy "class Foo:\n    x = 10\nFoo.y = 99\nprint(Foo.y)\n" "99\n"
+
+-- Augmented attribute assignment
+#eval assertPy "class C:\n    count = 0\nC.count += 5\nprint(C.count)\n" "5\n"
+
+-- ============================================================
+-- String % formatting
+-- ============================================================
+
+#eval assertPy "print(\"hello %s\" % \"world\")\n" "hello world\n"
+#eval assertPy "print(\"%d + %d = %d\" % (1, 2, 3))\n" "1 + 2 = 3\n"
+#eval assertPy "print(\"val=%d\" % 42)\n" "val=42\n"
+#eval assertPy "print(\"100%%\" % ())\n" "100%\n"
+#eval assertPy "print(\"%x\" % 255)\n" "ff\n"
+#eval assertPy "print(\"%o\" % 8)\n" "10\n"
+
+-- ============================================================
+-- String .format() method
+-- ============================================================
+
+#eval assertPy "print(\"{} {}\".format(\"hello\", \"world\"))\n" "hello world\n"
+#eval assertPy "print(\"{0} {1}\".format(\"a\", \"b\"))\n" "a b\n"
+#eval assertPy "print(\"{1} {0}\".format(\"a\", \"b\"))\n" "b a\n"
+#eval assertPy "print(\"x={{y}}\".format())\n" "x={y}\n"
+#eval assertPy "print(\"{} is {}\".format(42, True))\n" "42 is True\n"
+
+-- ============================================================
+-- Exception chaining (raise X from Y)
+-- ============================================================
+
+#eval assertPy "try:\n    raise ValueError(\"x\") from TypeError(\"y\")\nexcept ValueError as e:\n    print(\"caught\")\n" "caught\n"
+#eval assertPy "try:\n    raise ValueError(\"x\") from None\nexcept ValueError as e:\n    print(\"ok\")\n" "ok\n"

PLAN.md

@@ -768,8 +768,8 @@ For non-deterministic tests, structural equivalence is checked.
 | 0 | Project scaffolding | Done |
 | 1 | Lexer | Done |
 | 2 | Parser | Done |
-| 3 | Core interpreter (expressions, types) | In progress |
-| 4 | Control flow and functions | Not started |
+| 3 | Core interpreter (expressions, types) | Done |
+| 4 | Control flow and functions | In progress |
 | 5 | Object model (classes, inheritance) | Not started |
 | 6 | Module system | Not started |
 | 7a | Stdlib: core utilities | Not started |