Marshalling

The marshalling layer converts between Python values and Lean runtime objects (lean_object* pointers). It handles scalars, strings, arrays, options, and arbitrary inductives — in both directions.

Source: lean_py/marshal.py

How values cross the boundary

When you call lib.increment(7), the marshaller:

Looks up the function’s parameter types from the registry.
Converts 7 (a Python int) to a Lean Int object using the appropriate to_lean function.
After the C call returns, converts the Lean result back to a Python int using the corresponding from_lean function.

Each type has a TypeWrapper — a pair of (to_lean, from_lean) functions plus the ctypes type used at the C ABI level.

Scalar types

Lean scalars map directly to Python primitives:

Lean type	Python type	Notes
`Nat`, `Int`	`int`	Arbitrary precision (uses `lean_int_big_*` for large values)
`Float`	`float`
`String`	`str`	UTF-8 encoded
`Bool`	`bool`	Boxed as `lean_box(0)` / `lean_box(1)`
`Char`	`str` (single char)
`UInt8` .. `UInt64`	`int`	Fixed-width, unboxed at the C level

Container types

Lean type	Python type	Notes
`Array α`	`list`	Elements recursively marshalled
`List α`	`list`	Converted via linked-list ctors
`Option α`	value or `None`
`Prod α β`	`tuple`	`(a, b)`

Inductive types

Any Lean inductive registered with derive_python is marshalled to and from LeanInductiveValue:

>>> lib.Shape.circle(5)
Shape.circle(5)

>>> val = lib.perimeter(lib.Shape.circle(5))
30

Going to Lean, the marshaller encodes each LeanInductiveValue recursively: allocating a lean_ctor_object with the right tag, writing object fields and scalar fields, and using smart constructors (lean_name_mk_string, lean_expr_mk_app, etc.) for types that have computed fields like hashes.

Coming from Lean, the marshaller reads the constructor tag, looks up the CtorInfo, and extracts fields by index.

LeanObj — owned pointers

LeanObj is a Python-side RAII wrapper around a lean_object*:

from lean_py.marshal import LeanObj

# Takes ownership — will call lean_dec_ref on __del__
obj = LeanObj(raw_pointer)

# Borrow without taking ownership
borrowed = LeanObj.borrow(raw_pointer)

# Release ownership back to caller
ptr = obj.release()

The key invariant: constructing a LeanObj does not increment the reference count. It assumes the caller is transferring ownership. On destruction (or garbage collection), it calls lean_dec_ref to release the reference.

LeanInductiveValue — Python-side inductives

LeanInductiveValue represents a Lean constructor application:

>>> val = LeanInductiveValue("Shape", "circle", tag=0, fields=(5,))
>>> val.ctor
'circle'
>>> val.tag
0
>>> val.fields
(5,)
>>> val._0
5

It supports Python 3.10+ structural pattern matching:

match val:
    case Shape.circle(r):
        print(f"radius = {r}")

The _CtorMeta metaclass makes isinstance(val, Shape.circle) work by checking the constructor name rather than the Python class hierarchy.

Smart constructors

Some Lean types (Name, Level, Expr) have computed fields — scalar values (like hashes) that are derived from the constructor arguments. Allocating a plain lean_ctor_object and writing the fields by hand would leave these computed fields uninitialised, breaking environment lookups.

The marshaller uses smart constructors — C functions exported by the Lean runtime with @[export] — that correctly compute and store these fields:

C symbol	Lean constructor	Type
`lean_name_mk_string`	`Name.str`	`Name`
`lean_name_mk_numeral`	`Name.num`	`Name`
`lean_expr_mk_app`	`Expr.app`	`Expr`
`lean_expr_mk_forall`	`Expr.forallE`	`Expr`
`lean_expr_mk_lambda`	`Expr.lam`	`Expr`
…	…	…

These smart constructors take ownership of their arguments without incrementing the reference count — the marshaller must not call lean_dec on the children after construction. This matches Lean’s compiler codegen convention.

The Marshaller class

Marshaller is the central registry of type wrappers. It is created automatically by LeanLibrary from the LibraryRegistry:

# Usually you don't create this directly — LeanLibrary does it
marshaller = Marshaller(registry)

# Look up conversion functions for a type
wrapper = marshaller.wrapper_for(type_repr)
lean_val = wrapper.to_lean(python_val)
python_val = wrapper.from_lean(lean_val)

For custom types, the marshaller builds recursive encode/decode functions at wrapper-creation time, so the per-call overhead is a chain of Python function calls rather than a registry lookup.