Skip to content

CHANGELOG.md

Latest commit

 

History

History
169 lines (121 loc) · 6.85 KB

CHANGELOG.md

File metadata and controls

169 lines (121 loc) · 6.85 KB

Changelog

2025-12-23

Added

Interpreter (PythonOfLean/Semantics/Interp.lean)

Ported the computational interpreter from lambda-py/base/python-interp.rkt.

  • Result type: Control flow handling matching Racket's Result datatype

    • value - Normal completion (v*s in Racket)
    • return_ - Early return from function
    • break_ / continue_ - Loop control flow
    • exception - Raised exception
    • stuck - Debugging aid for stuck states

  • Big-step interpreter (interp): Handles all λπ expression types

    • Memory operations: fetch, set!, alloc
    • Objects and collections: object, list, tuple, set
    • Control flow: seq, if, while, loop, break, continue
    • Bindings: let (global/local), id, assign
    • Functions: fun_, app, appVararg, frame, return
    • Exception handling: raise, tryExcept, tryFinally
    • Modules: module, constructModule, inModule

  • Primitive operations (interpPrim):

    • Arithmetic: $add, $sub, $mult, $div
    • Comparison: $num=, $str=, $num<, $num>, $num<=, $num>=
    • I/O: $print (returns None)

  • Small-step evaluator (tryStepBase):

    • Computational version of propositional StepBase rules
    • Context-aware stepping through expressions
    • Fuel-bounded evaluation via evalSmallStep

  • Entry points:

    • run - Big-step interpreter from empty state
    • runSmallStep - Small-step with fuel limit

Test Utilities (PythonOfLean/Examples/Utils.lean)

  • showResult - Format big-step Result for display
  • showSmallStepResult - Format small-step SmallStepResult for display
  • runShow / runSmallStepShow - Convenience wrappers

Examples (PythonOfLean/Examples/Basic.lean)

Added interpreter test cases:

  • Number allocation
  • Sequence evaluation
  • Let bindings
  • Function application (identity function)
  • Arithmetic primitives (3 + 4 = 7)
  • While loops
  • Comparison operators
  • Exception handling (try/except)

Fixed

Interpreter bugs

  • .ref r handling: Now returns the pointer directly instead of allocating an unnecessary copy
  • .letIn bindings: Now copies the actual object pointed to, not wrapping the pointer in a new object with .noMeta
  • Function application (interpApp, interpAppVararg): Added valToObj helper to properly copy argument objects
  • Exception handling (.tryExcept): Fixed exception binding to copy the actual exception object

Semantic correctness (matching Racket interpreter)

  • Symbol truthiness (isTruthy): Only the symbol "true" is truthy, not all symbols. Matches Racket's (equal? t 'true) check.
  • Function return semantics (interpApp, interpAppVararg): Functions now correctly return None on normal completion (no explicit return). Only explicit return statements return the actual value. This matches Python semantics and Racket's [v*s (vb sb) (alloc-result vnone sb)].
  • Frame usage in big-step: Removed .frame wrapper in interpApp/interpAppVararg since the big-step interpreter handles return/break/continue directly. Frame is used in small-step semantics only.

Store (PythonOfLean/Semantics/Store.lean)

  • Added Inhabited State instance to support partial functions in the interpreter

Changed

  • Updated PythonOfLean.lean to import Interp.lean
  • Simplified test code in Basic.lean using the new utilities

Python Parsing Integration

Parser (PythonOfLean/Parser/)

  • S-expression Parser (SExpr.lean): Parses Racket's S-expression output format

    • Handles atoms, numbers, quoted strings, and nested lists
    • Tokenizer with proper whitespace and escape sequence handling

  • S-expr to Expr Converter (SExprToExpr.lean): Converts S-expressions to Lean Expr type

    • Maps all λπ constructs: sym, id, seq, let, fun, app, if, while, etc.
    • Handles true/false/none → object construction
    • MetaVal parsing for meta-num, meta-str, meta-list, etc.

  • Racket Integration (Racket.lean): Spawns Racket process to parse Python

    • parsePythonString - Parse Python code from string
    • parsePythonFile - Parse Python file
    • Uses scripts/python-to-sexp.rkt as the frontend

Racket Script (scripts/python-to-sexp.rkt)

  • Parses Python source using lambda-py's get-core-syntax
  • Outputs desugared core syntax as S-expressions via core->sexp

CLI (Main.lean)

  • --run <file.py> - Parse and execute Python file
  • --parse <file.py> - Parse and print Expr representation
  • --parse-sexp <file> - Parse S-expression file directly
  • --eval <code> - Parse and execute Python code string

Faithful Python Semantics

Builtins (PythonOfLean/Semantics/Builtins.lean)

Complete rewrite to support Python's object model with method dispatch:

  • Type Objects with Magic Methods:

    • %int, %float: Arithmetic methods (__add__, __sub__, __mul__, __div__, __floordiv__, __mod__)
    • Comparison methods (__eq__, __lt__, __gt__, __le__, __ge__)
    • %str: String operations (__add__, __eq__)
    • %bool, %object: Base __getattribute__
    • num: Parent type for numeric operations

  • Method Binding: mkGetAttributeMethod creates bound methods with __func__ and __self__ attributes

  • Initial State Setup: setupBuiltinTypes creates all type objects with their methods as fields

  • Constants: True, False, None singletons

  • Exception Types: BaseException, Exception, TypeError, ValueError, NameError, AttributeError, KeyError, IndexError, StopIteration, ZeroDivisionError, AssertionError

  • Runtime Support: %special_getattr, %locals

Primitives (PythonOfLean/Semantics/Interp.lean)

Extended interpPrim with full Python runtime primitives:

  • Object Attribute Operations:

    • obj-getattr, obj-hasattr, obj-setattr, obj-delattr - Internal dict access
    • $getattribute - Method binding (creates bound method objects)

  • Numeric Operations (Racket-compatible names):

    • num+, num-, num*, num/, num//, num%
    • num=, num<, num>, num<=, num>=, numcmp

  • String Operations: str+, str=

  • Type Introspection:

    • $class - Get object's class
    • isinstance - Type checking
    • is-func?, is-bound-method?, is-none?

  • Collections:

    • len - Length of list/tuple/set/string
    • list-getitem, tuple-getitem - Index access

  • Conversion: num-str - Number to string

Bug Fixes

  • Assignment preserves class: Fixed assign to copy the actual object instead of wrapping the pointer, which was losing class information and breaking method dispatch on variables

Tested Features

The interpreter now correctly executes:

  • Arithmetic expressions: 1 + 2 * 3
  • Comparisons: 5 > 3, i < 10
  • Control flow: if/else, while loops with break/continue
  • Functions: def, recursion, return
  • Variables: Global assignment and lookup
  • Complex programs: Factorial, Fibonacci, prime counting