Function _build_callable

lean_py/library.py:189–269

Build a Python wrapper around an `@[export]`'d Lean function. Conventions for the C ABI of Lean-exported functions: * Most parameter types are `lean_object*`. Exceptions: scalar value types (Bool, UInt8/16/32/64, USize, Float) are passed as their natural C types, but induc

(lib: ctypes.CDLL, finfo: FuncInfo, marshaller: Marshaller)

        return LeanInductiveValue(self._ti.name, self._ctor.name, self._ctor.tag, tuple(args))


# Optional runtime validation of arguments against their Lean `TypeRepr`.
# Off by default (the marshaller is intentionally lenient); enable it for
# clearer errors during development. See `set_argument_typechecking`.
_argument_typechecking = False


def set_argument_typechecking(enabled: bool) -> None:
    """Enable/disable runtime validation of arguments to `@[python]` functions.

    When enabled, each argument is checked against the same `TypeRepr` that
    drives marshalling (:meth:`lean_py.registry.TypeRepr.check`), raising a
    clear ``TypeError`` before the value crosses the FFI boundary. Applies to
    functions bound after — and calls made while — it is enabled.
    """
    global _argument_typechecking
    _argument_typechecking = bool(enabled)


# ============================================================================
# Generated function wrappers
# ============================================================================


def _build_callable(lib: ctypes.CDLL, finfo: FuncInfo, marshaller: Marshaller) -> Callable:
    """Build a Python wrapper around an `@[export]`'d Lean function.

    Conventions for the C ABI of Lean-exported functions:
      * Most parameter types are `lean_object*`. Exceptions: scalar value
        types (Bool, UInt8/16/32/64, USize, Float) are passed as their
        natural C types, but inductive parameters are pointer-shaped.
      * IO-returning functions take a trailing `lean_io.RealWorld` arg
        (just `lean_box(0)`); the result is a tagged Result object.
    """
    try:
        cfn = getattr(lib, finfo.exportName)
    except AttributeError as e:
        raise RuntimeError(
            f"Symbol {finfo.exportName} not found in library "
            f"(declared in registry but missing from dylib)"
        ) from e

    ret = finfo.returnType
    is_io = ret.kind == "io"

    pwraps: list[TypeWrapper] = [marshaller.wrapper_for(p) for p in finfo.params]
    rwrap: TypeWrapper = marshaller.wrapper_for(ret)

    # We use `c_void_p` for any pointer-shaped argument or return value
    # to sidestep a ctypes oddity on macOS where storing a returned
    # `POINTER(struct)` and then passing it to another C function
    # corrupts the pointer in some configurations.
    def _ctype_for_call(ct):
        # Pointer-shaped: collapse to c_void_p.
        if isinstance(ct, type) and issubclass(ct, ctypes._Pointer):
            return c_void_p
        return ct