Implement Phase 2 parser: PEG recursive-descent parser for Python 3.12

Build a complete parser that transforms the lexer's token stream into a
Python 3.12 AST. This establishes the source → tokens → AST pipeline
needed for the interpreter.

AST types (Lython/AST/Types.lean):
- Expr (27 variants), Stmt (25 variants) in mutual inductive blocks
- Supporting types: Comprehension, Arguments, Arg, CallKeyword,
  ExceptHandler, FunctionDef, ClassDef, Alias, WithItem, Module
- Dump functions for test assertions via string comparison

Parser infrastructure:
- ParserM monad (StateT over Except) with token array + index
- PEG combinators: attempt/backtrack, many, sepBy, optional
- Token matching helpers for keywords, operators, delimiters, literals

Expression parser (18 precedence levels):
- Atoms through named expressions, full operator precedence
- Primaries: attribute access, calls, subscripts, slicing
- Comprehensions (list/set/dict), implicit string concatenation
- Boolean/comparison chaining, ternary if, lambda, yield, starred

Statement parser:
- Simple: assignment, augmented/annotated assignment, return, pass,
  break, continue, raise, assert, global, nonlocal, del, import
- Compound: if/elif/else, while, for, with, try/except/finally,
  def, class, async, decorators
- Block parsing via NEWLINE/INDENT/DEDENT tokens
- Function parameter parsing (*args, **kwargs, defaults, annotations)

70+ parser tests covering expressions, statements, and integration.

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

Author: pirapira

CLAUDE.md

@@ -24,21 +24,34 @@ Lython/
     StringLit.lean   — String/bytes/raw/f-string literal lexing
     Indent.lean      — INDENT/DEDENT generation from leading whitespace
     Core.lean        — Main tokenization loop, operator dispatch
-  Parser.lean        — PEG parser (stub)
-  AST.lean           — Python AST node types (stub)
+  AST.lean           — AST umbrella import
+  AST/
+    Types.lean       — Expr, Stmt, Module, and supporting types (mutual inductives)
+  Parser.lean        — parser umbrella import
+  Parser/
+    Types.lean       — ParseError, ParserState, ParserM monad
+    Combinators.lean — PEG combinators (attempt, many, sepBy, etc.)
+    Tokens.lean      — Token matching helpers (expectKeyword, parseName, etc.)
+    Expr.lean        — Expression parser (18 precedence levels)
+    Stmt.lean        — Statement parser (simple + compound statements)
+    Core.lean        — Entry point: parse : String → Except String Module
   Interpreter.lean   — tree-walking interpreter (stub)
   Runtime.lean       — runtime support (stub)
 Main.lean            — CLI entry point
 LythonTest.lean      — test driver root
 LythonTest/
   Basic.lean         — lexer tests (keywords, operators, numbers, strings, indent)
+  Parser.lean        — parser tests (expressions, statements, integration)
 ```
 
 ## Code Style
 
 - `set_option autoImplicit false` at the top of every file
 - No trailing whitespace
 - Follow existing patterns in the codebase
+- Do NOT use `/-! ... -/` module doc comments inside `mutual` blocks (they are commands, not comments; use `-- ...` instead)
+- Use `partial def` for all recursive parser functions
+- Structures cannot be in `mutual` blocks; use `inductive Foo where | mk : ...` instead
 
 ## Development Plan
 

Lython/AST.lean

@@ -1,4 +1,3 @@
-set_option autoImplicit false
+import Lython.AST.Types
 
-namespace Lython.AST
-end Lython.AST
+set_option autoImplicit false